lab-rv32i-freertos-c-resource-management/doc/card-plan.md

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

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.