Modular Reasoning about Global Variables and Their Initialization
summary
Presents a verification method that lets clients assume global state only when three concrete conditions hold: module invariants are established, initialization has started and is not ongoing (checked via initialization levels), and the caller holds a module token granting safe access. Technique is formalized in a concurrent separation logic in Iris and proven sound in Rocq, implemented in verifiers (Vor and Gobra) and applied to a reproduced build including a 5,000-line Go router; artifacts and DOI available.
AI-written summary · about
chapters (11)
- 0:00Modular reasoning about globals
- 1:46Initialization order challenges
- 3:09Module invariants as specs
- 4:53Three proof obligations
- 5:58Proving initialization started
- 7:00Preventing ongoing initialization
- 9:06Ensuring invariant safety
- 10:31Module tokens for access
- 11:12Concurrent separation logic
- 12:17Verification results
- 12:39Q&A
related talks
17mModular Verification of Safe Memory Reclamation in Concurrent Separation Logic
15mModular Verification of Op-Based CRDTs in Separation Logic
28mReasoning about Distributed Reconfigurable Systems
20mNola: Later-Free Ghost State for Verifying Termination in Iris
40mRelational Reasoning in Object-based Programs
20mA Modular Approach to Metatheoretic Reasoning for Extensible Languages
20mA conceptual framework for safe object initialization: a principled and mechani...
19mLeaf: Modularity for Temporary Sharing in Separation Logic