A Pragmatic Approach to Stateful Partial Order Reduction
summary
Proposes stateful POR variants: a cheap static safe-set pass plus two dynamic source-set trackers (eager and lazy) implemented in Java Pathfinder. Benchmarks on concurrent data-structure clients (sampled 75 clients, 3 threads, ≤5 calls) show the lazy version cuts dependency comparisons and retraversals, outperforms the eager variant and JPF’s baseline, while the theoretically optimal source-set implementation often times out. Recommends a parallel portfolio of static and lazy for best wall-clock performance.
AI-written summary · about
chapters (9)
- 0:00Stateful partial order reduction
- 1:21Partial order reduction basics
- 2:23Stateless vs stateful trade-offs
- 3:49Restricting sets in POR
- 5:14Static algorithm with safe sets
- 5:58Dynamic algorithms with current sets
- 9:27Eager vs lazy dynamic differences
- 13:02Experimental results
- 14:44Conclusion
related talks
10mNerv: Probabilistic Dynamic Partial Order Reduction for Hardware
20mTruly Stateless, Optimal Dynamic Partial Order Reduction
36mIntroduction to stateful property based testing
28mEfficient Demand Evaluation of Fixed-Point Attributes Using Static Analysis
22mCompositional Programming and Testing of Dynamic Distributed Systems
19mState Space Estimation for DPOR-Based Model Checkers
17mSSRD: Shapes and Summaries for Race Detection in Concurrent Data Structures
10mEfficient Decrease-And-Conquer Linearizability Monitoring