19 lines
837 B
Markdown
19 lines
837 B
Markdown
# FC05 — queues, blocking and byte-copy semantics
|
|
|
|
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.
|
|
|
|
```sh
|
|
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`.
|