22 lines
694 B
Markdown
22 lines
694 B
Markdown
# 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.
|