feat: add lab-rv32i-freertos-mutex card
This commit is contained in:
@@ -0,0 +1,61 @@
|
||||
# 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.
|
||||
Reference in New Issue
Block a user