Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness
summary
Lilo is a higher-order concurrent separation logic that adds a promise mechanism to reason about liveness: threads record a promise list and must consume progress credits to make steps, preventing bogus circular or unfulfillable promises. It reuses FOS-style primitives, provides Iris-style invariants, supports higher-order reasoning without step-indexing via stratified propositions (Nola-inspired), proves refinement/termination properties in Coq, and gives the first modular termination proof of the elimination stack plus ticket-lock liveness specs.
AI-written summary · about
chapters (13)
- 0:00Lilo introduction and promise
- 1:09Message passing example
- 2:33Safety proofs with invariants
- 3:35Invariants fail for liveness
- 3:57Promise mechanism for liveness
- 4:38Promise mechanism soundness
- 6:22Promise list and credits rules
- 7:05Progress credits prevent unsoundness
- 8:11Writer thread termination proof
- 9:13Ticket lock triple with promises
- 10:40Unlock triple and credits
- 11:02Summary and conclusion
- 11:23Question and answer session
related talks
20mDeadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-O...
20mTrillium: Higher-Order Concurrent and Distributed Separation Logic for Intension...
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
24mA Concurrent Program Logic with a Future and History
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz
24mTaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr
22mVerifying Lock-Free Traversals in Relaxed Memory Separation Logic
27mConcurrent Incorrectness Separation Logic