Give disks a write buffer that crashes can tear

CHANGELOG.md

@@ -53,8 +53,17 @@
   leaving peers to notice the outage from their own timeouts. Crashes are
   recorded too: `crash()` writes a trace event and consumes a uid.
 - Every host now has `host.disk`, a mapping that survives its crashes:
-  where state a real process would fsync belongs. Writes are atomic at
-  assignment; there is no partial-write model.
+  where state a real process would fsync belongs. Writes are durable at
+  assignment and `disk.sync()` does nothing — until the host asks for
+  otherwise with `loop.net.set_disk(name, buffered=True)`, which queues
+  writes and deletes until a `sync()` while the host itself reads them
+  back immediately. A crash then takes the queue with it, and `torn=True`
+  keeps a seeded prefix of it instead: the state a machine that lost power
+  mid-batch actually reboots into. A prefix is all it claims to be —
+  nothing is reordered and no value is ever half-written. A disk nobody
+  configured is untouched down to the draw: storage records no trace
+  events and consumes no randomness, so those runs decide everything
+  exactly as they did before.
 - Clocks can lie per host: `loop.net.set_clock(name, offset=...)` skews
   what that host's tasks read from `loop.time()`, and the deadlines they
   hand to `call_at` with it, while durations (`sleep`, `timeout`,
@@ -64,10 +73,12 @@
   exactly the decisions it made without the feature.
 - A second flagship demo: `examples/raft/` is a teaching-sized Raft (leader
   election + log replication, plain asyncio on streams) tested only under
-  simulation — four safety invariants checked over 50,000 chaos seeds, five
+  simulation — four safety invariants checked over 50,000 chaos seeds, six
   safeguard ablations each caught and replayed from a seed, and failing
   schedules minimized toward FIFO — down to a single interesting step in the
-  sharpest case.
+  sharpest case. Its state can live on host disks that buffer and tear, with
+  the syncs Raft owes before it answers an RPC; drop the sync before an
+  append is acknowledged and the first seed loses a committed entry.
 - Campaign evidence at scale, regenerable via `benchmarks/campaign.py`:
   100,000 seeds of jobqueue chaos green in under six minutes on a laptop,
   every ablation caught with its failure density recorded, and 20 sampled

README.md

@@ -233,7 +233,9 @@ net.crash("node2")                              # no reset, just silence
 - **Crashes with a way back** — `net.crash` kills a host's tasks and
   binds, `net.restart` brings it back as a fresh incarnation, and
   `host.disk` is a mapping that outlives both: machines die, reboot, and
-  remember what they wrote down.
+  remember what they wrote down. `net.set_disk(name, buffered=True,
+  torn=True)` makes the disk lie too — writes only land on `sync()`, and a
+  crash keeps a seeded prefix of whatever was still queued.
 - **Clocks that lie** — `net.set_clock(name, offset=...)` skews what one
   host reads from the clock without changing how long anything takes, for
   testing lease and timeout code against machines that disagree about the

docs/design.md

@@ -202,6 +202,17 @@ Decisions inside that model, each doing real work:
   listeners close, and they go silent. Peers cannot distinguish a crash from
   a partition except by timeout — which is the entire epistemology of
   distributed failure detection, enforced by construction.
+- **A disk lies only when asked to.** Storage is durable at assignment
+  unless a host opts into `set_disk(name, buffered=True)`, because the
+  default has to be the one that costs nothing: an unconfigured disk draws
+  no numbers, records no events, and leaves every existing trace hash where
+  it was. Opted in, writes queue until `sync()`, and a crash keeps a seeded
+  *prefix* of the queue. A prefix, deliberately: real hardware also reorders
+  and corrupts individual sectors, and modeling that would need a sector
+  layer nothing else here would use, while a prefix is the failure an
+  application can actually defend against — write, sync, and only then act
+  on it. Skipping that sync is a bug the simulation can now find, which is
+  the whole reason the model exists.
 - **The accept is sequence 0.** The server builds its transport and sends
   `accept` before its protocol's `connection_made` can write; the client
   transport is built when the accept is *dispatched*, not when the connector

docs/supported-api.md

@@ -41,7 +41,8 @@ a host belong to an implicit `driver` host.
 | `loop.net.partition` / `heal` | Silent blackhole: datagrams are lost, stream traffic is held and resumes intact after healing; nothing errors — only your own timeouts fire |
 | `loop.net.crash` | A host's tasks are cancelled and it goes silent; no reset is sent — peers cannot tell a crash from a partition |
 | `loop.net.restart` / `host.restart()` | The counterpart to a crash: the host comes back as a fresh incarnation. Liveness is all that is revived — the old tasks stay cancelled, its listeners and binds are gone, and the caller boots whatever should run on the machine again, the same way it booted it the first time. Cancellation is requested at crash and lands on the next scheduler step, so a restart in the same step can briefly coexist with a dying task that swallows `CancelledError`. A packet is checked against liveness when it arrives, so traffic due during the dead window is lost; a packet that was already in flight and lands after the machine is back is delivered, and finds a host that no longer holds the old incarnation's connections. Peers still learn about the outage only from their own timeouts |
-| `host.disk` | Storage that survives the crash: a `MutableMapping` per host, where state a real process would fsync belongs. Writes are atomic at assignment; there is no partial-write model. Values are stored as given, so mutating a stored object afterwards is the caller's own aliasing, exactly as with a cache in front of a real disk |
+| `host.disk` | Storage that survives the crash: a `MutableMapping` per host, where state a real process would fsync belongs. By default a write is durable the moment it is made. Values are stored as given, so mutating a stored object afterwards is the caller's own aliasing, exactly as with a cache in front of a real disk. `disk.sync()` exists on every disk and does nothing on one that does not buffer, so the code under test is written the same way either way |
+| `loop.net.set_disk` | Makes a host's disk lie about when a write lands. `buffered=True` queues writes and deletes in order and only makes them durable on `sync()`; reads on that host see the queue merged over what is durable, in a fixed order — durable keys where the durable state has them, then the keys the queue invented, in write order, with a queued delete hiding a key. A crash throws the queue away and the reboot finds what was synced; with `torn=True` a seeded prefix of the queue survives instead, which is the state a machine that lost power part-way through a batch comes back with. A prefix is the whole model: writes never land out of order, and no value is ever half-written. Tearing needs a buffer to tear (`torn=True` alone is a `ValueError`), and reconfiguring a disk flushes whatever it was holding. The prefix is drawn from a seed-derived stream of its own, so a torn run makes exactly the network draws it would have made untorn, and a run that never calls `set_disk` draws nothing and records nothing — storage is not a scheduling event and has no trace events at all |
 | `loop.net.set_clock` / `clock_offset` | Per-host clock skew, in seconds. The offset changes what that host's tasks *read*: `loop.time()` (and `sim.time()` with it) returns true time plus the offset, and a deadline handed to `call_at` is interpreted on the calling task's clock. Durations are immune — `asyncio.sleep`, `asyncio.timeout`, `wait_for` and `call_later` cost the same everywhere, which is exactly what a wrong wall clock does to a real machine. By default the driver and unconfigured hosts read true time; the driver can be given an offset too. Trace timestamps stay on the true clock, so skew never perturbs scheduling and traces from skewed runs stay comparable |
 | `transport.abort()` | Peer gets `connection_lost(ConnectionResetError)` |
 | `loop.getaddrinfo` | Resolves against the host table, never DNS: a registered host name, its synthetic address, or a loopback-shaped name (`None`, `""`, `localhost`, `127.0.0.1`, `0.0.0.0`) meaning the calling task's own host. Returns stdlib-shaped rows — `(AF_INET, SOCK_STREAM, IPPROTO_TCP, "", (address, port))` and the `SOCK_DGRAM` / `IPPROTO_UDP` row — filtered by `family`, `type` and `proto`. Ports are numeric (`int`, a digit string, or `None` for 0); resolver `flags` have nothing to vary |

examples/raft/README.md

@@ -12,7 +12,9 @@ changes, no client sessions. Submission is at-least-once and says so: a
 command a leader accepts before being deposed can be resubmitted and commit
 twice, under two indices, and the safety claims below deliberately do not
 mind. Storage is an in-memory stand-in that survives a process restart within
-a run, the way a disk survives a reboot.
+a run, the way a disk survives a reboot — or, when a scenario asks for it,
+a simulated host disk that only makes a write durable when the node syncs it
+and keeps a seeded prefix of the rest when the power goes.
 
 ## The claim, stated honestly
 
@@ -24,6 +26,8 @@ Each rule that carries the safety argument sits behind its own flag in
 `Safeguards`, so the tests can switch exactly one off and watch the explorer
 find the schedule it lets through: stale-term rejection, one vote per term
 (§5.2), the log-freshness check on votes (§5.4.1), persistence before reply,
+the two syncs that make that persistence mean something on a disk that
+buffers — before a vote is granted and before an append is acknowledged —
 the own-term commit gate (§5.4.2), and the per-term no-op that lets a quiet
 term commit (§8).
 
@@ -53,13 +57,22 @@ leader that committed it:
 
 - Scenario suite: 11 seeded scenarios (elections, replication, RPC framing)
   × 10 seeds each, alongside unit tests for the log, vote and persistence
-  rules — 63 fast tests plus the slow proofs, green.
+  rules — 71 fast tests plus the slow proofs, green.
 - Campaign: **50,000 seeds** of five-node chaos — three randomized partition
   windows per seed, a process restart after about half of them, 2% message
   drop and 2% duplication throughout, with a client proposing — invariants
   held on every seed. 917.29s (15m17s) with `--simloop-jobs=8` on an M4
   MacBook Air, about 54 seeds a second. The same scenario runs 300 seeds
   sequentially in 27.97s and 2,000 seeds in 36.34s at `--simloop-jobs=8`.
+- The same chaos on disks that lose power: state on `host.disk` configured
+  `buffered=True, torn=True`, every restart a hard crash. **5,000 seeds**
+  green in 51.55s at `--simloop-jobs=8`, and the 300 the suite runs by
+  default in 14.10s sequentially (M4 MacBook Air, approximate — measured
+  with other work on the machine). Sync discipline is exactly what makes
+  that boring: across 25 seeds the power went out 39 times and found an
+  empty write buffer every time, because the node has already flushed
+  whatever it answered with. Switch one sync off and the same power cuts
+  land on disks holding 13 unflushed records apiece.
 - Replay stability: a one-off local measurement re-explored each ablation's
   found-at seed 100 times on a fresh loop — 5 seeds × 100 replays, one trace
   hash apiece, byte-identical throughout. The standing check is
@@ -76,10 +89,11 @@ leader that committed it:
 | 3 | Persistence before reply off (`persist_before_reply=False`) | leader-completeness | 4 | 5 | `... ::test_skipped_persistence_forgets_committed_entries` |
 | 4 | Stale-term rejection off (`reject_stale_term=False`) | state-machine-safety | 0 | 1 | `... ::test_accepting_stale_terms_rewrites_history` |
 | 5 | Commit gate off (`commit_own_term_only=False`, no-op off both sides) | state-machine-safety | 3 | 4 | `... ::test_committing_old_terms_by_count_loses_writes` |
+| 6 | Sync before acking an append off (`sync_before_ack=False`, on buffered, torn disks) | leader-completeness | 0 | 1 | `... ::test_an_unsynced_ack_loses_a_committed_entry` |
 
-Rows 1–4 searched a budget of 300 seeds, row 5 a budget of 500. All five are
-labeled ablations — detection demonstrations, not bugs that were ever
-shipped.
+Rows 1–4 and 6 searched a budget of 300 seeds, row 5 a budget of 500. All
+six are labeled ablations — detection demonstrations, not bugs that were
+ever shipped.
 
 "Invariant violated" records what the found seed actually produced, not the
 only thing that ablation can produce. Three of the five tests deliberately
@@ -88,6 +102,26 @@ instance, takes both stale appends and stale vote grants, so naming one of the
 four claims would say less than letting the checker report which one broke
 first.
 
+Row 6 is the disk's. A node keeps its whole record — term, vote and log —
+under one key, so a power cut can rewind it to an earlier record but can
+never leave it holding this term beside the previous vote; what makes a
+record durable is the `sync()` the node owes before it answers an RPC. Drop
+the one before an append is acknowledged and the leader counts a follower
+that has the entries in a write buffer and nowhere else: cut the power to
+the followers behind a partition and the term the survivors elect next has
+never heard of an entry that was already committed. Seed 0 produces it, and
+the schedule minimizes to FIFO except one step of 1,273. Put the sync back
+and the same scenario holds across 150 seeds
+(`test_the_synced_ack_carries_the_same_scenario`, slow-marked).
+
+The vote's sync is the same argument with the same flag shape
+(`sync_before_vote`), but the explorer is not what proves it here: the
+window it opens is one heartbeat wide — the winner's first AppendEntries
+flushes the vote behind the voter's back — and 4,000 seeds of a scenario
+built to walk through it never did. `tests/test_votes.py` shows the hazard
+directly instead: grant a vote on a buffered disk, cut the power, and the
+machine that boots grants the same term to somebody else.
+
 Two safeguards are also shown to be load-bearing *on their own*, which is the
 other half of the argument: with the commit gate the only thing standing (the
 per-term no-op switched off on both sides), the paper's Figure 8 runs clean
@@ -140,14 +174,15 @@ take `shrink=True` as an argument.
 ## Run it
 
     uv run pytest examples/raft/tests -q            # fast suite: scenarios, units, ablations
-    uv run pytest examples/raft/tests -q -m slow    # campaign, the two safe proofs, the replay guard
+    uv run pytest examples/raft/tests -q -m slow    # campaigns, the safe proofs, the replay guard
 
 Add `-s` to either and the ablations print the explorer's report — the failing
 seed and the trace around it.
 
-Turn the campaign up and spread the seeds over cores:
+Turn a campaign up and spread the seeds over cores:
 
-    uv run pytest examples/raft/tests/test_chaos_campaign.py -q -m slow --simloop-seeds=50000 --simloop-jobs=8
+    uv run pytest 'examples/raft/tests/test_chaos_campaign.py::test_chaos_campaign_holds_the_invariants' -q -m slow --simloop-seeds=50000 --simloop-jobs=8
+    uv run pytest 'examples/raft/tests/test_chaos_campaign.py::test_the_campaign_holds_on_disks_that_lose_power' -q -m slow --simloop-seeds=5000 --simloop-jobs=8
 
 Replay any campaign failure exactly:
 

examples/raft/raft/node.py

@@ -41,6 +41,11 @@ class Safeguards:
     one_vote_per_term: bool = True      # never grant two candidates one term
     check_log_up_to_date: bool = True   # §5.4.1: voters gate on log freshness
     persist_before_reply: bool = True   # durability before acknowledgement
+    # A write is only as durable as the disk it landed on. On a buffered disk
+    # these two are what push it past the buffer before the answer that
+    # depends on it goes out; on a disk that never buffers they cost nothing.
+    sync_before_vote: bool = True       # a vote is on the disk before it is granted
+    sync_before_ack: bool = True        # entries are on the disk before they are acked
     # §5.4.2: count replicas only for own-term entries. With leader_noop on,
     # every reachable quorum index already carries the leader's term, so this
     # gate only shows its teeth when the no-op is off too.
@@ -149,8 +154,9 @@ async def _connection(
         except (asyncio.IncompleteReadError, OSError, wire.FrameError):
             # IncompleteReadError is named on its own because it is not an
             # OSError. OSError here means a torn socket -- which also swallows
-            # one raised out of handle(), acceptable only while storage is in
-            # memory; a file-backed Storage needs its own except clause.
+            # one raised out of handle(), acceptable only while no Storage
+            # here can fail a write; a real file-backed one needs its own
+            # except clause.
             pass
         finally:
             writer.close()
@@ -329,7 +335,7 @@ def _handle_request_vote(self, m: dict[str, Any]) -> dict[str, Any]:
         if self._safeguards.check_log_up_to_date and theirs < ours:
             return refused
         self._state.voted_for = m["candidate"]
-        self._persist()
+        self._persist(sync=self._safeguards.sync_before_vote)
         self._reset.set()  # granting a vote defers our own candidacy
         return {"term": self._state.term, "granted": True}
 
@@ -351,7 +357,7 @@ def _handle_append_entries(self, m: dict[str, Any]) -> dict[str, Any]:
                 del log[index - 1 :]
             if index > len(log):
                 log.append(Entry(entry_term, command))
-        self._persist()
+        self._persist(sync=self._safeguards.sync_before_ack)
         if m["leader_commit"] > self.commit_index:
             # max(): a backed-off heartbeat carries a short verified prefix;
             # the commit mark never moves backwards for it.
@@ -380,9 +386,11 @@ def _become_follower(self, term: int) -> None:
         self._persist()
         self.role = FOLLOWER
 
-    def _persist(self) -> None:
+    def _persist(self, *, sync: bool = True) -> None:
         if self._safeguards.persist_before_reply:
             self._storage.save(self._state)
+            if sync:
+                self._storage.sync()
 
     def _last_log_term(self) -> int:
         return self._state.log[-1].term if self._state.log else 0