46 lines
1.4 KiB
Markdown
46 lines
1.4 KiB
Markdown
# FC08 — mutexes and priority inheritance
|
|
|
|
This card is a deterministic Hazard3/RV32I experiment for Chapter 8 of the
|
|
FreeRTOS Kernel Book. It proves the mechanism, not only the final value.
|
|
|
|
```text
|
|
Low p1 owns mutex
|
|
→ High p3 blocks on the mutex
|
|
→ Low effective priority becomes 3
|
|
→ Medium p2 is Ready but does not run
|
|
→ Low gives the mutex
|
|
→ High acquires before Medium runs
|
|
→ Low returns to priority 1
|
|
```
|
|
|
|
Only public FreeRTOS APIs are used for acceptance assertions. The internal
|
|
`uxBasePriority` and `uxPriority` fields are shown as debugger evidence, not
|
|
as application dependencies. No manual `vTaskPrioritySet` substitutes for
|
|
priority inheritance.
|
|
|
|
## Build and evidence
|
|
|
|
```sh
|
|
make task1
|
|
make host-test
|
|
make check-abi
|
|
make sim
|
|
make check-determinism
|
|
```
|
|
|
|
The final verifier checks the real mutex holder, effective priorities, public
|
|
task state, three distinct task stacks, protected-resource invariant, exact
|
|
event order and a stable digest from three clean simulator processes.
|
|
|
|
## Interactive views
|
|
|
|
- A2 — mutex, owner, waiters and protected resource;
|
|
- A4 — deterministic task topology;
|
|
- A5 — complete inheritance and hand-off sequence;
|
|
- A6 — mutex ownership and effective-priority states;
|
|
- A7 — handles, stacks, public observations and TCB debugger evidence;
|
|
- A8 — critical section, scheduler suspension, mutex and gatekeeper choices.
|
|
|
|
Source basis: FreeRTOS Kernel Book, Chapter 8. No source example is copied
|
|
verbatim.
|