Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
59 changes: 59 additions & 0 deletions rfd/0003/EVIDENCE.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -377,6 +377,65 @@ Repeated independent runs reproduced every canonical digest and serial digest
exactly; only durations and replay-log sizes moved with host scheduling, so no
divergence, retry, or nondeterminism was observed in semantic output.

==== Replay divergence under the host-coupled model

That claim has an observed exception, and it matters to the model question rather
than to this increment's construction. A continuous-integration run of the Phase 4
acceptance (which runs this demonstration) failed in the binary source's first
replay with

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

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

What it means. The replaying guest performed a character write at an instruction
position where the replay log's next event is an instruction event. QEMU's
`replay_char_write_event_load()` accepts only `EVENT_CHAR_WRITE` there, so the
replaying guest's instruction stream had diverged from the recording's before
that point. The run was recorded under the model the product launches today,
`shift=auto`, where the guest's virtual clock is coupled to host real time, so
the number of instructions the guest executes between its serial writes depends
on how the host schedules it.

What it rules out. A truncated or incomplete recording is ruled out by the
message rather than by a digest: the log still held a well-formed event at that
position, where a truncated log fails while reading one. The recording's own log
digest could not be compared against its manifest for this run, because the
uploaded bundle carries the replay's logs and `failure.json` only; a replay of a
recording whose log was truncated would fail differently, and no such failure has
been observed. A QEMU defect is not ruled out, but the same binary replays the
same demonstration correctly under the pinned model below, and the message is the
machinery reporting a divergence rather than misreading an intact log.

Rate and reproduction. One failure in the continuous-integration history of this
step (run 35713214491; the neighbouring revisions of the same branch passed it),
and no failure in the local phase 3 acceptance run under deliberate load (eight
CPU consumers and three parallel QEMU guests) that was recorded for comparison.
The failure is rare rather than impossible, so a green run is not evidence that
the recording is reproducible.

The pinned model. The same demonstration, recorded and replayed under
`shift=4,sleep=off` with the spike QEMU of RFD 4
(`poc/time-model/qemu-nosleep-replay-flush.patch`), completed with both replays
matching under the same load shape, and the Phase 4 acceptance under that model
passes. Under `shift=4,sleep=off` the guest's virtual time is a function of its
instruction count, so the positions this failure depends on cannot move with host
scheduling. That is evidence for the pin, not proof that `shift=auto` is the only
model that can diverge: the failure is too rare to bound a rate from one sample.

Guards, proposed rather than built. Validate the recorded log's integrity against
the manifest before replaying, so an incomplete recording is reported as an
incomplete recording rather than as a guest divergence; and classify QEMU's
replay-divergence message as a typed error, because the frame-level
`truncated serial event frame` this currently surfaces as points at the symptom
rather than at the divergence. Neither guard would make a host-coupled recording
reproducible, which is the model question RFD 4 records.

=== Unsupported OCI constructs

Eighteen representative constructs were refused before any output was
Expand Down
12 changes: 10 additions & 2 deletions rfd/0004/README.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -112,8 +112,16 @@ matching SimFerret executable and rebuilt initial state, the specific verified
replay log, normal QEMU termination, and matching normalized events,
assertions, and semantic outcome digest. Matching VM identity is a necessary
condition among these, not a sufficient one. Replay reproduces the timing the
guest observed because the log records it, which is why variable clock scaling
never broke replay.
guest observed because the log records it. That is not unconditional either: the
phase 3 acceptance observed a replay fail under the model the product launches
today, where the guest's clock is coupled to host real time, when the replaying
guest's instruction stream diverged from the recording's before a character
write. `rfd/0003/EVIDENCE.adoc` records that failure, what it rules out (an
incomplete recording, by the message rather than by a digest), that the mechanism
is narrowed rather than proven and a QEMU defect is not ruled out, and that the
observed rate is too thin to bound. The log records the timeline the guest
observed; it does not make a timeline that depends on host scheduling
reproducible.

What is narrower than it may have appeared is *fresh execution*: a new
recording of the same workload with the same inputs. That is the property this
Expand Down
Loading