lab-rv32i-freertos-c-queue/doc/card-plan.md

FC05 card plan

Thesis

A FreeRTOS queue owns a fixed-size byte copy of each enqueued item. Queue occupancy controls which sender or receiver is Blocked, while priority decides which unblocked task runs next.

Views

• A2 — message, queue and task structure;
• A5 — deterministic send/receive sequence;
• A6 — occupancy and task-state transitions;
• A7 — GDB-visible full-queue checkpoint;
• A8 — value versus pointer ownership decision.

Required evidence

The replay must prove empty blocking, full blocking, FIFO M1→M2→M3, retained M2=0x2222 after the producer changes its source to 0xDEAD, distinct task stacks and a deterministic ten-record evidence stream.