Login
Phase 11: Logging
Login

xv6 §11, "Logging". "One of the most interesting problems in file system design is crash recovery."

Glint keeps a small amount of state that must survive a crash: which guests exist, how they boot and what happened at the last boot. Phase 11 makes updates to that state atomic, so after any crash the state is either entirely the old version or entirely the new one. The state and its write-ahead log live in two files on the ESP, glint/state and glint/state.log, written through the FAT writer from 10.4. xv6's log is small enough to build in a few slices, which is why it stays the model here, even though Hailperin's chapter on transactions is the fuller treatment. The slices form a chain: a format (11.1), a log that writes it (11.2), recovery that reads the log (11.3), and a test that proves the three together (11.4).

Provisional slices. Each is refined, with its quoted sentence, when the phase starts.

Slices

11.1 The state format. This slice defines a plain, versioned record format for Glint's persistent state. One record describes each guest (image, memory, devices) and one records each boot. It includes the Crystal code that parses and writes those records. It comes first because both the log in 11.2 and recovery in 11.3 store and read records in this format. The code is host-testable (plan principle 3): specs round-trip every record type and reject truncated or unknown versions. That Demonstrability needs no firmware at all. Keeping the format plain text, with a version number, is Clarity: anyone can read Glint's state file with a text viewer.

11.2 The write-ahead log. This slice makes each update atomic in three steps. The new records are appended to glint/state.log, then a commit record is appended, and only then are the records installed into glint/state. Its passages are xv6 §11.1 ("Log design") and Hailperin §5.4 (write-ahead logging). It needs 11.1's record format for what it writes, and 10.4's FAT writer for where it writes. It is kept to that one protocol with no concurrent transactions, because Glint's state changes rarely, which is Parsimony in the sense of solving the problem and no more.

11.3 Recovery at boot. Before Glint reads its state during boot, this slice replays every update whose commit record from 11.2 reached the log, and discards any update that has no commit record. It then empties the log. It follows 11.2 because recovery can only interpret records that the log protocol defines. Recovery is idempotent: running it twice gives the same result. That makes it simple to state and to test, which is Clarity.

11.4 Crash testing. This slice proves 11.1–11.3 together. A harness boots Glint, starts a stream of state updates, kills QEMU at a random point, reboots, and checks that the state is exactly the before or the after, never a mixture. It reuses Track T's boot-test harness (T.11), which already boots an ESP image headless and watches the serial console, adding only the kill-and-reboot loop. It comes last because it tests the whole chain. It is the phase's Demonstrability: a crash-safety claim is accepted only once it survives this test.

Phase demo: QEMU is killed mid-update, and the state recovers.

References