KRN-WAIT requirements¶
Default wake order shall be highest effective priority first, FIFO among equal priority. Rationale: Priority order is what every real-time analysis assumes; FIFO among equals gives bounded waiting. ThreadX’s FIFO default is a documented source of unexpected inversion (R-001 §4.1). Status: Accepted 2026-10-07 Verification: Test: conformance Trace: SPEC-004 §3; 03 §3.3; R-001 §4.1 |
Objects may be created with pure FIFO wake order where the application requires fairness over priority. Rationale: Barriers and some streams need arrival order. Status: Accepted 2026-10-07 Verification: Test: conformance Trace: SPEC-004 §3; 03 §3.3 |
A waiter whose effective priority changes while blocked shall be repositioned in a PRIORITY_FIFO wait queue. Rationale: Inheritance and explicit priority changes are meaningless if the queue keeps the old order. Status: Accepted 2026-10-07 Verification: Test: conformance Trace: SPEC-004 §6.4; 03 §3.3; KRN-SYNC-009 |
Exactly one wake source shall win for a given blocked thread; the losers shall observe that the thread is no longer waiting and shall not modify it. Rationale: Two sources acting on one wait corrupt queues and deliver two results. Status: Accepted 2026-10-07 Verification: Analysis: exhaustive exploration of the reference model (SPEC-004 §13) proves it for the bounded configuration. Test: conformance Trace: SPEC-004 §5; 03 §3.4; ADR-026 |
The winning wake source shall set the wake result and the hand-off word before making the thread READY. Rationale: A woken thread may run on another CPU or at the next instruction; it must find its result. Status: Accepted 2026-10-07 Verification: Analysis: model property; review of Trace: SPEC-004 §5.2; 03 §3.4 |
Removal from the wait queue and from the timeout structure shall be atomic with respect to each other, as seen by any other wake source. Rationale: A node left in one structure after being removed from the other produces a stale wake. Status: Accepted 2026-10-07 Verification: Analysis: model property “no timeout acts after its generation changed”; Test: Trace: SPEC-004 §5.2, §5.3, §8; 03 §3.4 |
The protocol shall be expressed in the executable reference model and verified by randomized and, where practical, exhaustive state exploration before implementation. Rationale: Race rules cannot be reviewed by reading; they are checked by exploring every interleaving. Status: Accepted 2026-10-07 Verification: Analysis: the model and its exploration log are committed before the first kernel source file of M2; CI runs the exhaustive exploration on every change to the model. Trace: SPEC-004 §13; 03 §3.4; ADR-013; 05 §4 |
The wait state shall be a three-state flag (READY, INTEND_TO_BLOCK, BLOCKED) changed by compare-and-set on cores that provide it and by a bounded critical section otherwise; no lock or masked section shall be held from the decision to block until the switch. Rationale: This is what bounds the kernel’s longest masked section by one list operation instead of by the whole block path (R-001 §4.2; R-003 target T7). Status: Accepted 2026-10-07 Verification: Analysis: model invariant 6 of SPEC-004 §5.4. Test: the critical-section monitor (ADR-034) on the conformance run reports every masked section of the wait path within the T7 budget. Trace: SPEC-004 §5.1, §5.4; ADR-026 |
Every wait shall carry a generation; a timeout, cancel, or destroy that observes a different generation shall do nothing. On SMP a timeout whose handler is running on another CPU shall be marked superseded and its cancellation retried. Rationale: Generations make late wake sources harmless without holding locks across them; the superseded bit closes the SMP window between popping a node and acting on it. Status: Accepted 2026-10-07 Verification: Analysis: model property “no timeout acts after its generation changed”; the SMP model exercises the superseded path. Test: Trace: SPEC-004 §5.3, §8; ADR-026; KRN-TIM-026 |
A thread shall wait on at most one object at a time; its wait node and its timeout node shall be embedded in its thread control block, and the kernel shall allocate nothing to block a thread. Rationale: Static memory, O(1) wake, and a single place for a debugger to look. Status: Accepted 2026-10-07 Verification: Analysis: structure review; the debug descriptor exports the node offsets. Test: footprint test shows no allocation on the wait path. Trace: SPEC-004 §2.1; KRN-MEM |
A blocking operation shall consist of at most three lock-domain sections (condition check and enqueue; timeout arm; commit and switch), with the lock domain released between phases; each phase shall state its complete configured bound including list operations, wake hooks, inheritance propagation, and scheduler scans. Rationale: Makes the T7 masked-time bound a structural property rather than a measurement. Status: Accepted 2026-10-07 Verification: Analysis: review of Trace: SPEC-004 §5.1; R-003 §4 T7 |
A wake source that satisfies a wait shall deliver the satisfaction (ownership, unit, message, bits, exit code) with the result in one step, and the woken thread shall not re-check the object’s condition. Rationale: Prevents barging, gives wait-order fairness, and removes the retry loops that other kernels need (R-001 §4.2, FreeRTOS “loop back to the top”). Status: Accepted 2026-10-07 Verification: Test: conformance Trace: SPEC-004 §6.1; SPEC-005; SPEC-007 |
Waking all waiters of a queue shall deliver results in queue order, make every thread ready, and request one reschedule at the end. Rationale: Deterministic order and no switch storm. Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-004 §6.7, §7 |
Suspending a blocked thread shall leave its wait-queue position and its deadline untouched; a wake that arrives while suspended shall complete the wait and take effect when the thread is resumed. Rationale: Defines the classic “suspend while waiting” ambiguity once, from the protocol’s side (KRN-THR-010). Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-004 §6.5; 03 §1.1; KRN-THR-010 |
A thread cancellation request shall wake a thread blocked with reason SLEEP, OBJECT, JOIN, or NOTIFY with result CANCELED; a thread blocked with reason START or SUSPEND, or not blocked, shall receive the request at its next blocking call, which returns CANCELED before enqueuing. There shall be no other way for one thread to end another’s wait. Rationale: One mechanism for cooperative cancellation (KRN-THR-011); no “wait abort” API with ambiguous ownership. Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-004 §6.6; KRN-THR-011 |
Destroying an object created with Rationale: Restates KRN-OBJ-001, 002, and 005 from the protocol’s side so that one flush primitive serves both. Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-004 §6.7; ADR-020; ADR-032; KRN-OBJ-001, 002, 005 |
Wait queues shall be protected by the lock domain of the object that embeds them. On SMP the order shall be object, then scheduler, then timeout, never reversed; the timeout expiry path shall call the wake with no lock held. Rationale: A fixed order is the only deadlock-free discipline; the expiry rule is what makes the order hold for timeouts. Status: Accepted 2026-10-07 Verification: Analysis: the spinlock validator (SMP checked builds) records lock order and faults on inversion; the SMP reference model encodes the order. Trace: SPEC-004 §8; ADR-012; KRN-SMP |
A wake that readies a thread which should preempt the current thread of another CPU shall send that CPU the reschedule interrupt; a wake on a thread in INTEND_TO_BLOCK shall not touch any ready structure. Rationale: Preemption latency on SMP must not depend on the woken CPU’s next tick; the INTEND_TO_BLOCK rule keeps the common wake lock-free. Status: Accepted 2026-10-07 Verification: Test: SMP conformance Trace: SPEC-004 §5.2, §8; KRN-IRQ-024 |
With the table scheduler, a wait queue shall be one word with one bit per thread; prepare sets the bit, wake-first is the highest set bit, wake clears it; the state machine, generations, results, and the suspend overlay shall be identical to the list form. Rationale: Saves two pointers per thread and makes wake-highest O(1) on the smallest targets (ADR-036). Status: Accepted 2026-10-07 Verification: Test: the whole Trace: SPEC-004 §11; ADR-036; KRN-SCH-042 |
The protocol shall emit trace events for wait begin, wait end with result and blocked duration, wake with source, and requeue; and, as an option, per-object contention count and maximum queue length, per-thread blocked time, and per-CPU stale-timeout count. Rationale: “Blocked on what, behind whom, for how long” is the first question in every scheduling investigation. Status: Accepted 2026-10-07 Verification: Test: the trace decoder reconstructs every wait of the conformance run; OBS tests check compile-out. Trace: SPEC-004 §10; OBS-005, OBS-008 |
Checked builds shall fault on: blocking with a nonzero timeout from an ISR, under the scheduler lock, or inside the caller’s critical section; blocking while the wait state is not READY; a wake asserted on a thread that does not wait on the given queue; a queue order violation after insert; destroy with waiters without Rationale: SPEC-001 §5.3 rule applied to this protocol. Status: Accepted 2026-10-07 Verification: Test: Trace: SPEC-004 §9; SPEC-001 §5.3; KRN-IRQ-001, 021, 035; ADR-035 |
The reference model shall exhaustively explore all enabled section-granularity interleavings of each declared finite scenario within its recorded state budget, including scenarios of up to 3 threads, 2 objects, and one armed timeout per thread over the operations block, wake, expire, cancel, suspend, resume, flush, set-priority, interrupt entry and exit, scheduler lock and unlock, and yield; and by randomized stateful testing beyond those bounds with a committed seed corpus. Rationale: Fixes what “explored” means so that KRN-WAIT-007 is checkable. Status: Accepted 2026-10-07 Verification: Analysis: the exploration tool reports the state count and the bounds reached; CI fails if the bounds are lowered. Trace: SPEC-004 §13; KRN-WAIT-007; TEST-008 |