The trim that hid the fence

A log that keeps everything forever gets long. A writer that saves snapshots of its state doesn't need the history below the latest one. It wants to say "drop everything before offset 500" and have the stream start there.

Felix's head trim is designed for that, with one condition: the trim lands only if the stream's tail is still where the writer expects. That condition is how a writer that lost its lease is kept from trimming. While we modelled it, the model checker found a way for a trim to hide the very write that was meant to stop the old writer. This post is about that trace, the fix, and the broken versions we keep around on purpose.

Why trim, and why it has to be conditional

felixd is the case we design for. A node runs a workload while it holds the workload's lease. It writes the workload's output to a stream, saves snapshots, and would like history below its snapshot to go away.

The dangerous node isn't the dead one. It's the one that froze, lost its lease while frozen, and woke up still thinking it's in charge. felixd stops it without trusting anyone's clock. Every write is conditional on the tail: it lands only if the stream's next offset is the one the writer expects. A new lease holder makes one such write as soon as it takes over. We call that its fenced write. After it, the old holder's idea of the tail is wrong, so its next write is refused. It then reads the stream from where it left off, sees a record from a newer lease epoch, and stops.

A trim is a record in the log too, appended under the same tail check. Of a stale holder's trim and the new holder's write at the same tail, exactly one lands. The trim carries the floor it asks for, and reads below the floor are refused with CursorTooOld. Readers skip trim records, as they skip other bookkeeping records.

That all sounded tight. We wrote it down in TLA+ before building the parts above storage.

What TLA+ and TLC are

TLA+ is a language for writing down how a system is allowed to behave. You describe its state, like what each broker's log holds and what each lease holder thinks the tail is, and the steps that can change it, like "a holder writes at the tail it expects" or "a broker deletes old segments". It's a precise description of the design. It isn't code, and nothing runs it in production.

TLC is the model checker for TLA+. Give it small limits, say three brokers, two lease holders, two writes and three trims, and it tries every possible order of those steps. In every state it reaches it checks the rules we care about. One of ours is "no reader is ever served a record below a trim that was acknowledged". When a rule breaks, TLC prints the exact sequence of steps that got there. That's a counterexample.

Races like the one below need a particular order of a handful of steps across two writers and three brokers. A test might hit that order once in a million runs, or never. TLC doesn't sample. It walks every order within the limits.

The model is FelixHeadTrim.tla. It has three brokers with Raft-shaped leadership, two lease holders, writes and trims that carry the holder's epoch, deletion of old segments, failover, and a leader that keeps taking writes after it has been deposed. Its rules include StaleTrimRefused: no committed write or trim from one holder follows a committed write from a newer holder. That is the whole point of fencing, stated as an invariant.

The trace

TLC broke StaleTrimRefused in a couple of seconds. The model numbers log positions from 1.

1. Holder 1 has the lease but hasn't written anything yet. The lease moves to holder 2, and nobody tells holder 1.
2. Holder 2 makes its fenced write at position 1. It's acknowledged.
3. Holder 2 trims before 2. That's allowed: a trim may ask for a floor up to its own position, and the fenced write is just old history once there's a snapshot. The trim record lands at 2, and the floor moves to 2.
4. Holder 1 reads from position 1, where its cursor is. That's below the floor, so the read is refused as too old. It resumes at the floor, position 2. The only thing there is the trim record, which readers skip. It sees no write from epoch 2, so it takes the tail as its own.
5. Holder 1 writes at 3 and trims at 4, after holder 2.

The fenced write did its job until it was trimmed. After that, the only trace of epoch 2 below the tail was the trim record, and nobody reads those. The trim hid the fence.

The first fix

The obvious fix is to let readers see trim records, with the epoch on them. Holder 1 resumes at the floor, reads the trim record, sees epoch 2 and stops. We made that change to the model and the trace went away.

We didn't keep it. A stale holder only learns from a trim record if the record is still there to read, and retention can delete records past the floor. The change also put a new kind of record in front of every reader. Every subscriber and every client library would need to learn to skip it, just so one kind of writer could spot a fence. Felix adds features so that a peer that predates them exchanges the same frames as before, and that change would have broken it for every reader of a trimmed stream.

The fix we chose

A stale holder that was trimmed past always gets the same answer: CursorTooOld. So that answer is where the news goes.

A trim carries the caller's headers, which is where felixd puts its epoch. When a read starts below where the log can serve, CursorTooOld is to carry the headers of the trim that set the floor, as an optional field that is absent by default. A reader that predates trims sees the same frame it always did. Holder 1 is refused, sees epoch 2 in the refusal, and stops. Readers still skip trim records.

The tag has to survive deletion, and it does without any extra bookkeeping. A trim's floor can be at most the position the trim record itself lands at, so the record that set the floor always sits at or above it. Each broker deletes only whole segments below the floor, and never the active one, so with retention off that record is never deleted. Felix's storage keeps one entry per trim record, its offset, floor and headers, and that entry is derived like the indexes. If it's lost, a scan of the records rebuilds it. This part is built: storage applies the floor, deletes below it and returns the floor-setting trim's headers when it refuses a read. The model checks it too, with FloorRecordKept: the serving leader's floor is always the one its trim records set, deleted ones included.

The model holds felixd to a few more rules.

• Re-read from your own cursor. Reading from earliest resolves to the floor, so the read isn't refused, the trim records are skipped, and the holder never sees the tag.
• Never take the tail from a refusal. A write refused with OffsetMismatch names the current tail. A stale holder that adopted it could write straight after the new holder without reading anything. The tail comes only from what a holder reads or from its own acknowledged answers.
• A no-op trim still checks the tail. A trim at or below the current floor writes nothing, but felixd takes its next tail from the answer. If the no-op skipped the check, the stale holder would learn the new tail from it and write after the new holder.
• Retention stays off. Retention can delete the new holder's fenced write with no trim involved, and then the refusal has no tag to carry. Neither fix survives that, so a stream fenced by its tail runs with retention off.

Keeping the bugs around

Each rule has a switch in the model, and each switch has a configuration that turns it off and must fail. These are twins: the passing configuration with one rule removed. scripts/check_tla.sh holds each twin to the invariant it's expected to break, so a twin that stops failing fails CI. We wrote about why that matters in Our model said everything passed.

Each name drops the FelixHeadTrim prefix. The twins fail in seconds. The passing side is slower: the main configuration, with three trims or no-ops and one promotion, explores about 9.75 million distinct states in ten minutes. Checking everything together, three trims, two promotions and a crash, didn't finish in 75 minutes, so the pass is split across four configurations that each cover part of it.

The heart of the fix is a few lines in the step where a holder reads:

    /\ LET from == expected[h] + 1
           rs == ReadableStart(s)
           tooOld == from < rs
           newer == { i \in Max(from, rs)..commit[s] :
                        log[s][i].k = "w" /\ log[s][i].h > h }
       IN IF (tooOld /\ FloorTag(s) > h) \/ newer /= {}
             THEN /\ retired' = [retired EXCEPT ![h] = TRUE]
                  /\ UNCHANGED expected
             ELSE /\ expected' = [expected EXCEPT ![h] = commit[s]]
                  /\ UNCHANGED retired

With Untagged on, FloorTag is 0, the first half of the test can never be true, and TLC walks straight back to the trace above.

What we learned

A fence is only as good as a stale writer's ability to see it. We had thought about who could write at the tail. We hadn't thought about a newer writer erasing its own proof that it exists.

The place to tell someone they've lost is the answer they're guaranteed to get. A stale holder that was trimmed past will always be refused as too old. Putting the news in that refusal works for any reader, needs nothing new from readers that don't care, and leans on a record the storage layout already keeps.

The tag, the no-op check and retention each have a twin that breaks without them. If someone later decides a no-op trim can skip the tail check to save a lookup, CI will show them the trace.

Trying it

The model and every configuration are in docs/formal/, and the README section "A trim is a record" walks through them. The design is in "Conditional head trim" in docs/replication-design.md and docs/durable-storage.md, and the decisions are in #1662. #1663 added the model.

To watch TLC find the trace, from the repo root:

scripts/check_tla.sh FelixHeadTrimHiddenTrims

That needs Java 11 or later, or Docker or Podman. TLC prints the counterexample, and the script passes, because that twin is expected to fail.

docker compose up -d