README
¶
GoTxn: a verified, concurrent, crash-safe transaction system
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
Directories
¶
| Path | Synopsis |
|---|---|
|
buf manages sub-block disk objects, to be packed into disk blocks
|
buf manages sub-block disk objects, to be packed into disk blocks |
|
Package jrnl is the top-level journal API.
|
Package jrnl is the top-level journal API. |
|
lockmap is a sharded lock map.
|
lockmap is a sharded lock map. |
|
Package obj atomically installs objects from modified buffers in their corresponding disk blocks and writes the blocks to the write-ahead log.
|
Package obj atomically installs objects from modified buffers in their corresponding disk blocks and writes the blocks to the write-ahead log. |
|
Package txn implements a full transaction interface on top of GoJournal.
|
Package txn implements a full transaction interface on top of GoJournal. |
|
wal implements write-ahead logging
|
wal implements write-ahead logging |
Click to show internal directories.
Click to hide internal directories.