diff options
Diffstat (limited to 'debug/risc-v-gsp-rm-vm/docs/37-SIM-QEMU-LINE.md')
| -rw-r--r-- | debug/risc-v-gsp-rm-vm/docs/37-SIM-QEMU-LINE.md | 47 |
1 files changed, 38 insertions, 9 deletions
diff --git a/debug/risc-v-gsp-rm-vm/docs/37-SIM-QEMU-LINE.md b/debug/risc-v-gsp-rm-vm/docs/37-SIM-QEMU-LINE.md index 42c76cc..06fa943 100644 --- a/debug/risc-v-gsp-rm-vm/docs/37-SIM-QEMU-LINE.md +++ b/debug/risc-v-gsp-rm-vm/docs/37-SIM-QEMU-LINE.md @@ -29,11 +29,12 @@ and analyze/compare, probes/plugins, Ghidra bridges, trace, injection SDK and `Session.call`/`run_until`, plus the documented first fault at firmware vaddr `0x4009014` (4-byte read of `0x2000000000000A00`). -The boot ladder (docs/35 §3.3) is `pre-B0` (image loads, first MMIO observed -*as a fault*) < `B0` (first MMIO observed; lenient) < `B1` (first fault past -the QEMU point, explained by device semantics) < `B2` (boot-stage progress) < -`B3` (first mailbox poll) < `B4` (message loop) < `B5` (one scripted message -served). +The boot ladder (docs/35 §3.3, revised 2026-10-03) is `pre-B0` (image loads, +first MMIO observed *as a fault*) < `B0` (first MMIO observed; lenient) < +`B1` (first fault past the QEMU point, explained by device semantics) < +`B2` (boot-stage progress: relocation copy) < `B3` (libos init complete; +message-loop task blocks in the port wait) < `B4` (first CSB/TRANSCOM poll +served, host-traffic-triggered) < `B5` (one scripted message served). **"Above the QEMU line"** requires *all* of the frozen checks in §3, including the docs/35 §1.1 requirement that the milestone be reached "with @@ -196,6 +197,33 @@ MMIO. Frozen thresholds unchanged. Measured run on the same image `harness/qemu_line/sim-qemu-line.json|.md`). Wall figures are host-load dependent. +### 4.4 Re-measurement after the XMPU/libos wave (2026-10-03, session 4c) + +The native side now runs the real image with the XMPU (MPU) translation model +and the libos service model (docs/36 §3.2/§3.3), so the DMEM-runspace unknown +is gone. Fresh run, frozen thresholds unchanged, same image +(sha256 `2d1bb5c60b208cfd…`), `--instructions 2000000`: + +| side | ran | rung | instructions | cycles (modeled) | stop | wall s | evidence | +|---|---|---|---:|---:|---|---:|---| +| QEMU probe | yes | `pre-B0` | – | – | `fault_load` fw `0x4009014` -> `0x2000000000000A00` | 0.98 | `harness/qemu_line/sessions/qemu-probe` | +| native run 1 | yes | `B3` | 474,043 | 871,904 | `ecall@0x4018038` (`task_port_send_recv_wait`) | 0.65 | `harness/qemu_line/sessions/native-1` | +| native run 2 | yes | `B3` | 474,043 | 871,904 | `ecall@0x4018038` | 0.66 | `harness/qemu_line/sessions/native-2` | + +* all five frozen checks pass: `qemu_first_fault_reproduced`, + `native_above_qemu`, `identical_runs` (device-state sha256 + `5b3cc7e4af933e01…` on both runs), `native_pair_wall_s`, and + `device_model_documented`; **verdict `above`**. +* milestones observed: `bootargs_consumer`, `relocation_copy`; + `unknown MMIO = 0`, `device_unhandled = 0`; `armed_mask=0xFF`. +* What this does **not** claim: B4/B5 are not reached (the message-loop task + blocks before any CSB access without host traffic); the shim values are + declared assumptions; cycles are modeled (docs/32); no timing or + device-environment claim. +* Command: `python3 harness/sim_qemu_line.py --instructions 2000000` + (regenerates `harness/qemu_line/sim-qemu-line.json|.md`; the tracked report + is this run). Wall figures are host-load dependent. + ## 5. Failure signals (when to disable, per U48/U56) * Any frozen check false **with QEMU available and the firmware present**: @@ -227,10 +255,11 @@ report is emitted with `unverified_qemu_absent`. ## 7. Honest limits -* **S1 partial** — the device model reaches B2 (relocation copy) with the - recorded boot shim; B3/B4 (CSB poll, message loop) are not reached and the - DMEM-runspace unknown is the documented ceiling (docs/36 §6). The §4.1 - lenient record predates S1; §4.3 is the post-S1 measurement. +* **S1 partial** — the device model reaches B3 (libos init complete; + message-loop port wait) with the XMPU model, the recorded boot shim and the + libos service model (docs/36); B4/B5 (host-traffic-triggered CSB poll and a + scripted message) are not reached. §4.1/§4.3 are the pre-XMPU records; + §4.4 is the current measurement. * **L2/L3 partial** — cycles are modeled (`rv64imac-modeled/1`, docs/32), not measured; the device model is partial and carries per-register evidence (docs/36). No timing or full device-environment claim is made. |
