Automated reasoning on consistency models with MONA
summary
Claim: satisfiability of MSO over finite execution histories is decidable and can be checked by translating histories into MONA’s finite-word MSO. Implementation: a compiler encodes each timestamp as a bit‑vector with rows for process/state, type/input/output/object, an arbitration matrix (upper triangle encoded) and per‑process visibility counters; MONA then builds automata for formulas. Status: proof completed, encoder implemented and exercised on examples, toolchain works end‑to‑end for finite histories; ongoing work extends to infinite traces and weaker visibility/arbitration assumptions.
AI-written summary · about
chapters (7)
- 0:00Automated reasoning intro
- 2:09Why MONA for verification
- 3:56MONA and MSO logic
- 9:08Histories as bit vectors
- 13:51Arbitration and visibility
- 18:28Compiler for MSO formulas
- 19:09Conclusion
related talks
22mA Partial Order View of Message-Passing Communication Models
26mKater: Automating Weak Memory Model Metatheory and Consistency Checking
24mCertifying the decidability of the word problem in monoids at large
13mSharding the State Machine: Automated Modular Reasoning for Complex Concurrent System
27mRecurrence Sets for Proving Fair Non-termination under Axiomatic Memory Consistency Models
24mFormal Verification of a Distributed Dynamic Reconfiguration Protocol
13mCharacterizing Implementability of Global Protocols with Infinite States and Data
16mCyclic Message Histories for Automated Safety Verification of Distributed Algorithms