Kater: Automating Weak Memory Model Metatheory and Consistency Checking
summary
Kater reduces meta theoretic questions about axiomatic weak memory models to language inclusion between CAT expressions, proving decidability for a wide class of models and turning irreflexivity implications into automatable checks. It implements an algorithm that generates time- and space-efficient bounded verifiers and consistency-checkers (integrated with GenMC), reproduces literature positives and negatives, and finds a real counterexample: a broken C11→Power compilation scheme in about 45 seconds, showing the approach works on practical models.
AI-written summary · about
chapters (10)
- 0:00Kater introduction
- 2:15Weak memory models
- 5:45Memory model verification
- 7:30Declarative semantics
- 10:15Model checks to language inclusion
- 13:06Language inclusion fixes
- 13:26Demo: Memory model equivalence
- 17:02Demo: C11 to x86 proof
- 18:46Summary
- 19:32Q&A
related talks
21mMechanizing the CMP Abstraction for Parameterized Verification
16mModel Checking for a Multi-Execution Memory Model
27mRecurrence Sets for Proving Fair Non-termination under Axiomatic Memory Consistency Models
05mWelcome
25mSafe Replication through Bounded Concurrency Verification
22mAutomated reasoning on consistency models with MONA
20mDeciding Asynchronous Hyperproperties for Recursive Programs
16mCyclic Message Histories for Automated Safety Verification of Distributed Algorithms