Skip to content

Verified, concurrent, crash-safe transaction system

License

Notifications You must be signed in to change notification settings

mit-pdos/go-journal

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

GoTxn: a verified, concurrent, crash-safe transaction system

CI

GoTxn is a transaction system that makes it easy to safely access a disk with concurrent transactions that are atomic if the system crashes in the middle. The implementation is verified in Perennial, and the proof can be found alongside the Perennial framework.

The biggest use of GoTxn is GoNFS, a verified implementation of the Network File System (NFS) API that uses GoTxn to simplify implementing and verifying a concurrent file system.

This repository is still called go-journal, as GoTxn evolved from a journaling system to a transaction system. The journaling layer is still available as github.com/mit-pdos/go-journal/jrnl.

Publications

GoJournal: a verified, concurrent, crash-safe journaling system at OSDI 2021