Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic
summary
Proposes a connection-based multi-succedent calculus that reduces blind backtracking for disjunctive invariants in fine-grained concurrent separation logic, extends Iris features (modalities, higher-order quantification, ghost state, invariants), and is implemented in Coq on top of Diaphrag. Evaluated on 24 challenging benchmarks: 14/24 verified automatically (seven more than before), proofs shrink about 30% shorter, and proof search avoids backtracking for all but one example, making automation failures easier to diagnose.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 1:23Fine-grained concurrency challenges
- 3:50Backtracking proof search issues
- 7:22Classical logic limits
- 8:48Connection calculus for disjunctions
- 10:34How connection approach works
- 12:43Implementation and evaluation
- 13:27Conclusion and future work
- 14:08Q&A
- 15:10Q&A: Implicit dynamic frames
- 16:32Q&A: New verifications with diaphrag
- 17:41Q&A: Automation duration
- 18:02Q&A: Relaxed memory and disjunctions
related talks
17mFormalizing Determinacy of Concurrent Revisions
24mConcurrent Quantum Separation Logic for Fine-Grained Parallelism
28mFormalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems
17mCalculational design of Incorrectness Separation Logic
25mA Relational Separation Logic for Effect Handlers
20mPulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs
21mOutcome Separation Logic: Local Reasoning for Correctness and Incorrectness with(…)
20mQuiver: Guided Abductive Inference of Separation Logic Specifications in Coq