GoJournal - A Verified, Concurrent, Crash-Safe Journaling System
Explore a verified, concurrent, crash-safe journaling system called GoJournal in this OSDI '21 conference talk. Dive into the main contribution of GoJournal and its companion framework, Perennial 2.0, which enables formal specification and verification of concurrent crash-safe systems. Learn about the techniques introduced to formalize GoJournal's specification and manage implementation proof complexity, including lifting predicates, crash framing, and logically atomic crash specifications. Discover how GoJournal, implemented in Go, was used to build a functional NFSv3 server called GoNFS, and examine performance experiments comparing GoNFS to Linux's NFS server. Gain insights into the challenges of concurrent and crash-safe systems, the modular implementation and proof of GoJournal, and the benefits of its approach for application verification.