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.
GoJournal - A Verified, Concurrent, Crash-Safe Journaling System
Overview
Syllabus
Intro
Suppose we want to write a correct file system
Gojournal gives a storage system efficient, atomic writes
Current approaches cannot handle a system of this complexity
Contributions
Gojournal writes operations atomically to disk
Operations can concurrently manipulate objects within a block
Specification challenge: what do concurrently committed operations do?
Sequential journaling only maintains old and next state
An operation's specification only refers to its disk footprint
Introduce assertion for operation's view of disk
Key idea: operations manipulate an in-memory view of each object
Gojournal has a modular implementation and proof
Write-ahead log implements the core atomicity of the journal
Writes are buffered before being logged
Challenge 1: Reads can observe unstable writes
Object layer implements sub-block object access
Challenge 2: Reads and writes can proceed concurrently
Concurrent writes are unsafe due to read- modify-write sequence
Implementation overview
Experimental setup
GONFS gets comparable performance even with a single client
Gojournal allows GONFS to scale with number of clients
Concurrency in the journal matters
Summary
Taught by
USENIX
