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

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

make check

Debug

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.