53 lines
2.1 KiB
Markdown
53 lines
2.1 KiB
Markdown
# Card plan — FC03
|
|
|
|
## Goal
|
|
|
|
Make scheduler policy observable without teaching delays, queues, semaphores
|
|
or C++ prematurely. A student must be able to distinguish priority selection
|
|
from time slicing and show the difference in Hazard3/GDB.
|
|
|
|
## Task
|
|
|
|
```text
|
|
Task01 · Controlled scheduler experiment
|
|
├── A1 CONTEXT timer -> tick ISR -> scheduler -> tasks
|
|
├── A2 STRUCTURE contexts and bounded evidence records
|
|
├── A4 APPLICATION four-task topology and priority contract
|
|
├── A5 FLOW deterministic E01-E12 replay
|
|
├── A6 STATE Ready/Running/Deleted and priority transition
|
|
├── A7 RUNTIME CSRs, ISR stack, TCB/stack and committed traces
|
|
└── Exercise bounded observation with time slicing disabled
|
|
```
|
|
|
|
A3 is not repeated because callback dispatch was established in FC02. A8 is
|
|
not used because the scheduler policy is a kernel configuration rather than an
|
|
application design pattern.
|
|
|
|
## Runtime contract
|
|
|
|
1. `high_probe` is Ready at priority 0.
|
|
2. `peer_a` and `peer_b` are CPU-bound at priority 2.
|
|
3. `verifier` is Ready at priority 1 and cannot run while peers remain Ready.
|
|
4. The committed task-change trace must contain A-B-A.
|
|
5. Peer A records `before_raise` and calls `vTaskPrioritySet(high, 3)`.
|
|
6. High records `HIGH` and self-deletes before the API call returns.
|
|
7. Peer A records `after_raise`, requests peer termination and both peers
|
|
self-delete.
|
|
8. The verifier checks every invariant and exits with PASS.
|
|
|
|
The exact ordering claim applies to the three-marker projection only. Other
|
|
legal scheduling activity may occur before peer A is selected again.
|
|
|
|
## Exercise
|
|
|
|
Disable `configUSE_TIME_SLICING` while keeping both CPU-bound peers at the same
|
|
priority. This is an expected-noncompletion experiment: observe for a bounded
|
|
number of ticks that one peer may starve the other, capture the debugger state,
|
|
then restore the configuration. The exercise does not redefine the card's PASS
|
|
contract.
|
|
|
|
The series-level rationale and all FC03 acceptance gates are maintained in:
|
|
|
|
`meta/workspace-info/plans/informatyka/freertos-c-fc03-a1-a8.md`.
|
|
|