We found a bug in a verified file system! We ran Crashmonkey's suite of tests on MIT's FSCQ and found that it does not persist data on fdatasync properly. We emailed the authors, they have acked and fixed the bug.
Come see our paper at #osdi18!
Details: https://github.com/utsaslab/crashmonkey …https://twitter.com/vj_chidambaram/status/1045714072950501377 …
-
-
Yup, I’ve acknowledged it’s the unverified part of the final software artifact that has the bug — these parts are often ignored!
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.