Repository navigation
feat(time-model): gate the pinned guest time model on x86-64 Linux - #45
Merged
Merged
Conversation
darwin67
force-pushed
the
rfd-4-phase0-gate
branch
6 times, most recently
from
September 22, 2026 09:29
ee0924e to
050d82d
Compare
Add the RFD 4 Phase 0 acceptance gate and the evidence it produces, record the record-mode limitation that blocks pinning the model in the product, and spike the QEMU fix for that limitation. - scripts/time-model-gate.sh runs the real probe under the pinned model and fails unless every requested run completed, the verdict is an explicit reproducible, the QEMU executable, guest kernel, and initramfs digests match the reference host's, and the four time measurements and the control checksum equal its recorded values exactly. A host that cannot complete fails as an unsupported execution; no fallback model is attempted. - poc/time-model/reference-host-values.txt records the model, the artifact digests, and the measurements a host must reproduce. The QEMU identity is the executable's SHA-256 rather than its version string, so a rebuilt or patched QEMU cannot pass as the reference build. - scripts/time-model-input-probe.sh and poc/time-model/input-probe.c measure whether a guest that waits for host input receives it. Under the pinned model with rr=record it does not: QEMU queues live serial input as a replay asynchronous event and flushes the queue only from icount_account_warp_timer(), which returns early when sleep=off. The probe's --expect mode asserts that known result, and the qemu-replay job runs it, so a QEMU change that fixes the flush becomes visible. - The input probe's ordering is causal rather than timing-dependent: the guest polls until the probe stops it, and the probe stops the guest with an acknowledged QMP command, drains what the guest produced before it stopped, writes the line, and resumes it with a second acknowledged command. Waiting for the reply is what makes the ordering sound, because a request QEMU has not acted on cannot be mistaken for a stopped guest. A stopped guest cannot poll and cannot produce output, so the polling it does after the resume is polling after the write and no report read after the resume can be one it produced earlier. After the wait the probe stops the emulator and reads its output to its end before closing the pipe, so a delivery report emitted during shutdown is classified rather than lost, and only an output that ended in one piece can support a non-delivery claim: an output that never ends, a report cut off mid-line, and the emulator's own deadline expiring are all inconclusive, as are a guest that stopped polling, an emulator that exited on its own, an experiment that never wrote, and output that could not be drained. The guest's own loop is covered by poc/time-model/input-probe-test.c, which fails if an iteration limit or a give-up report is restored. - rfd/0004/EVIDENCE.adoc records what the measurement does not establish as well as what it does: the acknowledgement is asserted in the harness and the delayed-pause case is reasoned about rather than fixtured, the claim that nothing stays buffered in the guest or the output path at the pause is the source-level argument (QEMU's stdio chardev writes through io_channel_send, with no user-space buffer), and the causal claim is confirmed independently of the probe's instrumentation by the spike, which changes one early return and makes delivery appear under the same model. - That blocker is why the product's launch paths keep the model they can complete under, named TIME_MODEL. rfd/0004/EVIDENCE.adoc records the measurement, the reproduction, the re-validation trigger, and a spike that builds the pinned QEMU with a ten-line patch moving the flush ahead of the sleep check: with that binary the pinned model delivers input, the product records and replays twice with matching normalized events, assertions, and semantic outcome digest, and the gate passes against a record carrying the patched digest. The patch is retained as a spike and is not wired into the build. - The gate and both probes fail closed and classify rather than merge: an experiment that cannot say what happened is inconclusive rather than a result, the acceptance deadline and the five-run minimum are fixed rather than inherited, a malformed or duplicated reference record is rejected, every invocation records its result in its own directory created before validation, so a failed rerun cannot leave an earlier success standing, and failures are configuration errors, unsupported executions, or validation failures with the exit status each one means. A probe's own setup or harness failure, including a guest that does not compile, an output that cannot be created, and a result that cannot be recorded, is a configuration error rather than a host that could not complete, and an undocumented status is not read as a statement about the host. Both probes tag their intentional outcomes, so an untagged failure is a configuration error rather than a validation or unsupported-execution finding, and the input probe's monitor socket location and controller are checked before any run starts. - The qemu-replay CI job runs the gate, its regression tests, the host-input assertion, and the host-input guest tests on ubuntu-latest.
darwin67
force-pushed
the
rfd-4-phase0-gate
branch
from
September 22, 2026 09:56
050d82d to
aa4eb85
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Implements RFD 4 Phase 0 — Pin and validate the time model, and records the
record-mode limitation that blocks pinning it in the product.
Pinned model as implemented:
-icount shift=4,sleep=off, recorded inpoc/time-model/reference-host-values.txtas the single source of truth for thegate. The product's launch model stays
TIME_MODEL = "shift=auto"incrates/simferret/src/vm.rs; see "Record mode cannot use the pinned model"below for why, and for the spike that shows the blocker is one early return in
QEMU.
What changed
scripts/time-model-gate.sh— the acceptance gate: runs the real probe underthe pinned model with a fixed 180 s deadline and the RFD's five-run minimum,
and fails unless every requested run completed, the verdict is an explicit
reproducible, the QEMU executable, guest kernel, and initramfs digests matchthe reference host's, and the four time measurements and control checksum equal
its recorded values exactly. A host that cannot complete fails as an
unsupported execution; no fallback model is attempted.
poc/time-model/reference-host-values.txt— the model, artifact digests (QEMUby executable SHA-256, not version string), and the measurements a host must
reproduce.
scripts/time-model-input-probe.sh+poc/time-model/input-probe.c— measureswhether a guest that waits for host input receives it, with a causal ordering:
the guest polls until the probe stops it; the probe stops the guest with an
acknowledged QMP command, drains what it produced before it stopped, writes the
line, and resumes it with a second acknowledged command, so the polling after
the resume is provably after the write; and it then stops the emulator and reads
its output to its end, so a delivery report emitted during shutdown is
classified rather than lost. A non-delivery claim needs that clean end of
output, and a guest that stopped polling, an emulator that exited on its own, an
output that never ended or ended mid-report, an expired emulator deadline, or an
experiment that never wrote is
inconclusive, nevernot-delivered.poc/time-model/input-probe-test.c+scripts/time-model-input-probe-test.sh— drive the real guest loop through stubs: a line arriving after more than the
polls the guest used to stop after is still reported as received, and the guest
never reports giving up.
poc/time-model/qemu-nosleep-replay-flush.patch+qemu-nosleep-replay-spike.nix— the spike that builds the pinned QEMU with a ten-line patch moving the replay
flush ahead of the sleep check. Not wired into any build.
.github/workflows/ci.yml— theqemu-replayjob runs the gate, itsregression tests, the guest tests, and the host-input assertion
(
--expect not-delivered) on x86-64 Linux.rfd/0004/EVIDENCE.adoc— scale selection, Phase 0 validation on the referencehost, cross-host equality, the record-mode limitation with its minimal
reproduction, the spike measurements, and the re-validation trigger.
docs/time-model.adoc— the investigation index, including the gate.Scope boundaries
pre-launch rejection of a mismatched manifest, and the legacy profile.
and wakeup semantics in the README and the run manifest.
shift=auto). Phase 0's productpin and the record/replay confirmation are blocked by the record-mode
limitation recorded in the evidence; the model question and whether to carry a
patched QEMU are the RFD's decision.
Verification
scripts/time-model-gate.sh— 5/5 runs completed, verdictreproducible, allmeasurements equal to the reference record.
scripts/time-model-input-probe.sh --expect not-delivered— not delivered; theguest polled for 84 s (32,120 polls) and never received the line. The controls
(
--live,shift=4,shift=auto) deliver.against a record carrying the patched digest, the product records and replays
twice with matching normalized events, assertions, and semantic outcome digest
(see the evidence table).
scripts/time-model-gate-test.sh,time-model-probe-test.sh,time-model-input-probe-test.sh— pass.flake check,cargo fmt --check, clippy with--deny warnings,cargo test --locked --workspace --all-targets --all-features,bash -n .agents/dev .agents/setup scripts/*.sh,make check-rfds, therecord/replay smoke suites, both acceptance suites, and the two sudo runtime
suites — pass.
ubuntu-latesthalf of the matrix is validated by this PR'sqemu-replayjob: all six checks pass, including the gate, the host-input assertion (with the
acknowledged-QMP ordering), and the host-input guest tests —
https://github.com/chaba-dev/simferret/actions/runs/35710675048
phase 4 runtime suites (under sudo),
flake check,cargo fmt --check, clippywith
--deny warnings, the workspace test suite,bash -n, andmake check-rfdsall pass on the reference host.dropped, because its timing could not be made to distinguish the acknowledgement
from the delay reliably; the acknowledgement itself is asserted through the
monitor log in the handshake case. QEMU's own serial-output path is treated as
synchronous (its stdio backend writes through
io_channel_send), which is whatlets a drained pipe be the pre-write boundary.
This branch was stacked on #44 (the RFD 4 evidence and the investigation
index); #44 has since been merged into
main, and the branch is rebased ontothat merge, so it is no longer stacked on an open PR.