= Journal replay
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.
\Image[/file-system-journal-crash-state-recovery.png]
{title=All 17 abstract crash states recover to the old or new three-record append under the stated <storage flush> and <atomic storage write> assumptions}
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>.
Back to article page
