Speaker: Nitish Yadav
Topic: Partial Order Methods for the Verification of Concurrent Systems
Description: Concurrent program verification is crucial for ensuring correctness in systems where multiple processes operate simultaneously and interact through shared resources. A primary method for verifying concurrent programs involves exhaustive exploration of the system’s state space to detect potential errors such as deadlocks or race conditions. However, exhaustive search is typically impractical due to the phenomenon of state-space explosion, where the number of possible system states grows exponentially with the number of concurrent processes. To mitigate this challenge, Partial Order Reduction (POR) techniques are employed to significantly reduce the explored state space while preserving verification correctness.
Two prominent POR techniques are persistent sets and sleep sets. Persistent sets select subsets of enabled transitions from each state, strategically avoiding redundant interleavings. Sleep sets track transitions that can safely be deferred (“slept”), preventing repetitive exploration of equivalent sequences. However, utilizing persistent or sleep sets alone may still result in redundant explorations. Thus, their combination is essential to achieve optimal state-space reduction.
In this talk, we will explore the basics of partial order reduction, focusing specifically on persistent sets and sleep sets.