4 ms·

I can't help but think of a couple things: "Beware of bugs in the above code; I have only proved it correct, not tried it." -Donald Knuth And this bug: http:/

by Natsu 11y ago

I can't help but think of a couple things: "Beware of bugs in the above code; I have only proved it correct, not tried it." -Donald Knuth And this bug: http://googleresearch.blogspot.com/2006/06/extra-extra-read-all-about-it-nearly.html http://googleresearch.blogspot.com/2006/06/extra-extra-read-... 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.

anishathalye 11y ago
That's what is really cool about this work -- it's not just an algorithm that's proven correct on paper, it's a formally verified _implementation_, so there's no formality gap.
- avsm 11y ago
  There is a gap between the formal specification and reality though. We published some work (coincidentally presented right after this paper at SOSP 2015) on building a real-world mathematical model of POSIX and using it to test existing filesystems; http://sibylfs.io http://sibylfs.io Running SibylFS on Fscq showed up some limitations: - https://github.com/mit-pdos/fscq-impl/issues https://github.com/mit-pdos/fscq-impl/issues (mostly basic missing POSIXisms) - https://github.com/mit-pdos/fscq-impl/issues/2 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 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.
  - unboxed_type 11y ago
    There is a gap between human understanding and reality, so any abstraction including mathematics may have a flaw, in my opinion. But refinement of that understanding is crucial to get better at building mostly-reliable systems.
throwaway999888 11y ago
Pretty middlebrow dismissal. How about educating us about something pertinent to the paper in particular, instead of seemingly just scoffing at the idea of formal verification of software in general?
- Natsu 11y ago
  My comment was in no way intended as a dismissal of this work.
  - throwaway999888 11y ago
    Those types of comments that lead off with a "by the way" of some witty quote has the effect of being dismissive in a pretty non-informative way. It's not that I think that's your intent at all; I have no doubts about your sincerity. Just telling you what effect it has, at least to my eyes. :)
    - Natsu 11y ago
      Well it's not that I can't see how someone could read it that way, that's why I edited in the disclaimer.
- 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 ago
    I 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.
oh_sigh 11y ago
I believe that if a formal proof system had knowledge of fixed width integers, it could detect the potential overflow in your googleresearch link.

by Natsu 11y ago

anishathalye 11y ago

That's what is really cool about this work -- it's not just an algorithm that's proven correct on paper, it's a formally verified _implementation_, so there's no formality gap.

avsm 11y ago
There is a gap between the formal specification and reality though. We published some work (coincidentally presented right after this paper at SOSP 2015) on building a real-world mathematical model of POSIX and using it to test existing filesystems; http://sibylfs.io http://sibylfs.io Running SibylFS on Fscq showed up some limitations: - https://github.com/mit-pdos/fscq-impl/issues https://github.com/mit-pdos/fscq-impl/issues (mostly basic missing POSIXisms) - https://github.com/mit-pdos/fscq-impl/issues/2 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 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.
- unboxed_type 11y ago
  There is a gap between human understanding and reality, so any abstraction including mathematics may have a flaw, in my opinion. But refinement of that understanding is crucial to get better at building mostly-reliable systems.

throwaway999888 11y ago

Pretty middlebrow dismissal. How about educating us about something pertinent to the paper in particular, instead of seemingly just scoffing at the idea of formal verification of software in general?

Natsu 11y ago
My comment was in no way intended as a dismissal of this work.
- throwaway999888 11y ago
  Those types of comments that lead off with a "by the way" of some witty quote has the effect of being dismissive in a pretty non-informative way. It's not that I think that's your intent at all; I have no doubts about your sincerity. Just telling you what effect it has, at least to my eyes. :)
  - Natsu 11y ago
    Well it's not that I can't see how someone could read it that way, that's why I edited in the disclaimer.
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 ago
  I 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.

oh_sigh 11y ago

I believe that if a formal proof system had knowledge of fixed width integers, it could detect the potential overflow in your googleresearch link.