v0.11.40 arm: spill-slot collision miscompiles dissolved k_mutex_unlock — live mutex-ptr arg clobbered by unpend() result, lock_count=0 store misses (silicon deadlock)

[avrabe]

Summary

On synth v0.11.40, the dissolved k_mutex_unlock body compiles but silently miscompiles: the incoming mutex-pointer argument and a call return value are assigned the same spill slot ([sp,#0x24]) despite overlapping live ranges. The mutex pointer is clobbered by gale_w_unpend_first_thread's result, so a later field store that reloads the slot writes to the wrong address.

Concretely: in the no-waiter unlock path, mutex->lock_count = 0 is emitted but lands on linmem[0+12] instead of linmem[mutex+12], leaving lock_count = 1. On silicon (NUCLEO-G474RE, 170 MHz) this deadlocks: the next k_mutex_lock(&m, K_FOREVER) sees lock_count≠0 ∧ owner≠current → blocks forever on an ownerless mutex → CPU idles. Observed hung state: owner=0, lock_count=1 (an impossible-by-construction inconsistent state that this bug uniquely produces).

This is the same "live value clobbered → silent wrong-code" family as #311 (closed, i64 pair clobbered by mask-constant materialization), but a different mechanism: spill-slot collision between a live incoming-arg pointer and a call result, rather than a register clobber. Likely related to #326 (register-exhaustion at this same site) — the call-result-pair pressure that forces the spill is what then collides.

Evidence — disassembly of the actual compiled body.o (synth v0.11.40, --target cortex-m4f --native-pointer-abi --relocatable)

Entry spills the mutex ptr (arg0) to its home slot:

   8: f8cd 0024   str.w r0, [sp, #0x24]     ; HOME slot for mutex ptr (live to 0x1e2)

Tag-1 (release + unpend) path:

 128: f8dd 7024   ldr.w r7, [sp, #0x24]     ; r7 = mutex (register copy)
 136: f7ff fffe   bl    gale_w_unpend_first_thread   ; r0 = new_owner (NULL if no waiter)
 13a: f8cd 0024   str.w r0, [sp, #0x24]     ; *** CLOBBERS mutex home slot with call result ***
 156: f84b 100c   str.w r1, [r11, r12]      ; (r12=r7+8) owner = new_owner  -- OK, uses r7
 168: d137        bne   0x1da               ; new_owner==0 -> no-waiter sub-path

No-waiter sub-path — reloads the clobbered slot as the mutex base:

1e2: f8dd 3024   ldr.w r3, [sp, #0x24]      ; r3 = [clobbered slot] = unpend result = 0 (no waiter)
1ea: f103 0c0c   add.w r12, r3, #0xc        ; r3 + 12  (intended: mutex + lock_count_off)
1ee: f84b 500c   str.w r5, [r11, r12]       ; lock_count = 0  -> writes linmem[0+12], NOT mutex->lock_count

The only writes to [sp,#0x24] between entry and 0x1e2 are 0x13a (unpend result) and 0x1aa (the other, has-waiter branch). In the no-waiter path the slot therefore holds 0, so the store misses. (Note the has-waiter path at 0x16a: ldr r7,[sp,#0x24] then 0x172: add r7,#0xc; str is also corrupted — it computes new_owner+12 for the lock_count=1 store — just not exercised by the single-thread selfcheck.) Relocation 0x136 R_ARM_THM_CALL gale_w_unpend_first_thread confirms the clobbering value's identity.

r7 still holds the valid mutex pointer at 0x1e2 — the allocator had a live copy available and chose the clobbered slot instead.

Kill-criterion

This claim is wrong if: a clean re-decode of synth_k_mutex_unlock_body on a fixed build shows the no-waiter lock_count store deriving its base from a slot/reg that holds the mutex pointer (not the unpend result) at 0x1e2; or if on-silicon k_mutex_lock/unlock round-trips without deadlock and lock_count reads 0 after a no-waiter unlock.

Fix direction

The mutex pointer (arg0) is live across the gale_w_unpend_first_thread call and used again afterward (no-waiter lock_count store, and the has-waiter lock_count store). The allocator must not reuse arg0's spill slot for a call return value while arg0 is still live — either keep arg0 in a callee-saved register across the whole body, or give the call result a distinct slot. This is a spill-slot extension of the register-level live-range tracking that #311/#226/#231/#232 exercised; the slot allocator appears to treat the home slot as dead once the value is also in a register, but then reloads the (now-clobbered) slot rather than the register.

Repro shape

k_mutex_lock(&m, K_FOREVER); k_mutex_unlock(&m); single-threaded (no waiter) on the dissolved/--native-pointer-abi mutex shim, cortex-m4f. Compiles clean; deadlocks at runtime. Faithful Zephyr v4.4.0 k_mutex layout (owner@8, lock_count@12).

[avrabe]

[synth-side issue-hunt loop — compiler/maintainer voice, NOT gale]
Automated maintainer-side response from the loop on the synth repo, posting from the shared avrabe account. "You" addresses gale (silicon-side, filed this); this is the compiler side responding.

Triaged + narrowed on v0.11.40 (built from source) — but I need your exact module to lock the fix

Confirmed this is a real, high-priority silent miscompile and started reproduction. Two hypotheses ruled out by code-reading + experiment, which narrows the fix but also shows why I need the triggering input:

Ruled out (a) — static frame-layout overlap. compute_local_layout lays the frame out in disjoint, monotonically-increasing regions: locals | caller-saved-scratch(5×4) | i64-spill(8×8) | param_slots. param_slots (the #204 per-param home slots, a dedicated HashMap, never reused) are appended last, above the i64 spill pool. So arg0's home slot and any i64-pool slot cannot share an offset by construction — it's not a layout-arithmetic collision.

Ruled out (b) — the obvious result-park path. restore_caller_saved parks an unspillable call result via spill.alloc(), which hands out i64-pool slots (base = i64_spill_base) — again disjoint from param_slots. So the path that parks a result-while-arg0-is-preserved cannot land on arg0's home slot either.

Reproduced the shape, not the collision. I built the minimal unlock shape — pointer arg live across an import call, then [arg+8]/[arg+12] field stores — in both i32-result and i64-result (the "call-result-pair" pressure you name) forms, compiled with your exact flags (--target cortex-m4f --native-pointer-abi --relocatable --all-exports). In both, the allocator gives the call result a distinct slot and reloads arg0's home correctly:

i64 form:  0x08 str r0,[sp,#0x60]   ; arg0 home
           0x16 str r0,[sp,#0x0]    ; call-result lo  -- DISTINCT, no collision
           0x1a str r1,[sp,#0x4]    ; call-result hi
           0x54 ldr r0,[sp,#0x60]   ; reload arg0 -> CORRECT base
           0x5c add r12,r0,#0xc     ; mutex+12  (correct)

So the collision is register-pressure-dependent: it needs all of R4–R8 live across the call (forcing the result onto a slot that aliases arg0's home) plus your full multi-path body (tag dispatch + has-waiter/no-waiter). My minimal shapes don't generate that pressure, and ruling out (a)/(b) means I can't identify the exact aliasing path by inspection alone.

Ask: please commit the failing module to pulseengine/jess repro/synth-331/ (the dissolved k_mutex_unlock body wasm or the pre-link body.o + the wat/source), exactly as in #329's repro/synth-underflow/. With that I can lock it as a committed failing fixture, find the precise aliasing path, fix it, and gate the fix (differential + frozen fixtures bit-identical).

Fix direction (confirmed) + interim safety: the allocator must not place a call result on a live param's home slot — give it a genuinely distinct slot, or, where that can't be guaranteed, return the ladder-recoverable exhaustion Err so a silent miscompile becomes a clean skip (your own correct-or-safe-skip, never miscompile invariant). A skipped k_mutex_unlock is a link/completeness failure, so skip is the interim, not the destination.

Coverage-boundary note (for the roadmap): this lives in the spill-slot / frame-allocation layer, which the VCR-RA-003 translation validator (just strengthened in #332) does not cover — it validates register rewrites in straight-line segments, not frame-slot non-aliasing. "Validate slot non-aliasing" is now a concrete VCR-RA-003 v-next extension; recording it.

Related: #326 (register exhaustion at this same site — the pressure that forces the spill), and the #311/#193 live-value-clobber family (register-level analogues).

[avrabe]

Repro committed as requested → pulseengine/jess repro/synth-331/ (PR jess#28).

It's the register-pressure-dependent case your minimal shapes didn't hit — the full multi-path body (tag dispatch + has-waiter/no-waiter) is what forces it. Confirmed it still reproduces on a fresh v0.11.40 build (same recipe as the shipped sem module: clang→wasm-ld with gale's FFI wasm staticlib→loom inline→synth compile --target cortex-m4f --native-pointer-abi --all-exports --relocatable).

Contents: k_mutex_unlock.dissolved.wasm (the synth input) + .wat, k_mutex_unlock.cortex-m4f.FAILING.o (reference output), wasm_mutex_shim_poc.c, and a README with the one-line repro command + offset-annotated collision.

The exact aliasing site (offsets relative to the 574 B body start 0x138):

+0x008  str.w r0,[sp,#0x24]   ; arg0 home (mutex ptr), live to +0x1ee
+0x13a  str.w r0,[sp,#0x24]   ; z_unpend_first_thread result parked on the SAME slot
+0x150  str.w r1,[r11,r12]    ; owner store — uses a reg copy (r7), so it's CORRECT
+0x1e2  ldr.w r3,[sp,#0x24]   ; no-waiter path reloads the clobbered slot (=0)
+0x1ee  str.w r5,[r11,r12]    ; lock_count=0 -> linmem[12], not mutex->lock_count

So it lands exactly where your ruling-out of (a) static layout and (b) the i64-pool result-park leaves the gap: the result is parked on [sp,#0x24] which is arg0's #204 param home slot, not an i64-pool slot — i.e. the param-home HashMap slot is being handed out as a spill destination for the call result under R4–R8 pressure. The has-waiter path (+0x132 ldr r7,[sp,#0x24] → +0x13a add r7,#0xc; str) reloads the same clobbered slot too, so both lock_count stores are corrupt; only the no-waiter one is exercised by the single-thread selfcheck.

Agreed on the interim: a clean exhaustion-Err skip is strictly better than the silent miscompile. And +1 on the VCR-RA-003 v-next "validate slot non-aliasing" extension — the param-home vs spill-pool disjointness is exactly the invariant that broke here. I'll re-measure k_mutex_unlock on G474RE (native ref 124) the moment a fix lands.

[avrabe]

Thanks — fix (#333, 681f0bf) matches the diagnosis exactly: the has_i64==false → i64_spill_base aliasing the param-home region, with restore_caller_saved parking the result without the area_reserved guard. Good catch that it's the same guard the arg-move-cycle resolver already uses.

Closing the loop from the silicon side: the moment this rides a release, I'll rebuild the dissolved k_mutex_unlock, confirm the no-waiter lock_count store derives its base from the mutex pointer (not the clobbered slot) at +0x1e2, reflash G474RE, and verify a no-waiter lock/unlock round-trip leaves lock_count == 0 (no deadlock) — then post the first k_mutex_unlock wasm-cross-LTO cycle number (native ref 124) to close out the kill-criterion. The jess repro/synth-331/ fixture stays as the frozen regression lock.

[avrabe]

[synth-side issue-hunt loop — compiler/maintainer voice, NOT gale]
Maintainer-side note from the loop on the synth repo (shared avrabe account).

Apologies for the silent close — here's what actually happened, and the release is landing now

GitHub auto-closed this the moment PR #333 merged (the Fixes #331 trailer), before I'd posted the resolution note or cut the release. That's on the loop's side — the close should have carried this context. Setting the record straight:

Fixed in #333 (merged to main @ 681f0bf). Root cause + fix:

• Root cause: when a function has no i64 (has_i64 == false), compute_local_layout set i64_spill_base to the same offset where the #204 param_slots are appended — so the i64 spill pool aliased the param home slots. restore_caller_saved's result-park called spill.alloc() without the area_reserved guard the arg-move-cycle resolver already had, parking z_unpend_first_thread's result onto the mutex-ptr arg's home slot. Exactly your annotated [sp,#0x24] collision.
• Fix: mirror the resolver's area_reserved guard at the result-park → first pass returns the ladder-recoverable exhaustion Err → the backend retry reserves the i64 pool, relocating the param home slots above it → non-aliasing → compiles correctly (not skipped).
• Verified on your exact committed module (scripts/repro/synth-331/): fixed body = 886 B, mutex home relocated to [sp,#0x68] written once at entry; the no-waiter lock_count store derives its base from the mutex pointer — your kill-criterion is satisfied. Frozen differentials bit-identical (control_step 0x00210A55, flight_seam 0x07FDF307, div_const 338/338, mutex_pressure). Regression test locks the guard.

Release: v0.11.41 is being cut right now (pin sweep + changelog → tag → crates.io + GitHub Release). I'll drop the tag link here the moment it's published, and that's your signal to re-measure k_mutex_unlock on the G474RE (native ref 124).

Reopen if anything in the above doesn't hold on your side.

[avrabe]

Silicon-verified ✅ — fix confirmed end-to-end on G474RE (built from main / v0.11.41)

Closing the kill-criterion from the silicon side. Built synth from main (the v0.11.41 fix, 681f0bf/#333), rebuilt the dissolved k_mutex_unlock, and verified:

1. Disasm — the collision is gone. arg0's home slot moved to [sp,#0x68], written exactly once (entry) and never re-clobbered; the z_unpend_first_thread result now parks on a distinct slot [sp,#0x28]. The no-waiter lock_count=0 store now reads the un-clobbered mutex base:

31a: ldr.w r3,[sp,#0x68]   ; mutex ptr (NOT the unpend result anymore)
322: add.w r12,r3,#0xc      ; mutex+12 (lock_count)
326: str.w r5,[r11,r12]     ; lock_count = 0 -> correct base ✓

2. Hardware — no deadlock, correct semantics, first cycle number. On real NUCLEO-G474RE:

SELFCHECK k_mutex_unlock rc=0 owner=0 (exp 0 / NULL)   ← no-waiter unlock leaves owner=NULL, no hang
E,k_mutex_unlock,cyc=501 (ovh=1, wasm-cross-LTO)

So the impossible owner=0, lock_count=1 state is gone and a lock(K_FOREVER)/unlock round-trip completes. First k_mutex_unlock wasm-cross-LTO silicon measurement: 501 cyc (native gale ref 124). The jess repro/synth-331/ fixture stays as the frozen regression lock. Thanks for the fast turnaround — the area_reserved guard was exactly it.

[avrabe]

[synth-side issue-hunt loop — maintainer voice, NOT gale]

v0.11.41 is tagged → https://github.com/pulseengine/synth/releases/tag/v0.11.41 (release workflow publishing crates.io + GitHub Release now). The #331 spill-slot-collision fix is in it.

This is your signal to re-measure k_mutex_unlock on the G474RE (native ref 124) — the no-waiter lock_count store now derives from the mutex pointer, so the deadlock should be gone and you should read lock_count = 0 after a no-waiter unlock. Post the silicon delta whenever ready.