Psym: Efficient Symbolic Exploration of Distributed Systems
summary
Psym implements a symbolic explorer for P programs that merges frontier states using composite value summaries and canonical BDD-backed SECI guards so overlapping message-processing updates run once instead of repeatedly. The tool outperforms TLC on the evaluated ports, achieving a 2.5× speedup on average and solving nine of ten benchmarks faster, and it verifies real-world systems—including verified four AWS protocols (≈1k LOC, 13–22 concurrent nodes)—while composing with partial-order reductions, predicate abstraction, and fixpoint detection.
AI-written summary · about
chapters (14)
- 0:00Psym introduction
- 1:27Distributed systems challenges
- 2:53Avoiding redundant computations
- 3:57Experimental results speedup
- 4:38State representation needs
- 5:20Scheduling control guards
- 7:25Value summaries for states
- 8:50Composite value summaries
- 9:53Exploration algorithm
- 12:21Benchmark vs TLC
- 13:46Industrial protocol verification
- 14:51Infinite states with abstractions
- 15:12Takeaways and future work
- 16:00Question and answer session
related talks
20mSPORE: Combining Symmetry and Partial Order Reduction
16mDi-PS: System-Algorithm Co-Design for Asynchronous and Heterogeneous Cross-cluster...
21mMassive proofs for the masses
16mCyclic Message Histories for Automated Safety Verification of Distributed Algorithms
25mSymbolic Bisimulation for Open and Parameterized Systems
16mSwiftPaxos: Fast Geo-Replicated State Machines
11mXerxes: Extensive Exploration of Scalable Hardware Systems with CXL-Based Simulation...
41mProgramming Distributed Systems