TY - GEN
T1 - Verifying the DaisyNFS concurrent and crash-safe file system with sequential reasoning
AU - Chajed, Tej
AU - Tassarotti, Joseph
AU - Theng, Mark
AU - Kaashoek, M. Frans
AU - Zeldovich, Nickolai
N1 - Funding Information:
Many people helped improve this paper, including the anonymous reviewers, the PDOS students who gave feedback, Henry Corrigan-Gibbs, and our shepherd, Manos Kapritsos. James Wilcox provided expert debugging assistance. Robert Morris tested DaisyNFS and reported the bugs in Figure 15. This research was supported by NSF awards CNS-1563763 and CCF-1836712.
Publisher Copyright:
© 2022 by The USENIX Association. All rights reserved.
PY - 2022
Y1 - 2022
N2 - This paper develops a new approach to verifying a performant file system that isolates crash safety and concurrency reasoning to a transaction system that gives atomic access to the disk, so that the rest of the file system can be verified with sequential reasoning. We demonstrate this approach in DaisyNFS, a Network File System (NFS) server written in Go that runs on top of a disk. DaisyNFS uses GoTxn, a new verified, concurrent transaction system that extends GoJournal [9] with two-phase locking and an allocator. The transaction system's specification formalizes under what conditions transactions can be verified with only sequential reasoning, and comes with a mechanized proof in Coq [37] that connects the specification to the implementation. As evidence that proofs enjoy sequential reasoning, DaisyNFS uses Dafny [26], a sequential verification language, to implement and verify all the NFS operations on top of GoTxn. The sequential proofs helped achieve a number of good properties in DaisyNFS: easy incremental development (for example, adding support for large files), a relatively short proof (only 2× as many lines of proof as code), and a performant implementation (at least 60% the throughput of the Linux NFS server exporting ext4 across a variety of benchmarks).
AB - This paper develops a new approach to verifying a performant file system that isolates crash safety and concurrency reasoning to a transaction system that gives atomic access to the disk, so that the rest of the file system can be verified with sequential reasoning. We demonstrate this approach in DaisyNFS, a Network File System (NFS) server written in Go that runs on top of a disk. DaisyNFS uses GoTxn, a new verified, concurrent transaction system that extends GoJournal [9] with two-phase locking and an allocator. The transaction system's specification formalizes under what conditions transactions can be verified with only sequential reasoning, and comes with a mechanized proof in Coq [37] that connects the specification to the implementation. As evidence that proofs enjoy sequential reasoning, DaisyNFS uses Dafny [26], a sequential verification language, to implement and verify all the NFS operations on top of GoTxn. The sequential proofs helped achieve a number of good properties in DaisyNFS: easy incremental development (for example, adding support for large files), a relatively short proof (only 2× as many lines of proof as code), and a performant implementation (at least 60% the throughput of the Linux NFS server exporting ext4 across a variety of benchmarks).
UR - http://www.scopus.com/inward/record.url?scp=85141075327&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85141075327&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:85141075327
T3 - Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2022
SP - 447
EP - 463
BT - Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2022
PB - USENIX Association
T2 - 16th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2022
Y2 - 11 July 2022 through 13 July 2022
ER -