Speaker: Nitish Yadav
Topic: Partial Order Reduction for Concurrent Program Verification
Description: Verifying concurrent programs is challenging due to the vast number of possible interleavings between threads. Model checking systematically explores the program’s state space to verify safety properties, but this becomes infeasible in practice due to state-space explosion. Stateless model checking avoids storing these states by using a runtime scheduler, though it still suffers from state-space explosion. To mitigate this, Partial Order Reduction (POR) explores exactly one representative per equivalence class of executions, defined via Mazurkiewicz traces, using techniques like persistent sets and sleep sets to prune redundant interleavings. Traditional POR relies on static analysis, which limits reduction. Dynamic Partial Order Reduction (DPOR) improves on this by computing dependencies during execution to identify backtracking points and construct persistent sets dynamically, ensuring coverage but not optimality, as it may still explore multiple interleavings per equivalence class. To achieve optimality, source sets and wakeup trees were introduced. Source sets identify minimal sufficient process subsets, while wakeup trees manage the scheduling of alternative interleavings to avoid sleep-set blocking. Together, they form the optimal-DPOR algorithm, which guarantees exploration of exactly one interleaving per equivalence class.
Time 5 pm to 6 pm (IST)
Presenter: Nitish Yadav
About the Presenter: https://www.linkedin.com/in/nitishyadavny/