# 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.