A Graded Monad for Deadlock-Free Concurrency (Functional Pearl)
summary
Claims a type-oriented framework that guarantees deadlock freedom by encoding a total lock order in types and implements it as a graded monad over IO. Lock sets appear as type-level sorted lock lists and a type-level merge plus a partial-cons constraint enforce acquisition-before-release order. Implementation maps lists of unit MVars to IO, provides syncX operations and parallel composition, rejects the classic deadlocking dining-philosophers encoding, and the grading algebra yields types that can be inferred in polynomial time.
AI-written summary · about
chapters (19)
- 0:00Intro
- 0:34Concurrent programming in Haskell
- 1:18MVar synchronisation
- 2:24Software transactional memory
- 3:18Motivation
- 4:13Talk overview
- 6:24Graded monads in Haskell
- 8:02Framework (cont'd)
- 9:24Usage examples
- 11:33Dining philosophers (implemented)
- 13:04Dining philosophers (shorter)
- 13:54Lock algebra
- 15:34Underlying Sync implementation
- 17:28Implementing synchronization
- 18:24Implementing parallelism
- 19:24In the paper: memory regions
- 20:40In the paper handling recursion
- 21:52Further work
- 23:31Summary
related talks
26mHigher-Order Leak and Deadlock Free Locks
26mConcurrency: Unlocking a Solution
01h 30mLive Lock-Free or Deadlock (Practical Lock-free Programming)
01h 08mSimplifying Concurrent Programming via Synchronization Synthesis
44mCAN WE FREE CONCURRENT PROGRAMMING FROM THE MONADIC STYLE
20mDeadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-O...
01h 14mBeyond Free Monads
47mDeadlocks: The Dark Side of Concurrency