All for One and One for All: Program Logics for Exploiting Internal Determinism in(…)
summary
Defines schedule-independent safety: showing one terminating execution is safe suffices to guarantee safety for all schedules. Introduces separation logic Musketeer to prove that property and a second logic Angelic to verify a chosen sequential interleaving. Proves soundness of MiniDet, an affine type system that enforces internal determinism and enables Angelic verification. All proofs are mechanized in Coq on top of Iris; artifacts and benchmarks (including a deterministic concurrent hash set) are on Zenodo and linked from the DOI.
AI-written summary · about
chapters (23)
- 0:00Introduction
- 0:22Duma motivating example
- 1:27Verifying concurrent programs
- 3:14Internal determinism
- 4:39Musketeer and Angelic logics
- 5:23Musketeer triples
- 6:49Differences from separation logic
- 8:54Existential quantification in Musketeer
- 10:23Ghost return values
- 11:50Musketeer design
- 12:32Duma schedule independence
- 13:13Miniet type system
- 14:22Angelic logic intro
- 15:05Angelic logic rules
- 16:28Interleaving selection
- 17:11Resuming tasks in proofs
- 17:52Duma proof with Angelic
- 18:53Conclusion and future work
- 19:56Questions on commutativity and logic
- 20:59Type system safety
- 21:46Fairness assumptions
- 22:52Equivalence relations
- 23:54Combining proofs
related talks
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz
24mTaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr
21mContextual Refinement of Higher-Order Concurrent Probabilistic Programs
19mAn Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: T...
24mA Concurrent Program Logic with a Future and History
01h 00mKeynote Talk: Outcome Logic: a foundational framework for concurrent and probabilistic(…)
20mDisentanglement with Futures, State, and Interaction