user
62 lines
1.8 KiB
Markdown
62 lines
1.8 KiB
Markdown
# K11 — Mutex, LockGuard and priority inheritance
|
|
|
|
K11 wraps a caller-owned static FreeRTOS mutex in `Mutex` and pairs
|
|
`lock(timeout)`/`unlock()` with a non-copyable `LockGuard<Mutex>`. The target
|
|
experiment forces a deterministic inversion scenario:
|
|
|
|
1. LOW (priority 1) takes the mutex;
|
|
2. HIGH (priority 3) attempts to take it and blocks;
|
|
3. MEDIUM (priority 2) is ready;
|
|
4. LOW inherits priority 3, runs before MEDIUM and releases through the guard;
|
|
5. HIGH acquires; LOW later returns to priority 1.
|
|
|
|
## Hazard3 evidence
|
|
|
|
```text
|
|
LOW base priority = 1
|
|
LOW inherited priority = 3
|
|
LOW after release = 1
|
|
MEDIUM ran before release = 0
|
|
protected shared counter = 11
|
|
```
|
|
|
|
The observed holder equals LOW/HIGH native handles at the appropriate points,
|
|
HIGH is `eBlocked` while LOW holds the mutex, and the event order is
|
|
LOW-take, HIGH-attempt, LOW-release, HIGH-take, MEDIUM-run.
|
|
|
|
## Build
|
|
|
|
```sh
|
|
make check
|
|
```
|
|
|
|
Host tests prove destruction balances three early returns and that a second
|
|
take of an ordinary non-recursive mutex fails. ABI checks keep static control in
|
|
`.bss` and reject vtables, RTTI, exceptions and hosted runtime.
|
|
|
|
## Debug
|
|
|
|
```gdb
|
|
b mutex_debug_checkpoint
|
|
p g_low_base_priority
|
|
p g_low_inherited_priority
|
|
p g_low_priority_after_release
|
|
p g_high_state_seen_by_low
|
|
p g_medium_ran_before_release
|
|
p g_owner_low
|
|
p g_owner_high
|
|
p g_sequence_low_take
|
|
p g_sequence_high_attempt
|
|
p g_sequence_low_release
|
|
p g_sequence_high_take
|
|
p g_sequence_medium_run
|
|
p g_mutex_pass
|
|
```
|
|
|
|
## Scope boundary
|
|
|
|
An ordinary mutex is task-context only, must be released by its owner and is
|
|
not recursive. A binary semaphore does not provide mutex ownership or priority
|
|
inheritance. `LockGuard` balances control flow but cannot make ISR use,
|
|
non-owner unlock or unbounded critical work valid.
|