C4: verified transactional objects
summary
C4 claims a mechanized, compositional way to prove both linearizability and strict serializability and to stitch those proofs together for mixed implementations; the paper builds a verified transactional set by composing a concurrent locator (proven pure/lazy), a TM protocol (a verified TML-style protocol), and instrumentation implemented as interaction-tree transformers. Proofs follow a simulation-based, five-obligation proof principle and are fully mechanized in Coq, and the composed predicated set is shown to be serializable.
AI-written summary · about
chapters (17)
- 0:00C4 verified transactional objects
- 0:42Single-method atomicity limits
- 2:08Linearizability vs serializability
- 4:37Mechanized compositional verification
- 5:21Concurrent objects with interaction trees
- 7:08Linearizability as simulation
- 8:12Compositional linearizable properties
- 9:36Proof principles for linearizability
- 10:59Transactional objects and serializability
- 12:26Transactional objects structure
- 14:57Strict serializability as linearizability
- 16:25Transactional predication use case
- 19:35Verifying predicated map serializability
- 21:45Locator’s pure behavior proof
- 23:32Mechanized verification components
- 24:14Summary
- 24:38Q&A
related talks
19mScenario-based Proofs for Concurrent Objects
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
23mStratified Commutativity in Verification Algorithms for Concurrent Programs
19mCompCertOC: Verified Compositional Compilation of Multi-threaded Programs with Shared(…)
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
21mCommCSL: Proving Information Flow Security for Concurrent Programs using Abstract(…)
01h 16mVerifying, Inferring and Exploiting Code Commutativity
01h 00mCooperative Verification: Towards Reliable Safety-Critical Systems