# FC08 card plan — resource management

## Thesis

A FreeRTOS mutex combines ownership with priority inheritance. A binary
semaphore does not provide the same scheduling contract.

## Task tree

```text
FC08 · Mutexes and priority inheritance
└── Task01 · bounded priority inversion
    ├── Block · A2/A4 static contract
    │   └── Phase · STRUCTURE
    │       ├── Step 01 · genuine mutex object
    │       ├── Step 02 · Low owns the resource
    │       ├── Step 03 · High waits forever
    │       └── Step 04 · Medium is Ready
    ├── Block · A5/A6 execution
    │   └── Phase · INHERIT / HANDOFF
    │       ├── Step 05 · Low inherits priority 3
    │       ├── Step 06 · Medium has not run
    │       ├── Step 07 · Low gives
    │       ├── Step 08 · High acquires first
    │       └── Step 09 · Low returns to priority 1
    ├── Block · A7 runtime proof
    │   └── Step 10 · PASS and stable digest
    └── Exercise · lock-order table for two mutexes
```

## Acceptance gates

- `configUSE_MUTEXES=1`; one genuine mutex; no manual priority changes.
- High uses a non-zero wait and blocks while Low owns the mutex.
- `uxTaskPriorityGet(Low)` changes 1 → 3 → 1.
- Medium is `eReady` and `medium_started==0` while Low is inherited p3.
- High acquires before Medium runs; protected value changes under ownership.
- Event records are committed last and three clean simulations agree.