Scenario-based Proofs for Concurrent Objects
summary
Defines a small set of representative interleavings — the commutativity quotient — and an expression language (regular/context-free) that encodes them so linearizability proofs work over those few canonical traces instead of all interleavings. Builds quotient automata that make linearization points explicit, captures helping, elimination, and future-dependent cases, and matches original authors’ scenario arguments. Implements a reduction to two-thread reachability and uses Ultimate Automizer to synthesize candidate quotients within minutes.
AI-written summary · about
chapters (9)
- 0:00Scenario-based proofs intro
- 1:04Verifying concurrent correctness
- 3:32Michael Scott Q algorithm
- 6:51Quotient expressions
- 9:19Quotients with automata
- 11:48Method for other structures
- 13:31Automating automata
- 14:34Conclusion and future
- 15:15Q&A
related talks
23mStratified Commutativity in Verification Algorithms for Concurrent Programs
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
27mC4: verified transactional objects
54mReasoning about Progress of Concurrent Objects
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz
21mCommCSL: Proving Information Flow Security for Concurrent Programs using Abstract(…)
24mA Compositional Theory of Linearizability
24mA Concurrent Program Logic with a Future and History