Skip to content

wasm-synth z_impl: sem->count not incremented on give (stays 0, limit=1) on hardware — u64-packed new_count miscompiled; binary sem never signals (v0.11.12) #204

Description

@avrabe

Summary

On synth v0.11.12 (3dd70675), the wasm-cross-LTO z_impl_k_sem_give runs on real Cortex-M4 hardware without faulting (thanks — #202 fixed that), but it is functionally wrong: a k_sem_give on a binary semaphore (limit=1) with no waiter does not increment sem->count — it stays 0. The semaphore therefore never signals, and a blocked k_sem_take never wakes → the program hangs.

On-target evidence (NUCLEO-G474RE, gdb via openocd)

z_impl_k_sem_give is the loom-inlined wasm shim (decide folded in), called from the bench's ISR. Breakpointing it:

give entry  (0x08000260): sem=0x20000040  count[+8]=0  limit[+12]=1
give end    (reschedule):                 count[+8]=0     <-- still 0, should be 1
  • z_unpend_first_thread(&sem->wait_q) correctly returns NULL (wait_q at 0x20000040 is empty: head==tail==self), so this is the no-waiter → increment path.
  • gale's decision for decide(count=0, limit=1, has_waiter=0) is "increment, new_count = min(count+1, limit) = 1".
  • The store sem->count = new_count leaves count at 0, not 1.

The WAKE branch is correctly not taken (verified: arch_thread_return_value_set/z_ready_thread never fire; z_reschedule does). So the bug is specifically the new_count value written on the no-waiter path.

gale_k_sem_give_decide returns the decision AAPCS-packed into a u64 (action byte in low bits, new_count in the high 32). The shim extracts du.d.new_count (high word) and stores it. Either the inlined decide computes new_count wrong, or synth's u64→u32 high-word extraction (i64 shift/field access) yields 0. The native rustc-direct build of the identical logic increments correctly, so it's specific to the wasm→loom→synth path's i64 handling.

Reproduction

loom optimize merged.faithful.loom.wasm ... # decide inlined into z_impl (loom v1.1.5)
synth compile <that> --target cortex-m4f --all-exports --relocatable -o z.o   # synth v0.11.12
# link into the engine_control bench on nucleo_g474re, flash, run:
# boots, prints header, then hangs — sem->count never increments (gdb above).

WAT of the loom-inlined module: https://gist.github.com/avrabe/d30f965ac96b8ca4cac7d4fea2832a6a

Impact

Last functional blocker for the wasm-cross-LTO on-silicon measurement: the object compiles, links, flashes, and runs without faulting, but the semaphore give is semantically incorrect (count not incremented), so the bench can't complete a handoff. A unit-level check of the u64-packed-return extraction on the inlined z_impl would catch it (the IR-level Z3 validator evidently doesn't, since this is the encoded i64 high-word extraction).

Environment

  • synth v0.11.12 (3dd70675), arm backend, cortex-m4f; input from loom v1.1.5 (95a5f982) --passes inline
  • NUCLEO-G474RE; Zephyr SDK 1.0.1

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugSomething isn't working

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions