On Algebraic Abstractions for Concurrent Separation Logics
summary
Defines morphisms of PCMs and separating relations as the concrete algebraic machinery that preserves ownership across parallel composition, then uses them to specify and verify a ticket lock: constructs a ticketmap PCM, a psi morphism that computes display = max(used)+1, and an alpha mapping to an ownership PCM; shows a sub-pcm construction and invertible morphisms that let framing and abstraction collapse an internal ticketmap spec into a compact ownership spec that composes soundly.
AI-written summary · about
chapters (18)
- 0:00Intro
- 0:14Partial Commutative Monold (PCM)
- 2:07Partiality of Disjoint Union
- 2:24Ghost State of Locking
- 3:08Morphisms - structure preserving maps
- 3:32thread
- 4:19Partiality of Morphisms
- 4:33Separating Relations
- 6:15Finite Maps and Ticket Lock
- 8:12PCM - natural numbers under maximum
- 8:40Display Morphism
- 10:38Subjective State
- 13:09Intermediate Small Footprint Spec
- 15:09Intermediate Large-Footprint Spec
- 18:04Abstracting the Intermediate Spec
- 19:48Intermediate Abstract Spec
- 20:40Algebraic Constructions - sub-PCM
- 24:12Conclusions
related talks
23mVerifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
19mLeaf: Modularity for Temporary Sharing in Separation Logic
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
27mC4: verified transactional objects
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
20mOn Multi-Language Abstraction: Towards a Static Analysis of Multi-Language Programs
24mTaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr
15mContract System Metatheories à la Carte: A Transition-System View of Contracts