How vanlightly/s3-wal-collection works
This repository is a research collection of TLA+ specifications for WAL designs using object storage, not a running WAL service. The principal workflow is to review the collection’s criteria and design categories, then inspect a model to understand its protocol. The README documents single-writer, multi-writer, and not-quite-WAL designs, plus proposals that are not yet modeled. Relationships below reflect documented links only; source excerpts were unavailable, so model internals and execution behavior are not inferred.
Main entry points: README.md Criteria and index · SlateDBWAL.tla SlateDB WAL · SlateDBWAL_CAS.tla SlateDB CAS · BufferAsWAL.tla BufferAsWAL
Components 9
Design catalog
- Criteria and index
README.md
Single-writer
- SlateDB WAL
slatedb/SlateDBWAL.tla - SlateDB CAS
slatedb/SlateDBWAL_CAS.tla - BufferAsWAL
opendata/BufferAsWAL.tla
Multi-writer
- OSWALD
oswald/Oswald.tla - Continuity
cursor/Continuity.tla - Walgit
walgit/Walgit.tla
Not quite WAL
- OpenData Buffer
opendata/Buffer.tla
Other components
- Engineer
Connections 15
- Engineer → Criteria and index: reviews criteria
- Criteria and index → SlateDB WAL: links to
- Criteria and index → SlateDB CAS: links to
- Criteria and index → BufferAsWAL: links to
- Criteria and index → OSWALD: links to
- Criteria and index → Continuity: links to
- Criteria and index → Walgit: links to
- Criteria and index → OpenData Buffer: links to
- Engineer → SlateDB WAL: inspects model
- Engineer → SlateDB CAS: inspects model
- Engineer → BufferAsWAL: inspects model
- Engineer → OSWALD: inspects model
- Engineer → Continuity: inspects model
- Engineer → Walgit: inspects model
- Engineer → OpenData Buffer: inspects model