user
60 lines
1.8 KiB
Markdown
60 lines
1.8 KiB
Markdown
# K12 — semaphores and task notifications
|
|
|
|
K12 separates three synchronization meanings behind small C++ wrappers:
|
|
|
|
- `BinarySemaphore` is an empty/full signal with no payload or owner;
|
|
- `CountingSemaphore<Max>` models a bounded count of available resources;
|
|
- `TaskNotification` is a non-owning view of one task's TCB notification slot,
|
|
with explicit action/value semantics.
|
|
|
|
Both semaphore wrappers use caller-owned static control blocks. The
|
|
notification wrapper allocates no kernel object: its state is already inside
|
|
the target task's TCB.
|
|
|
|
## Hazard3 evidence
|
|
|
|
```text
|
|
binary count 0 -> 1 -> 0
|
|
second binary give false (already full)
|
|
counting slots 2 -> 1 -> 0
|
|
third counting take waiter Blocked
|
|
one give wakes waiter; count consumed back to 0
|
|
notification take result 1
|
|
explicit overwrite value 0xA5A55A5A
|
|
```
|
|
|
|
The same high-priority waiter is observed in `eBlocked` for counting take,
|
|
notification take and value wait. `vTaskSuspendAll` creates a stable checkpoint
|
|
after notification give but before the waiter consumes the TCB value.
|
|
|
|
## Build
|
|
|
|
```sh
|
|
make check
|
|
```
|
|
|
|
## Debug
|
|
|
|
```gdb
|
|
b synchronization_debug_checkpoint
|
|
p g_binary_initial_count
|
|
p g_binary_after_give
|
|
p g_binary_second_give
|
|
p g_counting_initial_count
|
|
p g_count_after_take1
|
|
p g_count_after_take2
|
|
p g_waiter_state_for_counting
|
|
p g_waiter_state_for_notification
|
|
p g_notification_pending_checkpoint
|
|
p g_notification_take_value
|
|
p/x g_notification_message_value
|
|
p g_sync_pass
|
|
```
|
|
|
|
## Scope boundary
|
|
|
|
A semaphore is not payload storage. A notification has exactly one receiving
|
|
task per TCB slot and action/clear policy must be explicit; it is not a
|
|
multi-consumer queue. Binary/counting `take` and `notify wait` use different
|
|
state machines even when their visible wakeup looks identical.
|