Recovery

Honest by Construction

Winners, losers, redo, undo, and recovered state are recomputed before rendering.

highlighted = computed this step

Honest by construction

The author supplies a log, crash point, and optional expected facts. The engine recomputes winners, losers, redo, undo, and recovered state before rendering. Note: expected facts can reject a mismatch but cannot create the answer.

recompute boundary\text{recompute boundary}

Compiled recovery

The compiled recovery has 1 redo write, 1 undo write, and 2 recovered items. Note: every number comes from compile output.

redo=1,undo=1,recovered items=2\text{redo}=1,\quad \text{undo}=1,\quad \text{recovered items}=2

a simplified redo/undo recovery over a tiny log; ARIES detail (fuzzy checkpoints, CLRs, media recovery) and real durability/fsync are beyond these traces - no product claims.

Honest recovery - CRASH after LSN 5lsntxntypeitembefore->after1T1begin2T1writeA0->53T1commit4T2begin5T2writeB0->9 winners: T1 | losers: T2; redo LSNs: 2; undo LSNs: 5itemvalueA5B0

Wrong state reject

A wrong expected recovered state is rejected during the lesson self-test. Note: the rejection happens before an inconsistent diagram can publish.

reject mismatch\text{reject mismatch}

Summary

Write-ahead log lessons are honest because recovered state is recomputed from log and crash. Note: this is simplified redo and undo; ARIES detail, fuzzy checkpoints, CLRs, media recovery, and real fsync durability are deferred.

honest recovery\text{honest recovery}