CAAT: Consistency as a Theory
summary
Claims a family of logical theories that capture memory-model consistency (TSO, POWER, ARMv8, RISC‑V, RC11, IMM, Linux kernel) and builds a generic, efficient theory solver that handles recursion/transitive closure. The solver plugs into a lazy SMT backend for a bounded model checker, yielding 2x–100x speedups versus standard encodings (largest gains on Power), produces small conflict cores as explanations, and finds real bugs (e.g., the Linux Q spinlock issue) that drove model fixes.
AI-written summary · about
chapters (14)
- 0:00Intro
- 0:15A Typical Verification Problem
- 2:17Memory Model (TSO)
- 4:03What is CAT?
- 6:50Peterson's Mutual Exclusion Algorithm
- 12:17CAT in logical theories
- 13:34CAT as logical theory
- 15:17CAAT: Consistency as a Theory
- 16:00A Theory Solver for Consistency
- 16:35A Decision Procedure for Consistency
- 17:21Theory solving for SC
- 21:10Evaluation: simple CATS
- 22:11Evaluation: very complex CATS
- 22:25Conclusion
related talks
18mThe Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++
26mArmed cats: formal concurrency modelling at Arm
20mHow Hard is Weak-Memory Testing?
15mSoundness of Predictive Concurrency Analyses
15mOptimal Reads-From Consistency Checking for C11-Style Memory Models
01h 11mProgramming language memory models: Problems, solutions, and directions
23mMemory Consistency Model Status Update
14mMaking Weak Memory Models Fair