 codex/file-system-journal-crash-state-recovery.py

"""Exhaust the stated three-record crash model and draw its recovery table.
Tested with Python 3.14, matplotlib 3.10.7 and numpy 2.3.5.
Run from _media. Records are atomic, flushes honored, and there is one writer.
"""

from collections import deque
from pathlib import Path

import matplotlib.pyplot as plt


def successors(state):
    journal, commit, home, retired = state
    if retired:
        return []
    if not commit:
        steps = [(journal | (1 << i), 0, 0, False) for i in range(3)
                 if not journal & (1 << i)]
        if journal == 7:
            steps.append((7, 1, 0, False))
        return steps
    steps = [(7, 1, home | (1 << i), False) for i in range(3)
             if not home & (1 << i)]
    if home == 7:
        steps.append((0, 0, 7, True))
    return steps


def reachable_states():
    initial = (0, 0, 0, False)
    seen, pending = {initial}, deque([initial])
    while pending:
        for state in successors(pending.popleft()):
            if state not in seen:
                seen.add(state)
                pending.append(state)
    return seen


def recover(state):
    journal, commit, home, retired = state
    if commit:
        assert journal == 7 and not retired
        return 7
    return home


def triple(mask):
    return "".join(str((mask >> i) & 1) for i in range(3))


def main():
    states = reachable_states()
    assert len(states) == 17
    assert all(recover(state) in (0, 7) for state in states)
    assert sum(recover(state) == 0 for state in states) == 8
    assert sum(recover(state) == 7 for state in states) == 9
    masks = sorted(range(8), key=triple)
    ordered = [(j, 0, 0, False) for j in masks]
    ordered += [(7, 1, h, False) for h in masks]
    ordered += [(0, 0, 7, True)]
    assert set(ordered) == states

    fig, ax = plt.subplots(figsize=(11.2, 8.8), dpi=100, facecolor="white")
    ax.axis("off")
    fig.subplots_adjust(left=0.04, right=0.96, bottom=0.17, top=0.85)
    fig.text(0.5, 0.955, "Every crash state of a three-record redo journal",
             ha="center", fontsize=18, weight="bold", color="#15354a")
    fig.text(0.5, 0.911, "Triples are I, B, D; 1 means the new record is durable",
             ha="center", fontsize=12, color="#435667")
    columns = ["Crash phase", "Journal\npayload", "Durable\ncommit", "Final records\nbefore recovery", "Recovery action", "Final records\nafter recovery"]
    rows = []
    for j, c, h, retired in ordered:
        phase = "Retired" if retired else ("After commit" if c else "Before commit")
        action = "Already complete" if retired else ("Replay I + B + D" if c else "Ignore payload")
        rows.append([phase, "—" if retired else triple(j), str(c), triple(h), action,
                     triple(recover((j, c, h, retired)))])
    table = ax.table(cellText=rows, colLabels=columns, cellLoc="center", loc="center",
                     colWidths=[0.16, 0.12, 0.11, 0.19, 0.23, 0.19], bbox=[0, 0, 1, 1])
    table.auto_set_font_size(False)
    table.set_fontsize(11)
    for (row, col), cell in table.get_celld().items():
        cell.set_edgecolor("#c9d4dc")
        if row == 0:
            cell.set_facecolor("#15354a")
            cell.set_text_props(color="white", weight="bold")
            cell.set_height(0.088)
        else:
            cell.set_facecolor("#edf3f8" if row <= 8 else ("#e4f3ed" if row <= 16 else "#e8e9ef"))
            if col in (1, 2, 3, 5):
                cell.set_text_props(fontfamily="DejaVu Sans Mono")
            if col == 5:
                cell.set_text_props(weight="bold")
    fig.text(0.5, 0.12, "8 pre-commit states + 8 checkpoint states + 1 retired state = 17",
             ha="center", fontsize=12, weight="bold", color="#15354a")
    fig.text(0.5, 0.083, "Atomic records • payload flush before commit • commit flush before final writes",
             ha="center", fontsize=11, color="#435667")
    fig.text(0.5, 0.052, "Final copies flushed before retirement • intact durable storage • recovery before access",
             ha="center", fontsize=11, color="#435667")
    fig.text(0.5, 0.022, "The table lists abstract durable states, not measurements of a real filesystem.",
             ha="center", fontsize=10, color="#435667")
    fig.savefig(Path.cwd() / (Path(__file__).stem + ".png"), facecolor="white", transparent=False)
    plt.close(fig)


if __name__ == "__main__":
    main()