Leaf: Modularity for Temporary Sharing in Separation Logic
summary
Claims a single abstraction that encodes temporary read sharing across different permission systems and shows it works concretely: a guarding operator that makes a proposition represent a releasable shared view, backed by storage protocols that extend resource algebras and recover fractional and counting permissions as instances. Implemented as a verified library in Iris, with mechanized proofs and evaluated artifacts: a verified reader‑writer lock and a hash table client built on top that successfully compose with the abstract specs.
AI-written summary · about
chapters (17)
- 0:00Introduction to Leaf
- 0:21Concurrent programming patterns
- 1:06Temporary sharing in separation logic
- 2:10Limitations of fractional permissions
- 3:32Permission logic interoperability
- 4:36Leaf framework for sharing
- 5:38Leaf’s permission systems
- 6:21Reader resources with guarding
- 7:44Deriving fractional permissions
- 8:49Memory load with guards
- 9:55Notation for shared resources
- 10:38Resource algebra extensions
- 12:05Modular specs with locks
- 13:52Client-side opacity
- 14:14Non-separating conjunction
- 15:16Conclusion
- 15:42Q&A
related talks
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
15mRecursive Mutexes in Separation Logic
28mReasoning about Distributed Reconfigurable Systems
22mThe Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic
21mEmbedding Hindsight Reasoning in Separation Logic
26mOn Algebraic Abstractions for Concurrent Separation Logics
15mModular Reasoning about Global Variables and Their Initialization
15mModular Verification of Op-Based CRDTs in Separation Logic