SPORE: Combining Symmetry and Partial Order Reduction
summary
SPORE is a stateless model checker that actually combines symmetry reduction and dynamic partial order reduction to cut interleavings exponentially; it proves sound, complete and optimal exploration under sequential consistency (with extensions to weak memory) and introduces internal symmetries to treat idempotent helping operations as no-ops. On benchmarks it collapses thousands or factorial families of schedules down to a single interleaving in key cases, ships reusable artifacts, and integrates with the TRuST-style POR graph enumeration to produce the representative execution graphs SPORE enumerates.
AI-written summary · about
chapters (11)
- 0:00Stateless model checking intro
- 1:50Limitations of reductions
- 3:14Combined techniques example
- 5:01Spore’s combined approach
- 6:04How Spore combines methods
- 8:56Symmetries in lock-free queues
- 11:52Leveraging internal symmetries
- 13:59Applicability beyond symmetry
- 14:19Evaluation on real data structures
- 15:22Summary and future
- 17:52Q&A
related talks
16mDynamic Partial Order Reduction for Checking Correctness Against Transaction Isolation(…)
18mPsym: Efficient Symbolic Exploration of Distributed Systems
14mThe Reads-From Equivalence for the TSO and PSO Memory Models
35mSymmetry-Preserving Finite Synthesis and Amalgamation
33mPruning Redundancy in Answer Set Optimization Applied to Preventive Maintenance ...
24mA Robust Theory of Series Parallel Graphs
44mSpores: Distributable Functions in Scala
14mFeedback-guided Adaptive Testing of Distributed Systems Designs