3 ms·
It's pretty cool, but it's a little disappointing that they handwave away the possibility that block writes might not happen atomically. Formal verification is
by tokenrove 11y ago
It's pretty cool, but it's a little disappointing that they handwave away the possibility that block writes might not happen atomically. Formal verification is only as good as the assumptions you start from.
- anishathalye 11y agoI think it's more work to reason about partial block writes. The paper does have a paragraph on this: > The `disk_write` specification states that blocks are written atomically; that is, after a crash, a block must contain either the last-written value or one of the previous values, and partial block writes are not allowed. This is a common assumption made by file systems, as long as each block is exactly one sector, and we believe it matches the behavior of many disks in practice (modern disks often have 4 KB sectors). Using CHL, we could capture the notion of partial sector writes by specifying a more complicated crash condition, but the specification shown here matches the common assumption about atomic sector writes. We leave to future work the question of how to build a certified file system without that assumption.