hesela.devCrash Hoare Logic
Crash Hoare Logic extends Hoare-style program specifications with crash conditions, recovery execution and logical address spaces for reasoning about persistent state.
In FSCQ, an interrupted operation must leave a state admitted by recovery's precondition. Recovery must preserve that admission condition if it too is interrupted. This permits repeated recovery attempts. [2]
The authors distinguish this recovery use of idempotence from the mathematical property of repeating a completed function. A complete-run retry check alone does not cover interrupted recovery. [2]
Completion and recovery can have different postconditions. The paper's two-block example requires both updates on ordinary completion, while recovery can admit either complete version. [1]
CHL is a specification and proof framework, not a universal durability policy. The later DFSCQ system uses deferred writes and a different metadata-prefix contract. [3]
Relations
- related
- Crash refinement, Crash-test oracle, Idempotency
Advantages
- Makes the obligations for recovery-time crashes explicit. [1]
Limitations
- A correctness theorem remains relative to its specification, modeled primitives and trusted implementation components. [1]
Citations
- Chen et al. Using Crash Hoare Logic for Certifying the FSCQ File System. SOSP 2015; sections 3.4, 4.3 and 6. DOI: 10.1145/2815400.2815402.
- Chajed et al. Certifying a File System Using Crash Hoare Logic: Correctness in the Presence of Crashes. CACM 60(4), 2017; section 3. DOI: 10.1145/3051092.
- Chen et al. Verifying a high-performance crash-safe file system using a tree specification. SOSP 2017; sections 1 and 4. DOI: 10.1145/3132747.3132776.
Further reading
Sources & caveats
- Primary-source synthesis and a separate synthetic redo illustration; no FSCQ installation, Coq proof rerun or power-loss experiment by Hesela.