Truly Stateless, Optimal Dynamic Partial Order Reduction
summary
Claim: TruSt explores exactly one interleaving per Mazurkiewicz-equivalence class while using linear (paper shows how to get from N^2 to linear) memory instead of exponential. It implements an execution graphs representation (extends GENMC), handles SC and weak models like TSO/PSO/RC11 under mild assumptions, and makes backward revisits unique via maximal extensions so explored revisits can be forgotten. The tool is Coq-verified, embarrassingly parallel, and the artifact outperforms prior DPOR implementations.
AI-written summary · about
related talks
10mNerv: Probabilistic Dynamic Partial Order Reduction for Hardware
19mState Space Estimation for DPOR-Based Model Checkers
16mA Pragmatic Approach to Stateful Partial Order Reduction
30mStateful Dynamic Partial Order Reduction for Model Checking Event-Driven Applic
21mCSL and relaxed memory
22mOptimal Stateless Model Checking under the Release-Acquire Semantics
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
19mScenario-based Proofs for Concurrent Objects