Higher-Order Leak and Deadlock Free Locks
summary
Presents a linearly typed lambda calculus that enforces both deadlock and memory-leak freedom for first-class, nestable locks, proving that well-typed programs cannot deadlock or leak; introduces a sharing topology invariant for acyclic cases and a dynamic lock order mechanism for cyclic groups, implements a log‑group API and encodes examples including a dynamic Dining Philosophers, and fully mechanizes the soundness proofs mechanized in Coq.
AI-written summary · about
chapters (13)
- 0:00Start
- 1:29Memory management with substructural types
- 2:01Memory leaks in Rust
- 3:03Deadlocks in Rust
- 3:40The paper in a nutshell
- 4:55Mock's lock type
- 5:34Mock's lock API
- 7:55Which concurrency patterns does lock support?
- 8:47Locks in locks in Mock
- 12:53Swap within a lock group
- 13:43Dijkstra's dining philosophers
- 15:05Leak and deadlock freedom theorem
- 17:42Related and future work (non-exhaustive)
related talks
20mDeadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-O...
23mConnectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation L
39mLive Lock-Free or Deadlock (Practical Lock-free Programming)
22mVerifying Lock-Free Traversals in Relaxed Memory Separation Logic
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
26mConcurrency: Unlocking a Solution
15mLilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness
24mA Concurrent Program Logic with a Future and History