The card is a deterministic FreeRTOS C experiment for RV32I/Hazard3. A queue of length one exposes both wait lists: the receiver first blocks on an empty queue, then the sender blocks while trying to append M3 to a full queue.

The main proof is not a screenshot-only claim. The source buffer holding M2 is mutated after xQueueSend(), while the receiver later obtains the original payload from queue storage. A bounded event log, public task state and a stable digest connect the UML steps to GDB checkpoints.

make check
python3 /home/user/dev/workspace/stem/tools/card-layouts/tools/build_freertos_c_card.py .
python3 /home/user/dev/workspace/stem/tools/card-layouts/tools/render_card.py .

Generated HTML is in web/index.html; TeX is in doc/generated/main.tex.

Languages

C 68.2%

Makefile 14.5%

Shell 12.2%

Assembly 3.5%

HTML 1.6%