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 lsn txn type item before->after 1 T1 begin 2 T1 write A 0->5 3 T1 commit 4 T2 begin 5 T2 write B 0->9 CRASH winners: T1 losers: T2 recovered state item value A 5 B 0 redo LSNs: 2 undo LSNs: 5

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}