Recursive Mutexes in Separation Logic
summary
Develops a separation-logic specification for recursive mutex built on the Brick logic and derived from a lower-level logically-atomic spec, with a per-thread holds predicate that stores an acquisition count and an args vector of existential state to preserve information across reentrant borrows. Verifies concrete C++ examples and proves update A, update B and a transfer function (modulo integer overflow), and proves the resource spec against the atomic spec; specs and code are available in the open-source standard-library spec repo.
AI-written summary · about
chapters (9)
- 0:00Recursive mutexes in C++
- 1:25Standard library support in C++
- 2:51Separation logic for mutexes
- 5:40Recursive mutex differences
- 7:48Formalizing recursive mutex
- 10:14Preserving info on recursive lock
- 11:57Proving mutex operations correct
- 12:59Open-source stdlib specs project
- 13:43Q&A
related talks
51mMemory Model: Get your shared data under control
01h 00mConcurrency in C++20: A Deep Dive
19mLeaf: Modularity for Temporary Sharing in Separation Logic
39mRust Atomics in the Wild: Memory Ordering Design Patterns [...]
54mReasoning about Progress of Concurrent Objects
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz
24mA Concurrent Program Logic with a Future and History
19mVerifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic