PLSE Seminar — Tej Chajed: Combining automated and interactive proofs to verify the DaisyNFS concurrent and crash-safe NFS server
Abstract: DaisyNFS is an NFS server implemented in Go with a proof that each operation is atomic with respect to concurrency, atomic if the system crashes, and returns correct results according to the NFS specification. It is the first verified file system with crash safety and concurrency. To make DaisyNFS's operations atomic, we implemented GoJournal, a high-performance transaction system.
The proof also divides reasoning about GoJournal from file-system reasoning, with a proof that GoJournal executes transactions atomically and file-system proofs that show each operation is implemented correctly. A key contribution of this work is an approach to combine different tools for these two verification efforts: the proof of the transaction system uses a custom program logic, Perennial, to handle reasoning about concurrency and crash safety, while the proof of the file-system operations uses Dafny to reason about sequential code with a high degree of automation. The technical contribution that enables this separation is a careful choice of intermediate specification for the transaction system and an (on-paper) proof that composes theorems from Perennial and Dafny.
Measurements of DaisyNFS shows it achieves good performance compared to ext4 exported through the Linux NFS server (at least 75% throughput across a range of in-memory benchmarks). Dafny's automated verification was productive enough to implement and verify a variety of features, including large files and enough to run git clone and make. The proof of this functionality was manageable: although the proof-to-code ratio of the transaction system is 22x, the file system is only 2x as many lines of proof as code.
In this talk I will focus on DaisyNFS while also conveying some interesting challenges in the GoJournal implementation and proof. Details on GoJournal can be found in our recently-published OSDI paper at https://www.chajed.io/papers/gojournal:osdi2021.pdf, while DaisyNFS is still under submission.
Bio: Tej Chajed works with Frans Kaashoek and Nickolai Zeldovich in the PDOS group.
The proof also divides reasoning about GoJournal from file-system reasoning, with a proof that GoJournal executes transactions atomically and file-system proofs that show each operation is implemented correctly. A key contribution of this work is an approach to combine different tools for these two verification efforts: the proof of the transaction system uses a custom program logic, Perennial, to handle reasoning about concurrency and crash safety, while the proof of the file-system operations uses Dafny to reason about sequential code with a high degree of automation. The technical contribution that enables this separation is a careful choice of intermediate specification for the transaction system and an (on-paper) proof that composes theorems from Perennial and Dafny.
Measurements of DaisyNFS shows it achieves good performance compared to ext4 exported through the Linux NFS server (at least 75% throughput across a range of in-memory benchmarks). Dafny's automated verification was productive enough to implement and verify a variety of features, including large files and enough to run git clone and make. The proof of this functionality was manageable: although the proof-to-code ratio of the transaction system is 22x, the file system is only 2x as many lines of proof as code.
In this talk I will focus on DaisyNFS while also conveying some interesting challenges in the GoJournal implementation and proof. Details on GoJournal can be found in our recently-published OSDI paper at https://www.chajed.io/papers/gojournal:osdi2021.pdf, while DaisyNFS is still under submission.
Bio: Tej Chajed works with Frans Kaashoek and Nickolai Zeldovich in the PDOS group.