Play all

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

Description:

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

USENIX

Add to list

#Conference Talks #OSDI (Operating Systems Design and Implementation) #Programming #Programming Languages #Go #Computer Science #Software Engineering #Formal Verification

0:00 / 0:00