GoJournal: a verified, concurrent, crash-safe journaling system

on YouTube ↗14m

" summary

GoJournal implements a verified, concurrent, crash-safe journaling API in Go and proves it in Coq with Perennial 2.0, using the Goose translator to model Go code. The proof is about 26,000-line proof (≈20× code:proof ratio) and uncovers one serious concurrency bug. A practical unverified NFS server, GoNFS, uses GoJournal and achieves roughly 90–95% throughput of Linux NFS on an NVMe-backed AWS i3 machine while scaling better under many clients.

AI-written summary · about

" chapters (24)

1. 0:00Intro
2. 0:15Suppose we want to write a correct file system
3. 0:36Gojournal gives a storage system efficient, atomic writes
4. 1:29Current approaches cannot handle a system of this complexity
5. 1:59Contributions
6. 2:29Gojournal writes operations atomically to disk
7. 2:57Operations can concurrently manipulate objects within a block
8. 3:17Specification challenge: what do concurrently committed operations do?
9. 3:47Sequential journaling only maintains old and next state
10. 4:42An operation's specification only refers to its disk footprint
11. 5:32Introduce assertion for operation's view of disk
12. 6:07Key idea: operations manipulate an in-memory view of each object
13. 7:17Gojournal has a modular implementation and proof
14. 7:40Write-ahead log implements the core atomicity of the journal
15. 8:11Writes are buffered before being logged
16. 8:49Challenge 1: Reads can observe unstable writes
17. 9:22Object layer implements sub-block object access
18. 9:34Challenge 2: Reads and writes can proceed concurrently
19. 10:10Concurrent writes are unsafe due to read- modify-write sequence
20. 11:06Implementation overview
21. 12:08Experimental setup
22. 12:45GONFS gets comparable performance even with a single client
23. 13:11Gojournal allows GONFS to scale with number of clients
24. 13:53Summary