Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-O...
summary
LinearActris is a linear concurrent separation logic that claims to give deadlock and leak freedom for message-passing programs by design. The adequacy proof uses a step-indexed model built from connectivity graphs, a separate separation-logic world per thread/channel linked by ownership, and treats receive as a primitive that can get stuck; crucial proof changes are linearity, combining newChan with fork, and removing Iris invariance. The development proves soundness of a higher-order GV-style session system by logical relations and is mechanized in Coq, with artifacts available.
AI-written summary · about
chapters (11)
- 0:00Deadlock-free separation logic intro
- 1:52Iris and actress separation logic
- 4:04Deadlocks in actress problem
- 5:49Linear separation logic for deadlock freedom
- 7:11Changes to actress proof rules
- 8:38Escape attempts impossible
- 10:25Linear actress model architecture
- 11:28Concurrent merge sort example
- 12:11Session type program verification
- 12:53Future work and limitations
- 13:17Q&A
related talks
23mConnectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation L
26mHigher-Order Leak and Deadlock Free Locks
24mA Concurrent Program Logic with a Future and History
15mLilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness
54mReasoning about Progress of Concurrent Objects
22mVerifying Lock-Free Traversals in Relaxed Memory Separation Logic
28mDependent Session Protocols in Separation Logic from First Principles
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic