Embedding Hindsight Reasoning in Separation Logic
summary
The work embeds hindsight reasoning into separation logic via a new proof rule called temporal interpolation, implemented in an automated tool that proves linearizability of concurrent set implementations. The tool automatically verifies the challenging Logical Ordering tree, producing the first formal proof, exposing an unknown bug and an earlier erroneous pencil‑and‑paper proof. It currently handles pure non‑fixed linearization points (not impure ones), lacks array support and cannot verify RDCSS/HLyWinq examples. Artifacts are available.
AI-written summary · about
chapters (20)
- 0:00Verifying concurrent data structures
- 1:06Concurrent set traversal challenges
- 2:51Linearizability and linearization points
- 3:56Prophecy variables limitations
- 4:38Hindsight reasoning in separation logic
- 6:45Formal linearizability proof
- 10:01Temporal interpolation rule
- 12:10Tool benchmarks
- 13:14Q&A
- 13:35Support for RDCSS and Harris lock-free queue
- 14:40Handling weak memory models
- 15:01Completeness vs prophecy reasoning
- 15:23Pure vs impure linearization points
- 16:06Comparison with prior work
- 17:10Tool requirements and automation
- 17:53Trace properties for linearizability
- 18:57Scalability to interval linearizability
- 19:20Bug in Logical Ordering Tree
- 19:41Timestamped stack and Q-type structures
- 20:22Conclusion and future work
related talks
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
19mProof Automation for Linearizability in Separation Logic
11mIntroduction
05mNew foundations for probabilistic separation logic
18mDistributed Causal Memory for Higher-Order Distributed Separation Logic
28mReasoning about Distributed Reconfigurable Systems
40mRelational Reasoning in Object-based Programs
27mRooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separatio...