Verified Lock-Free Session Channels with Linking
summary
Claims a verified lock-free implementation of asynchronous, bidirectional session channels (with per-direction buffers and a link/forward operation), proved correct against a high-level session-type specification. Verification uses layered Iris proofs: logically-atomic triples for linking, two new abstractions—ghost linking and pairing invariants—and reusable queue specs instantiated with singly linked-list and array-segment implementations. All proofs are mechanized in Coq and artifacts are available and reproducible, so the implementation and proof are fully completed.
AI-written summary · about
chapters (11)
- 0:00Verified lock-free session channels
- 1:44Session types and low-level impls
- 4:11Proving end-to-end correctness
- 5:14Linking with singly linked lists
- 6:16Logically atomic triples
- 7:41Maximizing verification reusability
- 8:45Ghost linking for queue ops
- 10:49Ghost linking enables linearizability
- 11:55Ghost linking with different queues
- 12:37Conclusion and verification principles
- 13:20Q&A
related talks
28mDependent Session Protocols in Separation Logic from First Principles
22mVerifying Lock-Free Traversals in Relaxed Memory Separation Logic
20mDeadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-O...
54mShared Session Types for Safe, Practical Concurrency
23mConnectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation L
35mAsynchronous and Synchronous Mixed Sessions
21mCommCSL: Proving Information Flow Security for Concurrent Programs using Abstract(…)
25mA Logical Interpretation of Asynchronous Multiparty Compatibility