A Concurrent Program Logic with a Future and History
summary
A new separation logic that preserves local reasoning while enabling automation introduces ghost update chunks to decompose unbounded physical removals into small, automatable updates and past states to record and propagate hindsight facts for linearizability. A proof-generation tool implements these ideas, requires zero user annotations, and successfully and automatically verifies challenging concurrent search structures (Harris set, ~50–100 LOC) under an arbitrary-number-of-threads model. The paper proves the logic sound and shows the technique scales to real lock-free examples.
AI-written summary · about
chapters (7)
- 0:00Intro
- 0:15Motivation
- 1:43Example: Unbounded Removal
- 6:39Ghost Update Chunks
- 13:00Example: contains(7)
- 15:47Past Reasoning
- 19:28Recap: A Concurrent Program Logic with a Future and History
related talks
54mReasoning about Progress of Concurrent Objects
20mDeadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-O...
01h 01mThe Future of Concurrency and Parallelism
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
23mProbabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and(…)
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz
25mThe Path to Durable Linearizability
15mLilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness