The full source code of FSCQ is available online: https://github.com/mit-pdos/fscq-impl
"Beware of bugs in the above code; I have only proved it correct, not tried it." -Donald Knuth
And this bug:
EDIT: I should have elaborated further. I did not intend to sound like I'm dismissing this work, because it's a cool step forward. It's just that this reminded me of those things that happened before.
Running SibylFS on Fscq showed up some limitations:
- https://github.com/mit-pdos/fscq-impl/issues (mostly basic missing POSIXisms)
- https://github.com/mit-pdos/fscq-impl/issues/2 an interesting one where the proof about truncate was incorrect in the specification and lead to very weird observable filesystem behaviour.
Copy of the SibylFS paper here for the interested; http://anil.recoil.org/papers/2015-sosp-sibylfs.pdf
Having said that, these are edges to be polished -- Fscq is an absolutely fantastic advancement in filesystems, and it shouldn't be too many years before we can have a formally verified and specified filesystem in production.
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.
I think it's interesting, and would be great if something like this were applied to ZFS.
The words "checksum", "digest", or "integrity" don't appear in the paper at all.
It's probably a case of "in theory the bits you write to the disk are the bits you later read back, in practice they are not"