A crash-recovery lesson
Visible does not
mean durable.
I modeled a producer that signals “ready” before flushing its source. The consumer can save a manifest whose input disappears after a crash.
The recovery rule is manifest ≤ source. A saved result must not name a newer version than the source that survived. Step through the instructions, then inspect every crash image the model allows at that boundary.
The fix is ordering, not a stronger signal.
Flush the source before signaling ready. In the fixed model the consumer cannot read the new source until it is forced to survive a crash. The unsafe schedule also ends with both records flushed and no violation: the failure lives in an earlier prefix.
What schedule choice changes
Crash checks can revisit the same disk image. Bad observations are distinct recovery outcomes, not distinct bugs. A consumer-first single-trace baseline finds the same failure: I do not claim a new algorithm or a speedup.
Every boundary, without JavaScript
These tables and the interactive view come from the same generated model data.
Publish before flushing
0. Initial state
Every allowed crash image at this boundary| Source on disk | Manifest on disk | Recovery |
|---|
| 0 | 0 | Recovers: rule holds |
1. Producer: write source 1
Every allowed crash image at this boundary| Source on disk | Manifest on disk | Recovery |
|---|
| 0 | 0 | Recovers: rule holds |
| 1 | 0 | Recovers: rule holds |
2. Producer: signal ready
Every allowed crash image at this boundary| Source on disk | Manifest on disk | Recovery |
|---|
| 0 | 0 | Recovers: rule holds |
| 1 | 0 | Recovers: rule holds |
3. Consumer: wait ready
Every allowed crash image at this boundary| Source on disk | Manifest on disk | Recovery |
|---|
| 0 | 0 | Recovers: rule holds |
| 1 | 0 | Recovers: rule holds |
4. Consumer: read source seen
Every allowed crash image at this boundary| Source on disk | Manifest on disk | Recovery |
|---|
| 0 | 0 | Recovers: rule holds |
| 1 | 0 | Recovers: rule holds |
5. Consumer: copy manifest seen
Every allowed crash image at this boundary| Source on disk | Manifest on disk | Recovery |
|---|
| 0 | 0 | Recovers: rule holds |
| 0 | 1 | Violates manifest<=source |
| 1 | 0 | Recovers: rule holds |
| 1 | 1 | Recovers: rule holds |
6. Consumer: flush manifest
Every allowed crash image at this boundary| Source on disk | Manifest on disk | Recovery |
|---|
| 0 | 1 | Violates manifest<=source |
| 1 | 1 | Recovers: rule holds |
7. Producer: flush source
Every allowed crash image at this boundary| Source on disk | Manifest on disk | Recovery |
|---|
| 1 | 1 | Recovers: rule holds |
Flush before publishing
0. Initial state
Every allowed crash image at this boundary| Source on disk | Manifest on disk | Recovery |
|---|
| 0 | 0 | Recovers: rule holds |
1. Producer: write source 1
Every allowed crash image at this boundary| Source on disk | Manifest on disk | Recovery |
|---|
| 0 | 0 | Recovers: rule holds |
| 1 | 0 | Recovers: rule holds |
2. Producer: flush source
Every allowed crash image at this boundary| Source on disk | Manifest on disk | Recovery |
|---|
| 1 | 0 | Recovers: rule holds |
3. Producer: signal ready
Every allowed crash image at this boundary| Source on disk | Manifest on disk | Recovery |
|---|
| 1 | 0 | Recovers: rule holds |
4. Consumer: wait ready
Every allowed crash image at this boundary| Source on disk | Manifest on disk | Recovery |
|---|
| 1 | 0 | Recovers: rule holds |
5. Consumer: read source seen
Every allowed crash image at this boundary| Source on disk | Manifest on disk | Recovery |
|---|
| 1 | 0 | Recovers: rule holds |
6. Consumer: copy manifest seen
Every allowed crash image at this boundary| Source on disk | Manifest on disk | Recovery |
|---|
| 1 | 0 | Recovers: rule holds |
| 1 | 1 | Recovers: rule holds |
7. Consumer: flush manifest
Every allowed crash image at this boundary| Source on disk | Manifest on disk | Recovery |
|---|
| 1 | 1 | Recovers: rule holds |
Where this model stops
I use synthetic atomic integer records, independent persistence, volatile handoffs, and instruction-boundary scheduling. This is not ext4, SQLite, mmap, torn-write simulation, or a physical power-loss experiment. Exploration is bounded; the fixed result is not a proof about arbitrary storage protocols.
Read the semantics, explorer, and generated data with source hashes. The established visibility-before-durability problem is studied in PMRace and DURINN; PerSeVerE explores concurrency and persistence together.