pub struct HeldLines { /* private fields */ }Expand description
The run’s line of history: the lines appended but not yet durable,
and the refs of the lines already durable, in the order they were
appended. It lives as long as the run (Run<Active>) and every turn
borrows it, so a turn’s last lines wait for the barrier of the next
turn instead of paying one of their own (runtime D36).
HeldLines::barrier hands every held line to the ledger in one
Ledger::append_all and only then keeps their refs, so a ref it hands
out names a durable record. A turn calls it before each outside
effect - a model call, a write - and the run calls it once more before
it freezes, and nowhere else (runtime D24, D36,
crates/runtime/spec/Turn/Durability.lean).
Implementations§
Source§impl HeldLines
impl HeldLines
Sourcepub fn open(run: RunId, who: String) -> HeldLines
pub fn open(run: RunId, who: String) -> HeldLines
The lines of run run, written by who; nothing is held yet.
Sourcepub fn barrier(&mut self, ledger: &mut dyn Ledger) -> Result<(), AxError>
pub fn barrier(&mut self, ledger: &mut dyn Ledger) -> Result<(), AxError>
Every held line, in the order it was appended, through one
Ledger::append_all. Holding nothing, it asks the ledger nothing.
§Errors
Propagates the ledger’s refusal; the lines it refused are dropped, and the run ends on that error.