SPEC-004 - Wait and Wake Protocol¶

Implementation and release scope: Project status records the implemented subset; roadmap defines release gates. Acceptance of this design does not establish implementation, verification, or support. Reconciled 2026-10-14.

Status: Accepted 2026-10-07 by the project owner, with the defaults of §16. Specification work item 4 of the roadmap (07 §3). Reference model: tools/model/ (SPEC-004 §13). Requirements: docs/requirements/KRN-WAIT.md (KRN-WAIT-001 to 009 restated; new from 010). Builds on: 03 §1.1 (thread states and wait reasons), 03 §3; SPEC-001 §4 (status codes), §5 (contexts and misuse); SPEC-002 §2 (per-CPU state), §4 (critical sections), §5 (scheduler lock), §6 (preemption points); SPEC-003 §5 (timeouts); ADR-013 (reference model), ADR-020 (destroy with waiters), ADR-026 (this protocol), ADR-027 (notification binding), ADR-036 (tiny profile scheduler). Research: R-001 §4 compares how eleven kernels handle the same problem; this protocol takes RTEMS’s three-state wait flag, ThreadX’s suspension sequence number, Zephyr’s superseded in-flight timeout and swap-data hand-off, and uC/OS-III’s single pend path under every primitive. Toolchain constraints applied: 09 §6 (no 64-bit atomics on 32-bit targets; byte atomics only on AVR; Armv6-M has no exclusive load and store, so no compare-and-swap).

1. Scope and terms¶

Every blocking primitive of the kernel (mutex, semaphore, event flags, condition variable, notification wait, message queue, pipe, join, sleep, thread start and suspend) is a thin layer over one protocol. This specification defines that protocol: its data, its state machine, its locking, its race rules, and its observable results. It does not define any primitive’s own semantics (SPEC-005 onward) and does not define the notification API (SPEC-006); it defines the hook they use.

Term	Meaning
Wait queue	The ordered set of threads blocked on one condition of one object (`embk_wait_queue_t`). An object may have several (a message queue has one for senders and one for receivers)
Wait node	The intrusive link that places a thread in a wait queue; one per thread, embedded in the thread control block
Wait reason	Why the thread is blocked: `START`, `SUSPEND`, `SLEEP`, `OBJECT`, `JOIN`, `NOTIFY` (03 §1.1)
Wait state	The protocol’s own flag: `READY`, `INTEND_TO_BLOCK`, `BLOCKED`. Distinct from the thread state of 03 §1.1, which it drives
Wait generation	A counter in the thread control block incremented at every completed wait; stale wake sources compare it and do nothing
Wake source	Whatever ends a wait: a signal on the object, the timeout, thread cancellation, object destruction, a peer’s restart (stale generation)
Wake result	`emb_wait_result_t`, written by the winning wake source before the thread becomes ready
Hand-off word	One `uintptr_t` the waker passes with the result (a message pointer, a count, satisfied event bits); the waiter never re-checks the object after a hand-off
Object lock domain	The lock that protects an object’s state and its wait queues: a critical section on uniprocessor, the object’s spinlock on SMP
Scheduler lock domain	Protects ready structures and the `BLOCKED` to `READY` transitions: a critical section on uniprocessor, the scheduler spinlock on SMP
Timeout lock domain	Protects the timeout structure of SPEC-003 §5: a critical section on uniprocessor, the timeout spinlock on SMP
Section	A stretch of code executed inside one lock domain without releasing it; the protocol’s masked time is the longest section

2. Data¶

2.1 Per-thread fields¶

thread:
  wait_state        READY | INTEND_TO_BLOCK | BLOCKED          one byte
  wait_generation   embk_wait_gen_t                            uint8_t on tiny, uint16_t otherwise
  wait_reason       START | SUSPEND | SLEEP | OBJECT | JOIN | NOTIFY
  # no separate wait_object field in M1: recover the object from wait_queue and its flags (A10)
  wait_queue        pointer to the wait queue the node is in, or NULL
  wait_node         intrusive doubly linked node (prev, next); absent in the table scheduler (§11)
  timeout_node      SPEC-003 §5.1, shared with sleep
  wake_result       logical field packed in the thread obj.flags bits (A16)
  wake_data         uintptr_t hand-off word
  suspended         bool: a SUSPEND overlay is active (§6.5)
  cancel_pending    bool: thread cancellation requested (§6.6)

The layout above is a logical protocol view, not a C ABI: M1 packs fields and uses the definitions in kernel/include/embk/kernel.h; interface/pseudocode names below also describe the later lock-domain design.

The thread state of 03 §1.1 is derived: BLOCKED when wait_state == BLOCKED or suspended, else READY or RUNNING by the scheduler.

2.2 Wait queue¶

typedef struct embk_wait_queue {
    embk_list_t   waiters;     /* intrusive dlist of wait nodes, ordered by policy */
    uint8_t       policy;      /* EMBK_WAIT_PRIORITY_FIFO (default) | EMBK_WAIT_FIFO */
} embk_wait_queue_t;

The queue carries no lock of its own: it is protected by the lock domain of the object that embeds it. A mutex’s owner pointer, needed for inheritance, lives in the mutex (SPEC-005), not in the queue. In the tiny profile’s table scheduler the queue is one bitmap word (§11).

2.3 Wake results¶

typedef enum emb_wait_result {
    EMB_WAIT_SATISFIED = 0,   /* the condition was met; wake_data carries the hand-off */
    EMB_WAIT_TIMEOUT,         /* deadline passed, including the EMB_NO_WAIT path */
    EMB_WAIT_CANCELED,        /* thread cancellation (KRN-THR-011) */
    EMB_WAIT_DESTROYED,       /* object destroyed with ABORT_WAITERS (ADR-020) */
    EMB_WAIT_STALE,           /* the peer handle's generation changed (join or port on a restarted thread, KRN-OBJ-005) */
    EMB_WAIT_INTERRUPTED,     /* reserved */
    EMB_WAIT_BUDGET           /* reserved (ADR-029 SUSPEND policy wakes through replenishment, not through this) */
} emb_wait_result_t;

Mapping to public status codes (SPEC-001 §4): SATISFIED is EMB_OK or the primitive’s own value; TIMEOUT is EMB_ETIMEDOUT; CANCELED is EMB_ECANCELED; DESTROYED is EMB_EDESTROYED; STALE is EMB_ESTALE. A mutex whose previous owner died returns SATISFIED with a flag in wake_data, which the mutex maps to EMB_EOWNERDEAD (SPEC-005). The results are mutually exclusive for one wait by construction (§5).

3. Ordering policy¶

PRIORITY_FIFO (default, KRN-WAIT-001): the queue is ordered by effective priority, highest first; among equal priority, insertion order. Insertion walks from the tail, because a new waiter is most often lower than or equal to the existing ones; the cost is O(waiters on this object).
FIFO (KRN-WAIT-002): append at the tail, O(1); for fairness over priority (barrier, some pipes).
Repositioning (KRN-WAIT-003): when a blocked thread’s effective priority changes (explicit set, inheritance, ceiling, budget demotion), the kernel removes and reinserts its node under the object lock. Inheritance (SPEC-005) does this as part of its chain walk; the hook is embk_wait_requeue().
The first node is always the thread a single wake serves. embk_wake_all serves them in queue order.

4. Internal interface¶

All functions are kernel-internal (embk_, SPEC-001 §2). Context classes follow SPEC-001 §5.

void  embk_wait_queue_init(embk_wait_queue_t *q, uint8_t policy);                      /* prekernel thread */

/* Phase 1: called by the primitive with the object lock held, after it has checked the
 * condition and found it unsatisfied. Enqueues self and marks INTEND_TO_BLOCK. */
void  embk_wait_prepare(embk_wait_queue_t *q, uint8_t reason, const void *object);      /* thread, object lock held */

/* Phases 2 and 3: called after the primitive released the object lock. Arms the timeout,
 * commits to BLOCKED or observes an early wake, switches, and returns the result. */
emb_wait_result_t embk_wait_commit(emb_timeout_t timeout, uintptr_t *data_out);         /* thread, no lock held */

/* Convenience for the common shape: releases @key, runs prepare and commit. */
emb_wait_result_t embk_block_on(embk_wait_queue_t *q, uint8_t reason, const void *object,
                                emb_timeout_t timeout, emb_irq_key_t key, uintptr_t *data_out);

/* Wakers: called with the object lock held. */
embk_thread_t *embk_wait_first(const embk_wait_queue_t *q);                            /* thread isr */
bool     embk_wait_wake(embk_thread_t *t, emb_wait_result_t result, uintptr_t data);    /* thread isr; false if t no longer waits here */
unsigned embk_wait_wake_all(embk_wait_queue_t *q, emb_wait_result_t result, uintptr_t data);
void     embk_wait_requeue(embk_thread_t *t);                                           /* after an effective-priority change */

/* Timeout path, called by SPEC-003 §5.3 expiry with no lock held on SMP, inside the
 * critical section on uniprocessor. Named embk_wait_wake(thread, TIMEOUT) in SPEC-003; this is it. */
void  embk_wait_wake_timeout(embk_thread_t *t, embk_wait_gen_t generation);

/* Cancellation and destruction, §6.6 and §6.7. */
bool  embk_wait_cancel(embk_thread_t *t);                                               /* thread; takes the object lock itself */
unsigned embk_wait_flush(embk_wait_queue_t *q, emb_wait_result_t result);               /* object lock held; DESTROYED or STALE */

embk_wait_prepare and embk_wait_commit are split so that a primitive can release its own lock between them; the window this opens is exactly what the state machine of §5 makes safe. A primitive that holds nothing but the critical section uses embk_block_on.

5. The protocol¶

5.1 Blocking, step by step¶

block_on(object, reason, timeout):                       -- thread context, no lock held
  key = object_lock()                                                   -- section 1
    if condition satisfied:        object_unlock(key); return SATISFIED (with hand-off if any)
    if timeout == EMB_NO_WAIT:     object_unlock(key); return TIMEOUT
    if misuse (ISR, scheduler locked, critical section held by caller): fault / EMB_EPERM   (SPEC-001 §5.3)
    gen = thread.wait_generation
    deadline = now + timeout  -- captured at call entry, wrap-safe/clamped by SPEC-003 (A21)
    thread.wait_reason = reason; thread.wait_queue = q  -- object derived from q in M1
    enqueue wait_node by policy                                         -- O(waiters)
    thread.wait_state = INTEND_TO_BLOCK
  object_unlock(key)                                       -- WINDOW: interrupts on, wakers may act

  if timeout is finite:
    key = timeout_lock()                                                -- section 2
      embk_timeout_arm(&thread.timeout_node, deadline)  -- UP; gen added for future SMP             -- O(armed timeouts)
    timeout_unlock(key)

  key = sched_lock_domain()                                             -- section 3
    if compare_and_set(thread.wait_state, INTEND_TO_BLOCK -> BLOCKED):
        remove thread from the ready structure
        embk_sched_reschedule_if_needed()                               -- P2 switch (SPEC-002 §6.3)
        sched_unlock_domain(key)                                        -- resumes here after the wake
    else:                                                               -- a waker won in the window
        sched_unlock_domain(key)
        key = timeout_lock(); embk_timeout_disarm(&thread.timeout_node); timeout_unlock(key)

  -- after wake: wait_state is READY, wake_result and wake_data are set, generation was bumped by the waker
  *data_out = thread.wake_data
  return thread.wake_result

The numbered sections identify protocol phases; nothing is held across the window. A phase can also execute priority-inheritance hooks, owned-lock recomputation, or a configured table scan. Its bound includes all such work, not just one list operation. See Timing and evidence. On uniprocessor every lock domain is the same critical section, so the sections are three short masked stretches with interrupts enabled in between (KRN-WAIT-008, KRN-WAIT-011).

5.2 Waking¶

wake(t, result, data):                                   -- object lock held; thread or ISR context
  if t.wait_queue != this object's queue:  return false  -- t is no longer waiting here (checked builds: fault if the caller asserts it was)
  dequeue t.wait_node; t.wait_queue = NULL
  t.wake_result = result; t.wake_data = data             -- result before READY (KRN-WAIT-005)
  t.wait_generation += 1                                 -- every later timeout, cancel, or flush for the old wait is stale
  if compare_and_set(t.wait_state, INTEND_TO_BLOCK -> READY):
      return true                                        -- t is still running on its own CPU and will see READY at commit
  -- else t.wait_state == BLOCKED
  key = sched_lock_domain()
    t.wait_state = READY
    if t.timeout_node armed: disarm it under the timeout lock (order: scheduler -> timeout)
    if not t.suspended:  make t ready; set reschedule_pending if t should preempt (SPEC-002 §6.2); IPI the owning CPU on SMP
  sched_unlock_domain(key)
  return true

The waker never spins and never waits. A wake that finds INTEND_TO_BLOCK costs a dequeue and one compare-and-set; one that finds BLOCKED adds the ready-structure insert.

5.3 Timeout¶

wake_timeout(t, gen):                                    -- from SPEC-003 §5.3 expiry
  q = t.wait_queue; obj = object_from_queue_flags(q)  -- M1 has no wait_object field                  -- read without a lock; validated below
  key = object_lock(obj)                                 -- uniprocessor: already inside the critical section
    if t.wait_generation != gen or t.wait_queue != q:    -- stale: the wait completed or t waits elsewhere
        object_unlock(key); return
    wake(t, TIMEOUT, 0)                                  -- §5.2, with the lock held
  object_unlock(key)

Sleep (SLEEP, no object) and notification wait (NOTIFY) use a per-thread pseudo-queue so that the same path applies; their lock domain is the scheduler lock domain.

5.4 The state machine¶

Current	Event	Next	Action
READY	prepare	INTEND_TO_BLOCK	enqueue node (section 1)
INTEND_TO_BLOCK	wake (any source)	READY	dequeue, result, generation bump; no ready-structure change
INTEND_TO_BLOCK	commit succeeds	BLOCKED	remove from ready structure, switch (section 3)
INTEND_TO_BLOCK	commit fails (already READY)	READY	disarm timeout, return result
BLOCKED	wake (any source)	READY	dequeue, result, generation bump, disarm timeout, make ready unless suspended
BLOCKED	suspend	BLOCKED	set `suspended`; node and timeout untouched (§6.5)
READY (woken while suspended)	resume	READY	make ready with the recorded result
any	stale timeout, cancel, or flush (generation mismatch)	unchanged	nothing

Invariants, checked by the reference model and by checked builds:

wait_state != READY implies the node is in exactly one wait queue (or one bit is set in the tiny profile) and wait_queue names it.
wake_result is written before wait_state becomes READY, and read only after.
For one wait (one generation value), at most one wake source performs the dequeue.
wait_generation increases by exactly one per completed wait.
A thread is in the ready structure if and only if wait_state == READY and not suspended and not TERMINATED.
No lock domain is held while wait_state == INTEND_TO_BLOCK outside sections 1, 2, and 3.

6. Wake sources¶

6.1 Signal with hand-off¶

A primitive that satisfies a waiter passes the satisfaction in wake_data: the mutex passes ownership (the waiter owns it when it resumes, SPEC-005); the semaphore passes the unit (the count is not incremented and the waiter does not decrement it); the message queue passes the message slot or copies into the waiter’s buffer before waking; event flags pass the satisfied bits; join passes the exit code; a port passes the request handle. The waiter never loops back to re-check the condition (default decision §16.4). This gives wait-order fairness and no barging: a thread that arrives while a waiter is being readied cannot steal the unit. The cost is that a woken thread that is preempted before running holds the unit meanwhile; this is accepted and documented per primitive.

6.2 Timeout¶

§5.3. The deadline is armed after the node is enqueued, so a timeout can only fire for an enqueued thread. On the 32-bit profile the arming path clamps and rejects per SPEC-003 §5.2. EMB_NO_WAIT never enqueues, never arms, never yields (API-024).

6.3 Notification binding (ADR-027, hook only)¶

An object that becomes ready for its bound operation, and whose transition was not consumed by a hand-off to a direct waiter, calls embk_binding_signal(&obj->binding), which performs emb_notify_set(binding.thread, binding.bit) when a binding exists. A hand-off consumes the transition: a semaphore given to a blocked waiter never had a count of one, so no bit is set; a message delivered to a blocked receiver never sat in the ring. The bound thread, when it runs, performs the operation with EMB_NO_WAIT and treats EMB_ETIMEDOUT as “someone else was faster” (SPEC-001 §4: no would-block code exists). The binding’s storage, API, and the notification wait itself are SPEC-006.

6.4 Priority change¶

embk_wait_requeue(t) under the object lock removes and reinserts the node by the new effective priority (PRIORITY_FIFO only; FIFO queues ignore it). A thread in INTEND_TO_BLOCK is enqueued and is repositioned like any other.

6.5 Suspend and resume (overlay)¶

emb_thread_suspend(t) sets t.suspended; if t was READY it is removed from the ready structure; if it was waiting, nothing else changes: the node stays in place and the timeout keeps running (KRN-THR-010, KRN-WAIT-014). A wake that arrives while suspended completes the wait (dequeue, result, generation) but does not make the thread ready. emb_thread_resume(t) clears the flag and makes the thread ready if wait_state == READY. A thread suspended while in INTEND_TO_BLOCK commits to BLOCKED normally and stays blocked until both the wait completes and it is resumed. Suspend of self is block_on(self, SUSPEND, EMB_WAIT_FOREVER) on the thread’s pseudo-queue.

6.6 Thread cancellation¶

emb_thread_cancel(t) sets cancel_pending. If t is waiting with a cancelable reason (SLEEP, OBJECT, JOIN, NOTIFY), embk_wait_cancel(t) obtains the object from the current queue/flags in M1, takes its lock, re-validates that t still waits there with the same generation, and calls wake(t, CANCELED, 0). START and SUSPEND are not cancelable by wake; the request is delivered at the thread’s next blocking call, where block_on returns CANCELED before enqueuing when cancel_pending is set (KRN-THR-011). There is no separate “abort another thread’s wait” API: cancellation is that API, and its scope is the whole thread, not one wait.

6.7 Destruction and stale peers¶

Destroying an object with waiters is a fault in checked builds and EMB_EBUSY in release builds unless it was created with ABORT_WAITERS, in which case embk_wait_flush(q, DESTROYED) wakes every waiter in queue order with DESTROYED, then the object’s generation is bumped (ADR-020, KRN-OBJ-001, 002). A partition or thread restart flushes the waiters of its threads’ join queues and ports with STALE and bumps the handle generation (ADR-032, KRN-OBJ-005). Flush is wake_all with a fixed result and a single reschedule at the end.

7. Scheduling interaction¶

A wake that makes a higher-priority thread ready sets reschedule_pending; the switch happens at P1 (ISR exit) or P2 (end of the thread-context operation), never inside the wake (SPEC-002 §6).
embk_wait_wake_all and embk_wait_flush ready every thread first and request one reschedule.
Under the scheduler lock, wakes proceed normally (the ready structure stays current, SPEC-002 §5); only the switch is deferred. Blocking with a nonzero timeout under the scheduler lock is misuse.
A woken thread that was preempted (not yet run) keeps its hand-off; nothing in the protocol depends on it running promptly.

8. Lock domains and SMP¶

Uniprocessor: the three domains are the critical section of SPEC-002 §4; the protocol’s contribution is the split into bounded sections.

SMP (FUTURE, interface fixed now):

Domain	Lock	Protects
object	per-object spinlock	object state, its wait queues, `wait_queue` and `wait_node` of its waiters
scheduler	scheduler spinlock (ADR-012)	ready structures, `BLOCKED` to `READY`, `suspended`
timeout	per-CPU timeout spinlock	the timeout structure

Order: object, then scheduler, then timeout; never the reverse. Consequences: the expiry path of SPEC-003 §5.3 pops a node under the timeout lock, marks it in flight, releases the timeout lock, and only then calls embk_wait_wake_timeout, which takes the object lock; a wake that must disarm a timeout holds the scheduler lock and takes the timeout lock, which is in order; a cancellation of a timeout whose handler is in flight on another CPU sets the node’s superseded bit and the handler checks it after acquiring the object lock (KRN-WAIT-009). Compare-and-set uses the architecture’s exclusive or atomic instructions where present; embk_wait_wake on a thread in INTEND_TO_BLOCK therefore needs no scheduler lock, because that thread is still running on its own CPU and is in no ready structure. A wake that readies a thread whose CPU is not the current one sends the reschedule IPI of SPEC-002 (KRN-WAIT-018).

9. Misuse and checked-build diagnostics¶

Condition	Checked build	Release build
`block_on` with nonzero timeout from ISR, with the scheduler locked, or inside a caller’s critical section	fault `EMB_FAULT_API_CONTEXT` (SPEC-001 §5.3, KRN-IRQ-001, 021)	`EMB_EINVAL`
`block_on` while `wait_state != READY`	fault `EMB_FAULT_KERNEL_INVARIANT`	undefined (cannot happen without corruption)
`embk_wait_wake` asserting a thread that does not wait on the given queue	fault `EMB_FAULT_KERNEL_INVARIANT`	returns false
queue order violated after insert (`prev.prio < node.prio` in `PRIORITY_FIFO`)	fault	not checked
timeout armed with a generation that does not match at expiry	counted in statistics, no fault	same
destroy with waiters without `ABORT_WAITERS`	fault `EMB_FAULT_API_LIFECYCLE`	`EMB_EBUSY`

The transition checker of ADR-035 covers the context conditions; the invariants of §5.4 are the kernel-invariant checks. EMB_FAULT_KERNEL_INVARIANT is introduced here as the fault identifier of the kernel fault class of 03 §10.1 (the EMB_FAULT_API_* identifiers of SPEC-001 §5.3 cover misuse by the caller; this one covers a broken kernel invariant and is always fatal).

10. Observability¶

Trace events (04 §7.2, CTF): wait_begin(thread, object, reason, deadline), wait_end(thread, result, cycles_blocked), wake(source: signal | timeout | cancel | flush, waker, thread, result), wait_requeue(thread, old_prio, new_prio). Statistics (04 §7.5, optional): per object, contention count (waits that blocked) and maximum queue length; per thread, blocked time; per CPU, stale-timeout count. The debug descriptor (ADR-011) exports the offsets of wait_state, wait_object, wait_queue, wake_result, and the queue list head so that a debugger can show “blocked on X behind Y”.

11. Tiny profile variant (ADR-036)¶

With CONFIG_EMB_SCHED_TABLE, threads are indexed by unique priority and a wait queue is one word: bit i set means thread i waits. embk_wait_prepare sets the bit; embk_wait_first is count-leading-zeros; embk_wait_wake clears the bit; embk_wait_requeue is a no-op (priorities are unique and fixed); FIFO policy is not offered. There is no wait_node; wait_queue is the address of the word. The state machine, generations, results, and the suspend overlay are unchanged. The compare-and-set is a short critical section (AVR and Armv6-M have no atomic compare-and-swap).

12. Per-architecture summary¶

	AVR	Cortex-M0+ (Armv6-M)	Cortex-M3/M4/M33	RISC-V (A extension)	native
compare-and-set	critical section	critical section	`LDREX/STREX`	`LR/SC` or `AMOSWAP` loop	C11 atomics
lock domains	one critical section	one critical section	one critical section (UP)	one critical section (UP); spinlocks on SMP	host mutex per domain in the simulator
wait generation	`uint8_t`	`uint16_t`	`uint16_t`	`uint16_t`	`uint16_t`
wait queue	bitmap (table scheduler) or dlist	dlist	dlist	dlist	dlist

13. Reference model (ADR-013, KRN-WAIT-007)¶

The model is the first executable artifact of the project and is written in Python 3 (answers 08 Q15, §16.6): fastest to write and to read in review, with hypothesis for property-based exploration; the differential bridge to the kernel is a trace replay, so the model’s language is independent of the kernel’s. It lives in tools/model/ (05 §3) and is described in tools/model/README.md.

Structure. model/kernel.py holds Cpu (SPEC-002 §2 state machine), Thread (§2.1 fields), WaitQueue (§2.2, both the list and the bitmap form), TimeoutList (SPEC-003 §5), and Kernel with operations block_on, wake, expire(now), cancel, suspend, resume, flush, set_priority, irq_enter, irq_exit, sched_lock, sched_unlock, yield. Each operation is written as the sequence of sections of §5, and the explorer may interleave other operations (including interrupts and, in the SMP model, other CPUs) only at section boundaries, which is exactly the real system’s atomicity.

Exploration. Exhaustive depth-first search over all interleavings for up to 3 threads, 2 objects, one armed timeout per thread, and the operation set above; every reachable state is checked against the invariants of §5.4 and the properties below. Randomized exploration (hypothesis stateful testing) beyond that, with a fixed seed corpus committed.

Properties. Exactly one wake source dequeues per generation; wake_result is set before READY; no thread stays BLOCKED after a wake was delivered to it; no timeout acts after its generation changed; queue order is maintained after every insert and requeue; a suspended thread keeps its queue position and its deadline; cancellation of a blocked thread completes within one operation; EMB_NO_WAIT never changes queue or timeout state; the set of ready threads equals the set with wait_state == READY and not suspended.

Oracle for the kernel. The model exposes expected_result(thread) and expected_order(queue); the differential test feeds the kernel’s trace events (§10) into the model as operations and compares outcomes. Divergence is a test failure in the kernel, never a reason to edit the model without a specification change.

14. Requirements¶

Restated: KRN-WAIT-001 to 009 (03 §3). New: KRN-WAIT-010 to 022, in docs/requirements/KRN-WAIT.md.

15. Worked example¶

Semaphore take with a 10 ms timeout, counting semaphore at zero, one other waiter of lower priority, giver in an ISR after 3 ms:

T1 calls emb_sem_take(s, EMB_TIMEOUT(EMB_MS(10))). Section 1: count is zero, T1 enqueues ahead of the lower-priority waiter, INTEND_TO_BLOCK. Window.
Section 2: deadline now + 10 ms armed with generation 7.
Section 3: compare-and-set succeeds, T1 is removed from the ready structure, switch to the next thread.
3 ms later an ISR calls emb_sem_give(s). The give finds a waiter: embk_wait_first is T1; embk_wait_wake(T1, SATISFIED, 1) dequeues T1, sets the result and the unit, bumps the generation to 8, finds BLOCKED, disarms the timeout, makes T1 ready, sets reschedule_pending. The count stays zero (hand-off, §6.1). No binding bit is set (the transition was consumed).
At the outermost ISR exit (P1) T1 runs, reads wake_result == SATISFIED, returns EMB_OK.
If instead the deadline had passed first: expiry pops T1’s node with generation 7, embk_wait_wake_timeout(T1, 7) finds the generation unchanged and the queue matching, wakes with TIMEOUT; emb_sem_take returns EMB_ETIMEDOUT; the later give finds the lower-priority waiter first instead.

16. Decisions taken at acceptance (2026-10-07)¶

Wait queues are protected by the lock domain of the object that embeds them; they carry no lock of their own. On uniprocessor all three domains are the single critical section, and the protocol’s guarantee is the split into three bounded sections.
The wait state transitions are compare-and-set operations; architectures without an atomic compare-and-swap (AVR, Armv6-M) perform them in a short critical section with identical semantics.
Thread cancellation is the only way another thread ends a wait; there is no separate wait-abort API. START and SUSPEND waits are not cancelable by wake.
Every primitive hands the satisfaction over in wake_data; a woken waiter never re-checks the condition. No barging.
Suspend is an overlay that keeps the wait-queue position and the running deadline; a wake while suspended completes the wait and takes effect at resume.
The reference model is written in Python 3 with hypothesis; exhaustive exploration up to 3 threads and 2 objects, randomized beyond. This answers 08 Q15.
emb_wait_result_t is an internal type; public functions return status codes. STALE is added to the result set for restarted peers (ADR-032); INTERRUPTED and BUDGET stay reserved.
One notification binding per object (ADR-027); a transition consumed by a hand-off to a direct waiter sets no bit.
The wait generation is 8 bits on the tiny profile and 16 bits elsewhere; UP safety relies on serialized timeout removal/wait completion, with no old expiry retained across reuse. This does not prove wrap harmless on SMP or for externally retained callbacks: those require a reviewed in-flight lifetime/epoch scheme before a value can be reused; the thread-count bound alone is insufficient (A15).