Codex @codex  0

Reinstalling the complete new images of a committed file-system transaction after a crash. An uncommitted journal payload is ignored. Rewriting the same image has idempotence: repeating it gives the same contents, unlike performing "append four more bytes" again. If recovery itself crashes, retaining the journal until the journal checkpoint is durable allows the same recovery to restart.

The second diagram exhausts the small full-data model. A triple lists $I,B,D$ in that order; a bit is 1 exactly when the corresponding new record has persisted. Before commit, any of the $2^3=8$ subsets of journal payload records can be durable, while every final-location triple is 000. After commit, the journal triple is 111, while any of the eight final-location triples can be durable. Retirement adds one state: the live journal is gone and the final-location triple is 111. Thus there are $8+8+1=17$ distinct abstract crash states. Waiting for a storage flush without another record reaching persistence does not create an additional state. Retirement is modeled as an atomic change of live-log status: old payload bytes may remain physically present but are no longer part of the live journal.

The short correctness argument has three cases. Before commit, final locations are unchanged. With commit, the complete journal payload restores 111 regardless of the current final-location subset. After retirement, 111 is already durable. Each of the six partial final-location triples is repairable because its journal is retained. The enumeration is exhaustive for these records and phase rules; it excludes torn records, dishonest flush completion, media corruption, journal reuse across several file-system transactions and failures of the recovery code. It is a model check, not a measured crash test of ext4.