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.

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

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.