Making a KV store linearizable on Raft — and proving it with a checker

The last two weeks built a replicated log that stays consistent across partitions, leader changes, and
crashes. This week I put a key-value store on top of it — and then did something I hadn’t done yet in
this series: instead of testing “does it look right,” I used a real linearizability checker to ask “is
there any valid explanation for what this cluster just did.” It found nothing wrong. Along the way,
writing the test that tried to break it found a real bug — two weeks upstream, in code I’d already
shipped.

What I built

A Get/Put/Append API, same shape as Week 2’s single-node version, now replicated: every operation
— reads included — goes through the Raft log before it’s answered.

client ──Get/Put/Append──► leader
                              │ propose as a log entry (Op{Type, Key, Value, ClientID, Seq})
                              ▼
                     replicate + commit (Weeks 3-4)
                              │
                              ▼
                 apply to state machine (Week 1's storage engine, again)
                              │
                              ▼
                   answer, matched back to the waiting client by (ClientID, Seq)

The concepts that made it work

• Even reads go through consensus. The obvious shortcut — answer a Get straight from local state —
  can return stale data: a partitioned-away former leader, or a leader that hasn’t confirmed via a
  majority that it’s still the leader, could both hand back an old value. Routing Get through the
  log exactly like a write sidesteps the whole question: it’s ordered consistently with every other
  operation because, as far as Raft is concerned, it is one. Slower per read, but correct by
  construction instead of correct-if-you-get-a-subtler-protocol-exactly-right.
• A stale leader must never return a stranger’s result as its own. A leader can accept a write, then
  lose its majority before replicating it. If it later reconnects, its stale entry gets overwritten by
  whatever the actual leader committed at that same log position — and if the original client request
  is still waiting, it has to notice the swap and fail, not hand back the other operation’s result
  wearing its name. One equality check does this, but it only matters because of a sequence of events
  that’s easy to describe and surprisingly fiddly to actually force in a test.
• A linearizability checker answers a different, stronger question than a convergence test.
  “Does Get eventually return the right value” proves the system settles correctly. A checker
  (Porcupine) takes the full recorded history — real
  concurrent clients, real timestamps — and asks: does any sequential ordering, consistent with how
  those operations actually overlapped in time, explain what was observed? That’s linearizability’s
  actual definition, not an approximation of it.
• Partition by key. Checking linearizability is NP-hard in general — the search space is every
  possible interleaving of concurrent operations. But if keys never interact, each key’s history can be
  checked independently, which is both correct and the difference between “instant” and “don’t bother.”

The thing that bit me

I wrote a test to force the stale-leader scenario directly — isolate a leader right after it accepts a
write, let the rest of the cluster elect someone else and commit something different at the same index,
reconnect, confirm the original request fails instead of returning the wrong answer. It passed. Good —
except it also passed when I deliberately broke the check it was supposed to be testing, about half
the time. It was passing for the wrong reason: timing out, not detecting the swap.

Chasing that down — polling and logging actual term and leadership state through a slow run instead of
guessing — led somewhere I didn’t expect: a real liveness bug in my Week 3 code. A node that gets
demoted after merely seeing a higher term (not granting a vote, not hearing a real heartbeat) never
had its election timer reset. So it would immediately re-campaign, forcing whoever it contacted to step
down too, and the cluster could spend a second or two in pointless repeated elections before settling.
Never a safety problem — no split-brain, no lost data, every existing test had stayed green through
weeks of -race runs — but a latency problem invisible to patient tests that only becomes visible once
something above it imposes a tight timeout. The fix was one line. Finding it required treating a flaky
test as a lead, not a nuisance to silence with a longer timeout.

Tradeoffs & the road not taken

• Reads pay a full log round-trip. The real optimization — ReadIndex (the leader confirms its
  leadership with one heartbeat round before answering locally) or a time-bounded leader lease — buys
  back that latency without giving up correctness, but only once the simple version is provably
  correct. I left it as a stretch goal rather than building it first: earning the right to the fast path
  felt more honest than assuming it.
• The liveness fix was the narrow one, not the general one. The textbook answer for “a straggler
  node keeps disrupting a healthy leader” is PreVote (what etcd runs) — probe for votes without actually
  bumping your term, so you can’t force a step-down unless you could really win. I fixed the specific
  pathology I found instead of building the general mechanism; PreVote is now also on the stretch list.

Where this sits in the system

Storage (Week 1), a networked server that’s honest about retries (Week 2), and a replicated log that
survives partitions and crashes (Weeks 3-4) just became one thing: a key-value store where every
operation, proven rather than assumed, behaves exactly as if there were only one copy of the data. Next:
shard the keyspace across multiple Raft groups — the unit of sharding is the system built this week, not
a toy.

Part of a series building a distributed database from scratch.