hesela.devCrash refinement
Crash refinement relates an implementation to a specification by requiring crash-free equivalence and permitting no additional observable outcomes after modeled crashes and recovery.
Yggdrasil defines the relation from equivalent consistent states and includes recovery idempotence. Equivalence is specified, not raw disk-byte identity. [1]
In Yxv6, validating the free-block or free-inode candidate protects allocation safety without proving that the search succeeds whenever space is available. A refinement result must be read alongside the operation's permitted failures and resource guarantees. [1]
A proof does not repair an inadequate specification or certify unverified integration code. The released artifact warns about both boundaries. [2]
Relations
Advantages
- Supports modular verification against explicit storage contracts. [1]
Limitations
- The research prototype assumes atomic block writes and does not verify concurrent execution. [1]
Citations
- Sigurbjarnarson et al. Push-Button Verification of File Systems via Crash Refinement. OSDI 2016, pp. 1-16; sections 2-3, 4.2, 4.5 and 6.
- Yggdrasil authors. README: guarantees, version differences and limitations; revision e1de61d798acafb9ae2d8387d176c4b091773623.
Further reading
Sources & caveats
- Literature review; no theorem-prover rerun, filesystem execution or hardware validation by Hesela.