Proof Automation for Linearizability in Separation Logic
summary
Implements proof automation for contextual refinement and logical atomicity inside Diaframe 2.0, encoded in Iris and Coq, and uses both program shape and logical state to pick rules while deliberately minimizing backtracking. Fully automates small examples, makes partial progress on complex proofs so users can interleave manual steps, and yields large proof-size drops (contextual refinement proofs about 7x shorter, logical-atomicity and Iris proofs about 4x shorter). Artifact package is available and evaluated; Michael-Scott queue is shown logically atomic.
AI-written summary · about
chapters (12)
- 0:00Proof automation intro
- 1:10Existing tools limits
- 2:35Adding automation to approaches
- 4:21Diaphragm 2.0 library
- 5:25Contextual refinement counter
- 8:57Symbolic execution counter
- 12:48Automating Coq proof
- 13:30Logical atomicity strategy
- 14:14Evaluation results
- 14:57Key takeaways
- 15:46Q&A: atomicity vs refinement
- 16:36Q&A: clarifying work
related talks
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
21mEmbedding Hindsight Reasoning in Separation Logic
52mThink Abstractly, Work Concretely
21mMechanised Hypersafety Proofs about Structured Data
22mThe Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic
23mSeparating the Wheat from the Chaff: Understanding (In-)Completeness of Proof(…)
24mTaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr
20mNola: Later-Free Ghost State for Verifying Termination in Iris