The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic
summary
Proposes a new modality that permits non-frame-preserving updates to ghost state inside Iris, formalizes a parameterized stack-cutting transformation that removes frames above a threshold, and uses it to give the first separation-logic spec for a high-level language with explicit stack allocation and multi-frame return that clears frames. Shows two existing Iris modalities as special cases, proves monotonicity and commutation properties, integrates with Iris invariants, and is mechanized in Iris/Coq with artifact archive.
AI-written summary · about
chapters (23)
- 0:00Introduction
- 0:23Frame preserving limits in separation logic
- 1:46Non-frame preserving stack deallocation
- 3:30Basic nextgen modality
- 4:35Iris separation logic background
- 5:39Technical definition of nextgen
- 6:41Properties with existing Iris modalities
- 7:27Comparison with Perennial
- 8:29Extending to multiple resource algebras
- 9:55Case study: Starling stack deallocation
- 11:38Ghost state for stack and heap
- 12:22Stack allocation rule
- 12:43Return rule with deallocation
- 13:04Stack cut transformation
- 13:44Program logic rule with nextgen
- 15:09Example walkthrough
- 16:36Applying return rule
- 17:40Benefits without frame loss
- 18:01Trade-offs and frame rule loss
- 18:44Recovering frame rule
- 19:07Interaction with invariants and variants
- 20:12Conclusion and mechanization
- 21:04Q&A
related talks
20mNola: Later-Free Ghost State for Verifying Termination in Iris
19mProof Automation for Linearizability in Separation Logic
19mLeaf: Modularity for Temporary Sharing in Separation Logic
16mA metalanguage for multi-phase modularity
15mModal Abstractions for Virtualizing Memory Addresses
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
05mNew foundations for probabilistic separation logic
17mModular Verification of Safe Memory Reclamation in Concurrent Separation Logic