Repository navigation
Abstract commands are not bound to the hart selected at admission — hartsel change mid-command relocates execution to a different hart #203
Description
Description
dm_mem keys go/resume, the WhereTo program-counter offer, and abstract-command completion off the live hartsel value rather than the hart selected when the command was admitted. While abstractcs.busy=1, any write to dmcs.hartsel (or a dmactive pulse, which zeroes hartsel) relocates the in-flight command to a different hart.
Reproduction
On pristine RTL (Verilator, NrHarts=2):
- command admitted for hart 0;
hartselwritten 0→1 whilebusy=1 hart0_saw_go=0, hart1_saw_go=1— hart 1 executes the AccessRegister program- hart 1's
x1(0xDEADBEE1) lands indata0;busyclears on hart 1's re-halt - the debugger silently reads/writes the wrong hart's registers; the access-register write direction gives cross-hart register injection
Formal: SymbiYosys BMC counterexamples for both the offer/withhold divergence and the wrong-hart completion (step 5, NrHarts=2). The dm_csrs hartsel decode itself is formally clean (haltreq/resumereq one-hot, out-of-range gated) — the defect is the missing admission-time binding in dm_mem.
Additional consequence
If the hartsel change (or dmactive pulse) lands on an empty hart slot, the module enters the Go state and wedges — unrecoverable even via dmactive reset.
Related
#196 (admission window — this is the sustained window while busy=1, not the 1-cycle race), #197 (dmactive reset — extended here: it is also why the wedge is unrecoverable and relocates go to hart 0).
Suggested fix
Latch the target hart at command admission and use the latched value for go/resume/completion; ignore or stall hartsel writes while busy=1.
PoC testbench + formal harnesses available — happy to attach.
Activity
phsauter commentedon Sep 2, 2026
According to 0.13.2 spec while
abstractcs.busyis asserted, the debugger must not changehartsel, so the debugger is already prohibited from causing this situation.However, the current spec gives a recommendation:
I think it is still worth fixing as suggested.
phsauter commentedon Sep 2, 2026
This is also the same flavor of problem as #198 and #199, though not directly related.
The problem is the same, it is not consistent/clear which selection 'snapshot' goes with an operation.
dm_mem: bind abstract commands to admission hartsel
john-kearney commentedon Sep 11, 2026
Thanks @phsauter for the spec analysis and to @devtyagi3909 for #204 — binding abstract commands to the admission hartsel matches the snapshot semantics we saw failing in the report, and it's a cleaner rule than gating the write. The connection to the #198/#199 family ("which selection snapshot goes with an operation") is a useful way to frame it; if it's ever helpful to have the multi-hart sequences from our report as regression seeds for that family, happy to clean them up.