Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation L
summary
Introduces connectivity graphs as a generic, parametric graph abstraction plus local Separation Logic predicates that let one prove preservation and global progress for session-typed message passing, and mechanizes the result in Coq (generic library ~50k LOC, language-specific proofs ~1.7k LOC). Shows a local graph-transformation calculus and a waiting induction principle to locate a thread that can step, and claims the first mechanized proof of deadlock and memory-leak freedom for a higher-order binary session-typed language; artifacts available and evaluated.
AI-written summary · about
chapters (16)
- 0:00Start
- 2:33Why Do Session Types Give Deadlock Freedom
- 3:41Connectivity Graph Proof Method
- 4:15Connectivity Graph
- 6:47Connectivity Graph Framework
- 7:42Tools for Proving the Preservation Step
- 9:37Rule for Typing a Channel Reference
- 10:28Replacement Lemma
- 11:33Rules for the Channel Operations
- 12:18Fork
- 13:35Prove Progress
- 14:54Weighting Induction Principle
- 16:33General Recursive Types
- 18:09Strong Reachability
- 20:46Questions
- 21:08Why Did You Include an Explicit Close Operation if the Channels Are Linear
related talks
20mDeadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-O...
26mHigher-Order Leak and Deadlock Free Locks
01h 01mThe Future of Concurrency and Parallelism
54mReasoning about Progress of Concurrent Objects
24mA Concurrent Program Logic with a Future and History
14mMultiparty GV: Functional Multiparty Session Types with Certified Deadlock Fre...
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
28mDependent Session Protocols in Separation Logic from First Principles