Skip to content

docs(plan): record the observed replay divergence and narrow the replay claim - #46

Merged
darwin67 merged 1 commit into
mainfrom
rfd3-replay-divergence-record
Sep 22, 2026
Merged

darwin67 merged 1 commit into
mainfrom
rfd3-replay-divergence-record

Conversation

@darwin67

@darwin67 darwin67 commented Sep 22, 2026 •

Copy link
Copy Markdown
Member

What

Records an observed replay divergence in rfd/0003/EVIDENCE.adoc — in the increment whose claim it affects — and narrows the related claim in rfd/0004/README.adoc, which asserted that variable clock scaling never broke replay.

Docs only: two files, +69/−2, no code or behavior change.

The failure

A continuous-integration run of the Phase 4 acceptance (which runs the phase-3 demonstration) failed in the binary source's first replay:

qemu-system-x86_64: Missing character write event in the replay log
  (insn total 2362086659/74 left, event 5431704 is EVENT_INSTRUCTION)

with a failure bundle recording error_kind: early-termination, error: truncated serial event frame, stage: execution, and backend_mode: replay.

Why it is not a flake

The replaying guest performed a character write at an instruction position where the log's next event is an instruction event, so its instruction stream had diverged from the recording's before that point. The run was recorded under shift=auto, whose guest clock is coupled to host real time. A truncated recording is ruled out by the message; a QEMU defect is not ruled out, but the same binary replays the same demonstration correctly under shift=4,sleep=off.

Rate: one failure in the CI history of that step, and none in a local phase-3 acceptance run under deliberate load (eight CPU consumers, three parallel QEMU guests). Rare rather than impossible, so a green run is not evidence that a host-coupled recording reproduces.

The RFD 4 correction

RFD 4 said: "Replay reproduces the timing the guest observed because the log records it, which is why variable clock scaling never broke replay." The observed divergence falsifies the "never broke" part regardless of the underlying cause, so the sentence now states the incident, cross-references the RFD 3 record, keeps the mechanism as narrowed rather than proven, and notes that the rate is too thin to bound. It claims nothing about the pinned model being proven safe. The surrounding "replay is not unconditional" paragraph and its conditions list are untouched.

Why it matters here

The failure is evidence for RFD 4's pin: under shift=4,sleep=off the positions this failure depends on cannot move with host scheduling, and the same demonstration completed with both replays matching under the same load shape. Neither guard the record proposes would make a host-coupled recording reproducible; that is the model question RFD 4 already carries.

Verification

  • make check-rfds

The Phase 3 record-and-two-replay demonstration has an observed exception: a
continuous-integration run of the Phase 4 acceptance failed in the binary
source's first replay with QEMU reporting a missing character write event where
the log's next event is an instruction event, under the model the product
launches today (shift=auto, whose guest clock is coupled to host real time).

rfd/0003/EVIDENCE.adoc records it in the increment whose claim it affects: what
the failure means, what it rules out (a truncated recording, by the message
rather than by a digest), the observed rate, that the same demonstration
completes under shift=4,sleep=off with the spike QEMU, and the guards that are
proposed rather than built.

rfd/0004/README.adoc no longer asserts that variable clock scaling "never broke
replay": the sentence states the incident, cross-references the evidence record,
and keeps the paragraph's framing that replay is not unconditional.

The product's launch model is unchanged and nothing is added to the RFD 4
Phase 0 change.
@darwin67
darwin67 force-pushed the rfd3-replay-divergence-record branch from 6a1fb15 to e254057 Compare September 22, 2026 10:50
@darwin67 darwin67 changed the title docs(rfd3): record the replay divergence under the host-coupled model docs(plan): record the observed replay divergence and narrow the replay claim Sep 22, 2026
@darwin67
darwin67 merged commit 90e1d4f into main Sep 22, 2026
7 checks passed
@darwin67
darwin67 deleted the rfd3-replay-divergence-record branch September 22, 2026 15:45
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant