Expand description
Durable state, read and written synchronously.
A write does not return until it would survive a crash. So a protocol that writes and then sends cannot be seen to have made a promise it has no record of — there is no other point at which a driver could synchronise with a synchronous protocol.
Reads are synchronous too, which is honest while the record is mirrored in memory. For a log larger than memory a read is a real disk read; that is a bound of this interface.
Structs§
- Keyed
Slot - Where one of a family of children keeps its record, inside its parent’s.
- MemStore
- A store held in memory: the simulator’s, and a test’s.
- NoStore
- What a child that keeps nothing durably is handed.
- Position
- A position in the appended sequence.
- SeqSlot
- Where a child’s appended entries live inside its parent’s sequence.
- Slot
- Where a child’s durable record lives inside its parent’s.
Traits§
- Store
- One value that is replaced, and a sequence that grows.