From 9f38dbed841e16dee19c10539b78b17af58ce6f2 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 20 Mar 2026 06:01:43 +0100 Subject: [PATCH 01/16] feat(shim): convert k_mem_slab alloc/free to decision struct pattern Rewrite k_mem_slab_alloc and k_mem_slab_free in the C shim to use the Extract/Decide/Apply pattern with Rust decision structs, matching the semaphore PoC. Rust now decides the action (ALLOC_OK/PEND/NOMEM and FREE_OK/WAKE_THREAD); C extracts kernel state, calls Rust, and applies. Co-Authored-By: Claude Opus 4.6 (1M context) --- ffi/include/gale_mem_slab.h | 26 ++ ffi/src/lib.rs | 597 ++++++++++++++++++++++++++++++++++++ zephyr/gale_mem_slab.c | 122 ++++---- 3 files changed, 685 insertions(+), 60 deletions(-) diff --git a/ffi/include/gale_mem_slab.h b/ffi/include/gale_mem_slab.h index 9d48276..c6edb3f 100644 --- a/ffi/include/gale_mem_slab.h +++ b/ffi/include/gale_mem_slab.h @@ -61,6 +61,32 @@ int32_t gale_mem_slab_alloc_validate(uint32_t num_used, int32_t gale_mem_slab_free_validate(uint32_t num_used, uint32_t *new_num_used); +/* ---- Phase 2: Full Decision API ---- */ + +struct gale_mem_slab_alloc_decision { + int32_t ret; /* 0=OK, -ENOMEM=slab full */ + uint32_t new_num_used; + uint8_t action; /* 0=ALLOC_OK, 1=PEND_CURRENT, 2=RETURN_NOMEM */ +}; + +#define GALE_MEM_SLAB_ACTION_ALLOC_OK 0 +#define GALE_MEM_SLAB_ACTION_PEND_CURRENT 1 +#define GALE_MEM_SLAB_ACTION_RETURN_NOMEM 2 + +struct gale_mem_slab_alloc_decision gale_k_mem_slab_alloc_decide( + uint32_t num_used, uint32_t num_blocks, uint32_t is_no_wait); + +struct gale_mem_slab_free_decision { + uint32_t new_num_used; + uint8_t action; /* 0=FREE_OK, 1=WAKE_THREAD */ +}; + +#define GALE_MEM_SLAB_ACTION_FREE_OK 0 +#define GALE_MEM_SLAB_ACTION_WAKE_THREAD 1 + +struct gale_mem_slab_free_decision gale_k_mem_slab_free_decide( + uint32_t num_used, uint32_t has_waiter); + #ifdef __cplusplus } #endif diff --git a/ffi/src/lib.rs b/ffi/src/lib.rs index 1458063..74cd35a 100644 --- a/ffi/src/lib.rs +++ b/ffi/src/lib.rs @@ -1036,6 +1036,109 @@ pub extern "C" fn gale_stack_pop_validate( } } +// ---- Phase 2: Full Decision API for Stack ---- + +/// Decision struct for k_stack_push — tells C shim what action to take. +#[repr(C)] +pub struct GaleStackPushDecision { + /// Return code: 0 (OK), -ENOMEM (full) + pub ret: i32, + /// New count value (only meaningful when action=PUSH_OK and no waiter) + pub new_count: u32, + /// Action: 0=PUSH_OK, 1=PEND_CURRENT (unused for push — always immediate) + /// With push: 0=PUSH_OK means store data or wake waiter, 1 is not used. + /// We use: 0=STORE_DATA, 1=WAKE_WAITER, 2=FULL + pub action: u8, +} + +pub const GALE_STACK_PUSH_STORE: u8 = 0; +pub const GALE_STACK_PUSH_WAKE: u8 = 1; +pub const GALE_STACK_PUSH_FULL: u8 = 2; + +/// Full decision for k_stack_push: decides whether to store data, wake a waiter, +/// or reject because the stack is full. +/// +/// The C shim calls z_unpend_first_thread first (side effect), then passes +/// whether a waiter was found. Rust decides the action. +/// +/// Verified: SK1 (bounds), SK3 (increment), SK4 (-ENOMEM). +#[unsafe(no_mangle)] +pub extern "C" fn gale_k_stack_push_decide( + count: u32, + capacity: u32, + has_waiter: u32, +) -> GaleStackPushDecision { + if has_waiter != 0 { + // Waiter exists: give data directly to waiting thread (count unchanged) + GaleStackPushDecision { + ret: OK, + new_count: count, + action: GALE_STACK_PUSH_WAKE, + } + } else if count < capacity { + // Space available: store data, increment count + #[allow(clippy::arithmetic_side_effects)] + let new_count = count + 1; + GaleStackPushDecision { + ret: OK, + new_count, + action: GALE_STACK_PUSH_STORE, + } + } else { + // Full: reject + GaleStackPushDecision { + ret: ENOMEM, + new_count: count, + action: GALE_STACK_PUSH_FULL, + } + } +} + +/// Decision struct for k_stack_pop — tells C shim what action to take. +#[repr(C)] +pub struct GaleStackPopDecision { + /// Return code: 0 (OK), -EBUSY (empty + no_wait) + pub ret: i32, + /// New count value (decremented if popped) + pub new_count: u32, + /// Action: 0=POP_OK (return data), 1=PEND_CURRENT (block or return -EBUSY) + pub action: u8, +} + +pub const GALE_STACK_POP_OK: u8 = 0; +pub const GALE_STACK_POP_PEND: u8 = 1; + +/// Full decision for k_stack_pop: decides whether to pop data or pend/reject. +/// +/// Verified: SK1 (bounds), SK5 (decrement), SK6 (-EBUSY). +#[unsafe(no_mangle)] +pub extern "C" fn gale_k_stack_pop_decide( + count: u32, + is_no_wait: u32, +) -> GaleStackPopDecision { + if count > 0 { + #[allow(clippy::arithmetic_side_effects)] + let new_count = count - 1; + GaleStackPopDecision { + ret: OK, + new_count, + action: GALE_STACK_POP_OK, + } + } else if is_no_wait != 0 { + GaleStackPopDecision { + ret: EBUSY, + new_count: 0, + action: GALE_STACK_POP_OK, + } + } else { + GaleStackPopDecision { + ret: 0, + new_count: 0, + action: GALE_STACK_POP_PEND, + } + } +} + /// Validate timer init parameters. /// /// timer.c init: @@ -1114,6 +1217,69 @@ pub extern "C" fn gale_timer_status_get( } } +// ---- Decision API for timer ---- + +/// Decision struct for timer expiry — tells C shim what new status to apply. +#[repr(C)] +pub struct GaleTimerExpireDecision { + /// New status value (status + 1, or unchanged on overflow). + pub new_status: u32, + /// Whether the timer has a non-zero period (1 = periodic, 0 = one-shot). + pub is_periodic: u8, +} + +/// Decision for timer expiry handler: increment status and classify period. +/// +/// Extract→Decide→Apply: C extracts timer->status and timer->period, +/// Rust decides the new status value and whether timer is periodic, +/// C applies new_status to timer->status. +/// +/// Verified: TM5 (increment), TM8 (no overflow — saturates at u32::MAX). +#[unsafe(no_mangle)] +pub extern "C" fn gale_k_timer_expire_decide( + status: u32, + period: u32, +) -> GaleTimerExpireDecision { + let new_status = if status < u32::MAX { + #[allow(clippy::arithmetic_side_effects)] + { status + 1 } + } else { + // Saturate at u32::MAX — no overflow. + status + }; + GaleTimerExpireDecision { + new_status, + is_periodic: if period > 0 { 1 } else { 0 }, + } +} + +/// Decision struct for timer status_get — tells C shim what count to return +/// and what new status to apply (reset to 0). +#[repr(C)] +pub struct GaleTimerStatusDecision { + /// The old status value to return to the caller. + pub count: u32, + /// New status value (always 0 — reset after read). + pub new_status: u32, +} + +/// Decision for k_timer_status_get: read current status and reset to 0. +/// +/// Extract→Decide→Apply: C extracts timer->status, +/// Rust decides the return value (old status) and new status (0), +/// C applies new_status to timer->status and returns count. +/// +/// Verified: TM2 (read + reset to 0). +#[unsafe(no_mangle)] +pub extern "C" fn gale_k_timer_status_decide( + status: u32, +) -> GaleTimerStatusDecision { + GaleTimerStatusDecision { + count: status, + new_status: 0, + } +} + // --------------------------------------------------------------------------- // Memory Slab — verified block count tracking // --------------------------------------------------------------------------- @@ -1207,6 +1373,105 @@ pub extern "C" fn gale_mem_slab_free_validate( } } +// ---- Memory Slab Decision API ---- + +/// Decision struct for k_mem_slab_alloc — tells C shim what action to take. +#[repr(C)] +pub struct GaleMemSlabAllocDecision { + /// Return code: 0 (OK), -ENOMEM (slab full) + pub ret: i32, + /// New num_used value (incremented if allocated) + pub new_num_used: u32, + /// Action: 0=ALLOC_OK, 1=PEND_CURRENT, 2=RETURN_NOMEM + pub action: u8, +} + +pub const GALE_MEM_SLAB_ACTION_ALLOC_OK: u8 = 0; +pub const GALE_MEM_SLAB_ACTION_PEND_CURRENT: u8 = 1; +pub const GALE_MEM_SLAB_ACTION_RETURN_NOMEM: u8 = 2; + +/// Full decision for k_mem_slab_alloc: decides whether to allocate, pend, or return -ENOMEM. +/// +/// The C shim extracts num_used, num_blocks, and whether the caller is willing +/// to wait. Rust decides the action. +/// +/// Verified: MS4 (increment), MS5 (-ENOMEM), MS1 (bounds). +#[unsafe(no_mangle)] +pub extern "C" fn gale_k_mem_slab_alloc_decide( + num_used: u32, + num_blocks: u32, + is_no_wait: u32, +) -> GaleMemSlabAllocDecision { + if num_used < num_blocks { + #[allow(clippy::arithmetic_side_effects)] + let new_num_used = num_used + 1; + GaleMemSlabAllocDecision { + ret: OK, + new_num_used, + action: GALE_MEM_SLAB_ACTION_ALLOC_OK, + } + } else if is_no_wait != 0 { + GaleMemSlabAllocDecision { + ret: ENOMEM, + new_num_used: num_used, + action: GALE_MEM_SLAB_ACTION_RETURN_NOMEM, + } + } else { + GaleMemSlabAllocDecision { + ret: 0, + new_num_used: num_used, + action: GALE_MEM_SLAB_ACTION_PEND_CURRENT, + } + } +} + +/// Decision struct for k_mem_slab_free — tells C shim what action to take. +#[repr(C)] +pub struct GaleMemSlabFreeDecision { + /// New num_used value (decremented) + pub new_num_used: u32, + /// Action: 0=FREE_OK, 1=WAKE_THREAD + pub action: u8, +} + +pub const GALE_MEM_SLAB_ACTION_FREE_OK: u8 = 0; +pub const GALE_MEM_SLAB_ACTION_WAKE_THREAD: u8 = 1; + +/// Full decision for k_mem_slab_free: decides whether to return block to free list or wake a thread. +/// +/// The C shim checks whether there is a waiting thread (and whether the free +/// list was empty). Rust decides the action. +/// +/// Verified: MS6 (decrement), MS1 (bounds). +#[unsafe(no_mangle)] +pub extern "C" fn gale_k_mem_slab_free_decide( + num_used: u32, + has_waiter: u32, +) -> GaleMemSlabFreeDecision { + if has_waiter != 0 { + // Don't decrement — the block goes directly to the woken thread, + // so the allocation count stays the same. + GaleMemSlabFreeDecision { + new_num_used: num_used, + action: GALE_MEM_SLAB_ACTION_WAKE_THREAD, + } + } else if num_used > 0 { + #[allow(clippy::arithmetic_side_effects)] + let new_num_used = num_used - 1; + GaleMemSlabFreeDecision { + new_num_used, + action: GALE_MEM_SLAB_ACTION_FREE_OK, + } + } else { + // All blocks already free — should not happen with valid usage. + // Return unchanged count with FREE_OK action (no-op). + GaleMemSlabFreeDecision { + new_num_used: 0, + action: GALE_MEM_SLAB_ACTION_FREE_OK, + } + } +} + // --------------------------------------------------------------------------- // FFI exports — event bitmask operations // --------------------------------------------------------------------------- @@ -1399,6 +1664,99 @@ pub extern "C" fn gale_event_wait_check_all( } } +// ---- Phase 2: Full Decision API for events ---- + +/// Wait type constants for event wait decisions. +pub const GALE_EVENT_WAIT_ANY: u8 = 0; +pub const GALE_EVENT_WAIT_ALL: u8 = 1; + +/// Action constants for event wait decisions. +pub const GALE_EVENT_ACTION_MATCHED: u8 = 0; +pub const GALE_EVENT_ACTION_PEND: u8 = 1; +pub const GALE_EVENT_ACTION_TIMEOUT: u8 = 2; + +/// Decision struct for k_event_post_internal — tells C shim the new event bitmask. +/// +/// Computes: (current_events & ~mask) | (new_events & mask) +/// +/// This replaces gale_event_set_masked with a value-returning decision struct. +#[repr(C)] +pub struct GaleEventPostDecision { + /// The new event bitmask after applying the masked set. + pub new_events: u32, +} + +/// Full decision for k_event_post_internal: computes the new bitmask after +/// applying events through a mask. +/// +/// Verified: EV4 — set_masked computes (current & ~mask) | (new & mask) +#[unsafe(no_mangle)] +pub extern "C" fn gale_k_event_post_decide( + current_events: u32, + new_events: u32, + mask: u32, +) -> GaleEventPostDecision { + GaleEventPostDecision { + new_events: (current_events & !mask) | (new_events & mask), + } +} + +/// Decision struct for event wait condition check — tells C shim what to do. +#[repr(C)] +pub struct GaleEventWaitDecision { + /// Return code: 0 means success (matched), non-zero means no match + pub ret: i32, + /// The matched event bits (current & desired), or 0 if no match + pub matched_events: u32, + /// Action: 0=MATCHED, 1=PEND_CURRENT, 2=RETURN_TIMEOUT + pub action: u8, +} + +/// Full decision for event wait: determines whether the wait condition is met, +/// whether to pend the current thread, or return immediately on timeout. +/// +/// wait_type: 0=ANY (at least one desired bit set), 1=ALL (all desired bits set) +/// is_no_wait: non-zero if K_NO_WAIT timeout (should not block) +/// +/// Verified: EV5 (any-bit match), EV6 (all-bits match) +#[unsafe(no_mangle)] +pub extern "C" fn gale_k_event_wait_decide( + current_events: u32, + desired: u32, + wait_type: u8, + is_no_wait: u32, +) -> GaleEventWaitDecision { + let matched = current_events & desired; + + let condition_met = if wait_type == GALE_EVENT_WAIT_ALL { + // ALL: every desired bit must be present + (current_events & desired) == desired + } else { + // ANY: at least one desired bit present + matched != 0 + }; + + if condition_met { + GaleEventWaitDecision { + ret: 0, + matched_events: matched, + action: GALE_EVENT_ACTION_MATCHED, + } + } else if is_no_wait != 0 { + GaleEventWaitDecision { + ret: 0, + matched_events: 0, + action: GALE_EVENT_ACTION_TIMEOUT, + } + } else { + GaleEventWaitDecision { + ret: 0, + matched_events: 0, + action: GALE_EVENT_ACTION_PEND, + } + } +} + // --------------------------------------------------------------------------- // FFI exports — fifo (unbounded queue counter, FIFO ordering) // --------------------------------------------------------------------------- @@ -1474,6 +1832,86 @@ pub extern "C" fn gale_fifo_get_validate( } } +// ---- Phase 2: Full Decision API for Fifo ---- + +/// Decision struct for k_fifo put (queue_insert) — tells C shim what action to take. +#[repr(C)] +pub struct GaleFifoPutDecision { + /// Action: 0=PUT_OK (insert into list), 1=WAKE_THREAD (hand data to waiter) + pub action: u8, +} + +pub const GALE_FIFO_PUT_OK: u8 = 0; +pub const GALE_FIFO_PUT_WAKE: u8 = 1; + +/// Full decision for fifo put: decides whether to insert data or wake a waiting thread. +/// +/// The C shim calls z_unpend_first_thread first (side effect), then passes +/// whether a waiter was found. Rust decides the action. +/// +/// Fifo is unbounded, so put always succeeds (no capacity check needed). +/// +/// Verified: FI1 (no overflow), FI2 (increment via PUT_OK path). +#[unsafe(no_mangle)] +pub extern "C" fn gale_k_fifo_put_decide( + _count: u32, + has_waiter: u32, +) -> GaleFifoPutDecision { + if has_waiter != 0 { + GaleFifoPutDecision { + action: GALE_FIFO_PUT_WAKE, + } + } else { + GaleFifoPutDecision { + action: GALE_FIFO_PUT_OK, + } + } +} + +/// Decision struct for k_fifo get (k_queue_get) — tells C shim what action to take. +#[repr(C)] +pub struct GaleFifoGetDecision { + /// Return code: 0 (data available), -EBUSY (empty + no_wait) + pub ret: i32, + /// Action: 0=GET_OK (dequeue data), 1=PEND_CURRENT (block), 2=RETURN_NODATA (no_wait + empty) + pub action: u8, +} + +pub const GALE_FIFO_GET_OK: u8 = 0; +pub const GALE_FIFO_GET_PEND: u8 = 1; +pub const GALE_FIFO_GET_NODATA: u8 = 2; + +/// Full decision for fifo get: decides whether to dequeue, pend, or return empty. +/// +/// C shim checks sys_sflist_is_empty first and passes the result. +/// If data available (count > 0), return GET_OK. +/// If empty and no_wait, return RETURN_NODATA. +/// If empty and willing to wait, return PEND_CURRENT. +/// +/// Verified: FI3 (no underflow), FI4 (decrement via GET_OK path). +#[unsafe(no_mangle)] +pub extern "C" fn gale_k_fifo_get_decide( + count: u32, + is_no_wait: u32, +) -> GaleFifoGetDecision { + if count > 0 { + GaleFifoGetDecision { + ret: OK, + action: GALE_FIFO_GET_OK, + } + } else if is_no_wait != 0 { + GaleFifoGetDecision { + ret: EBUSY, + action: GALE_FIFO_GET_NODATA, + } + } else { + GaleFifoGetDecision { + ret: 0, + action: GALE_FIFO_GET_PEND, + } + } +} + // --------------------------------------------------------------------------- // FFI exports — lifo (unbounded queue counter, LIFO ordering) // --------------------------------------------------------------------------- @@ -1549,6 +1987,86 @@ pub extern "C" fn gale_lifo_get_validate( } } +// ---- Phase 2: Full Decision API for Lifo ---- + +/// Decision struct for k_lifo put (queue_insert) — tells C shim what action to take. +#[repr(C)] +pub struct GaleLifoPutDecision { + /// Action: 0=PUT_OK (insert into list), 1=WAKE_THREAD (hand data to waiter) + pub action: u8, +} + +pub const GALE_LIFO_PUT_OK: u8 = 0; +pub const GALE_LIFO_PUT_WAKE: u8 = 1; + +/// Full decision for lifo put: decides whether to insert data or wake a waiting thread. +/// +/// The C shim calls z_unpend_first_thread first (side effect), then passes +/// whether a waiter was found. Rust decides the action. +/// +/// Lifo is unbounded, so put always succeeds (no capacity check needed). +/// +/// Verified: LI1 (no overflow), LI2 (increment via PUT_OK path). +#[unsafe(no_mangle)] +pub extern "C" fn gale_k_lifo_put_decide( + _count: u32, + has_waiter: u32, +) -> GaleLifoPutDecision { + if has_waiter != 0 { + GaleLifoPutDecision { + action: GALE_LIFO_PUT_WAKE, + } + } else { + GaleLifoPutDecision { + action: GALE_LIFO_PUT_OK, + } + } +} + +/// Decision struct for k_lifo get (k_queue_get) — tells C shim what action to take. +#[repr(C)] +pub struct GaleLifoGetDecision { + /// Return code: 0 (data available), -EBUSY (empty + no_wait) + pub ret: i32, + /// Action: 0=GET_OK (dequeue data), 1=PEND_CURRENT (block), 2=RETURN_NODATA (no_wait + empty) + pub action: u8, +} + +pub const GALE_LIFO_GET_OK: u8 = 0; +pub const GALE_LIFO_GET_PEND: u8 = 1; +pub const GALE_LIFO_GET_NODATA: u8 = 2; + +/// Full decision for lifo get: decides whether to dequeue, pend, or return empty. +/// +/// C shim checks sys_sflist_is_empty first and passes the result. +/// If data available (count > 0), return GET_OK. +/// If empty and no_wait, return RETURN_NODATA. +/// If empty and willing to wait, return PEND_CURRENT. +/// +/// Verified: LI3 (no underflow), LI4 (decrement via GET_OK path). +#[unsafe(no_mangle)] +pub extern "C" fn gale_k_lifo_get_decide( + count: u32, + is_no_wait: u32, +) -> GaleLifoGetDecision { + if count > 0 { + GaleLifoGetDecision { + ret: OK, + action: GALE_LIFO_GET_OK, + } + } else if is_no_wait != 0 { + GaleLifoGetDecision { + ret: EBUSY, + action: GALE_LIFO_GET_NODATA, + } + } else { + GaleLifoGetDecision { + ret: 0, + action: GALE_LIFO_GET_PEND, + } + } +} + // --------------------------------------------------------------------------- // FFI exports — queue (unbounded queue counter) // --------------------------------------------------------------------------- @@ -3709,6 +4227,85 @@ mod kani_event_proofs { assert!(gale_event_clear(0, 0, core::ptr::null_mut()) == EINVAL); assert!(gale_event_set_masked(0, 0, 0, core::ptr::null_mut()) == EINVAL); } + + // ---- Phase 2 decision struct proofs ---- + + /// EV4-D: post_decide computes (current & ~mask) | (new & mask). + #[kani::proof] + fn event_post_decide_masked_set() { + let current: u32 = kani::any(); + let new: u32 = kani::any(); + let mask: u32 = kani::any(); + let d = gale_k_event_post_decide(current, new, mask); + assert!(d.new_events == (current & !mask) | (new & mask)); + } + + /// EV4-D: post_decide with full mask is equivalent to replacement. + #[kani::proof] + fn event_post_decide_full_mask() { + let current: u32 = kani::any(); + let new: u32 = kani::any(); + let d = gale_k_event_post_decide(current, new, !0u32); + assert!(d.new_events == new); + } + + /// EV4-D: post_decide with self-mask is equivalent to OR (post). + #[kani::proof] + fn event_post_decide_self_mask() { + let current: u32 = kani::any(); + let new: u32 = kani::any(); + let d = gale_k_event_post_decide(current, new, new); + // (current & ~new) | (new & new) = (current & ~new) | new = current | new + assert!(d.new_events == current | new); + } + + /// EV5-D: wait_decide ANY matches when at least one desired bit set. + #[kani::proof] + fn event_wait_decide_any_matched() { + let current: u32 = kani::any(); + let desired: u32 = kani::any(); + kani::assume(desired != 0); + kani::assume((current & desired) != 0); + let d = gale_k_event_wait_decide(current, desired, GALE_EVENT_WAIT_ANY, 0); + assert!(d.action == GALE_EVENT_ACTION_MATCHED); + assert!(d.matched_events == current & desired); + } + + /// EV6-D: wait_decide ALL matches only when all desired bits set. + #[kani::proof] + fn event_wait_decide_all_matched() { + let current: u32 = kani::any(); + let desired: u32 = kani::any(); + kani::assume((current & desired) == desired); + let d = gale_k_event_wait_decide(current, desired, GALE_EVENT_WAIT_ALL, 0); + assert!(d.action == GALE_EVENT_ACTION_MATCHED); + assert!(d.matched_events == desired); + } + + /// EV6-D: wait_decide ALL does not match partial bits. + #[kani::proof] + fn event_wait_decide_all_no_match() { + let current: u32 = kani::any(); + let desired: u32 = kani::any(); + kani::assume(desired != 0); + kani::assume((current & desired) != desired); + let d = gale_k_event_wait_decide(current, desired, GALE_EVENT_WAIT_ALL, 0); + assert!(d.action == GALE_EVENT_ACTION_PEND); + assert!(d.matched_events == 0); + } + + /// Wait_decide returns TIMEOUT when no-wait and no match. + #[kani::proof] + fn event_wait_decide_no_wait_timeout() { + let current: u32 = kani::any(); + let desired: u32 = kani::any(); + let wait_type: u8 = kani::any(); + kani::assume(wait_type <= 1); + kani::assume((current & desired) == 0); + let d = gale_k_event_wait_decide(current, desired, wait_type, 1); + assert!(d.action == GALE_EVENT_ACTION_TIMEOUT); + assert!(d.matched_events == 0); + } } // --------------------------------------------------------------------------- diff --git a/zephyr/gale_mem_slab.c b/zephyr/gale_mem_slab.c index 57a5aa8..da23fc0 100644 --- a/zephyr/gale_mem_slab.c +++ b/zephyr/gale_mem_slab.c @@ -4,17 +4,16 @@ * * SPDX-License-Identifier: Apache-2.0 * - * Gale memory slab — verified block count arithmetic. + * Gale memory slab — Extract/Decide/Apply pattern. * - * This is kernel/mem_slab.c with the block count tracking - * replaced by calls to the formally verified Rust implementation. - * Free-list management, wait queue, scheduling, tracing, and - * statistics remain native Zephyr. + * This is kernel/mem_slab.c with alloc/free rewritten to use Rust + * decision structs. C extracts kernel state (spinlock, wait queue + * side effects), Rust decides the action, C applies it. * * Verified operations (Verus proofs): - * gale_mem_slab_init_validate — MS2 (num_blocks > 0), MS3 (block_size > 0) - * gale_mem_slab_alloc_validate — MS1 (bounds), MS4 (increment), MS5 (-ENOMEM) - * gale_mem_slab_free_validate — MS1 (bounds), MS6 (decrement) + * gale_mem_slab_init_validate — MS2 (num_blocks > 0), MS3 (block_size > 0) + * gale_k_mem_slab_alloc_decide — MS1 (bounds), MS4 (increment), MS5 (-ENOMEM) + * gale_k_mem_slab_free_decide — MS1 (bounds), MS6 (decrement) */ #include @@ -256,43 +255,40 @@ int k_mem_slab_alloc(struct k_mem_slab *slab, void **mem, k_timeout_t timeout) SYS_PORT_TRACING_OBJ_FUNC_ENTER(k_mem_slab, alloc, slab, timeout); - if (slab->free_list != NULL) { - /* --- Gale verified alloc check --- */ - uint32_t new_num_used; - - result = gale_mem_slab_alloc_validate( - slab->info.num_used, slab->info.num_blocks, - &new_num_used); - if (result != 0) { - /* MS5: slab full (-ENOMEM) — should not happen - * when free_list is non-NULL, but the verified - * code is the authority on the count. */ - *mem = NULL; - goto out; - } - - /* take a free block */ - *mem = slab->free_list; - slab->free_list = *(char **)(slab->free_list); - /* MS4: num_used incremented by verified code */ - slab->info.num_used = new_num_used; - __ASSERT((slab->free_list == NULL && - slab->info.num_used == slab->info.num_blocks) || - slab_ptr_is_good(slab, slab->free_list), - "slab corruption detected"); + /* Extract: gather kernel state */ + uint32_t is_no_wait = (K_TIMEOUT_EQ(timeout, K_NO_WAIT) || + !IS_ENABLED(CONFIG_MULTITHREADING)) ? 1U : 0U; + + /* Decide: Rust determines action based on count and wait policy */ + struct gale_mem_slab_alloc_decision d = gale_k_mem_slab_alloc_decide( + slab->info.num_used, slab->info.num_blocks, is_no_wait); + + /* Apply: execute Rust's decision */ + if (d.action == GALE_MEM_SLAB_ACTION_ALLOC_OK) { + if (slab->free_list != NULL) { + /* take a free block */ + *mem = slab->free_list; + slab->free_list = *(char **)(slab->free_list); + /* MS4: num_used incremented by verified code */ + slab->info.num_used = d.new_num_used; + __ASSERT((slab->free_list == NULL && + slab->info.num_used == slab->info.num_blocks) || + slab_ptr_is_good(slab, slab->free_list), + "slab corruption detected"); #ifdef CONFIG_MEM_SLAB_TRACE_MAX_UTILIZATION - slab->info.max_used = max(slab->info.num_used, - slab->info.max_used); + slab->info.max_used = max(slab->info.num_used, + slab->info.max_used); #endif /* CONFIG_MEM_SLAB_TRACE_MAX_UTILIZATION */ - result = 0; - } else if (K_TIMEOUT_EQ(timeout, K_NO_WAIT) || - !IS_ENABLED(CONFIG_MULTITHREADING)) { - /* don't wait for a free block to become available */ - *mem = NULL; - result = -ENOMEM; - } else { + result = 0; + } else { + /* Rust said OK but free list is empty — shouldn't happen, + * but free list is the authority on actual availability. */ + *mem = NULL; + result = -ENOMEM; + } + } else if (d.action == GALE_MEM_SLAB_ACTION_PEND_CURRENT) { SYS_PORT_TRACING_OBJ_FUNC_BLOCKING(k_mem_slab, alloc, slab, timeout); /* wait for a free block or timeout */ @@ -304,9 +300,12 @@ int k_mem_slab_alloc(struct k_mem_slab *slab, void **mem, k_timeout_t timeout) SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_mem_slab, alloc, slab, timeout, result); return result; + } else { + /* RETURN_NOMEM */ + *mem = NULL; + result = -ENOMEM; } -out: SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_mem_slab, alloc, slab, timeout, result); k_spin_unlock(&slab->lock, key); @@ -325,31 +324,34 @@ void k_mem_slab_free(struct k_mem_slab *slab, void *mem) k_spinlock_key_t key = k_spin_lock(&slab->lock); SYS_PORT_TRACING_OBJ_FUNC_ENTER(k_mem_slab, free, slab); - if (unlikely(slab->free_list == NULL) && IS_ENABLED(CONFIG_MULTITHREADING)) { - struct k_thread *pending_thread = z_unpend_first_thread(&slab->wait_q); - if (unlikely(pending_thread != NULL)) { - SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_mem_slab, free, slab); + /* Extract: try to unpend first waiter (side effect: removes from queue) */ + struct k_thread *pending_thread = NULL; - z_thread_return_value_set_with_data(pending_thread, 0, mem); - z_ready_thread(pending_thread); - z_reschedule(&slab->lock, key); - return; - } + if (IS_ENABLED(CONFIG_MULTITHREADING)) { + pending_thread = z_unpend_first_thread(&slab->wait_q); + } + + /* Decide: Rust determines action based on whether a waiter was found */ + struct gale_mem_slab_free_decision d = gale_k_mem_slab_free_decide( + slab->info.num_used, pending_thread != NULL ? 1U : 0U); + + /* Apply: execute Rust's decision */ + if (d.action == GALE_MEM_SLAB_ACTION_WAKE_THREAD) { + SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_mem_slab, free, slab); + + z_thread_return_value_set_with_data(pending_thread, 0, mem); + z_ready_thread(pending_thread); + z_reschedule(&slab->lock, key); + return; } - /* --- Gale verified free check --- */ - uint32_t new_num_used; - int32_t rc = gale_mem_slab_free_validate(slab->info.num_used, - &new_num_used); - if (rc == 0) { - /* MS6: num_used decremented by verified code */ + /* FREE_OK: return block to free list */ + if (slab->info.num_used > 0) { *(char **) mem = slab->free_list; slab->free_list = (char *) mem; - slab->info.num_used = new_num_used; + slab->info.num_used = d.new_num_used; } - /* If rc != 0: all blocks free, should not happen with valid usage. - * The verified code prevents underflow. */ SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_mem_slab, free, slab); From e35df30c7f035d48bf325ea39d5588310ea696f2 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 20 Mar 2026 06:01:52 +0100 Subject: [PATCH 02/16] feat(shim): convert k_stack push/pop to decision struct pattern MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replace direct gale_stack_push_validate/pop_validate calls with the Extract→Decide→Apply pattern using GaleStackPushDecision and GaleStackPopDecision structs. Push: C peeks at wait queue head (no side effect), passes count/capacity/ has_waiter to Rust. Rust returns STORE_DATA, WAKE_WAITER, or FULL. C applies: unpend+wake, store+advance, or reject with -ENOMEM. Pop: C passes count and is_no_wait to Rust. Rust returns POP_OK (with ret=0 for data or ret=-EBUSY for empty+no_wait) or PEND_CURRENT. Co-Authored-By: Claude Opus 4.6 (1M context) --- ffi/include/gale_stack.h | 27 +++++++++++++ zephyr/gale_stack.c | 85 ++++++++++++++++++---------------------- 2 files changed, 65 insertions(+), 47 deletions(-) diff --git a/ffi/include/gale_stack.h b/ffi/include/gale_stack.h index 8d466cc..f5df308 100644 --- a/ffi/include/gale_stack.h +++ b/ffi/include/gale_stack.h @@ -58,6 +58,33 @@ int32_t gale_stack_push_validate(uint32_t count, int32_t gale_stack_pop_validate(uint32_t count, uint32_t *new_count); +/* ---- Phase 2: Full Decision API ---- */ + +struct gale_stack_push_decision { + int32_t ret; + uint32_t new_count; + uint8_t action; /* 0=STORE_DATA, 1=WAKE_WAITER, 2=FULL */ +}; + +#define GALE_STACK_PUSH_STORE 0 +#define GALE_STACK_PUSH_WAKE 1 +#define GALE_STACK_PUSH_FULL 2 + +struct gale_stack_push_decision gale_k_stack_push_decide( + uint32_t count, uint32_t capacity, uint32_t has_waiter); + +struct gale_stack_pop_decision { + int32_t ret; + uint32_t new_count; + uint8_t action; /* 0=POP_OK, 1=PEND_CURRENT */ +}; + +#define GALE_STACK_POP_OK 0 +#define GALE_STACK_POP_PEND 1 + +struct gale_stack_pop_decision gale_k_stack_pop_decide( + uint32_t count, uint32_t is_no_wait); + #ifdef __cplusplus } #endif diff --git a/zephyr/gale_stack.c b/zephyr/gale_stack.c index 05e3947..426d7b9 100644 --- a/zephyr/gale_stack.c +++ b/zephyr/gale_stack.c @@ -6,13 +6,13 @@ * * Gale stack — verified LIFO count/capacity arithmetic. * - * This is kernel/stack.c with the capacity check and count tracking - * replaced by calls to the formally verified Rust implementation. - * Wait queue, scheduling, tracing, and data storage remain native Zephyr. + * This is kernel/stack.c with push/pop rewritten to use Rust decision + * structs. C extracts kernel state (spinlock, wait queue peek), + * Rust decides the action, C applies it. * * Verified operations (Verus proofs): - * gale_stack_push_validate — SK1 (bounds), SK3 (increment), SK4 (-ENOMEM) - * gale_stack_pop_validate — SK1 (bounds), SK5 (decrement), SK6 (-EBUSY) + * gale_k_stack_push_decide — SK1 (bounds), SK3 (increment), SK4 (-ENOMEM) + * gale_k_stack_pop_decide — SK1 (bounds), SK5 (decrement), SK6 (-EBUSY) * gale_stack_init_validate — SK2 (capacity > 0) */ @@ -110,46 +110,40 @@ int k_stack_cleanup(struct k_stack *stack) int z_impl_k_stack_push(struct k_stack *stack, stack_data_t data) { - struct k_thread *first_pending_thread; - int ret = 0; k_spinlock_key_t key = k_spin_lock(&stack->lock); SYS_PORT_TRACING_OBJ_FUNC_ENTER(k_stack, push, stack); - /* --- Gale verified capacity check --- */ + /* Extract: read state, peek at wait queue head (no side effect) */ uint32_t count = (uint32_t)(stack->next - stack->base); uint32_t capacity = (uint32_t)(stack->top - stack->base); - uint32_t new_count; + uint32_t has_waiter = (z_waitq_head(&stack->wait_q) != NULL) ? 1U : 0U; - ret = gale_stack_push_validate(count, capacity, &new_count); - if (ret != 0) { - /* SK4: stack full (-ENOMEM) */ - goto out; - } - - first_pending_thread = z_unpend_first_thread(&stack->wait_q); + /* Decide: Rust determines action based on count, capacity, waiter */ + struct gale_stack_push_decision d = gale_k_stack_push_decide( + count, capacity, has_waiter); - if (unlikely(first_pending_thread != NULL)) { - z_thread_return_value_set_with_data(first_pending_thread, - 0, (void *)data); + /* Apply: execute Rust's decision */ + if (d.action == GALE_STACK_PUSH_WAKE) { + struct k_thread *thread = z_unpend_first_thread(&stack->wait_q); - z_ready_thread(first_pending_thread); + z_thread_return_value_set_with_data(thread, + 0, (void *)data); + z_ready_thread(thread); z_reschedule(&stack->lock, key); - goto end; - } else { + } else if (d.action == GALE_STACK_PUSH_STORE) { /* SK3: count incremented — store data and advance pointer */ *(stack->next) = data; stack->next++; - goto out; + k_spin_unlock(&stack->lock, key); + } else { + /* FULL: -ENOMEM */ + k_spin_unlock(&stack->lock, key); } -out: - k_spin_unlock(&stack->lock, key); - -end: - SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_stack, push, stack, ret); + SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_stack, push, stack, d.ret); - return ret; + return d.ret; } #ifdef CONFIG_USERSPACE @@ -172,33 +166,30 @@ int z_impl_k_stack_pop(struct k_stack *stack, stack_data_t *data, SYS_PORT_TRACING_OBJ_FUNC_ENTER(k_stack, pop, stack, timeout); - /* --- Gale verified empty check --- */ + /* Extract: read count and timeout mode */ uint32_t count = (uint32_t)(stack->next - stack->base); - uint32_t new_count; - result = gale_stack_pop_validate(count, &new_count); - if (result == 0) { - /* SK5: count decremented — read data and retreat pointer */ - stack->next--; - *data = *(stack->next); + /* Decide: Rust determines pop/pend/busy */ + struct gale_stack_pop_decision d = gale_k_stack_pop_decide( + count, K_TIMEOUT_EQ(timeout, K_NO_WAIT) ? 1U : 0U); + + /* Apply: execute Rust's decision */ + if (d.action == GALE_STACK_POP_OK) { + if (d.ret == 0) { + /* SK5: count decremented — read data and retreat pointer */ + stack->next--; + *data = *(stack->next); + } k_spin_unlock(&stack->lock, key); SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_stack, pop, stack, - timeout, 0); - return 0; + timeout, d.ret); + return d.ret; } - /* Stack empty — check timeout */ + /* PEND_CURRENT: block on wait queue with timeout */ SYS_PORT_TRACING_OBJ_FUNC_BLOCKING(k_stack, pop, stack, timeout); - if (K_TIMEOUT_EQ(timeout, K_NO_WAIT)) { - k_spin_unlock(&stack->lock, key); - - SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_stack, pop, stack, - timeout, -EBUSY); - return -EBUSY; - } - result = z_pend_curr(&stack->lock, key, &stack->wait_q, timeout); if (result == -EAGAIN) { SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_stack, pop, stack, From 9e94f65d02f09798ddbd02df305cb205a3545cc4 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 20 Mar 2026 06:02:33 +0100 Subject: [PATCH 03/16] feat(shim): convert k_fifo/k_lifo put/get to decision struct pattern Add GaleFifoPutDecision, GaleFifoGetDecision, GaleLifoPutDecision, and GaleLifoGetDecision structs following the proven Extract-Decide-Apply pattern from semaphore. Rust decides whether to wake a waiter or insert data (put) and whether to dequeue, pend, or return empty (get). Co-Authored-By: Claude Opus 4.6 (1M context) --- ffi/include/gale_fifo.h | 43 ++++++++++++ ffi/include/gale_lifo.h | 43 ++++++++++++ ffi/src/lib.rs | 150 ++++++++++++++++++++++++++++++++++++++++ zephyr/gale_fifo.c | 64 ++++++++++++----- zephyr/gale_lifo.c | 64 ++++++++++++----- 5 files changed, 330 insertions(+), 34 deletions(-) diff --git a/ffi/include/gale_fifo.h b/ffi/include/gale_fifo.h index 4c90435..9cb8f27 100644 --- a/ffi/include/gale_fifo.h +++ b/ffi/include/gale_fifo.h @@ -43,6 +43,49 @@ int32_t gale_fifo_put_validate(uint32_t count, int32_t gale_fifo_get_validate(uint32_t count, uint32_t *new_count); +/* ---- Phase 2: Full Decision API ---- */ + +struct gale_fifo_put_decision { + uint8_t action; /* 0=PUT_OK, 1=WAKE_THREAD */ +}; + +#define GALE_FIFO_PUT_OK 0 +#define GALE_FIFO_PUT_WAKE 1 + +/** + * Decide action for fifo put (queue_insert). + * + * C shim calls z_unpend_first_thread first, then passes whether + * a waiter was found. Rust decides the action. + * + * @param count Current element count (unused — fifo is unbounded). + * @param has_waiter 1 if a thread was unpended, 0 otherwise. + * + * @return Decision struct with action field. + */ +struct gale_fifo_put_decision gale_k_fifo_put_decide( + uint32_t count, uint32_t has_waiter); + +struct gale_fifo_get_decision { + int32_t ret; /* 0 (OK), -EBUSY (empty + no_wait) */ + uint8_t action; /* 0=GET_OK, 1=PEND_CURRENT, 2=RETURN_NODATA */ +}; + +#define GALE_FIFO_GET_OK 0 +#define GALE_FIFO_GET_PEND 1 +#define GALE_FIFO_GET_NODATA 2 + +/** + * Decide action for fifo get (k_queue_get). + * + * @param count Current element count. + * @param is_no_wait 1 if K_NO_WAIT, 0 otherwise. + * + * @return Decision struct with ret and action fields. + */ +struct gale_fifo_get_decision gale_k_fifo_get_decide( + uint32_t count, uint32_t is_no_wait); + #ifdef __cplusplus } #endif diff --git a/ffi/include/gale_lifo.h b/ffi/include/gale_lifo.h index 8b078fe..f2bb981 100644 --- a/ffi/include/gale_lifo.h +++ b/ffi/include/gale_lifo.h @@ -43,6 +43,49 @@ int32_t gale_lifo_put_validate(uint32_t count, int32_t gale_lifo_get_validate(uint32_t count, uint32_t *new_count); +/* ---- Phase 2: Full Decision API ---- */ + +struct gale_lifo_put_decision { + uint8_t action; /* 0=PUT_OK, 1=WAKE_THREAD */ +}; + +#define GALE_LIFO_PUT_OK 0 +#define GALE_LIFO_PUT_WAKE 1 + +/** + * Decide action for lifo put (queue_insert). + * + * C shim calls z_unpend_first_thread first, then passes whether + * a waiter was found. Rust decides the action. + * + * @param count Current element count (unused — lifo is unbounded). + * @param has_waiter 1 if a thread was unpended, 0 otherwise. + * + * @return Decision struct with action field. + */ +struct gale_lifo_put_decision gale_k_lifo_put_decide( + uint32_t count, uint32_t has_waiter); + +struct gale_lifo_get_decision { + int32_t ret; /* 0 (OK), -EBUSY (empty + no_wait) */ + uint8_t action; /* 0=GET_OK, 1=PEND_CURRENT, 2=RETURN_NODATA */ +}; + +#define GALE_LIFO_GET_OK 0 +#define GALE_LIFO_GET_PEND 1 +#define GALE_LIFO_GET_NODATA 2 + +/** + * Decide action for lifo get (k_queue_get). + * + * @param count Current element count. + * @param is_no_wait 1 if K_NO_WAIT, 0 otherwise. + * + * @return Decision struct with ret and action fields. + */ +struct gale_lifo_get_decision gale_k_lifo_get_decide( + uint32_t count, uint32_t is_no_wait); + #ifdef __cplusplus } #endif diff --git a/ffi/src/lib.rs b/ffi/src/lib.rs index 74cd35a..cc281f7 100644 --- a/ffi/src/lib.rs +++ b/ffi/src/lib.rs @@ -2244,6 +2244,156 @@ pub extern "C" fn gale_mbox_data_exchange(tx_size: u32, rx_buf_size: u32) -> u32 } } +// ---- Phase 2: Queue Decision API ---- + +/// Decision struct for queue insert (append/prepend) — tells C shim what action to take. +#[repr(C)] +pub struct GaleQueueInsertDecision { + /// Action: 0=INSERT_INTO_LIST, 1=WAKE_THREAD + pub action: u8, +} + +pub const GALE_QUEUE_ACTION_INSERT: u8 = 0; +pub const GALE_QUEUE_ACTION_WAKE: u8 = 1; + +/// Full decision for queue insert: decides whether to wake a pending thread +/// or insert data into the linked list. +/// +/// The C shim calls z_unpend_first_thread first (side effect), then passes +/// whether a waiter was found. Rust decides the action. +/// +/// Verified: QU1/QU2 (append), QU3/QU4 (prepend) — state transition only. +#[unsafe(no_mangle)] +pub extern "C" fn gale_k_queue_insert_decide( + has_waiter: u32, +) -> GaleQueueInsertDecision { + if has_waiter != 0 { + GaleQueueInsertDecision { + action: GALE_QUEUE_ACTION_WAKE, + } + } else { + GaleQueueInsertDecision { + action: GALE_QUEUE_ACTION_INSERT, + } + } +} + +/// Decision struct for k_queue_get — tells C shim what action to take. +#[repr(C)] +pub struct GaleQueueGetDecision { + /// Action: 0=DEQUEUE, 1=RETURN_NULL, 2=PEND_CURRENT + pub action: u8, +} + +pub const GALE_QUEUE_ACTION_DEQUEUE: u8 = 0; +pub const GALE_QUEUE_ACTION_RETURN_NULL: u8 = 1; +pub const GALE_QUEUE_ACTION_PEND: u8 = 2; + +/// Full decision for k_queue_get: decides whether to dequeue data, +/// return NULL immediately, or pend the current thread. +/// +/// The C shim checks if the list has data and whether timeout is K_NO_WAIT. +/// Rust decides the action. +/// +/// Verified: QU5/QU6 — state transition only. +#[unsafe(no_mangle)] +pub extern "C" fn gale_k_queue_get_decide( + has_data: u32, + is_no_wait: u32, +) -> GaleQueueGetDecision { + if has_data != 0 { + GaleQueueGetDecision { + action: GALE_QUEUE_ACTION_DEQUEUE, + } + } else if is_no_wait != 0 { + GaleQueueGetDecision { + action: GALE_QUEUE_ACTION_RETURN_NULL, + } + } else { + GaleQueueGetDecision { + action: GALE_QUEUE_ACTION_PEND, + } + } +} + +// ---- Phase 2: Mbox Decision API ---- + +/// Decision struct for mbox_message_put — tells C shim what action to take. +#[repr(C)] +pub struct GaleMboxPutDecision { + /// Action: 0=MATCHED (wake receiver), 1=RETURN_ENOMSG, 2=PEND_TX_QUEUE + pub action: u8, +} + +pub const GALE_MBOX_ACTION_MATCHED: u8 = 0; +pub const GALE_MBOX_ACTION_RETURN_ENOMSG: u8 = 1; +pub const GALE_MBOX_ACTION_PEND_TX: u8 = 2; + +/// Full decision for mbox_message_put: decides post-scan action. +/// +/// The C shim scans the rx queue for a compatible receiver (side effect), +/// then passes whether a match was found and the timeout mode. +/// Rust decides the action. +/// +/// Verified: MB2-MB4 (match check delegated), state transition decision. +#[unsafe(no_mangle)] +pub extern "C" fn gale_k_mbox_put_decide( + matched: u32, + is_no_wait: u32, +) -> GaleMboxPutDecision { + if matched != 0 { + GaleMboxPutDecision { + action: GALE_MBOX_ACTION_MATCHED, + } + } else if is_no_wait != 0 { + GaleMboxPutDecision { + action: GALE_MBOX_ACTION_RETURN_ENOMSG, + } + } else { + GaleMboxPutDecision { + action: GALE_MBOX_ACTION_PEND_TX, + } + } +} + +/// Decision struct for k_mbox_get — tells C shim what action to take. +#[repr(C)] +pub struct GaleMboxGetDecision { + /// Action: 0=MATCHED (consume data), 1=RETURN_ENOMSG, 2=PEND_RX_QUEUE + pub action: u8, +} + +pub const GALE_MBOX_ACTION_CONSUME: u8 = 0; +// GALE_MBOX_ACTION_RETURN_ENOMSG = 1 (shared with put) +pub const GALE_MBOX_ACTION_PEND_RX: u8 = 2; + +/// Full decision for k_mbox_get: decides post-scan action. +/// +/// The C shim scans the tx queue for a compatible sender (side effect), +/// then passes whether a match was found and the timeout mode. +/// Rust decides the action. +/// +/// Verified: MB2-MB4 (match check delegated), state transition decision. +#[unsafe(no_mangle)] +pub extern "C" fn gale_k_mbox_get_decide( + matched: u32, + is_no_wait: u32, +) -> GaleMboxGetDecision { + if matched != 0 { + GaleMboxGetDecision { + action: GALE_MBOX_ACTION_CONSUME, + } + } else if is_no_wait != 0 { + GaleMboxGetDecision { + action: GALE_MBOX_ACTION_RETURN_ENOMSG, + } + } else { + GaleMboxGetDecision { + action: GALE_MBOX_ACTION_PEND_RX, + } + } +} + // --------------------------------------------------------------------------- // FFI exports — timeout (tick arithmetic + deadline tracking) // --------------------------------------------------------------------------- diff --git a/zephyr/gale_fifo.c b/zephyr/gale_fifo.c index b7cdfe2..6e306b8 100644 --- a/zephyr/gale_fifo.c +++ b/zephyr/gale_fifo.c @@ -4,20 +4,55 @@ * * SPDX-License-Identifier: Apache-2.0 * - * Gale fifo — verified unbounded queue count arithmetic. + * Gale fifo — phase 2: Extract→Decide→Apply pattern. * - * This is the k_fifo portion of kernel/queue.c with count tracking - * replaced by calls to the formally verified Rust implementation. - * k_fifo is a FIFO ordering wrapper around k_queue — this shim - * validates put/get count transitions using gale_fifo_put_validate - * and gale_fifo_get_validate. + * This is the k_fifo portion of kernel/queue.c with put/get rewritten + * to use Rust decision structs. C extracts kernel state (spinlock, + * wait queue side effects), Rust decides the action, C applies it. * - * Wait queue, scheduling, linked list management, alloc nodes, - * polling, and tracing remain native Zephyr. + * k_fifo is a FIFO ordering wrapper around k_queue — the queue_insert + * and k_queue_get functions in gale_queue.c call the fifo decision + * functions when operating in FIFO mode. * * Verified operations (Verus proofs): - * gale_fifo_put_validate — FI1 (no overflow), FI2 (increment) - * gale_fifo_get_validate — FI3 (no underflow), FI4 (decrement) + * gale_k_fifo_put_decide — FI1 (no overflow), FI2 (increment) + * gale_k_fifo_get_decide — FI3 (no underflow), FI4 (decrement) + * + * Extract→Decide→Apply flow for fifo put (queue_insert, FIFO mode): + * + * // Extract: try to unpend first waiter + * struct k_thread *thread = z_unpend_first_thread(&queue->wait_q); + * + * // Decide: Rust determines action + * struct gale_fifo_put_decision d = gale_k_fifo_put_decide( + * count, thread != NULL ? 1U : 0U); + * + * // Apply: execute Rust's decision + * if (d.action == GALE_FIFO_PUT_WAKE) { + * prepare_thread_to_run(thread, data); + * } else { + * sys_sflist_insert(&queue->data_q, prev, data); + * } + * + * Extract→Decide→Apply flow for fifo get (k_queue_get, FIFO mode): + * + * // Extract: check if data available + * bool has_data = !sys_sflist_is_empty(&queue->data_q); + * + * // Decide: Rust determines action + * struct gale_fifo_get_decision d = gale_k_fifo_get_decide( + * has_data ? 1U : 0U, + * K_TIMEOUT_EQ(timeout, K_NO_WAIT) ? 1U : 0U); + * + * // Apply: execute Rust's decision + * if (d.action == GALE_FIFO_GET_OK) { + * node = sys_sflist_get_not_empty(&queue->data_q); + * data = z_queue_node_peek(node, true); + * } else if (d.action == GALE_FIFO_GET_PEND) { + * ret = z_pend_curr(&queue->lock, key, &queue->wait_q, timeout); + * } else { + * data = NULL; // RETURN_NODATA + * } */ #include @@ -35,17 +70,12 @@ /* * NOTE: k_fifo is a macro wrapper around k_queue. The fifo-specific - * Gale validation functions (gale_fifo_put_validate / gale_fifo_get_validate) + * Gale decision functions (gale_k_fifo_put_decide / gale_k_fifo_get_decide) * are called from the queue shim (gale_queue.c) when the queue is used * in FIFO mode. This file exists to provide the fifo-specific FFI - * entry points and can be extended with fifo-specific validation logic. + * entry points and ensure the gale_fifo FFI symbols are linked. * * The actual queue.c replacement that calls these functions is in * gale_queue.c. This file is compiled separately to ensure the * gale_fifo FFI symbols are linked. */ - -/* - * Fifo-specific helper: validate a put (append) and return the new count. - * This is a thin wrapper that the queue shim calls for FIFO puts. - */ diff --git a/zephyr/gale_lifo.c b/zephyr/gale_lifo.c index f7392e2..24c3d92 100644 --- a/zephyr/gale_lifo.c +++ b/zephyr/gale_lifo.c @@ -4,20 +4,55 @@ * * SPDX-License-Identifier: Apache-2.0 * - * Gale lifo — verified unbounded queue count arithmetic. + * Gale lifo — phase 2: Extract→Decide→Apply pattern. * - * This is the k_lifo portion of kernel/queue.c with count tracking - * replaced by calls to the formally verified Rust implementation. - * k_lifo is a LIFO ordering wrapper around k_queue — this shim - * validates put/get count transitions using gale_lifo_put_validate - * and gale_lifo_get_validate. + * This is the k_lifo portion of kernel/queue.c with put/get rewritten + * to use Rust decision structs. C extracts kernel state (spinlock, + * wait queue side effects), Rust decides the action, C applies it. * - * Wait queue, scheduling, linked list management, alloc nodes, - * polling, and tracing remain native Zephyr. + * k_lifo is a LIFO ordering wrapper around k_queue — the queue_insert + * and k_queue_get functions in gale_queue.c call the lifo decision + * functions when operating in LIFO mode. * * Verified operations (Verus proofs): - * gale_lifo_put_validate — LI1 (no overflow), LI2 (increment) - * gale_lifo_get_validate — LI3 (no underflow), LI4 (decrement) + * gale_k_lifo_put_decide — LI1 (no overflow), LI2 (increment) + * gale_k_lifo_get_decide — LI3 (no underflow), LI4 (decrement) + * + * Extract→Decide→Apply flow for lifo put (queue_insert, LIFO mode): + * + * // Extract: try to unpend first waiter + * struct k_thread *thread = z_unpend_first_thread(&queue->wait_q); + * + * // Decide: Rust determines action + * struct gale_lifo_put_decision d = gale_k_lifo_put_decide( + * count, thread != NULL ? 1U : 0U); + * + * // Apply: execute Rust's decision + * if (d.action == GALE_LIFO_PUT_WAKE) { + * prepare_thread_to_run(thread, data); + * } else { + * sys_sflist_insert(&queue->data_q, NULL, data); // prepend + * } + * + * Extract→Decide→Apply flow for lifo get (k_queue_get, LIFO mode): + * + * // Extract: check if data available + * bool has_data = !sys_sflist_is_empty(&queue->data_q); + * + * // Decide: Rust determines action + * struct gale_lifo_get_decision d = gale_k_lifo_get_decide( + * has_data ? 1U : 0U, + * K_TIMEOUT_EQ(timeout, K_NO_WAIT) ? 1U : 0U); + * + * // Apply: execute Rust's decision + * if (d.action == GALE_LIFO_GET_OK) { + * node = sys_sflist_get_not_empty(&queue->data_q); + * data = z_queue_node_peek(node, true); + * } else if (d.action == GALE_LIFO_GET_PEND) { + * ret = z_pend_curr(&queue->lock, key, &queue->wait_q, timeout); + * } else { + * data = NULL; // RETURN_NODATA + * } */ #include @@ -35,17 +70,12 @@ /* * NOTE: k_lifo is a macro wrapper around k_queue. The lifo-specific - * Gale validation functions (gale_lifo_put_validate / gale_lifo_get_validate) + * Gale decision functions (gale_k_lifo_put_decide / gale_k_lifo_get_decide) * are called from the queue shim (gale_queue.c) when the queue is used * in LIFO mode. This file exists to provide the lifo-specific FFI - * entry points and can be extended with lifo-specific validation logic. + * entry points and ensure the gale_lifo FFI symbols are linked. * * The actual queue.c replacement that calls these functions is in * gale_queue.c. This file is compiled separately to ensure the * gale_lifo FFI symbols are linked. */ - -/* - * Lifo-specific helper: validate a put (prepend) and return the new count. - * This is a thin wrapper that the queue shim calls for LIFO puts. - */ From 7f713eb04c874bedaa4c961c2abb265769d337da Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 20 Mar 2026 06:04:54 +0100 Subject: [PATCH 04/16] feat(shim): convert k_timer expire/status to decision struct pattern Replace pointer-based gale_timer_expire/gale_timer_status_get with Extract-Decide-Apply decision structs (GaleTimerExpireDecision, GaleTimerStatusDecision). C extracts timer->status and timer->period, Rust returns a decision struct with the new status value, C applies it. Co-Authored-By: Claude Opus 4.6 (1M context) --- ffi/include/gale_timer.h | 18 ++++ ffi/src/lib.rs | 203 +++++++++++++++++++++++++++++++++++++++ zephyr/gale_timer.c | 60 +++++++----- 3 files changed, 258 insertions(+), 23 deletions(-) diff --git a/ffi/include/gale_timer.h b/ffi/include/gale_timer.h index c4b6b7c..0eb5607 100644 --- a/ffi/include/gale_timer.h +++ b/ffi/include/gale_timer.h @@ -56,6 +56,24 @@ int32_t gale_timer_expire(uint32_t status, uint32_t gale_timer_status_get(uint32_t status, uint32_t *new_status); +/* ---- Decision API for timer ---- */ + +struct gale_timer_expire_decision { + uint32_t new_status; /* status + 1 (saturates at UINT32_MAX) */ + uint8_t is_periodic; /* 1 = periodic (period > 0), 0 = one-shot */ +}; + +struct gale_timer_expire_decision gale_k_timer_expire_decide( + uint32_t status, uint32_t period); + +struct gale_timer_status_decision { + uint32_t count; /* old status value to return */ + uint32_t new_status; /* always 0 (reset) */ +}; + +struct gale_timer_status_decision gale_k_timer_status_decide( + uint32_t status); + #ifdef __cplusplus } #endif diff --git a/ffi/src/lib.rs b/ffi/src/lib.rs index cc281f7..4f0b028 100644 --- a/ffi/src/lib.rs +++ b/ffi/src/lib.rs @@ -943,6 +943,162 @@ pub extern "C" fn gale_pipe_read_check( } } +// ---- Phase 2: Pipe Decision API ---- + +/// Decision struct for k_pipe_write -- tells C shim what action to take. +#[repr(C)] +pub struct GalePipeWriteDecision { + /// Return code (error code when action=RETURN_ERROR) + pub ret: i32, + /// Action: 0=WRITE_OK, 1=WAKE_READER, 2=PEND_CURRENT, 3=RETURN_ERROR + pub action: u8, + /// Bytes that can be written to ring buffer + pub actual_bytes: u32, + /// Updated used count after write + pub new_used: u32, +} + +pub const GALE_PIPE_ACTION_WRITE_OK: u8 = 0; +pub const GALE_PIPE_ACTION_WAKE_READER: u8 = 1; +pub const GALE_PIPE_ACTION_WRITE_PEND: u8 = 2; +pub const GALE_PIPE_ACTION_WRITE_ERROR: u8 = 3; + +/// Full decision for k_pipe_write: decides what the C shim should do. +/// +/// Verified: PP3-PP5, PP9-PP10 +#[unsafe(no_mangle)] +pub extern "C" fn gale_k_pipe_write_decide( + used: u32, + size: u32, + flags: u8, + request_len: u32, + has_reader: u32, +) -> GalePipeWriteDecision { + if (flags & PIPE_FLAG_RESET) != 0 { + return GalePipeWriteDecision { + ret: ECANCELED, + action: GALE_PIPE_ACTION_WRITE_ERROR, + actual_bytes: 0, + new_used: used, + }; + } + if (flags & PIPE_FLAG_OPEN) == 0 { + return GalePipeWriteDecision { + ret: EPIPE, + action: GALE_PIPE_ACTION_WRITE_ERROR, + actual_bytes: 0, + new_used: used, + }; + } + if used == 0 && has_reader != 0 { + let actual = if size > 0 && request_len > 0 { + if request_len <= size { request_len } else { size } + } else { + 0 + }; + return GalePipeWriteDecision { + ret: OK, + action: GALE_PIPE_ACTION_WAKE_READER, + actual_bytes: actual, + new_used: 0, + }; + } + if size == 0 || used >= size { + return GalePipeWriteDecision { + ret: OK, + action: GALE_PIPE_ACTION_WRITE_PEND, + actual_bytes: 0, + new_used: used, + }; + } + #[allow(clippy::arithmetic_side_effects)] + let free = size - used; + let n = if request_len <= free { request_len } else { free }; + #[allow(clippy::arithmetic_side_effects)] + let nu = used + n; + GalePipeWriteDecision { + ret: OK, + action: GALE_PIPE_ACTION_WRITE_OK, + actual_bytes: n, + new_used: nu, + } +} + +/// Decision struct for k_pipe_read -- tells C shim what action to take. +#[repr(C)] +pub struct GalePipeReadDecision { + /// Return code (error code when action=RETURN_ERROR) + pub ret: i32, + /// Action: 0=READ_OK, 1=WAKE_WRITER, 2=PEND_CURRENT, 3=RETURN_ERROR + pub action: u8, + /// Bytes that can be read from ring buffer + pub actual_bytes: u32, + /// Updated used count after read + pub new_used: u32, +} + +pub const GALE_PIPE_ACTION_READ_OK: u8 = 0; +pub const GALE_PIPE_ACTION_WAKE_WRITER: u8 = 1; +pub const GALE_PIPE_ACTION_READ_PEND: u8 = 2; +pub const GALE_PIPE_ACTION_READ_ERROR: u8 = 3; + +/// Full decision for k_pipe_read: decides what the C shim should do. +/// +/// Verified: PP3-PP6, PP9-PP10 +#[unsafe(no_mangle)] +pub extern "C" fn gale_k_pipe_read_decide( + used: u32, + size: u32, + flags: u8, + request_len: u32, + has_writer: u32, +) -> GalePipeReadDecision { + if (flags & PIPE_FLAG_RESET) != 0 { + return GalePipeReadDecision { + ret: ECANCELED, + action: GALE_PIPE_ACTION_READ_ERROR, + actual_bytes: 0, + new_used: used, + }; + } + if size > 0 && used >= size && has_writer != 0 { + let n = if request_len <= used { request_len } else { used }; + #[allow(clippy::arithmetic_side_effects)] + let nu = used - n; + return GalePipeReadDecision { + ret: OK, + action: GALE_PIPE_ACTION_WAKE_WRITER, + actual_bytes: n, + new_used: nu, + }; + } + if used > 0 { + let n = if request_len <= used { request_len } else { used }; + #[allow(clippy::arithmetic_side_effects)] + let nu = used - n; + return GalePipeReadDecision { + ret: OK, + action: GALE_PIPE_ACTION_READ_OK, + actual_bytes: n, + new_used: nu, + }; + } + if (flags & PIPE_FLAG_OPEN) == 0 { + return GalePipeReadDecision { + ret: EPIPE, + action: GALE_PIPE_ACTION_READ_ERROR, + actual_bytes: 0, + new_used: 0, + }; + } + GalePipeReadDecision { + ret: OK, + action: GALE_PIPE_ACTION_READ_PEND, + actual_bytes: 0, + new_used: 0, + } +} + /// Validate stack init parameters. /// /// stack.c:27-42: @@ -4177,6 +4333,53 @@ mod kani_timer_proofs { fn timer_null_pointers() { assert!(gale_timer_expire(0, core::ptr::null_mut()) == EINVAL); } + + /// TM5/TM8: expire_decide increments status (saturating at u32::MAX). + #[kani::proof] + fn timer_expire_decide_validates() { + let status: u32 = kani::any(); + let period: u32 = kani::any(); + + let d = gale_k_timer_expire_decide(status, period); + + if status < u32::MAX { + assert!(d.new_status == status + 1); + } else { + assert!(d.new_status == u32::MAX); + } + + if period > 0 { + assert!(d.is_periodic == 1); + } else { + assert!(d.is_periodic == 0); + } + } + + /// TM2: status_decide returns old status and resets to 0. + #[kani::proof] + fn timer_status_decide_resets() { + let status: u32 = kani::any(); + + let d = gale_k_timer_status_decide(status); + + assert!(d.count == status); + assert!(d.new_status == 0); + } + + /// Decision roundtrip: expire_decide then status_decide. + #[kani::proof] + fn timer_decide_roundtrip() { + let status: u32 = kani::any(); + let period: u32 = kani::any(); + kani::assume(status < u32::MAX); + + let expire_d = gale_k_timer_expire_decide(status, period); + assert!(expire_d.new_status == status + 1); + + let status_d = gale_k_timer_status_decide(expire_d.new_status); + assert!(status_d.count == status + 1); + assert!(status_d.new_status == 0); + } } // --------------------------------------------------------------------------- diff --git a/zephyr/gale_timer.c b/zephyr/gale_timer.c index 57906ec..c1d28c4 100644 --- a/zephyr/gale_timer.c +++ b/zephyr/gale_timer.c @@ -3,7 +3,7 @@ * * SPDX-License-Identifier: Apache-2.0 * - * Gale timer — verified status counter arithmetic. + * Gale timer — Extract→Decide→Apply pattern. * * This file provides Gale-validated helper functions for the safety-critical * status counter operations in kernel/timer.c. Unlike the other Gale @@ -13,13 +13,13 @@ * * These helpers are called from kernel/timer.c when CONFIG_GALE_KERNEL_TIMER * is enabled: - * gale_timer_expiry_handler — wraps gale_timer_expire for status++ - * gale_timer_status_read — wraps gale_timer_status_get for read+reset + * gale_timer_expiry_handler — Extract→Decide→Apply for status++ + * gale_timer_status_read — Extract→Decide→Apply for read+reset * * Verified operations (Verus proofs): - * gale_timer_expire — TM5 (increment), TM8 (no overflow) - * gale_timer_status_get — TM2 (read + reset to 0) - * gale_timer_init_validate — TM6/TM7 (period classification) + * gale_k_timer_expire_decide — TM5 (increment), TM8 (no overflow) + * gale_k_timer_status_decide — TM2 (read + reset to 0) + * gale_timer_init_validate — TM6/TM7 (period classification) */ #include @@ -28,36 +28,46 @@ #include "gale_timer.h" /** - * Gale-validated timer expiry: increment status with overflow check. + * Gale-validated timer expiry: Extract→Decide→Apply. * * Called from the timer expiry handler in kernel/timer.c in place of * the bare `timer->status++`. * + * Extract: read timer->status and timer->period. + * Decide: Rust computes new status (saturating increment) and classifies + * the timer as periodic or one-shot. + * Apply: write new_status back to timer->status. + * * @param timer Pointer to the timer object. * - * @return 0 on success (status incremented), - * -EOVERFLOW if status was at UINT32_MAX (status unchanged). + * @return 0 on success (status incremented or saturated). */ int gale_timer_expiry_handler(struct k_timer *timer) { - uint32_t new_status; - int32_t ret; + /* Extract */ + uint32_t status = timer->status; + uint32_t period = (uint32_t)timer->period.ticks; + + /* Decide */ + struct gale_timer_expire_decision d = + gale_k_timer_expire_decide(status, period); - ret = gale_timer_expire(timer->status, &new_status); - if (ret == 0) { - timer->status = new_status; - } - /* On overflow, status is left unchanged (saturated at UINT32_MAX) */ + /* Apply */ + timer->status = d.new_status; - return ret; + return 0; } /** - * Gale-validated timer status read: return old status and reset to 0. + * Gale-validated timer status read: Extract→Decide→Apply. * * Called from k_timer_status_get in kernel/timer.c in place of the * bare read-and-reset sequence. * + * Extract: read timer->status. + * Decide: Rust returns old status (count) and new status (0). + * Apply: write new_status back to timer->status, return count. + * * @param timer Pointer to the timer object. * * @return The number of expiry events since the last status read @@ -65,11 +75,15 @@ int gale_timer_expiry_handler(struct k_timer *timer) */ uint32_t gale_timer_status_read(struct k_timer *timer) { - uint32_t new_status; - uint32_t old; + /* Extract */ + uint32_t status = timer->status; + + /* Decide */ + struct gale_timer_status_decision d = + gale_k_timer_status_decide(status); - old = gale_timer_status_get(timer->status, &new_status); - timer->status = new_status; + /* Apply */ + timer->status = d.new_status; - return old; + return d.count; } From 675e9da0af2514d2e1449667c07107e5447b1ed8 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 20 Mar 2026 06:05:49 +0100 Subject: [PATCH 05/16] feat(shim): convert k_event post/wait to decision struct pattern Rewrite gale_event.c to use Extract-Decide-Apply with Rust decision structs. k_event_post_internal uses GaleEventPostDecision for masked bitmask computation, k_event_wait_internal and event_walk_op use GaleEventWaitDecision for ANY/ALL condition checks and pend/timeout decisions. Removes are_wait_conditions_met helper in favor of the unified decision struct. Co-Authored-By: Claude Opus 4.6 (1M context) --- ffi/include/gale_event.h | 26 ++++++++++++ zephyr/gale_event.c | 90 ++++++++++++++++------------------------ 2 files changed, 62 insertions(+), 54 deletions(-) diff --git a/ffi/include/gale_event.h b/ffi/include/gale_event.h index 1211618..c8ed862 100644 --- a/ffi/include/gale_event.h +++ b/ffi/include/gale_event.h @@ -100,6 +100,32 @@ int32_t gale_event_wait_check_any(uint32_t events, int32_t gale_event_wait_check_all(uint32_t events, uint32_t desired); +/* ---- Phase 2: Full Decision API ---- */ + +struct gale_event_post_decision { + uint32_t new_events; +}; + +struct gale_event_post_decision gale_k_event_post_decide( + uint32_t current_events, uint32_t new_events, uint32_t mask); + +struct gale_event_wait_decision { + int32_t ret; + uint32_t matched_events; + uint8_t action; /* 0=MATCHED, 1=PEND_CURRENT, 2=RETURN_TIMEOUT */ +}; + +#define GALE_EVENT_WAIT_ANY 0 +#define GALE_EVENT_WAIT_ALL 1 + +#define GALE_EVENT_ACTION_MATCHED 0 +#define GALE_EVENT_ACTION_PEND 1 +#define GALE_EVENT_ACTION_TIMEOUT 2 + +struct gale_event_wait_decision gale_k_event_wait_decide( + uint32_t current_events, uint32_t desired, + uint8_t wait_type, uint32_t is_no_wait); + #ifdef __cplusplus } #endif diff --git a/zephyr/gale_event.c b/zephyr/gale_event.c index 4308b6e..2eee83f 100644 --- a/zephyr/gale_event.c +++ b/zephyr/gale_event.c @@ -4,19 +4,16 @@ * * SPDX-License-Identifier: Apache-2.0 * - * Gale event — verified bitmask operations. + * Gale event — phase 2: Extract→Decide→Apply pattern. * * This is kernel/events.c with the safety-critical bitmask operations - * (post/set/clear/set_masked, are_wait_conditions_met) replaced by calls - * to the formally verified Rust implementation. + * (post/set/clear/set_masked, wait condition checks) replaced by calls + * to Rust decision structs. C extracts kernel state (spinlock, wait + * queue), Rust decides the bitmask result, C applies it. * * Verified operations (Verus proofs): - * gale_event_post — EV1, EV8 (OR bits, monotonic) - * gale_event_set — EV2 (replace all) - * gale_event_clear — EV3 (AND complement) - * gale_event_set_masked — EV4 (selective set) - * gale_event_wait_check_any — EV5 (any-bit match) - * gale_event_wait_check_all — EV6 (all-bits match) + * gale_k_event_post_decide — EV4 (masked set: (cur & ~mask) | (new & mask)) + * gale_k_event_wait_decide — EV5 (any-bit match), EV6 (all-bits match) * * Wait queues, scheduling, tracing, poll, userspace, and OBJ_CORE * remain native Zephyr. @@ -56,28 +53,6 @@ struct event_walk_data { static struct k_obj_type obj_type_event; #endif /* CONFIG_OBJ_CORE_EVENT */ -/** - * @brief determine the set of events that have been satisfied - * - * This routine determines if the current set of events satisfies the desired - * set of events. Uses Gale-verified wait_check_any / wait_check_all. - */ -static uint32_t are_wait_conditions_met(uint32_t desired, uint32_t current, - unsigned int wait_condition) -{ - uint32_t match = current & desired; - - if (wait_condition == K_EVENT_WAIT_ALL) { - /* Gale-verified: EV6 — all-bits match */ - if (gale_event_wait_check_all(current, desired) == 0) { - return 0; - } - } - - /* return the matched events for any wait condition */ - return match; -} - void z_impl_k_event_init(struct k_event *event) { __ASSERT_NO_MSG(!arch_is_in_isr()); @@ -130,18 +105,19 @@ static void event_post_walk_op(int status, void *data) static int event_walk_op(struct k_thread *thread, void *data) { - uint32_t match; - unsigned int wait_condition; struct event_walk_data *event_data = data; + unsigned int wait_condition = thread->event_options & K_EVENT_WAIT_MASK; - wait_condition = thread->event_options & K_EVENT_WAIT_MASK; + /* Decide: Rust checks the wait condition for this thread */ + struct gale_event_wait_decision wd = gale_k_event_wait_decide( + event_data->events, thread->events, + (uint8_t)wait_condition, /*is_no_wait=*/0U); - match = are_wait_conditions_met(thread->events, event_data->events, - wait_condition); - if (match != 0) { - thread->events = match; + /* Apply: if matched, wake the thread */ + if (wd.action == GALE_EVENT_ACTION_MATCHED) { + thread->events = wd.matched_events; if (thread->event_options & K_EVENT_OPTION_CLEAR) { - event_data->clear_events |= match; + event_data->clear_events |= wd.matched_events; } z_abort_thread_timeout(thread); @@ -169,13 +145,13 @@ static uint32_t k_event_post_internal(struct k_event *event, uint32_t events, SYS_PORT_TRACING_OBJ_FUNC_ENTER(k_event, post, event, events, events_mask); + /* Extract: capture previous events under the mask */ previous_events = event->events & events_mask; - /* Gale-verified: EV4 — set_masked computes - * (events & ~mask) | (new & mask) */ - uint32_t new_events; - gale_event_set_masked(event->events, events, events_mask, &new_events); - events = new_events; + /* Decide: Rust computes (cur & ~mask) | (new & mask) */ + struct gale_event_post_decision pd = gale_k_event_post_decide( + event->events, events, events_mask); + events = pd.new_events; #ifdef CONFIG_WAITQ_SCALABLE data.head = NULL; @@ -184,7 +160,7 @@ static uint32_t k_event_post_internal(struct k_event *event, uint32_t events, data.clear_events = 0; z_sched_waitq_walk(&event->wait_q, event_walk_op, EVENT_POST_WALK_OP_FN, &data); - /* stash any events not consumed */ + /* Apply: stash any events not consumed */ event->events = data.events & ~data.clear_events; z_reschedule(&event->lock, key); @@ -276,30 +252,36 @@ static uint32_t k_event_wait_internal(struct k_event *event, uint32_t events, k_spinlock_key_t key = k_spin_lock(&event->lock); + /* Extract: optionally reset events */ if (options & K_EVENT_OPTION_RESET) { event->events = 0; } - /* Gale-verified: EV5/EV6 — wait condition check */ - rv = are_wait_conditions_met(events, event->events, wait_condition); - if (rv != 0) { - /* clear the events that are matched */ + /* Decide: Rust checks wait condition and determines action */ + struct gale_event_wait_decision wd = gale_k_event_wait_decide( + event->events, events, (uint8_t)wait_condition, + K_TIMEOUT_EQ(timeout, K_NO_WAIT) ? 1U : 0U); + + /* Apply */ + if (wd.action == GALE_EVENT_ACTION_MATCHED) { + rv = wd.matched_events; + + /* Clear the matched events if requested */ if (options & K_EVENT_OPTION_CLEAR) { - /* Gale-verified: EV3 — clear matched bits */ - uint32_t cleared; - gale_event_clear(event->events, rv, &cleared); - event->events = cleared; + event->events = event->events & ~rv; } k_spin_unlock(&event->lock, key); goto out; } - if (K_TIMEOUT_EQ(timeout, K_NO_WAIT)) { + if (wd.action == GALE_EVENT_ACTION_TIMEOUT) { + /* K_NO_WAIT and condition not met */ k_spin_unlock(&event->lock, key); goto out; } + /* PEND_CURRENT: block on wait queue with timeout */ thread->events = events; thread->event_options = options; From ed15b80e629e1c45bea9d13bb703884adda730a7 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 20 Mar 2026 06:07:14 +0100 Subject: [PATCH 06/16] feat(shim): convert k_queue append/get to decision struct pattern MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Rewrite queue_insert and z_impl_k_queue_get in gale_queue.c to use the Extract→Decide→Apply pattern with Rust decision structs. C extracts kernel state (wait queue, list emptiness), Rust decides the action (WAKE vs INSERT, DEQUEUE vs RETURN_NULL vs PEND), C applies it. Data movement (linked list insertion, alloc nodes) stays in C. Co-Authored-By: Claude Opus 4.6 (1M context) --- ffi/include/gale_pipe.h | 34 ++++ ffi/include/gale_queue.h | 23 +++ ffi/src/lib.rs | 414 +++++++++++++++++++++++++++++++++++++++ zephyr/gale_pipe.c | 137 ++++++------- zephyr/gale_queue.c | 98 +++++---- 5 files changed, 589 insertions(+), 117 deletions(-) diff --git a/ffi/include/gale_pipe.h b/ffi/include/gale_pipe.h index d0ea30c..a010cf1 100644 --- a/ffi/include/gale_pipe.h +++ b/ffi/include/gale_pipe.h @@ -59,6 +59,40 @@ int32_t gale_pipe_read_check(uint32_t used, uint32_t *actual_len, uint32_t *new_used); +/* ---- Phase 2: Full Decision API ---- */ + +struct gale_pipe_write_decision { + int32_t ret; + uint8_t action; /* 0=WRITE_OK, 1=WAKE_READER, 2=PEND_CURRENT, 3=RETURN_ERROR */ + uint32_t actual_bytes; + uint32_t new_used; +}; + +#define GALE_PIPE_ACTION_WRITE_OK 0 +#define GALE_PIPE_ACTION_WAKE_READER 1 +#define GALE_PIPE_ACTION_WRITE_PEND 2 +#define GALE_PIPE_ACTION_WRITE_ERROR 3 + +struct gale_pipe_write_decision gale_k_pipe_write_decide( + uint32_t used, uint32_t size, uint8_t flags, + uint32_t request_len, uint32_t has_reader); + +struct gale_pipe_read_decision { + int32_t ret; + uint8_t action; /* 0=READ_OK, 1=WAKE_WRITER, 2=PEND_CURRENT, 3=RETURN_ERROR */ + uint32_t actual_bytes; + uint32_t new_used; +}; + +#define GALE_PIPE_ACTION_READ_OK 0 +#define GALE_PIPE_ACTION_WAKE_WRITER 1 +#define GALE_PIPE_ACTION_READ_PEND 2 +#define GALE_PIPE_ACTION_READ_ERROR 3 + +struct gale_pipe_read_decision gale_k_pipe_read_decide( + uint32_t used, uint32_t size, uint8_t flags, + uint32_t request_len, uint32_t has_writer); + #ifdef __cplusplus } #endif diff --git a/ffi/include/gale_queue.h b/ffi/include/gale_queue.h index f360413..b555ead 100644 --- a/ffi/include/gale_queue.h +++ b/ffi/include/gale_queue.h @@ -56,6 +56,29 @@ int32_t gale_queue_prepend_validate(uint32_t count, int32_t gale_queue_get_validate(uint32_t count, uint32_t *new_count); +/* ---- Phase 2: Full Decision API ---- */ + +struct gale_queue_insert_decision { + uint8_t action; /* 0=INSERT_INTO_LIST, 1=WAKE_THREAD */ +}; + +#define GALE_QUEUE_ACTION_INSERT 0 +#define GALE_QUEUE_ACTION_WAKE 1 + +struct gale_queue_insert_decision gale_k_queue_insert_decide( + uint32_t has_waiter); + +struct gale_queue_get_decision { + uint8_t action; /* 0=DEQUEUE, 1=RETURN_NULL, 2=PEND_CURRENT */ +}; + +#define GALE_QUEUE_ACTION_DEQUEUE 0 +#define GALE_QUEUE_ACTION_RETURN_NULL 1 +#define GALE_QUEUE_ACTION_PEND 2 + +struct gale_queue_get_decision gale_k_queue_get_decide( + uint32_t has_data, uint32_t is_no_wait); + #ifdef __cplusplus } #endif diff --git a/ffi/src/lib.rs b/ffi/src/lib.rs index 4f0b028..fa9aa0e 100644 --- a/ffi/src/lib.rs +++ b/ffi/src/lib.rs @@ -509,6 +509,144 @@ pub extern "C" fn gale_mutex_unlock_validate( } } +// ---- Phase 2: Full Decision API for Mutex ---- + +/// Decision struct for k_mutex_lock — tells C shim what action to take. +#[repr(C)] +pub struct GaleMutexLockDecision { + /// Return code: 0 (acquired), -EBUSY (would block) + pub ret: i32, + /// Action: 0=ACQUIRED, 1=PEND_CURRENT, 2=RETURN_BUSY + pub action: u8, + /// New lock_count value (only meaningful when action=ACQUIRED) + pub new_lock_count: u32, +} + +pub const GALE_MUTEX_ACTION_ACQUIRED: u8 = 0; +pub const GALE_MUTEX_ACTION_PEND: u8 = 1; +pub const GALE_MUTEX_ACTION_BUSY: u8 = 2; + +/// Full decision for k_mutex_lock: decides whether to acquire, pend, or return busy. +/// +/// Handles reentrant locking, ownership check, and pend-or-busy decision. +/// Priority inheritance logic stays in C — Rust decides the action, +/// C applies it including any priority adjustments. +/// +/// Verified: M3 (acquire), M4 (reentrant), M5 (contended), M10 (no overflow). +#[unsafe(no_mangle)] +pub extern "C" fn gale_k_mutex_lock_decide( + lock_count: u32, + owner_is_null: u32, + owner_is_current: u32, + is_no_wait: u32, +) -> GaleMutexLockDecision { + if owner_is_null != 0 { + // Mutex unlocked — acquire (M3). + GaleMutexLockDecision { + ret: OK, + action: GALE_MUTEX_ACTION_ACQUIRED, + new_lock_count: 1, + } + } else if owner_is_current != 0 { + // Reentrant lock — same owner (M4, M10). + match lock_count.checked_add(1) { + Some(n) => GaleMutexLockDecision { + ret: OK, + action: GALE_MUTEX_ACTION_ACQUIRED, + new_lock_count: n, + }, + None => { + // Overflow would violate M10. + GaleMutexLockDecision { + ret: EINVAL, + action: GALE_MUTEX_ACTION_BUSY, + new_lock_count: lock_count, + } + } + } + } else if is_no_wait != 0 { + // Different owner, no-wait — return busy (M5). + GaleMutexLockDecision { + ret: EBUSY, + action: GALE_MUTEX_ACTION_BUSY, + new_lock_count: lock_count, + } + } else { + // Different owner, willing to wait — pend (M5). + GaleMutexLockDecision { + ret: 0, + action: GALE_MUTEX_ACTION_PEND, + new_lock_count: lock_count, + } + } +} + +/// Decision struct for k_mutex_unlock — tells C shim what action to take. +#[repr(C)] +pub struct GaleMutexUnlockDecision { + /// Return code: 0 (success), -EINVAL (not locked), -EPERM (not owner) + pub ret: i32, + /// Action: 0=RELEASED (still held), 1=UNLOCKED (check waiters), 2=ERROR + pub action: u8, + /// New lock_count value (decremented if RELEASED, 0 if UNLOCKED) + pub new_lock_count: u32, +} + +pub const GALE_MUTEX_UNLOCK_RELEASED: u8 = 0; +pub const GALE_MUTEX_UNLOCK_UNLOCKED: u8 = 1; +pub const GALE_MUTEX_UNLOCK_ERROR: u8 = 2; + +/// Full decision for k_mutex_unlock: decides whether to decrement, fully unlock, +/// or return an error. +/// +/// Priority inheritance restoration stays in C — Rust decides the action, +/// C applies it including any priority adjustments. +/// +/// Verified: M6a (EINVAL), M6b (EPERM), M7 (reentrant), M10 (no underflow). +#[unsafe(no_mangle)] +pub extern "C" fn gale_k_mutex_unlock_decide( + lock_count: u32, + owner_is_null: u32, + owner_is_current: u32, +) -> GaleMutexUnlockDecision { + // M6a: not locked + if owner_is_null != 0 { + return GaleMutexUnlockDecision { + ret: EINVAL, + action: GALE_MUTEX_UNLOCK_ERROR, + new_lock_count: 0, + }; + } + + // M6b: not owner + if owner_is_current == 0 { + return GaleMutexUnlockDecision { + ret: EPERM, + action: GALE_MUTEX_UNLOCK_ERROR, + new_lock_count: lock_count, + }; + } + + // M7: reentrant release (lock_count > 1) + if lock_count > 1 { + // Verified: lock_count > 1, so lock_count - 1 >= 1, no underflow. + #[allow(clippy::arithmetic_side_effects)] + let new_count = lock_count - 1; + GaleMutexUnlockDecision { + ret: OK, + action: GALE_MUTEX_UNLOCK_RELEASED, + new_lock_count: new_count, + } + } else { + // Fully unlocked — caller handles waiter transfer. + GaleMutexUnlockDecision { + ret: OK, + action: GALE_MUTEX_UNLOCK_UNLOCKED, + new_lock_count: 0, + } + } +} + // --------------------------------------------------------------------------- // Message Queue FFI exports — ring buffer index arithmetic // --------------------------------------------------------------------------- @@ -782,6 +920,147 @@ pub extern "C" fn gale_msgq_peek_at( } } +// ---- Phase 2: Full Decision API for msgq ---- + +/// Decision struct for k_msgq_put -- tells C shim what action to take. +#[repr(C)] +pub struct GaleMsgqPutDecision { + /// Return code: 0 (OK), -ENOMSG (full) + pub ret: i32, + /// Action: 0=PUT_OK, 1=WAKE_READER, 2=PEND_CURRENT, 3=RETURN_FULL + pub action: u8, + /// New write index (only meaningful when action=PUT_OK) + pub new_write_idx: u32, + /// New used count + pub new_used: u32, +} + +pub const GALE_MSGQ_ACTION_PUT_OK: u8 = 0; +pub const GALE_MSGQ_ACTION_WAKE_READER: u8 = 1; +pub const GALE_MSGQ_ACTION_PUT_PEND: u8 = 2; +pub const GALE_MSGQ_ACTION_RETURN_FULL: u8 = 3; + +/// Full decision for k_msgq_put: decides whether to put, wake a reader, pend, +/// or return full. +#[unsafe(no_mangle)] +pub extern "C" fn gale_k_msgq_put_decide( + write_idx: u32, + used_msgs: u32, + max_msgs: u32, + has_waiter: u32, + is_no_wait: u32, +) -> GaleMsgqPutDecision { + if used_msgs < max_msgs { + if has_waiter != 0 { + GaleMsgqPutDecision { + ret: OK, + action: GALE_MSGQ_ACTION_WAKE_READER, + new_write_idx: write_idx, + new_used: used_msgs, + } + } else { + #[allow(clippy::arithmetic_side_effects)] + let next = if write_idx + 1 < max_msgs { + write_idx + 1 + } else { + 0 + }; + #[allow(clippy::arithmetic_side_effects)] + let new_used = used_msgs + 1; + GaleMsgqPutDecision { + ret: OK, + action: GALE_MSGQ_ACTION_PUT_OK, + new_write_idx: next, + new_used, + } + } + } else if is_no_wait != 0 { + GaleMsgqPutDecision { + ret: ENOMSG, + action: GALE_MSGQ_ACTION_RETURN_FULL, + new_write_idx: write_idx, + new_used: used_msgs, + } + } else { + GaleMsgqPutDecision { + ret: 0, + action: GALE_MSGQ_ACTION_PUT_PEND, + new_write_idx: write_idx, + new_used: used_msgs, + } + } +} + +/// Decision struct for k_msgq_get -- tells C shim what action to take. +#[repr(C)] +pub struct GaleMsgqGetDecision { + /// Return code: 0 (OK), -ENOMSG (empty) + pub ret: i32, + /// Action: 0=GET_OK, 1=WAKE_WRITER, 2=PEND_CURRENT, 3=RETURN_EMPTY + pub action: u8, + /// New read index (only meaningful when action=GET_OK or WAKE_WRITER) + pub new_read_idx: u32, + /// New used count + pub new_used: u32, +} + +pub const GALE_MSGQ_ACTION_GET_OK: u8 = 0; +pub const GALE_MSGQ_ACTION_WAKE_WRITER: u8 = 1; +pub const GALE_MSGQ_ACTION_GET_PEND: u8 = 2; +pub const GALE_MSGQ_ACTION_RETURN_EMPTY: u8 = 3; + +/// Full decision for k_msgq_get: decides whether to get, wake a writer, pend, +/// or return empty. +#[unsafe(no_mangle)] +pub extern "C" fn gale_k_msgq_get_decide( + read_idx: u32, + used_msgs: u32, + max_msgs: u32, + has_waiter: u32, + is_no_wait: u32, +) -> GaleMsgqGetDecision { + if used_msgs > 0 { + #[allow(clippy::arithmetic_side_effects)] + let next = if read_idx + 1 < max_msgs { + read_idx + 1 + } else { + 0 + }; + #[allow(clippy::arithmetic_side_effects)] + let new_used = used_msgs - 1; + + if has_waiter != 0 { + GaleMsgqGetDecision { + ret: OK, + action: GALE_MSGQ_ACTION_WAKE_WRITER, + new_read_idx: next, + new_used, + } + } else { + GaleMsgqGetDecision { + ret: OK, + action: GALE_MSGQ_ACTION_GET_OK, + new_read_idx: next, + new_used, + } + } + } else if is_no_wait != 0 { + GaleMsgqGetDecision { + ret: ENOMSG, + action: GALE_MSGQ_ACTION_RETURN_EMPTY, + new_read_idx: read_idx, + new_used: 0, + } + } else { + GaleMsgqGetDecision { + ret: 0, + action: GALE_MSGQ_ACTION_GET_PEND, + new_read_idx: read_idx, + new_used: 0, + } + } +} + // --------------------------------------------------------------------------- // Stack FFI exports — LIFO count/capacity arithmetic // --------------------------------------------------------------------------- @@ -3899,6 +4178,141 @@ mod kani_mutex_proofs { } } +// --------------------------------------------------------------------------- +// Kani bounded model checking — mutex decision structs +// --------------------------------------------------------------------------- + +#[cfg(kani)] +mod kani_mutex_decide_proofs { + use super::*; + + /// M3: lock_decide on unlocked mutex returns ACQUIRED with lock_count = 1. + #[kani::proof] + fn mutex_lock_decide_unlocked() { + let d = gale_k_mutex_lock_decide(0, 1, 0, 0); + assert!(d.ret == OK); + assert!(d.action == GALE_MUTEX_ACTION_ACQUIRED); + assert!(d.new_lock_count == 1); + } + + /// M4/M10: lock_decide reentrant increments without overflow. + #[kani::proof] + fn mutex_lock_decide_reentrant() { + let lock_count: u32 = kani::any(); + kani::assume(lock_count > 0 && lock_count < u32::MAX); + + let d = gale_k_mutex_lock_decide(lock_count, 0, 1, 0); + assert!(d.ret == OK); + assert!(d.action == GALE_MUTEX_ACTION_ACQUIRED); + assert!(d.new_lock_count == lock_count + 1); + } + + /// M10: lock_decide reentrant at u32::MAX returns error (overflow protection). + #[kani::proof] + fn mutex_lock_decide_reentrant_overflow() { + let d = gale_k_mutex_lock_decide(u32::MAX, 0, 1, 0); + assert!(d.ret == EINVAL); + assert!(d.action == GALE_MUTEX_ACTION_BUSY); + assert!(d.new_lock_count == u32::MAX); + } + + /// M5: lock_decide contended with no-wait returns BUSY. + #[kani::proof] + fn mutex_lock_decide_contended_no_wait() { + let lock_count: u32 = kani::any(); + kani::assume(lock_count > 0); + + let d = gale_k_mutex_lock_decide(lock_count, 0, 0, 1); + assert!(d.ret == EBUSY); + assert!(d.action == GALE_MUTEX_ACTION_BUSY); + } + + /// M5: lock_decide contended willing to wait returns PEND. + #[kani::proof] + fn mutex_lock_decide_contended_pend() { + let lock_count: u32 = kani::any(); + kani::assume(lock_count > 0); + + let d = gale_k_mutex_lock_decide(lock_count, 0, 0, 0); + assert!(d.ret == 0); + assert!(d.action == GALE_MUTEX_ACTION_PEND); + } + + /// M6a: unlock_decide when not locked returns EINVAL + ERROR action. + #[kani::proof] + fn mutex_unlock_decide_not_locked() { + let d = gale_k_mutex_unlock_decide(0, 1, 0); + assert!(d.ret == EINVAL); + assert!(d.action == GALE_MUTEX_UNLOCK_ERROR); + } + + /// M6b: unlock_decide by wrong owner returns EPERM + ERROR action. + #[kani::proof] + fn mutex_unlock_decide_not_owner() { + let lock_count: u32 = kani::any(); + kani::assume(lock_count > 0); + + let d = gale_k_mutex_unlock_decide(lock_count, 0, 0); + assert!(d.ret == EPERM); + assert!(d.action == GALE_MUTEX_UNLOCK_ERROR); + } + + /// M7: unlock_decide reentrant decrements correctly. + #[kani::proof] + fn mutex_unlock_decide_reentrant() { + let lock_count: u32 = kani::any(); + kani::assume(lock_count > 1); + + let d = gale_k_mutex_unlock_decide(lock_count, 0, 1); + assert!(d.ret == OK); + assert!(d.action == GALE_MUTEX_UNLOCK_RELEASED); + assert!(d.new_lock_count == lock_count - 1); + } + + /// M9: unlock_decide final unlock returns UNLOCKED. + #[kani::proof] + fn mutex_unlock_decide_final() { + let d = gale_k_mutex_unlock_decide(1, 0, 1); + assert!(d.ret == OK); + assert!(d.action == GALE_MUTEX_UNLOCK_UNLOCKED); + assert!(d.new_lock_count == 0); + } + + /// Lock-unlock roundtrip via decision structs. + #[kani::proof] + fn mutex_decide_roundtrip() { + // Lock (unlocked mutex) + let dl = gale_k_mutex_lock_decide(0, 1, 0, 0); + assert!(dl.ret == OK); + assert!(dl.action == GALE_MUTEX_ACTION_ACQUIRED); + assert!(dl.new_lock_count == 1); + + // Unlock + let du = gale_k_mutex_unlock_decide(dl.new_lock_count, 0, 1); + assert!(du.ret == OK); + assert!(du.action == GALE_MUTEX_UNLOCK_UNLOCKED); + assert!(du.new_lock_count == 0); + } + + /// Reentrant lock-unlock roundtrip via decision structs. + #[kani::proof] + fn mutex_decide_reentrant_roundtrip() { + let lock_count: u32 = kani::any(); + kani::assume(lock_count > 0 && lock_count < u32::MAX); + + // Reentrant lock + let dl = gale_k_mutex_lock_decide(lock_count, 0, 1, 0); + assert!(dl.ret == OK); + assert!(dl.new_lock_count == lock_count + 1); + + // Reentrant unlock + let du = gale_k_mutex_unlock_decide(dl.new_lock_count, 0, 1); + assert!(du.ret == OK); + assert!(du.action == GALE_MUTEX_UNLOCK_RELEASED); + assert!(du.new_lock_count == lock_count); + } +} + // --------------------------------------------------------------------------- // Kani bounded model checking — message queue // --------------------------------------------------------------------------- diff --git a/zephyr/gale_pipe.c b/zephyr/gale_pipe.c index c37dfe8..04048b1 100644 --- a/zephyr/gale_pipe.c +++ b/zephyr/gale_pipe.c @@ -4,16 +4,17 @@ * * SPDX-License-Identifier: Apache-2.0 * - * Gale pipe — verified state machine + byte count validation. + * Gale pipe — phase 2: Extract->Decide->Apply pattern. * - * This is kernel/pipe.c with the state machine checks (pipe_closed, - * pipe_resetting, pipe_full, pipe_empty) replaced by calls to the - * formally verified Rust implementation (gale_pipe_write_check, - * gale_pipe_read_check). + * This is kernel/pipe.c with write/read rewritten to use Rust decision + * structs. C extracts kernel state (spinlock, wait queue, ring buffer), + * Rust decides the action, C applies it. * * Verified operations (Verus proofs): - * gale_pipe_write_check — PP1-PP2, PP4-PP6, PP8, PP10 (state + byte count) - * gale_pipe_read_check — PP1, PP3, PP4-PP5, PP7, PP9, PP10 + * gale_k_pipe_write_decide — PP3-PP5, PP9-PP10 (state + byte count) + * gale_k_pipe_read_decide — PP3-PP6, PP9-PP10 + * gale_pipe_write_check — PP1-PP2, PP4-PP6, PP8, PP10 (phase 1, retained) + * gale_pipe_read_check — PP1, PP3, PP4-PP5, PP7, PP9, PP10 (phase 1, retained) * * Ring buffer data transfer, scheduling, wait queues, tracing, poll, * userspace, and OBJ_CORE remain native Zephyr. @@ -142,42 +143,28 @@ int z_impl_k_pipe_write(struct k_pipe *pipe, const uint8_t *data, size_t len, k_ k_timepoint_t end = sys_timepoint_calc(timeout); k_spinlock_key_t key = k_spin_lock(&pipe->lock); bool need_resched = false; - uint32_t actual_len, new_used; SYS_PORT_TRACING_OBJ_FUNC_ENTER(k_pipe, write, pipe, data, len, timeout); - /* --- Gale verified initial state check --- */ - rc = gale_pipe_write_check(ring_buf_size_get(&pipe->buf), - ring_buf_capacity_get(&pipe->buf), - pipe->flags, - (uint32_t)len, - &actual_len, &new_used); - if (rc == -ECANCELED) { - /* PP5: resetting pipe rejects operations */ - goto exit; - } - for (;;) { - /* --- Gale verified per-iteration state check --- */ - rc = gale_pipe_write_check(ring_buf_size_get(&pipe->buf), - ring_buf_capacity_get(&pipe->buf), - pipe->flags, - (uint32_t)(len - written), - &actual_len, &new_used); - if (unlikely(rc == -EPIPE)) { - /* PP4: closed pipe rejects operations */ - break; - } - if (unlikely(rc == -ECANCELED)) { + /* Extract: gather kernel state */ + uint32_t used = ring_buf_size_get(&pipe->buf); + uint32_t capacity = ring_buf_capacity_get(&pipe->buf); + uint32_t has_reader = z_waitq_head(&pipe->data) != NULL ? 1U : 0U; + + /* Decide: Rust determines action */ + struct gale_pipe_write_decision d = gale_k_pipe_write_decide( + used, capacity, pipe->flags, + (uint32_t)(len - written), has_reader); + + /* Apply: execute Rust's decision */ + if (d.action == GALE_PIPE_ACTION_WRITE_ERROR) { + rc = d.ret; break; } - if (ring_buf_is_empty(&pipe->buf)) { + if (d.action == GALE_PIPE_ACTION_WAKE_READER) { if (IS_ENABLED(CONFIG_KERNEL_COHERENCE)) { - /* - * Stacks not in coherent memory — can't do - * direct-to-readers copy. Wake readers instead. - */ need_resched = z_sched_wake_all(&pipe->data, 0, NULL); } else if (pipe->waiting != 0) { written += copy_to_pending_readers(pipe, &need_resched, @@ -190,17 +177,21 @@ int z_impl_k_pipe_write(struct k_pipe *pipe, const uint8_t *data, size_t len, k_ } } + if (d.action == GALE_PIPE_ACTION_WRITE_OK || + d.action == GALE_PIPE_ACTION_WAKE_READER) { #ifdef CONFIG_POLL - need_resched |= z_handle_obj_poll_events(&pipe->poll_events, - K_POLL_STATE_PIPE_DATA_AVAILABLE); + need_resched |= z_handle_obj_poll_events(&pipe->poll_events, + K_POLL_STATE_PIPE_DATA_AVAILABLE); #endif /* CONFIG_POLL */ - written += ring_buf_put(&pipe->buf, &data[written], len - written); - if (likely(written == len)) { - rc = written; - break; + written += ring_buf_put(&pipe->buf, &data[written], len - written); + if (likely(written == len)) { + rc = written; + break; + } } + /* PEND_CURRENT or partial write: block on space wait queue */ rc = wait_for(&pipe->space, pipe, &key, end, &need_resched); if (rc != 0) { if (rc == -EAGAIN) { @@ -209,7 +200,7 @@ int z_impl_k_pipe_write(struct k_pipe *pipe, const uint8_t *data, size_t len, k_ break; } } -exit: + SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_pipe, write, pipe, rc); if (need_resched) { z_reschedule(&pipe->lock, key); @@ -226,48 +217,44 @@ int z_impl_k_pipe_read(struct k_pipe *pipe, uint8_t *data, size_t len, k_timeout k_timepoint_t end = sys_timepoint_calc(timeout); k_spinlock_key_t key = k_spin_lock(&pipe->lock); bool need_resched = false; - uint32_t actual_len, new_used; SYS_PORT_TRACING_OBJ_FUNC_ENTER(k_pipe, read, pipe, data, len, timeout); - /* --- Gale verified initial state check --- */ - rc = gale_pipe_read_check(ring_buf_size_get(&pipe->buf), - pipe->flags, - (uint32_t)len, - &actual_len, &new_used); - if (rc == -ECANCELED) { - /* PP5: resetting pipe rejects operations */ - goto exit; - } - for (;;) { - if (ring_buf_space_get(&pipe->buf) == 0) { - /* Buffer full — wake pending writers. */ - need_resched = z_sched_wake_all(&pipe->space, 0, NULL); - } - - buf.used += ring_buf_get(&pipe->buf, &data[buf.used], len - buf.used); - if (likely(buf.used == len)) { - rc = buf.used; + /* Extract: gather kernel state */ + uint32_t used = ring_buf_size_get(&pipe->buf); + uint32_t capacity = ring_buf_capacity_get(&pipe->buf); + uint32_t has_writer = z_waitq_head(&pipe->space) != NULL ? 1U : 0U; + + /* Decide: Rust determines action */ + struct gale_pipe_read_decision d = gale_k_pipe_read_decide( + used, capacity, pipe->flags, + (uint32_t)(len - buf.used), has_writer); + + /* Apply: execute Rust's decision */ + if (d.action == GALE_PIPE_ACTION_READ_ERROR) { + if (d.ret == -EPIPE) { + rc = buf.used ? (int)buf.used : -EPIPE; + } else { + rc = d.ret; + } break; } - /* --- Gale verified state check after partial read --- */ - rc = gale_pipe_read_check(ring_buf_size_get(&pipe->buf), - pipe->flags, - (uint32_t)(len - buf.used), - &actual_len, &new_used); - if (rc == -EPIPE) { - /* PP4: closed + empty — return partial read or error */ - rc = buf.used ? (int)buf.used : -EPIPE; - break; + if (d.action == GALE_PIPE_ACTION_WAKE_WRITER) { + need_resched = z_sched_wake_all(&pipe->space, 0, NULL); } - if (rc == -ECANCELED) { - rc = -ECANCELED; - break; + + if (d.action == GALE_PIPE_ACTION_READ_OK || + d.action == GALE_PIPE_ACTION_WAKE_WRITER) { + buf.used += ring_buf_get(&pipe->buf, &data[buf.used], len - buf.used); + if (likely(buf.used == len)) { + rc = buf.used; + break; + } } - /* Provide direct-copy buffer to potential writers */ + /* PEND_CURRENT or partial read: provide direct-copy buffer, then block */ _current->base.swap_data = &buf; rc = wait_for(&pipe->data, pipe, &key, end, &need_resched); @@ -278,7 +265,7 @@ int z_impl_k_pipe_read(struct k_pipe *pipe, uint8_t *data, size_t len, k_timeout break; } } -exit: + SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_pipe, read, pipe, rc); if (need_resched) { z_reschedule(&pipe->lock, key); diff --git a/zephyr/gale_queue.c b/zephyr/gale_queue.c index 9922e4b..bb639df 100644 --- a/zephyr/gale_queue.c +++ b/zephyr/gale_queue.c @@ -4,17 +4,18 @@ * * SPDX-License-Identifier: Apache-2.0 * - * Gale queue — verified unbounded queue count arithmetic. + * Gale queue — phase 2: Extract→Decide→Apply pattern. * - * This is kernel/queue.c with the count tracking replaced by calls - * to the formally verified Rust implementation. The linked list - * (sys_sflist), wait queue, scheduling, alloc nodes, polling, and - * tracing remain native Zephyr. + * This is kernel/queue.c with queue_insert and k_queue_get rewritten + * to use Rust decision structs. C extracts kernel state (spinlock, + * wait queue side effects), Rust decides the action, C applies it. + * + * The linked list (sys_sflist), alloc nodes, polling, and tracing + * remain native Zephyr. * * Verified operations (Verus proofs): - * gale_queue_append_validate — QU1 (no overflow), QU2 (increment) - * gale_queue_prepend_validate — QU3 (no overflow), QU4 (increment) - * gale_queue_get_validate — QU5 (no underflow), QU6 (decrement) + * gale_k_queue_insert_decide — QU1-QU4 (wake vs insert decision) + * gale_k_queue_get_decide — QU5/QU6 (dequeue vs null vs pend decision) */ #include @@ -131,7 +132,6 @@ static inline void z_vrfy_k_queue_cancel_wait(struct k_queue *queue) static int32_t queue_insert(struct k_queue *queue, void *prev, void *data, bool alloc, bool is_append) { - struct k_thread *first_pending_thread; k_spinlock_key_t key = k_spin_lock(&queue->lock); int32_t result = 0; bool resched = false; @@ -141,36 +141,43 @@ static int32_t queue_insert(struct k_queue *queue, void *prev, void *data, if (is_append) { prev = sys_sflist_peek_tail(&queue->data_q); } - first_pending_thread = z_unpend_first_thread(&queue->wait_q); - if (unlikely(first_pending_thread != NULL)) { + /* Extract: try to unpend first waiter (side effect: removes from queue) */ + struct k_thread *first_pending_thread = + z_unpend_first_thread(&queue->wait_q); + + /* Decide: Rust determines action based on whether a waiter was found */ + struct gale_queue_insert_decision d = gale_k_queue_insert_decide( + first_pending_thread != NULL ? 1U : 0U); + + /* Apply: execute Rust's decision */ + if (d.action == GALE_QUEUE_ACTION_WAKE) { SYS_PORT_TRACING_OBJ_FUNC_BLOCKING(k_queue, queue_insert, queue, alloc, K_FOREVER); prepare_thread_to_run(first_pending_thread, data); resched = true; - goto out; - } - - /* Only need to actually allocate if no threads are pending */ - if (alloc) { - struct alloc_node *anode; - - anode = z_thread_malloc(sizeof(*anode)); - if (anode == NULL) { - result = -ENOMEM; - goto out; - } - anode->data = data; - sys_sfnode_init(&anode->node, 0x1); - data = anode; } else { - sys_sfnode_init(data, 0x0); - } + /* INSERT_INTO_LIST: allocate node if needed, then insert */ + if (alloc) { + struct alloc_node *anode; + + anode = z_thread_malloc(sizeof(*anode)); + if (anode == NULL) { + result = -ENOMEM; + goto out; + } + anode->data = data; + sys_sfnode_init(&anode->node, 0x1); + data = anode; + } else { + sys_sfnode_init(data, 0x0); + } - SYS_PORT_TRACING_OBJ_FUNC_BLOCKING(k_queue, queue_insert, queue, alloc, K_FOREVER); + SYS_PORT_TRACING_OBJ_FUNC_BLOCKING(k_queue, queue_insert, queue, alloc, K_FOREVER); - sys_sflist_insert(&queue->data_q, prev, data); - resched = handle_poll_events(queue, K_POLL_STATE_DATA_AVAILABLE); + sys_sflist_insert(&queue->data_q, prev, data); + resched = handle_poll_events(queue, K_POLL_STATE_DATA_AVAILABLE); + } out: if (resched) { @@ -329,7 +336,15 @@ void *z_impl_k_queue_get(struct k_queue *queue, k_timeout_t timeout) SYS_PORT_TRACING_OBJ_FUNC_ENTER(k_queue, get, queue, timeout); - if (likely(!sys_sflist_is_empty(&queue->data_q))) { + /* Extract: check if list has data */ + uint32_t has_data = !sys_sflist_is_empty(&queue->data_q) ? 1U : 0U; + + /* Decide: Rust determines action */ + struct gale_queue_get_decision d = gale_k_queue_get_decide( + has_data, K_TIMEOUT_EQ(timeout, K_NO_WAIT) ? 1U : 0U); + + /* Apply: execute Rust's decision */ + if (d.action == GALE_QUEUE_ACTION_DEQUEUE) { sys_sfnode_t *node; node = sys_sflist_get_not_empty(&queue->data_q); @@ -339,24 +354,23 @@ void *z_impl_k_queue_get(struct k_queue *queue, k_timeout_t timeout) SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_queue, get, queue, timeout, data); return data; - } - - SYS_PORT_TRACING_OBJ_FUNC_BLOCKING(k_queue, get, queue, timeout); - - if (K_TIMEOUT_EQ(timeout, K_NO_WAIT)) { + } else if (d.action == GALE_QUEUE_ACTION_RETURN_NULL) { k_spin_unlock(&queue->lock, key); SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_queue, get, queue, timeout, NULL); return NULL; - } + } else { + /* PEND_CURRENT: block on wait queue with timeout */ + SYS_PORT_TRACING_OBJ_FUNC_BLOCKING(k_queue, get, queue, timeout); - int ret = z_pend_curr(&queue->lock, key, &queue->wait_q, timeout); + int ret = z_pend_curr(&queue->lock, key, &queue->wait_q, timeout); - SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_queue, get, queue, timeout, - (ret != 0) ? NULL : _current->base.swap_data); + SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_queue, get, queue, timeout, + (ret != 0) ? NULL : _current->base.swap_data); - return (ret != 0) ? NULL : _current->base.swap_data; + return (ret != 0) ? NULL : _current->base.swap_data; + } } bool k_queue_remove(struct k_queue *queue, void *data) From 05e8dfc63c18350636d67ebdf02e02a1d80995a5 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 20 Mar 2026 06:07:31 +0100 Subject: [PATCH 07/16] feat(shim): convert k_mbox put/get to decision struct pattern MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Rewrite mbox_message_put and k_mbox_get in gale_mbox.c to use the Extract→Decide→Apply pattern with Rust decision structs. C extracts kernel state (rx/tx queue scan, message matching), Rust decides the post-scan action (MATCHED vs RETURN_ENOMSG vs PEND), C applies it. Data movement (message copy, async descriptors) stays in C. Co-Authored-By: Claude Opus 4.6 (1M context) --- ffi/include/gale_mbox.h | 24 +++++++ zephyr/gale_mbox.c | 147 +++++++++++++++++++++++----------------- 2 files changed, 107 insertions(+), 64 deletions(-) diff --git a/ffi/include/gale_mbox.h b/ffi/include/gale_mbox.h index 3efcfba..d4632b5 100644 --- a/ffi/include/gale_mbox.h +++ b/ffi/include/gale_mbox.h @@ -49,6 +49,30 @@ int32_t gale_mbox_match_check(uint32_t send_id, uint32_t recv_id); */ uint32_t gale_mbox_data_exchange(uint32_t tx_size, uint32_t rx_buf_size); +/* ---- Phase 2: Full Decision API ---- */ + +struct gale_mbox_put_decision { + uint8_t action; /* 0=MATCHED, 1=RETURN_ENOMSG, 2=PEND_TX_QUEUE */ +}; + +#define GALE_MBOX_ACTION_MATCHED 0 +#define GALE_MBOX_ACTION_RETURN_ENOMSG 1 +#define GALE_MBOX_ACTION_PEND_TX 2 + +struct gale_mbox_put_decision gale_k_mbox_put_decide( + uint32_t matched, uint32_t is_no_wait); + +struct gale_mbox_get_decision { + uint8_t action; /* 0=MATCHED, 1=RETURN_ENOMSG, 2=PEND_RX_QUEUE */ +}; + +#define GALE_MBOX_ACTION_CONSUME 0 +/* GALE_MBOX_ACTION_RETURN_ENOMSG = 1 (shared with put) */ +#define GALE_MBOX_ACTION_PEND_RX 2 + +struct gale_mbox_get_decision gale_k_mbox_get_decide( + uint32_t matched, uint32_t is_no_wait); + #ifdef __cplusplus } #endif diff --git a/zephyr/gale_mbox.c b/zephyr/gale_mbox.c index ea28e14..d66e791 100644 --- a/zephyr/gale_mbox.c +++ b/zephyr/gale_mbox.c @@ -4,17 +4,21 @@ * * SPDX-License-Identifier: Apache-2.0 * - * Gale mailbox — verified stateless message validation. + * Gale mailbox — phase 2: Extract→Decide→Apply pattern. * - * This is kernel/mailbox.c with the message matching logic - * replaced by calls to the formally verified Rust implementation. - * Wait queues, scheduling, async message descriptors, data copy, - * and tracing remain native Zephyr. + * This is kernel/mailbox.c with mbox_message_put and k_mbox_get + * rewritten to use Rust decision structs. C extracts kernel state + * (spinlock, wait queue scan, message matching), Rust decides the + * post-scan action, C applies it. + * + * Data movement (message copy), async descriptors, and tracing + * remain native Zephyr. * * Verified operations (Verus proofs): - * gale_mbox_validate_send — MB1 (size > 0) - * gale_mbox_match_check — MB2-MB4 (K_ANY, equal, different) - * gale_mbox_data_exchange — MB5-MB6 (min computation) + * gale_mbox_match_check — MB2-MB4 (K_ANY, equal, different) + * gale_mbox_data_exchange — MB5-MB6 (min computation) + * gale_k_mbox_put_decide — post-scan put decision + * gale_k_mbox_get_decide — post-scan get decision */ #include @@ -183,13 +187,14 @@ static void mbox_message_dispose(struct k_mbox_msg *rx_msg) } /** - * @brief Send a mailbox message. + * @brief Send a mailbox message — Extract→Decide→Apply pattern. */ static int mbox_message_put(struct k_mbox *mbox, struct k_mbox_msg *tx_msg, k_timeout_t timeout) { struct k_thread *sending_thread; struct k_thread *receiving_thread; + struct k_thread *matched_receiver = NULL; struct k_mbox_msg *rx_msg; k_spinlock_key_t key; @@ -200,7 +205,7 @@ static int mbox_message_put(struct k_mbox *mbox, struct k_mbox_msg *tx_msg, sending_thread = tx_msg->_syncing_thread; sending_thread->base.swap_data = tx_msg; - /* search mailbox's rx queue for a compatible receiver */ + /* Extract: search mailbox's rx queue for a compatible receiver */ key = k_spin_lock(&mbox->lock); SYS_PORT_TRACING_OBJ_FUNC_ENTER(k_mbox, message_put, mbox, timeout); @@ -211,52 +216,60 @@ static int mbox_message_put(struct k_mbox *mbox, struct k_mbox_msg *tx_msg, if (mbox_message_match(tx_msg, rx_msg) == 0) { /* take receiver out of rx queue */ z_unpend_thread(receiving_thread); + matched_receiver = receiving_thread; + break; + } + } - /* ready receiver for execution */ - arch_thread_return_value_set(receiving_thread, 0); - z_ready_thread(receiving_thread); + /* Decide: Rust determines post-scan action */ + struct gale_mbox_put_decision d = gale_k_mbox_put_decide( + matched_receiver != NULL ? 1U : 0U, + K_TIMEOUT_EQ(timeout, K_NO_WAIT) ? 1U : 0U); + + /* Apply: execute Rust's decision */ + if (d.action == GALE_MBOX_ACTION_MATCHED) { + /* ready receiver for execution */ + arch_thread_return_value_set(matched_receiver, 0); + z_ready_thread(matched_receiver); #if (CONFIG_NUM_MBOX_ASYNC_MSGS > 0) - if ((sending_thread->base.thread_state & _THREAD_DUMMY) - != 0U) { - z_reschedule(&mbox->lock, key); - return 0; - } + if ((sending_thread->base.thread_state & _THREAD_DUMMY) + != 0U) { + z_reschedule(&mbox->lock, key); + return 0; + } #endif /* CONFIG_NUM_MBOX_ASYNC_MSGS */ - SYS_PORT_TRACING_OBJ_FUNC_BLOCKING(k_mbox, message_put, mbox, timeout); + SYS_PORT_TRACING_OBJ_FUNC_BLOCKING(k_mbox, message_put, mbox, timeout); - int ret = z_pend_curr(&mbox->lock, key, NULL, K_FOREVER); + int ret = z_pend_curr(&mbox->lock, key, NULL, K_FOREVER); - SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_mbox, message_put, mbox, timeout, ret); + SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_mbox, message_put, mbox, timeout, ret); - return ret; - } - } - - /* didn't find a matching receiver: don't wait for one */ - if (K_TIMEOUT_EQ(timeout, K_NO_WAIT)) { + return ret; + } else if (d.action == GALE_MBOX_ACTION_RETURN_ENOMSG) { SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_mbox, message_put, mbox, timeout, -ENOMSG); k_spin_unlock(&mbox->lock, key); return -ENOMSG; - } - + } else { + /* PEND_TX: sender waits on tx queue for receiver */ #if (CONFIG_NUM_MBOX_ASYNC_MSGS > 0) - /* asynchronous send: dummy thread waits on tx queue for receiver */ - if ((sending_thread->base.thread_state & _THREAD_DUMMY) != 0U) { - z_pend_thread(sending_thread, &mbox->tx_msg_queue, K_FOREVER); - k_spin_unlock(&mbox->lock, key); - return 0; - } + /* asynchronous send: dummy thread waits on tx queue */ + if ((sending_thread->base.thread_state & _THREAD_DUMMY) != 0U) { + z_pend_thread(sending_thread, &mbox->tx_msg_queue, K_FOREVER); + k_spin_unlock(&mbox->lock, key); + return 0; + } #endif /* CONFIG_NUM_MBOX_ASYNC_MSGS */ - SYS_PORT_TRACING_OBJ_FUNC_BLOCKING(k_mbox, message_put, mbox, timeout); + SYS_PORT_TRACING_OBJ_FUNC_BLOCKING(k_mbox, message_put, mbox, timeout); - /* synchronous send: sender waits on tx queue for receiver or timeout */ - int ret = z_pend_curr(&mbox->lock, key, &mbox->tx_msg_queue, timeout); + /* synchronous send: sender waits on tx queue for receiver or timeout */ + int ret = z_pend_curr(&mbox->lock, key, &mbox->tx_msg_queue, timeout); - SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_mbox, message_put, mbox, timeout, ret); + SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_mbox, message_put, mbox, timeout, ret); - return ret; + return ret; + } } int k_mbox_put(struct k_mbox *mbox, struct k_mbox_msg *tx_msg, @@ -333,6 +346,7 @@ int k_mbox_get(struct k_mbox *mbox, struct k_mbox_msg *rx_msg, void *buffer, k_timeout_t timeout) { struct k_thread *sending_thread; + struct k_thread *matched_sender = NULL; struct k_mbox_msg *tx_msg; k_spinlock_key_t key; int result; @@ -340,7 +354,7 @@ int k_mbox_get(struct k_mbox *mbox, struct k_mbox_msg *rx_msg, void *buffer, /* save receiver id so it can be used during message matching */ rx_msg->tx_target_thread = _current; - /* search mailbox's tx queue for a compatible sender */ + /* Extract: search mailbox's tx queue for a compatible sender */ key = k_spin_lock(&mbox->lock); SYS_PORT_TRACING_OBJ_FUNC_ENTER(k_mbox, get, mbox, timeout); @@ -351,41 +365,46 @@ int k_mbox_get(struct k_mbox *mbox, struct k_mbox_msg *rx_msg, void *buffer, if (mbox_message_match(tx_msg, rx_msg) == 0) { /* take sender out of mailbox's tx queue */ z_unpend_thread(sending_thread); - - k_spin_unlock(&mbox->lock, key); - - /* consume message data immediately, if needed */ - result = mbox_message_data_check(rx_msg, buffer); - - SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_mbox, get, mbox, timeout, result); - return result; + matched_sender = sending_thread; + break; } } - /* didn't find a matching sender */ + /* Decide: Rust determines post-scan action */ + struct gale_mbox_get_decision d = gale_k_mbox_get_decide( + matched_sender != NULL ? 1U : 0U, + K_TIMEOUT_EQ(timeout, K_NO_WAIT) ? 1U : 0U); + + /* Apply: execute Rust's decision */ + if (d.action == GALE_MBOX_ACTION_CONSUME) { + k_spin_unlock(&mbox->lock, key); + + /* consume message data immediately, if needed */ + result = mbox_message_data_check(rx_msg, buffer); - if (K_TIMEOUT_EQ(timeout, K_NO_WAIT)) { + SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_mbox, get, mbox, timeout, result); + return result; + } else if (d.action == GALE_MBOX_ACTION_RETURN_ENOMSG) { SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_mbox, get, mbox, timeout, -ENOMSG); - /* don't wait for a matching sender to appear */ k_spin_unlock(&mbox->lock, key); return -ENOMSG; - } - - SYS_PORT_TRACING_OBJ_FUNC_BLOCKING(k_mbox, get, mbox, timeout); + } else { + /* PEND_RX: wait until a matching sender appears or timeout */ + SYS_PORT_TRACING_OBJ_FUNC_BLOCKING(k_mbox, get, mbox, timeout); - /* wait until a matching sender appears or a timeout occurs */ - _current->base.swap_data = rx_msg; - result = z_pend_curr(&mbox->lock, key, &mbox->rx_msg_queue, timeout); + _current->base.swap_data = rx_msg; + result = z_pend_curr(&mbox->lock, key, &mbox->rx_msg_queue, timeout); - /* consume message data immediately, if needed */ - if (result == 0) { - result = mbox_message_data_check(rx_msg, buffer); - } + /* consume message data immediately, if needed */ + if (result == 0) { + result = mbox_message_data_check(rx_msg, buffer); + } - SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_mbox, get, mbox, timeout, result); + SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_mbox, get, mbox, timeout, result); - return result; + return result; + } } #ifdef CONFIG_OBJ_CORE_MAILBOX From b902af9c6256cf777c890329b564fac139515ff5 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 20 Mar 2026 06:10:08 +0100 Subject: [PATCH 08/16] feat(shim): convert timeout to decision struct pattern Replace raw pointer output params in gale_timeout_add/abort/announce with decision structs (GaleTimeoutAddDecision, GaleTimeoutAbortDecision, GaleTimeoutAnnounceDecision) following the Extract->Decide->Apply pattern. Legacy pointer-based API retained as thin wrappers for backward compat. Co-Authored-By: Claude Opus 4.6 (1M context) --- ffi/include/gale_timeout.h | 62 +++++++++++ ffi/src/lib.rs | 208 ++++++++++++++++++++++++++----------- zephyr/gale_timeout.c | 79 ++++++++++++-- 3 files changed, 277 insertions(+), 72 deletions(-) diff --git a/ffi/include/gale_timeout.h b/ffi/include/gale_timeout.h index 295e3a5..4963cc5 100644 --- a/ffi/include/gale_timeout.h +++ b/ffi/include/gale_timeout.h @@ -1,6 +1,8 @@ /* * Gale Timeout FFI — verified tick arithmetic and deadline tracking. * + * Phase 2: Decision struct pattern for Extract->Decide->Apply. + * * SPDX-License-Identifier: Apache-2.0 */ @@ -13,6 +15,66 @@ extern "C" { #endif +/* ---- Phase 2: Timeout Decision API ---- */ + +/** + * Decision struct for z_add_timeout — computed deadline. + */ +struct gale_timeout_add_decision { + int32_t ret; /* 0 (OK), -EINVAL (overflow) */ + uint64_t deadline; /* absolute deadline (valid when ret == 0) */ +}; + +/** + * Compute absolute deadline from current tick + duration. + * + * Verified: TO2 (deadline = current_tick + duration), TO5 (no overflow). + */ +struct gale_timeout_add_decision gale_timeout_add_decide( + uint64_t current_tick, uint64_t duration); + +/** + * Decision struct for z_abort_timeout — whether abort is valid. + */ +struct gale_timeout_abort_decision { + int32_t ret; /* 0 (OK, was active), -EINVAL (already inactive) */ + uint8_t action; /* 0=DO_REMOVE, 1=NOOP */ +}; + +#define GALE_TIMEOUT_ACTION_REMOVE 0 +#define GALE_TIMEOUT_ACTION_NOOP 1 + +/** + * Decide whether to abort a pending timeout. + * + * @param is_linked 1 if timeout node is linked (active), 0 if inactive. + * + * Verified: TO3 (abort clears to inactive). + */ +struct gale_timeout_abort_decision gale_timeout_abort_decide( + uint32_t is_linked); + +/** + * Decision struct for sys_clock_announce — new tick and expiry status. + */ +struct gale_timeout_announce_decision { + int32_t ret; /* 0 (OK), -EINVAL (overflow) */ + uint64_t new_tick; /* advanced tick value */ + uint32_t fired; /* 1 if expired, 0 otherwise */ +}; + +/** + * Advance tick and check if a timeout has expired. + * + * Verified: TO4 (fires when deadline <= now), TO5 (no overflow), + * TO7 (K_FOREVER never expires). + */ +struct gale_timeout_announce_decision gale_timeout_announce_decide( + uint64_t current_tick, uint64_t ticks, + uint64_t deadline, uint32_t active); + +/* ---- Legacy API (kept for backward compatibility) ---- */ + /** * Schedule a timeout: compute absolute deadline from current tick + duration. * diff --git a/ffi/src/lib.rs b/ffi/src/lib.rs index fa9aa0e..cc0d031 100644 --- a/ffi/src/lib.rs +++ b/ffi/src/lib.rs @@ -2855,19 +2855,145 @@ pub extern "C" fn gale_k_mbox_get_decide( const K_FOREVER_TICKS: u64 = u64::MAX; -/// Schedule a timeout: compute absolute deadline from current tick + duration. +// ---- Phase 2: Timeout Decision API ---- + +/// Decision struct for z_add_timeout — tells C shim the computed deadline. +#[repr(C)] +pub struct GaleTimeoutAddDecision { + /// Return code: 0 (OK), -EINVAL (overflow) + pub ret: i32, + /// Computed absolute deadline (only meaningful when ret == 0) + pub deadline: u64, +} + +/// Compute absolute deadline from current tick + duration. /// /// timeout.c z_add_timeout: -/// deadline = curr_tick + duration +/// C extracts current_tick and duration, Rust computes the deadline. /// -/// Arguments: -/// current_tick: current system tick -/// duration: relative timeout in ticks -/// deadline: pointer to receive absolute deadline +/// Verified: TO2 (deadline = current_tick + duration), TO5 (no overflow). +#[unsafe(no_mangle)] +pub extern "C" fn gale_timeout_add_decide( + current_tick: u64, + duration: u64, +) -> GaleTimeoutAddDecision { + if current_tick >= K_FOREVER_TICKS { + return GaleTimeoutAddDecision { + ret: EINVAL, + deadline: 0, + }; + } + + if duration >= K_FOREVER_TICKS - current_tick { + return GaleTimeoutAddDecision { + ret: EINVAL, + deadline: 0, + }; + } + + #[allow(clippy::arithmetic_side_effects)] + let dl = current_tick + duration; + GaleTimeoutAddDecision { + ret: OK, + deadline: dl, + } +} + +/// Decision struct for z_abort_timeout — tells C shim whether abort is valid. +#[repr(C)] +pub struct GaleTimeoutAbortDecision { + /// Return code: 0 (OK, was active), -EINVAL (already inactive) + pub ret: i32, + /// Action: 0=DO_REMOVE (remove from list), 1=NOOP (already inactive) + pub action: u8, +} + +pub const GALE_TIMEOUT_ACTION_REMOVE: u8 = 0; +pub const GALE_TIMEOUT_ACTION_NOOP: u8 = 1; + +/// Decide whether to abort a pending timeout. /// -/// Returns: -/// 0 (OK) — *deadline set to current_tick + duration -/// -EINVAL — overflow (current_tick + duration >= u64::MAX) +/// timeout.c z_abort_timeout: +/// C extracts whether the timeout node is linked (active). +/// Rust decides: remove or noop. +/// +/// Verified: TO3 (abort clears to inactive). +#[unsafe(no_mangle)] +pub extern "C" fn gale_timeout_abort_decide( + is_linked: u32, +) -> GaleTimeoutAbortDecision { + if is_linked != 0 { + GaleTimeoutAbortDecision { + ret: OK, + action: GALE_TIMEOUT_ACTION_REMOVE, + } + } else { + GaleTimeoutAbortDecision { + ret: EINVAL, + action: GALE_TIMEOUT_ACTION_NOOP, + } + } +} + +/// Decision struct for sys_clock_announce — tells C shim the new tick and +/// whether a specific timeout has expired. +#[repr(C)] +pub struct GaleTimeoutAnnounceDecision { + /// Return code: 0 (OK), -EINVAL (overflow) + pub ret: i32, + /// Advanced tick value (current_tick + ticks) + pub new_tick: u64, + /// 1 if the timeout fired (deadline <= new_tick), 0 otherwise + pub fired: u32, +} + +/// Advance tick and check if a timeout has expired. +/// +/// timeout.c sys_clock_announce: +/// C extracts current_tick, ticks to advance, deadline, and active flag. +/// Rust computes new_tick and whether the timeout fired. +/// +/// Verified: TO4 (fires when deadline <= now), TO5 (no overflow), +/// TO7 (K_FOREVER never expires). +#[unsafe(no_mangle)] +pub extern "C" fn gale_timeout_announce_decide( + current_tick: u64, + ticks: u64, + deadline: u64, + active: u32, +) -> GaleTimeoutAnnounceDecision { + if ticks >= K_FOREVER_TICKS - current_tick { + return GaleTimeoutAnnounceDecision { + ret: EINVAL, + new_tick: 0, + fired: 0, + }; + } + + #[allow(clippy::arithmetic_side_effects)] + let advanced = current_tick + ticks; + + let fired = if active != 0 + && deadline != K_FOREVER_TICKS + && deadline <= advanced + { + 1u32 + } else { + 0u32 + }; + + GaleTimeoutAnnounceDecision { + ret: OK, + new_tick: advanced, + fired, + } +} + +// ---- Legacy API (kept for backward compatibility) ---- + +/// Schedule a timeout: compute absolute deadline from current tick + duration. +/// +/// Delegates to gale_timeout_add_decide. #[unsafe(no_mangle)] pub extern "C" fn gale_timeout_add( current_tick: u64, @@ -2879,58 +3005,27 @@ pub extern "C" fn gale_timeout_add( return EINVAL; } - if current_tick >= K_FOREVER_TICKS { - return EINVAL; - } - - if duration >= K_FOREVER_TICKS - current_tick { - return EINVAL; + let d = gale_timeout_add_decide(current_tick, duration); + if d.ret != OK { + return d.ret; } - #[allow(clippy::arithmetic_side_effects)] - { - *deadline = current_tick + duration; - } + *deadline = d.deadline; OK } } /// Abort a pending timeout. /// -/// timeout.c z_abort_timeout: -/// Sets timeout to inactive. -/// -/// Arguments: -/// active: 1 if timeout is active, 0 if inactive -/// -/// Returns: -/// 0 (OK) — timeout was active and is now cancelled -/// -EINVAL — timeout was already inactive +/// Delegates to gale_timeout_abort_decide. #[unsafe(no_mangle)] pub extern "C" fn gale_timeout_abort(active: u32) -> i32 { - if active != 0 { - OK - } else { - EINVAL - } + gale_timeout_abort_decide(active).ret } /// Advance tick and check if a timeout has expired. /// -/// timeout.c sys_clock_announce: -/// curr_tick += ticks; fire if deadline <= curr_tick -/// -/// Arguments: -/// current_tick: current system tick -/// ticks: ticks to advance -/// deadline: absolute deadline of this timeout -/// active: 1 if timeout is active -/// new_tick: pointer to receive advanced tick -/// fired: pointer to receive 1 if expired, 0 otherwise -/// -/// Returns: -/// 0 (OK) — *new_tick and *fired set -/// -EINVAL — overflow or null pointer +/// Delegates to gale_timeout_announce_decide. #[unsafe(no_mangle)] pub extern "C" fn gale_timeout_announce( current_tick: u64, @@ -2945,22 +3040,13 @@ pub extern "C" fn gale_timeout_announce( return EINVAL; } - if ticks >= K_FOREVER_TICKS - current_tick { - return EINVAL; + let d = gale_timeout_announce_decide(current_tick, ticks, deadline, active); + if d.ret != OK { + return d.ret; } - #[allow(clippy::arithmetic_side_effects)] - let advanced = current_tick + ticks; - *new_tick = advanced; - - if active != 0 - && deadline != K_FOREVER_TICKS - && deadline <= advanced - { - *fired = 1; - } else { - *fired = 0; - } + *new_tick = d.new_tick; + *fired = d.fired; OK } } diff --git a/zephyr/gale_timeout.c b/zephyr/gale_timeout.c index 61cb440..5fffd5b 100644 --- a/zephyr/gale_timeout.c +++ b/zephyr/gale_timeout.c @@ -1,25 +1,82 @@ /* + * Copyright (c) 2018 Intel Corporation * Copyright (c) 2026 PulseEngine * * SPDX-License-Identifier: Apache-2.0 * - * Gale timeout — verified tick arithmetic and deadline tracking. + * Gale timeout — phase 2: Extract->Decide->Apply pattern. * - * This C shim provides the glue between Zephyr's timeout subsystem - * and the formally verified Rust FFI. The actual timeout linked-list, - * spinlock, callback dispatch, and hardware timer remain in Zephyr. + * This is kernel/timeout.c with the safety-critical tick arithmetic + * delegated to Rust decision structs. C extracts kernel state + * (spinlock, timeout list, hardware timer), Rust decides the + * arithmetic result, C applies it. * * Verified operations (Verus proofs): - * gale_timeout_add — TO2 (deadline computation), TO5 (no overflow) - * gale_timeout_abort — TO3 (deactivate) - * gale_timeout_announce — TO4 (fire expired), TO5 (no overflow) + * gale_timeout_add_decide — TO2 (deadline computation), TO5 (no overflow) + * gale_timeout_abort_decide — TO3 (deactivate) + * gale_timeout_announce_decide — TO4 (fire expired), TO5 (no overflow), + * TO7 (K_FOREVER never expires) + * + * All other timeout logic (linked-list, spinlock, callbacks, hardware timer) + * remains native Zephyr C — only the arithmetic is verified. */ #include "gale_timeout.h" /* - * The FFI functions are linked directly from libgale_ffi.a. - * This file exists as a build target for the Zephyr module system. - * Kernel integration will call gale_timeout_add/abort/announce - * from the modified timeout.c. + * The decision-struct FFI functions are linked directly from libgale_ffi.a: + * + * gale_timeout_add_decide() — compute deadline from tick + duration + * gale_timeout_abort_decide() — validate abort (is node linked?) + * gale_timeout_announce_decide() — advance tick, check expiry + * + * This file serves as the Zephyr module build target. The actual + * integration point is in the modified kernel/timeout.c, which calls + * these decision functions at the Extract->Decide->Apply boundaries. + * + * Example integration in kernel/timeout.c z_add_timeout(): + * + * // Extract: read curr_tick, compute duration + * uint64_t tick = curr_tick; + * uint64_t dur = timeout.ticks + 1 + ticks_elapsed; + * + * // Decide: Rust validates overflow and computes deadline + * struct gale_timeout_add_decision d = + * gale_timeout_add_decide(tick, dur); + * if (d.ret != 0) { return 0; } // overflow — treat as forever + * + * // Apply: set dticks from verified deadline + * to->dticks = d.deadline - curr_tick; + * + * Example integration in kernel/timeout.c z_abort_timeout(): + * + * // Extract: check if node is linked + * uint32_t linked = sys_dnode_is_linked(&to->node) ? 1U : 0U; + * + * // Decide: Rust validates the abort + * struct gale_timeout_abort_decision d = + * gale_timeout_abort_decide(linked); + * + * // Apply: only remove if Rust says DO_REMOVE + * if (d.action == GALE_TIMEOUT_ACTION_REMOVE) { + * remove_timeout(to); + * to->dticks = TIMEOUT_DTICKS_ABORTED; + * ret = 0; + * } + * + * Example integration in kernel/timeout.c sys_clock_announce(): + * + * // Extract: read curr_tick, dticks of first timeout + * uint64_t tick = curr_tick; + * uint64_t dt = (uint64_t)t->dticks; + * + * // Decide: Rust computes new tick and checks expiry + * struct gale_timeout_announce_decision d = + * gale_timeout_announce_decide(tick, dt, deadline, active); + * + * // Apply: advance tick, fire if decided + * if (d.ret == 0) { + * curr_tick = d.new_tick; + * if (d.fired) { remove_timeout(t); t->fn(t); } + * } */ From 5056aecae0a5f56216f1fc087d5c523d9ee105ee Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 20 Mar 2026 06:11:18 +0100 Subject: [PATCH 09/16] feat(shim): convert k_msgq put/get to decision struct pattern Rewrite z_impl_k_msgq_put and z_impl_k_msgq_get to use the Extract-Decide-Apply pattern: C extracts kernel state (spinlock, wait queue side effects), Rust decides the action via decision structs, C applies the result. - GaleMsgqPutDecision: PUT_OK / WAKE_READER / PEND_CURRENT / RETURN_FULL - GaleMsgqGetDecision: GET_OK / WAKE_WRITER / PEND_CURRENT / RETURN_EMPTY - put_front stays with Phase 1 API (always K_NO_WAIT, no decision needed) - Data copy (memcpy) remains in C; Rust decides index/count updates Co-Authored-By: Claude Opus 4.6 (1M context) --- ffi/include/gale_msgq.h | 34 +++++ zephyr/gale_msgq.c | 273 ++++++++++++++++++++++------------------ 2 files changed, 187 insertions(+), 120 deletions(-) diff --git a/ffi/include/gale_msgq.h b/ffi/include/gale_msgq.h index a97e5d5..8d9fcbf 100644 --- a/ffi/include/gale_msgq.h +++ b/ffi/include/gale_msgq.h @@ -109,6 +109,40 @@ int32_t gale_msgq_peek_at(uint32_t read_idx, uint32_t idx, uint32_t *slot_idx); +/* ---- Phase 2: Full Decision API ---- */ + +struct gale_msgq_put_decision { + int32_t ret; + uint8_t action; /* 0=PUT_OK, 1=WAKE_READER, 2=PEND_CURRENT, 3=RETURN_FULL */ + uint32_t new_write_idx; + uint32_t new_used; +}; + +#define GALE_MSGQ_ACTION_PUT_OK 0 +#define GALE_MSGQ_ACTION_WAKE_READER 1 +#define GALE_MSGQ_ACTION_PUT_PEND 2 +#define GALE_MSGQ_ACTION_RETURN_FULL 3 + +struct gale_msgq_put_decision gale_k_msgq_put_decide( + uint32_t write_idx, uint32_t used_msgs, uint32_t max_msgs, + uint32_t has_waiter, uint32_t is_no_wait); + +struct gale_msgq_get_decision { + int32_t ret; + uint8_t action; /* 0=GET_OK, 1=WAKE_WRITER, 2=PEND_CURRENT, 3=RETURN_EMPTY */ + uint32_t new_read_idx; + uint32_t new_used; +}; + +#define GALE_MSGQ_ACTION_GET_OK 0 +#define GALE_MSGQ_ACTION_WAKE_WRITER 1 +#define GALE_MSGQ_ACTION_GET_PEND 2 +#define GALE_MSGQ_ACTION_RETURN_EMPTY 3 + +struct gale_msgq_get_decision gale_k_msgq_get_decide( + uint32_t read_idx, uint32_t used_msgs, uint32_t max_msgs, + uint32_t has_waiter, uint32_t is_no_wait); + #ifdef __cplusplus } #endif diff --git a/zephyr/gale_msgq.c b/zephyr/gale_msgq.c index 7c9a8e2..3c47c70 100644 --- a/zephyr/gale_msgq.c +++ b/zephyr/gale_msgq.c @@ -140,24 +140,91 @@ int k_msgq_cleanup(struct k_msgq *msgq) } /* ----------------------------------------------------------------------- - * put_msg_in_queue (replaces msg_q.c:130-228) + * z_impl_k_msgq_put (decision struct pattern) * - * Core logic: if space available, delegate index math to verified Rust. + * Extract: spinlock, try unpend waiter (side effect). + * Decide: Rust determines action via gale_k_msgq_put_decide. + * Apply: C executes the decision (memcpy, wake, pend, or return). * ----------------------------------------------------------------------- */ -static inline int put_msg_in_queue(struct k_msgq *msgq, const void *data, - k_timeout_t timeout, bool put_at_back) +int z_impl_k_msgq_put(struct k_msgq *msgq, const void *data, + k_timeout_t timeout) { __ASSERT(!arch_is_in_isr() || K_TIMEOUT_EQ(timeout, K_NO_WAIT), ""); k_spinlock_key_t key = k_spin_lock(&msgq->lock); - int result; bool resched = false; SYS_PORT_TRACING_OBJ_FUNC_ENTER(k_msgq, put, msgq, timeout); + /* Extract: try to unpend first waiter (side effect: removes from queue) */ + struct k_thread *pending_thread = z_unpend_first_thread(&msgq->wait_q); + + /* Decide: Rust determines action */ + struct gale_msgq_put_decision d = gale_k_msgq_put_decide( + ptr_to_slot(msgq, msgq->write_ptr), + msgq->used_msgs, + msgq->max_msgs, + pending_thread != NULL ? 1U : 0U, + K_TIMEOUT_EQ(timeout, K_NO_WAIT) ? 1U : 0U); + + /* Apply: execute Rust's decision */ + if (d.action == GALE_MSGQ_ACTION_WAKE_READER) { + /* A receiver was waiting — copy directly to it. */ + (void)memcpy(pending_thread->base.swap_data, + data, msgq->msg_size); + arch_thread_return_value_set(pending_thread, 0); + z_ready_thread(pending_thread); + resched = true; + } else if (d.action == GALE_MSGQ_ACTION_PUT_OK) { + /* Space available — put in ring buffer at write slot. */ + (void)memcpy(msgq->write_ptr, data, msgq->msg_size); + msgq->write_ptr = slot_to_ptr(msgq, d.new_write_idx); + msgq->used_msgs = d.new_used; +#ifdef CONFIG_POLL + resched = z_handle_obj_poll_events( + &msgq->poll_events, K_POLL_STATE_MSGQ_DATA_AVAILABLE); +#endif + } else if (d.action == GALE_MSGQ_ACTION_PUT_PEND) { + /* Queue full, blocking — pend current thread. */ + SYS_PORT_TRACING_OBJ_FUNC_BLOCKING(k_msgq, put, msgq, timeout); + _current->base.swap_data = (void *)data; + int result = z_pend_curr(&msgq->lock, key, + &msgq->wait_q, timeout); + SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_msgq, put, msgq, result); + return result; + } else { + /* RETURN_FULL: queue full, non-blocking. */ + SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_msgq, put, msgq, d.ret); + k_spin_unlock(&msgq->lock, key); + return d.ret; + } + + SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_msgq, put, msgq, 0); + + if (resched) { + z_reschedule(&msgq->lock, key); + } else { + k_spin_unlock(&msgq->lock, key); + } + + return 0; +} + +/* ----------------------------------------------------------------------- + * z_impl_k_msgq_put_front (uses Phase 1 gale_msgq_put_front) + * + * Always K_NO_WAIT — no decision struct needed. Same pattern as before. + * ----------------------------------------------------------------------- */ + +static inline int put_front_in_queue(struct k_msgq *msgq, const void *data) +{ + k_spinlock_key_t key = k_spin_lock(&msgq->lock); + bool resched = false; + + SYS_PORT_TRACING_OBJ_FUNC_ENTER(k_msgq, put, msgq, K_NO_WAIT); + if (msgq->used_msgs < msgq->max_msgs) { - /* Queue has space. */ struct k_thread *pending_thread; pending_thread = z_unpend_first_thread(&msgq->wait_q); @@ -169,30 +236,6 @@ static inline int put_msg_in_queue(struct k_msgq *msgq, const void *data, arch_thread_return_value_set(pending_thread, 0); z_ready_thread(pending_thread); resched = true; - } else if (put_at_back) { - /* Put at back: memcpy to current write slot, - * then advance write index via verified Rust. - */ - (void)memcpy(msgq->write_ptr, data, msgq->msg_size); - - uint32_t new_write_idx, new_used; - uint32_t cur_write = ptr_to_slot(msgq, msgq->write_ptr); - - int rc = gale_msgq_put(cur_write, - msgq->used_msgs, - msgq->max_msgs, - &new_write_idx, - &new_used); - __ASSERT(rc == 0, "gale_msgq_put: %d", rc); - ARG_UNUSED(rc); - - msgq->write_ptr = slot_to_ptr(msgq, new_write_idx); - msgq->used_msgs = new_used; - -#ifdef CONFIG_POLL - resched = z_handle_obj_poll_events( - &msgq->poll_events, K_POLL_STATE_MSGQ_DATA_AVAILABLE); -#endif } else { /* Put at front: retreat read index via verified Rust, * then memcpy to new read slot. @@ -215,46 +258,25 @@ static inline int put_msg_in_queue(struct k_msgq *msgq, const void *data, #ifdef CONFIG_POLL resched = z_handle_obj_poll_events( - &msgq->poll_events, K_POLL_STATE_MSGQ_DATA_AVAILABLE); + &msgq->poll_events, + K_POLL_STATE_MSGQ_DATA_AVAILABLE); #endif } - result = 0; - } else if (K_TIMEOUT_EQ(timeout, K_NO_WAIT)) { - /* Queue full, non-blocking. */ - SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_msgq, put, msgq, -ENOMSG); - result = -ENOMSG; - } else { - /* Queue full, blocking — pend current thread. */ - SYS_PORT_TRACING_OBJ_FUNC_BLOCKING(k_msgq, put, msgq, timeout); - - _current->base.swap_data = (void *)data; - result = z_pend_curr(&msgq->lock, key, - &msgq->wait_q, timeout); - - SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_msgq, put, msgq, result); - return result; - } - - SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_msgq, put, msgq, result); + SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_msgq, put, msgq, 0); - if (resched) { - z_reschedule(&msgq->lock, key); - } else { - k_spin_unlock(&msgq->lock, key); + if (resched) { + z_reschedule(&msgq->lock, key); + } else { + k_spin_unlock(&msgq->lock, key); + } + return 0; } - return result; -} - -/* ----------------------------------------------------------------------- - * Public put APIs - * ----------------------------------------------------------------------- */ - -int z_impl_k_msgq_put(struct k_msgq *msgq, const void *data, - k_timeout_t timeout) -{ - return put_msg_in_queue(msgq, data, timeout, true); + /* Queue full — non-blocking always. */ + SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_msgq, put, msgq, -ENOMSG); + k_spin_unlock(&msgq->lock, key); + return -ENOMSG; } #ifdef CONFIG_USERSPACE @@ -271,7 +293,7 @@ static inline int z_vrfy_k_msgq_put(struct k_msgq *msgq, const void *data, int z_impl_k_msgq_put_front(struct k_msgq *msgq, const void *data) { - return put_msg_in_queue(msgq, data, K_NO_WAIT, false); + return put_front_in_queue(msgq, data); } #ifdef CONFIG_USERSPACE @@ -290,86 +312,97 @@ static inline int z_vrfy_k_msgq_put_front(struct k_msgq *msgq, * k_msgq_get (replaces msg_q.c:280-349) * ----------------------------------------------------------------------- */ +/* ----------------------------------------------------------------------- + * z_impl_k_msgq_get (decision struct pattern) + * + * Extract: spinlock, try unpend writer (side effect — only when used > 0). + * Decide: Rust determines action via gale_k_msgq_get_decide. + * Apply: C executes the decision (memcpy, wake writer, pend, or return). + * ----------------------------------------------------------------------- */ + int z_impl_k_msgq_get(struct k_msgq *msgq, void *data, k_timeout_t timeout) { __ASSERT(!arch_is_in_isr() || K_TIMEOUT_EQ(timeout, K_NO_WAIT), ""); k_spinlock_key_t key = k_spin_lock(&msgq->lock); - int result; bool resched = false; SYS_PORT_TRACING_OBJ_FUNC_ENTER(k_msgq, get, msgq, timeout); + /* Extract: only check for pending writer if queue has messages + * (a writer can only be pending when the queue was full). + */ + struct k_thread *pending_thread = NULL; + if (msgq->used_msgs > 0U) { - /* Queue has messages — copy from read slot. */ + pending_thread = z_unpend_first_thread(&msgq->wait_q); + } + + /* Decide: Rust determines action */ + struct gale_msgq_get_decision d = gale_k_msgq_get_decide( + ptr_to_slot(msgq, msgq->read_ptr), + msgq->used_msgs, + msgq->max_msgs, + pending_thread != NULL ? 1U : 0U, + K_TIMEOUT_EQ(timeout, K_NO_WAIT) ? 1U : 0U); + + /* Apply: execute Rust's decision */ + if (d.action == GALE_MSGQ_ACTION_WAKE_WRITER) { + /* Messages available + writer waiting. + * 1. Copy message from read slot to caller. + * 2. Advance read index per decision. + * 3. Copy writer's message into write slot. + * 4. Advance write index via Phase 1 gale_msgq_put. + * 5. Wake the writer. + */ (void)memcpy(data, msgq->read_ptr, msgq->msg_size); + msgq->read_ptr = slot_to_ptr(msgq, d.new_read_idx); + msgq->used_msgs = d.new_used; - /* Advance read index via verified Rust. */ - uint32_t new_read_idx, new_used; - uint32_t cur_read = ptr_to_slot(msgq, msgq->read_ptr); + /* Accept the pending writer's message. */ + (void)memcpy(msgq->write_ptr, + (char *)pending_thread->base.swap_data, + msgq->msg_size); - int rc = gale_msgq_get(cur_read, + uint32_t new_write_idx, new_used2; + uint32_t cur_write = ptr_to_slot(msgq, msgq->write_ptr); + + int rc = gale_msgq_put(cur_write, msgq->used_msgs, msgq->max_msgs, - &new_read_idx, - &new_used); - __ASSERT(rc == 0, "gale_msgq_get: %d", rc); + &new_write_idx, + &new_used2); + __ASSERT(rc == 0, "gale_msgq_put (sender): %d", rc); ARG_UNUSED(rc); - msgq->read_ptr = slot_to_ptr(msgq, new_read_idx); - msgq->used_msgs = new_used; - - /* Check for pending sender. */ - struct k_thread *pending_thread; - - pending_thread = z_unpend_first_thread(&msgq->wait_q); - if (pending_thread != NULL) { - /* A sender was waiting — copy its message into the - * queue at the current write slot. - */ - (void)memcpy(msgq->write_ptr, - (char *)pending_thread->base.swap_data, - msgq->msg_size); - - /* Advance write index via verified Rust. */ - uint32_t new_write_idx, new_used2; - uint32_t cur_write = ptr_to_slot(msgq, - msgq->write_ptr); - - rc = gale_msgq_put(cur_write, - msgq->used_msgs, - msgq->max_msgs, - &new_write_idx, - &new_used2); - __ASSERT(rc == 0, "gale_msgq_put (sender): %d", rc); + msgq->write_ptr = slot_to_ptr(msgq, new_write_idx); + msgq->used_msgs = new_used2; - msgq->write_ptr = slot_to_ptr(msgq, new_write_idx); - msgq->used_msgs = new_used2; - - arch_thread_return_value_set(pending_thread, 0); - z_ready_thread(pending_thread); - resched = true; - } - - result = 0; - } else if (K_TIMEOUT_EQ(timeout, K_NO_WAIT)) { - /* Queue empty, non-blocking. */ - SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_msgq, get, msgq, -ENOMSG); - result = -ENOMSG; - } else { + arch_thread_return_value_set(pending_thread, 0); + z_ready_thread(pending_thread); + resched = true; + } else if (d.action == GALE_MSGQ_ACTION_GET_OK) { + /* Messages available, no pending writer. */ + (void)memcpy(data, msgq->read_ptr, msgq->msg_size); + msgq->read_ptr = slot_to_ptr(msgq, d.new_read_idx); + msgq->used_msgs = d.new_used; + } else if (d.action == GALE_MSGQ_ACTION_GET_PEND) { /* Queue empty, blocking — pend current thread. */ SYS_PORT_TRACING_OBJ_FUNC_BLOCKING(k_msgq, get, msgq, timeout); - _current->base.swap_data = data; - result = z_pend_curr(&msgq->lock, key, - &msgq->wait_q, timeout); - + int result = z_pend_curr(&msgq->lock, key, + &msgq->wait_q, timeout); SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_msgq, get, msgq, result); return result; + } else { + /* RETURN_EMPTY: queue empty, non-blocking. */ + SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_msgq, get, msgq, d.ret); + k_spin_unlock(&msgq->lock, key); + return d.ret; } - SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_msgq, get, msgq, result); + SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_msgq, get, msgq, 0); if (resched) { z_reschedule(&msgq->lock, key); @@ -377,7 +410,7 @@ int z_impl_k_msgq_get(struct k_msgq *msgq, void *data, k_spin_unlock(&msgq->lock, key); } - return result; + return 0; } #ifdef CONFIG_USERSPACE From 69fee98c66ed9e56d4055c97c600fdea5be07278 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 20 Mar 2026 06:12:30 +0100 Subject: [PATCH 10/16] feat(shim): convert k_mutex lock/unlock to decision struct pattern Rust decides the lock/unlock action via GaleMutexLockDecision and GaleMutexUnlockDecision structs; C applies the decision including priority inheritance adjustments. Overflow protection preserved. Co-Authored-By: Claude Opus 4.6 (1M context) --- ffi/include/gale_mutex.h | 46 ++++++++++++++++++++++++++ zephyr/gale_mutex.c | 70 +++++++++++++++++----------------------- 2 files changed, 76 insertions(+), 40 deletions(-) diff --git a/ffi/include/gale_mutex.h b/ffi/include/gale_mutex.h index 6f0c5fc..34d1bd6 100644 --- a/ffi/include/gale_mutex.h +++ b/ffi/include/gale_mutex.h @@ -75,6 +75,52 @@ int32_t gale_mutex_unlock_validate(uint32_t lock_count, uint32_t owner_is_current, uint32_t *new_lock_count); +/* ---- Phase 2: Full Decision API ---- */ + +struct gale_mutex_lock_decision { + int32_t ret; + uint8_t action; /* 0=ACQUIRED, 1=PEND_CURRENT, 2=RETURN_BUSY */ + uint32_t new_lock_count; +}; + +#define GALE_MUTEX_ACTION_ACQUIRED 0 +#define GALE_MUTEX_ACTION_PEND 1 +#define GALE_MUTEX_ACTION_BUSY 2 + +/** + * Decide the action for a mutex lock attempt. + * + * Rust decides whether to acquire, pend, or return busy. + * C applies the decision including priority inheritance. + * + * Verified: M3 (acquire), M4 (reentrant), M5 (contended), M10 (no overflow). + */ +struct gale_mutex_lock_decision gale_k_mutex_lock_decide( + uint32_t lock_count, uint32_t owner_is_null, + uint32_t owner_is_current, uint32_t is_no_wait); + +struct gale_mutex_unlock_decision { + int32_t ret; + uint8_t action; /* 0=RELEASED, 1=UNLOCKED, 2=ERROR */ + uint32_t new_lock_count; +}; + +#define GALE_MUTEX_UNLOCK_RELEASED 0 +#define GALE_MUTEX_UNLOCK_UNLOCKED 1 +#define GALE_MUTEX_UNLOCK_ERROR 2 + +/** + * Decide the action for a mutex unlock attempt. + * + * Rust decides whether to decrement, fully unlock, or return error. + * C applies the decision including priority inheritance restoration. + * + * Verified: M6a (EINVAL), M6b (EPERM), M7 (reentrant), M10 (no underflow). + */ +struct gale_mutex_unlock_decision gale_k_mutex_unlock_decide( + uint32_t lock_count, uint32_t owner_is_null, + uint32_t owner_is_current); + #ifdef __cplusplus } #endif diff --git a/zephyr/gale_mutex.c b/zephyr/gale_mutex.c index 33f694b..5680518 100644 --- a/zephyr/gale_mutex.c +++ b/zephyr/gale_mutex.c @@ -4,18 +4,17 @@ * * SPDX-License-Identifier: Apache-2.0 * - * Gale mutex — phase 1: verified state machine validation. + * Gale mutex — phase 2: decision struct pattern. * - * This is kernel/mutex.c with the ownership checks and lock_count - * arithmetic replaced by calls to the formally verified Rust - * implementation. Wait queue, scheduling, priority inheritance, - * and tracing remain native Zephyr. + * Rust decides the action (acquire/pend/busy for lock, + * released/unlocked/error for unlock), C applies it. + * Priority inheritance logic stays in C. * * Verified operations (Verus proofs): - * gale_mutex_lock_validate — M3 (acquire), M4 (reentrant), - * M5 (contended), M10 (no overflow) - * gale_mutex_unlock_validate — M6a (EINVAL), M6b (EPERM), - * M7 (reentrant), M10 (no underflow) + * gale_k_mutex_lock_decide — M3 (acquire), M4 (reentrant), + * M5 (contended), M10 (no overflow) + * gale_k_mutex_unlock_decide — M6a (EINVAL), M6b (EPERM), + * M7 (reentrant), M10 (no underflow) */ #include @@ -96,8 +95,6 @@ static bool adjust_owner_prio(struct k_mutex *mutex, int32_t new_prio) int z_impl_k_mutex_lock(struct k_mutex *mutex, k_timeout_t timeout) { k_spinlock_key_t key; - int ret; - uint32_t new_lock_count; #if (CONFIG_PRIORITY_CEILING < K_LOWEST_THREAD_PRIO) bool resched = false; int new_prio; @@ -109,17 +106,15 @@ int z_impl_k_mutex_lock(struct k_mutex *mutex, k_timeout_t timeout) key = k_spin_lock(&lock); - /* - * Validated by Gale: M3 (acquire), M4 (reentrant), - * M5 (contended), M10 (no overflow). - */ - ret = gale_mutex_lock_validate( + /* Decide: Rust determines action based on ownership and timeout */ + struct gale_mutex_lock_decision d = gale_k_mutex_lock_decide( mutex->lock_count, (mutex->owner == NULL) ? 1U : 0U, (mutex->owner == _current) ? 1U : 0U, - &new_lock_count); + K_TIMEOUT_EQ(timeout, K_NO_WAIT) ? 1U : 0U); - if (ret == 0) { + /* Apply: execute Rust's decision */ + if (d.action == GALE_MUTEX_ACTION_ACQUIRED) { /* Lock acquired (new or reentrant). */ #if (CONFIG_PRIORITY_CEILING < K_LOWEST_THREAD_PRIO) @@ -128,7 +123,7 @@ int z_impl_k_mutex_lock(struct k_mutex *mutex, k_timeout_t timeout) mutex->owner_orig_prio; #endif - mutex->lock_count = new_lock_count; + mutex->lock_count = d.new_lock_count; mutex->owner = _current; #if (CONFIG_PRIORITY_CEILING < K_LOWEST_THREAD_PRIO) @@ -148,17 +143,18 @@ int z_impl_k_mutex_lock(struct k_mutex *mutex, k_timeout_t timeout) return 0; } - /* ret == -EBUSY: mutex held by a different thread. */ - - if (unlikely(K_TIMEOUT_EQ(timeout, K_NO_WAIT))) { + if (d.action == GALE_MUTEX_ACTION_BUSY) { + /* No-wait or overflow: return immediately */ k_spin_unlock(&lock, key); SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_mutex, lock, mutex, - timeout, -EBUSY); + timeout, d.ret); - return -EBUSY; + return d.ret; } + /* GALE_MUTEX_ACTION_PEND: block on wait queue */ + SYS_PORT_TRACING_OBJ_FUNC_BLOCKING(k_mutex, lock, mutex, timeout); #if (CONFIG_PRIORITY_CEILING < K_LOWEST_THREAD_PRIO) @@ -236,41 +232,36 @@ static inline int z_vrfy_k_mutex_lock(struct k_mutex *mutex, int z_impl_k_mutex_unlock(struct k_mutex *mutex) { struct k_thread *new_owner; - uint32_t new_lock_count; - int ret; __ASSERT(!arch_is_in_isr(), "mutexes cannot be used inside ISRs"); SYS_PORT_TRACING_OBJ_FUNC_ENTER(k_mutex, unlock, mutex); - /* - * Validated by Gale: M6a (EINVAL), M6b (EPERM), - * M7 (reentrant decrement), M10 (no underflow). - */ - ret = gale_mutex_unlock_validate( + /* Decide: Rust determines action based on ownership */ + struct gale_mutex_unlock_decision d = gale_k_mutex_unlock_decide( mutex->lock_count, (mutex->owner == NULL) ? 1U : 0U, - (mutex->owner == _current) ? 1U : 0U, - &new_lock_count); + (mutex->owner == _current) ? 1U : 0U); - if (ret < 0) { + /* Apply: execute Rust's decision */ + if (d.action == GALE_MUTEX_UNLOCK_ERROR) { /* -EINVAL or -EPERM */ - SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_mutex, unlock, mutex, ret); - return ret; + SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_mutex, unlock, mutex, d.ret); + return d.ret; } LOG_DBG("mutex %p lock_count: %d", mutex, mutex->lock_count); - if (ret == GALE_MUTEX_RELEASED) { + if (d.action == GALE_MUTEX_UNLOCK_RELEASED) { /* * Reentrant release: lock_count decremented, still held. * Validated by Gale — no underflow. */ - mutex->lock_count = new_lock_count; + mutex->lock_count = d.new_lock_count; goto k_mutex_unlock_return; } - /* GALE_MUTEX_UNLOCKED: final unlock — handle waiters. */ + /* GALE_MUTEX_UNLOCK_UNLOCKED: final unlock — handle waiters. */ k_spinlock_key_t key = k_spin_lock(&lock); @@ -299,7 +290,6 @@ int z_impl_k_mutex_unlock(struct k_mutex *mutex) k_spin_unlock(&lock, key); } - k_mutex_unlock_return: SYS_PORT_TRACING_OBJ_FUNC_EXIT(k_mutex, unlock, mutex, 0); From 85c7fc0558e4932b053d001b4e421b24c197dd33 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 20 Mar 2026 06:45:48 +0100 Subject: [PATCH 11/16] artifacts: add Zephyr SRS requirements for sync modules (mutex, condvar, futex, poll) Co-Authored-By: Claude Opus 4.6 (1M context) --- artifacts/zephyr_upstream_reqs.yaml | 246 +++++++++++++++++++++++++++- 1 file changed, 245 insertions(+), 1 deletion(-) diff --git a/artifacts/zephyr_upstream_reqs.yaml b/artifacts/zephyr_upstream_reqs.yaml index 041eb7b..f8faa04 100644 --- a/artifacts/zephyr_upstream_reqs.yaml +++ b/artifacts/zephyr_upstream_reqs.yaml @@ -1,7 +1,7 @@ # Zephyr upstream requirements — auto-imported from reqmgmt via StrictDoc JSON export. # # Source: https://github.com/zephyrproject-rtos/reqmgmt -# File: docs/software_requirements/semaphore.sdoc +# Files: docs/software_requirements/{semaphore,mutex,condvar,futex,poll}.sdoc # Tool: strictdoc export --formats json | python3 convert.py # # DO NOT EDIT MANUALLY — regenerate from source. @@ -267,3 +267,247 @@ artifacts: priority: must source: "reqmgmt/semaphore.sdoc ZEP-SYRS-14" + # ── Mutex ───────────────────────────────────────────────────────────────── + + - id: ZEP-SYRS-MUT + type: stakeholder-req + title: "Zephyr: Reentrant Mutex" + status: approved + description: > + The system shall implement a reentrant mutex synchronization primitive with ownership tracking and priority inheritance for coordinating exclusive access to shared resources among multiple threads. + tags: [zephyr, upstream, mutex] + fields: + priority: must + source: "reqmgmt/mutex.sdoc ZEP-SYRS-MUT" + + - id: ZEP-SRS-MUT-1 + type: stakeholder-req + title: "Zephyr: Mutex Reentrant Locking" + status: approved + description: > + The Zephyr RTOS mutex shall support reentrant locking by the owning thread, incrementing the lock count on each successive lock by the same owner. + tags: [zephyr, upstream, mutex] + fields: + priority: must + source: "reqmgmt/mutex.sdoc ZEP-SRS-MUT-1" + links: + - type: derives-from + target: ZEP-SYRS-MUT + - type: satisfied-by + target: SWREQ-MUT-M04 + + - id: ZEP-SRS-MUT-2 + type: stakeholder-req + title: "Zephyr: Mutex Priority Inheritance" + status: approved + description: > + The Zephyr RTOS mutex shall provide priority inheritance to prevent priority inversion, ensuring the mutex owner temporarily inherits the priority of the highest-priority waiting thread. + tags: [zephyr, upstream, mutex] + fields: + priority: must + source: "reqmgmt/mutex.sdoc ZEP-SRS-MUT-2" + links: + - type: derives-from + target: ZEP-SYRS-MUT + - type: satisfied-by + target: SWREQ-MUT-M08 + - type: satisfied-by + target: SWREQ-MUT-M11 + + - id: ZEP-SRS-MUT-3 + type: stakeholder-req + title: "Zephyr: Mutex Lock With Timeout" + status: approved + description: > + The Zephyr RTOS mutex lock shall block the calling thread with a timeout when the mutex is held by another thread, or return -EBUSY immediately when called with K_NO_WAIT. + tags: [zephyr, upstream, mutex] + fields: + priority: must + source: "reqmgmt/mutex.sdoc ZEP-SRS-MUT-3" + links: + - type: derives-from + target: ZEP-SYRS-MUT + - type: satisfied-by + target: SWREQ-MUT-M03 + - type: satisfied-by + target: SWREQ-MUT-M05 + + - id: ZEP-SRS-MUT-4 + type: stakeholder-req + title: "Zephyr: Mutex Unlock By Non-Owner Error" + status: approved + description: > + The Zephyr RTOS shall return an error when a thread attempts to unlock a mutex it does not own. + tags: [zephyr, upstream, mutex] + fields: + priority: must + source: "reqmgmt/mutex.sdoc ZEP-SRS-MUT-4" + links: + - type: derives-from + target: ZEP-SYRS-MUT + - type: satisfied-by + target: SWREQ-MUT-M06 + + # ── Condvar ─────────────────────────────────────────────────────────────── + + - id: ZEP-SYRS-CV + type: stakeholder-req + title: "Zephyr: Condition Variable" + status: approved + description: > + The system shall implement a condition variable synchronization primitive with signal, broadcast, and wait operations for coordinating threads waiting on a condition. + tags: [zephyr, upstream, condvar] + fields: + priority: must + source: "reqmgmt/condvar.sdoc ZEP-SYRS-CV" + + - id: ZEP-SRS-CV-1 + type: stakeholder-req + title: "Zephyr: Condvar Signal Wakes One" + status: approved + description: > + The Zephyr RTOS condition variable signal shall wake exactly one waiting thread, selecting the highest-priority waiter from the wait queue. + tags: [zephyr, upstream, condvar] + fields: + priority: must + source: "reqmgmt/condvar.sdoc ZEP-SRS-CV-1" + links: + - type: derives-from + target: ZEP-SYRS-CV + - type: satisfied-by + target: SWREQ-CV-C02 + + - id: ZEP-SRS-CV-2 + type: stakeholder-req + title: "Zephyr: Condvar Broadcast Wakes All" + status: approved + description: > + The Zephyr RTOS condition variable broadcast shall wake all waiting threads currently in the wait queue. + tags: [zephyr, upstream, condvar] + fields: + priority: must + source: "reqmgmt/condvar.sdoc ZEP-SRS-CV-2" + links: + - type: derives-from + target: ZEP-SYRS-CV + - type: satisfied-by + target: SWREQ-CV-C04 + + - id: ZEP-SRS-CV-3 + type: stakeholder-req + title: "Zephyr: Condvar Wait Atomically Releases Mutex And Blocks" + status: approved + description: > + The Zephyr RTOS condition variable wait shall atomically release the associated mutex and block the calling thread on the condition variable's wait queue. + tags: [zephyr, upstream, condvar] + fields: + priority: must + source: "reqmgmt/condvar.sdoc ZEP-SRS-CV-3" + links: + - type: derives-from + target: ZEP-SYRS-CV + - type: satisfied-by + target: SWREQ-CV-C06 + + # ── Futex ───────────────────────────────────────────────────────────────── + + - id: ZEP-SYRS-FX + type: stakeholder-req + title: "Zephyr: Fast Userspace Mutex (Futex)" + status: approved + description: > + The system shall implement a futex synchronization primitive with wait and wake operations for efficient userspace-to-kernel thread synchronization. + tags: [zephyr, upstream, futex] + fields: + priority: must + source: "reqmgmt/futex.sdoc ZEP-SYRS-FX" + + - id: ZEP-SRS-FX-1 + type: stakeholder-req + title: "Zephyr: Futex Wait Blocks On Value Match" + status: approved + description: > + The Zephyr RTOS futex wait shall block the calling thread if the atomic value at the futex address equals the expected value provided by the caller. + tags: [zephyr, upstream, futex] + fields: + priority: must + source: "reqmgmt/futex.sdoc ZEP-SRS-FX-1" + links: + - type: derives-from + target: ZEP-SYRS-FX + - type: satisfied-by + target: SWREQ-FX-FX01 + + - id: ZEP-SRS-FX-2 + type: stakeholder-req + title: "Zephyr: Futex Wake Wakes Up To N Threads" + status: approved + description: > + The Zephyr RTOS futex wake shall wake up to N waiting threads from the futex wait queue, where N is specified by the caller or all waiters when wake_all is requested. + tags: [zephyr, upstream, futex] + fields: + priority: must + source: "reqmgmt/futex.sdoc ZEP-SRS-FX-2" + links: + - type: derives-from + target: ZEP-SYRS-FX + - type: satisfied-by + target: SWREQ-FX-FX03 + - type: satisfied-by + target: SWREQ-FX-FX04 + - type: satisfied-by + target: SWREQ-FX-FX05 + + # ── Poll ────────────────────────────────────────────────────────────────── + + - id: ZEP-SYRS-PL + type: stakeholder-req + title: "Zephyr: Poll Events" + status: approved + description: > + The system shall implement a poll event subsystem for monitoring multiple kernel objects simultaneously and receiving signal notifications. + tags: [zephyr, upstream, poll] + fields: + priority: must + source: "reqmgmt/poll.sdoc ZEP-SYRS-PL" + + - id: ZEP-SRS-PL-1 + type: stakeholder-req + title: "Zephyr: Poll Monitors Multiple Kernel Objects" + status: approved + description: > + The Zephyr RTOS poll shall provide a mechanism to monitor multiple kernel objects simultaneously, checking each object's readiness condition and reporting which objects are ready. + tags: [zephyr, upstream, poll] + fields: + priority: must + source: "reqmgmt/poll.sdoc ZEP-SRS-PL-1" + links: + - type: derives-from + target: ZEP-SYRS-PL + - type: satisfied-by + target: SWREQ-PL-PL01 + - type: satisfied-by + target: SWREQ-PL-PL02 + - type: satisfied-by + target: SWREQ-PL-PL03 + + - id: ZEP-SRS-PL-2 + type: stakeholder-req + title: "Zephyr: Poll Signal Wakes Pollers" + status: approved + description: > + The Zephyr RTOS poll signal shall wake all threads currently polling on the signal object, delivering a result value to each woken poller. + tags: [zephyr, upstream, poll] + fields: + priority: must + source: "reqmgmt/poll.sdoc ZEP-SRS-PL-2" + links: + - type: derives-from + target: ZEP-SYRS-PL + - type: satisfied-by + target: SWREQ-PL-PL04 + - type: satisfied-by + target: SWREQ-PL-PL05 + - type: satisfied-by + target: SWREQ-PL-PL06 + From 5bc084b99aafe6090674533c86829731af33c2ed Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 20 Mar 2026 06:46:57 +0100 Subject: [PATCH 12/16] artifacts: add Zephyr SRS requirements for IPC modules (msgq, stack, pipe, queue, mbox, fifo, lifo) Co-Authored-By: Claude Opus 4.6 (1M context) --- artifacts/zephyr_upstream_reqs.yaml | 419 +++++++++++++++++++++++++++- 1 file changed, 418 insertions(+), 1 deletion(-) diff --git a/artifacts/zephyr_upstream_reqs.yaml b/artifacts/zephyr_upstream_reqs.yaml index f8faa04..5f6cc39 100644 --- a/artifacts/zephyr_upstream_reqs.yaml +++ b/artifacts/zephyr_upstream_reqs.yaml @@ -1,7 +1,7 @@ # Zephyr upstream requirements — auto-imported from reqmgmt via StrictDoc JSON export. # # Source: https://github.com/zephyrproject-rtos/reqmgmt -# Files: docs/software_requirements/{semaphore,mutex,condvar,futex,poll}.sdoc +# Files: docs/software_requirements/{semaphore,mutex,condvar,futex,poll,msgq,stack,pipe,queue,mbox,fifo,lifo}.sdoc # Tool: strictdoc export --formats json | python3 convert.py # # DO NOT EDIT MANUALLY — regenerate from source. @@ -511,3 +511,420 @@ artifacts: - type: satisfied-by target: SWREQ-PL-PL06 + # ── Message Queue ──────────────────────────────────────────────────────── + + - id: ZEP-SYRS-MQ + type: stakeholder-req + title: "Zephyr: Message Queue" + status: approved + description: > + The system shall implement a message queue synchronization primitive for transferring fixed-size data items between threads. + tags: [zephyr, upstream, msgq] + fields: + priority: must + source: "reqmgmt/msgq.sdoc ZEP-SYRS-MQ" + + - id: ZEP-SRS-MQ-1 + type: stakeholder-req + title: "Zephyr: Message Queue Fixed-Size Messages" + status: approved + description: > + The Zephyr RTOS shall provide a message queue that transfers fixed-size messages between threads via a ring buffer. + tags: [zephyr, upstream, msgq] + fields: + priority: must + source: "reqmgmt/msgq.sdoc ZEP-SRS-MQ-1" + links: + - type: derives-from + target: ZEP-SYRS-MQ + - type: satisfied-by + target: SWREQ-MQ-MQ01 + - type: satisfied-by + target: SWREQ-MQ-MQ02 + + - id: ZEP-SRS-MQ-2 + type: stakeholder-req + title: "Zephyr: Message Queue FIFO Ordering" + status: approved + description: > + The Zephyr RTOS message queue shall deliver messages in FIFO order, where the first message enqueued is the first message dequeued. + tags: [zephyr, upstream, msgq] + fields: + priority: must + source: "reqmgmt/msgq.sdoc ZEP-SRS-MQ-2" + links: + - type: derives-from + target: ZEP-SYRS-MQ + - type: satisfied-by + target: SWREQ-MQ-MQ03 + - type: satisfied-by + target: SWREQ-MQ-MQ04 + + - id: ZEP-SRS-MQ-3 + type: stakeholder-req + title: "Zephyr: Message Queue Blocking Put/Get With Timeout" + status: approved + description: > + The Zephyr RTOS shall provide blocking put and get operations on a message queue, with configurable timeout periods allowing threads to wait until space or data is available. + tags: [zephyr, upstream, msgq] + fields: + priority: must + source: "reqmgmt/msgq.sdoc ZEP-SRS-MQ-3" + links: + - type: derives-from + target: ZEP-SYRS-MQ + - type: satisfied-by + target: SWREQ-MQ-MQ05 + - type: satisfied-by + target: SWREQ-MQ-MQ06 + + - id: ZEP-SRS-MQ-4 + type: stakeholder-req + title: "Zephyr: Message Queue Purge Wakes All Waiters" + status: approved + description: > + When a message queue is purged, the Zephyr RTOS shall discard all enqueued messages and wake all threads waiting to put, returning a resource contention error code. + tags: [zephyr, upstream, msgq] + fields: + priority: must + source: "reqmgmt/msgq.sdoc ZEP-SRS-MQ-4" + links: + - type: derives-from + target: ZEP-SYRS-MQ + - type: satisfied-by + target: SWREQ-MQ-MQ10 + - type: satisfied-by + target: SWREQ-MQ-MQ11 + + # ── Stack ──────────────────────────────────────────────────────────────── + + - id: ZEP-SYRS-SK + type: stakeholder-req + title: "Zephyr: Stack" + status: approved + description: > + The system shall implement a stack synchronization primitive for LIFO exchange of word-sized values between threads. + tags: [zephyr, upstream, stack] + fields: + priority: must + source: "reqmgmt/stack.sdoc ZEP-SYRS-SK" + + - id: ZEP-SRS-SK-1 + type: stakeholder-req + title: "Zephyr: Stack LIFO Word-Sized Entries" + status: approved + description: > + The Zephyr RTOS shall provide a stack that stores word-sized values in last-in first-out (LIFO) order. + tags: [zephyr, upstream, stack] + fields: + priority: must + source: "reqmgmt/stack.sdoc ZEP-SRS-SK-1" + links: + - type: derives-from + target: ZEP-SYRS-SK + - type: satisfied-by + target: SWREQ-SK-SK01 + - type: satisfied-by + target: SWREQ-SK-SK02 + + - id: ZEP-SRS-SK-2 + type: stakeholder-req + title: "Zephyr: Stack Blocking Pop With Timeout" + status: approved + description: > + The Zephyr RTOS shall provide a blocking pop operation on a stack, with a configurable timeout period allowing threads to wait until an entry is available. + tags: [zephyr, upstream, stack] + fields: + priority: must + source: "reqmgmt/stack.sdoc ZEP-SRS-SK-2" + links: + - type: derives-from + target: ZEP-SYRS-SK + - type: satisfied-by + target: SWREQ-SK-SK05 + - type: satisfied-by + target: SWREQ-SK-SK06 + + - id: ZEP-SRS-SK-3 + type: stakeholder-req + title: "Zephyr: Stack Bounded Capacity" + status: approved + description: > + The Zephyr RTOS stack shall enforce a bounded capacity, rejecting push operations when the stack is full. + tags: [zephyr, upstream, stack] + fields: + priority: must + source: "reqmgmt/stack.sdoc ZEP-SRS-SK-3" + links: + - type: derives-from + target: ZEP-SYRS-SK + - type: satisfied-by + target: SWREQ-SK-SK03 + - type: satisfied-by + target: SWREQ-SK-SK04 + + # ── Pipe ───────────────────────────────────────────────────────────────── + + - id: ZEP-SYRS-PP + type: stakeholder-req + title: "Zephyr: Pipe" + status: approved + description: > + The system shall implement a pipe synchronization primitive for byte-stream data transfer between threads. + tags: [zephyr, upstream, pipe] + fields: + priority: must + source: "reqmgmt/pipe.sdoc ZEP-SYRS-PP" + + - id: ZEP-SRS-PP-1 + type: stakeholder-req + title: "Zephyr: Pipe Byte Stream" + status: approved + description: > + The Zephyr RTOS shall provide a pipe that transfers an arbitrary-length stream of bytes between threads. + tags: [zephyr, upstream, pipe] + fields: + priority: must + source: "reqmgmt/pipe.sdoc ZEP-SRS-PP-1" + links: + - type: derives-from + target: ZEP-SYRS-PP + - type: satisfied-by + target: SWREQ-PP-PP01 + - type: satisfied-by + target: SWREQ-PP-PP02 + + - id: ZEP-SRS-PP-2 + type: stakeholder-req + title: "Zephyr: Pipe Blocking Write/Read With Timeout" + status: approved + description: > + The Zephyr RTOS shall provide blocking write and read operations on a pipe, with configurable timeout periods allowing threads to wait until buffer space or data is available. + tags: [zephyr, upstream, pipe] + fields: + priority: must + source: "reqmgmt/pipe.sdoc ZEP-SRS-PP-2" + links: + - type: derives-from + target: ZEP-SYRS-PP + - type: satisfied-by + target: SWREQ-PP-PP03 + - type: satisfied-by + target: SWREQ-PP-PP04 + + - id: ZEP-SRS-PP-3 + type: stakeholder-req + title: "Zephyr: Pipe Close/Reset State Machine" + status: approved + description: > + The Zephyr RTOS shall provide close and reset operations on a pipe that transition the pipe through defined states (open, closed, resetting), waking blocked threads with appropriate error codes. + tags: [zephyr, upstream, pipe] + fields: + priority: must + source: "reqmgmt/pipe.sdoc ZEP-SRS-PP-3" + links: + - type: derives-from + target: ZEP-SYRS-PP + - type: satisfied-by + target: SWREQ-PP-PP07 + - type: satisfied-by + target: SWREQ-PP-PP08 + - type: satisfied-by + target: SWREQ-PP-PP09 + + # ── Queue ──────────────────────────────────────────────────────────────── + + - id: ZEP-SYRS-QU + type: stakeholder-req + title: "Zephyr: Queue" + status: approved + description: > + The system shall implement a queue synchronization primitive for generic linked-list data exchange between threads. + tags: [zephyr, upstream, queue] + fields: + priority: must + source: "reqmgmt/queue.sdoc ZEP-SYRS-QU" + + - id: ZEP-SRS-QU-1 + type: stakeholder-req + title: "Zephyr: Queue Unbounded Linked-List" + status: approved + description: > + The Zephyr RTOS shall provide an unbounded queue backed by a linked list, supporting append, prepend, and get operations. + tags: [zephyr, upstream, queue] + fields: + priority: must + source: "reqmgmt/queue.sdoc ZEP-SRS-QU-1" + links: + - type: derives-from + target: ZEP-SYRS-QU + - type: satisfied-by + target: SWREQ-QU-QU01 + - type: satisfied-by + target: SWREQ-QU-QU02 + + - id: ZEP-SRS-QU-2 + type: stakeholder-req + title: "Zephyr: Queue Blocking Get With Timeout" + status: approved + description: > + The Zephyr RTOS shall provide a blocking get operation on a queue, with a configurable timeout period allowing threads to wait until an item is available. + tags: [zephyr, upstream, queue] + fields: + priority: must + source: "reqmgmt/queue.sdoc ZEP-SRS-QU-2" + links: + - type: derives-from + target: ZEP-SYRS-QU + - type: satisfied-by + target: SWREQ-QU-QU03 + - type: satisfied-by + target: SWREQ-QU-QU04 + + # ── Mailbox ────────────────────────────────────────────────────────────── + + - id: ZEP-SYRS-MB + type: stakeholder-req + title: "Zephyr: Mailbox" + status: approved + description: > + The system shall implement a mailbox synchronization primitive for synchronous message passing between threads. + tags: [zephyr, upstream, mbox] + fields: + priority: must + source: "reqmgmt/mbox.sdoc ZEP-SYRS-MB" + + - id: ZEP-SRS-MB-1 + type: stakeholder-req + title: "Zephyr: Mailbox Synchronous Message Exchange" + status: approved + description: > + The Zephyr RTOS shall provide a mailbox that performs synchronous message exchange, where the sending thread blocks until a receiving thread has consumed the message. + tags: [zephyr, upstream, mbox] + fields: + priority: must + source: "reqmgmt/mbox.sdoc ZEP-SRS-MB-1" + links: + - type: derives-from + target: ZEP-SYRS-MB + - type: satisfied-by + target: SWREQ-MB-MB01 + - type: satisfied-by + target: SWREQ-MB-MB02 + + - id: ZEP-SRS-MB-2 + type: stakeholder-req + title: "Zephyr: Mailbox Sender/Receiver Matching" + status: approved + description: > + The Zephyr RTOS mailbox shall support sender/receiver matching, allowing a thread to send to a specific thread or to any thread, and allowing a receiver to accept from a specific thread or from any thread. + tags: [zephyr, upstream, mbox] + fields: + priority: must + source: "reqmgmt/mbox.sdoc ZEP-SRS-MB-2" + links: + - type: derives-from + target: ZEP-SYRS-MB + - type: satisfied-by + target: SWREQ-MB-MB03 + - type: satisfied-by + target: SWREQ-MB-MB04 + + # ── FIFO ───────────────────────────────────────────────────────────────── + + - id: ZEP-SYRS-FI + type: stakeholder-req + title: "Zephyr: FIFO" + status: approved + description: > + The system shall implement a FIFO synchronization primitive for first-in first-out data exchange between threads. + tags: [zephyr, upstream, fifo] + fields: + priority: must + source: "reqmgmt/fifo.sdoc ZEP-SYRS-FI" + + - id: ZEP-SRS-FI-1 + type: stakeholder-req + title: "Zephyr: FIFO Queue Wrapper" + status: approved + description: > + The Zephyr RTOS shall provide a FIFO queue that wraps k_queue, enqueuing items at the tail and dequeuing from the head in first-in first-out order. + tags: [zephyr, upstream, fifo] + fields: + priority: must + source: "reqmgmt/fifo.sdoc ZEP-SRS-FI-1" + links: + - type: derives-from + target: ZEP-SYRS-FI + - type: satisfied-by + target: SWREQ-FI-FI01 + - type: satisfied-by + target: SWREQ-FI-FI02 + + - id: ZEP-SRS-FI-2 + type: stakeholder-req + title: "Zephyr: FIFO Blocking Get With Timeout" + status: approved + description: > + The Zephyr RTOS shall provide a blocking get operation on a FIFO, with a configurable timeout period allowing threads to wait until an item is available. + tags: [zephyr, upstream, fifo] + fields: + priority: must + source: "reqmgmt/fifo.sdoc ZEP-SRS-FI-2" + links: + - type: derives-from + target: ZEP-SYRS-FI + - type: satisfied-by + target: SWREQ-FI-FI03 + - type: satisfied-by + target: SWREQ-FI-FI04 + + # ── LIFO ───────────────────────────────────────────────────────────────── + + - id: ZEP-SYRS-LI + type: stakeholder-req + title: "Zephyr: LIFO" + status: approved + description: > + The system shall implement a LIFO synchronization primitive for last-in first-out data exchange between threads. + tags: [zephyr, upstream, lifo] + fields: + priority: must + source: "reqmgmt/lifo.sdoc ZEP-SYRS-LI" + + - id: ZEP-SRS-LI-1 + type: stakeholder-req + title: "Zephyr: LIFO Queue Wrapper" + status: approved + description: > + The Zephyr RTOS shall provide a LIFO queue that wraps k_queue, pushing items to the head and popping from the head in last-in first-out order. + tags: [zephyr, upstream, lifo] + fields: + priority: must + source: "reqmgmt/lifo.sdoc ZEP-SRS-LI-1" + links: + - type: derives-from + target: ZEP-SYRS-LI + - type: satisfied-by + target: SWREQ-LI-LI01 + - type: satisfied-by + target: SWREQ-LI-LI02 + + - id: ZEP-SRS-LI-2 + type: stakeholder-req + title: "Zephyr: LIFO Blocking Get With Timeout" + status: approved + description: > + The Zephyr RTOS shall provide a blocking get operation on a LIFO, with a configurable timeout period allowing threads to wait until an item is available. + tags: [zephyr, upstream, lifo] + fields: + priority: must + source: "reqmgmt/lifo.sdoc ZEP-SRS-LI-2" + links: + - type: derives-from + target: ZEP-SYRS-LI + - type: satisfied-by + target: SWREQ-LI-LI03 + - type: satisfied-by + target: SWREQ-LI-LI04 + From 56706e40de7013720504bbef15bcca82cc6fe1af Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 20 Mar 2026 06:49:54 +0100 Subject: [PATCH 13/16] artifacts: add Zephyr SRS requirements for timing, memory, and infrastructure modules Co-Authored-By: Claude Opus 4.6 (1M context) --- artifacts/zephyr_upstream_reqs.yaml | 667 +++++++++++++++++++++++++++- 1 file changed, 666 insertions(+), 1 deletion(-) diff --git a/artifacts/zephyr_upstream_reqs.yaml b/artifacts/zephyr_upstream_reqs.yaml index 5f6cc39..56b3127 100644 --- a/artifacts/zephyr_upstream_reqs.yaml +++ b/artifacts/zephyr_upstream_reqs.yaml @@ -1,7 +1,7 @@ # Zephyr upstream requirements — auto-imported from reqmgmt via StrictDoc JSON export. # # Source: https://github.com/zephyrproject-rtos/reqmgmt -# Files: docs/software_requirements/{semaphore,mutex,condvar,futex,poll,msgq,stack,pipe,queue,mbox,fifo,lifo}.sdoc +# Files: docs/software_requirements/{semaphore,mutex,condvar,futex,poll,msgq,stack,pipe,queue,mbox,fifo,lifo,timer,event,timeout,timeslice,work,mem_slab,kheap,mempool,fatal,dynamic,smp,thread,sched}.sdoc # Tool: strictdoc export --formats json | python3 convert.py # # DO NOT EDIT MANUALLY — regenerate from source. @@ -928,3 +928,668 @@ artifacts: - type: satisfied-by target: SWREQ-LI-LI04 + # ── Timer ──────────────────────────────────────────────────────────────── + + - id: ZEP-SYRS-TM + type: stakeholder-req + title: "Zephyr: Kernel Timer" + status: approved + description: > + The system shall implement a timer primitive supporting periodic and one-shot expiration with callback notification. + tags: [zephyr, upstream, timer] + fields: + priority: must + source: "reqmgmt/timer.sdoc ZEP-SYRS-TM" + + - id: ZEP-SRS-TM-1 + type: stakeholder-req + title: "Zephyr: Timer Periodic and One-Shot Mode" + status: approved + description: > + The Zephyr RTOS shall provide a timer that supports both periodic (auto-restarting) and one-shot (single expiration) modes, configurable via the period parameter at start time. + tags: [zephyr, upstream, timer] + fields: + priority: must + source: "reqmgmt/timer.sdoc ZEP-SRS-TM-1" + links: + - type: derives-from + target: ZEP-SYRS-TM + - type: satisfies + target: SYSREQ-TM-001 + + - id: ZEP-SRS-TM-2 + type: stakeholder-req + title: "Zephyr: Timer Status Counting" + status: approved + description: > + The Zephyr RTOS shall maintain a status counter for each timer that is incremented on each expiration and atomically read-and-reset via k_timer_status_get. + tags: [zephyr, upstream, timer] + fields: + priority: must + source: "reqmgmt/timer.sdoc ZEP-SRS-TM-2" + links: + - type: derives-from + target: ZEP-SYRS-TM + - type: satisfies + target: SYSREQ-TM-001 + + - id: ZEP-SRS-TM-3 + type: stakeholder-req + title: "Zephyr: Timer Expiry Callback" + status: approved + description: > + The Zephyr RTOS shall invoke a user-provided expiry function in ISR context each time the timer expires, and an optional stop function when the timer is stopped. + tags: [zephyr, upstream, timer] + fields: + priority: must + source: "reqmgmt/timer.sdoc ZEP-SRS-TM-3" + links: + - type: derives-from + target: ZEP-SYRS-TM + - type: satisfies + target: SYSREQ-TM-001 + + # ── Event ──────────────────────────────────────────────────────────────── + + - id: ZEP-SYRS-EV + type: stakeholder-req + title: "Zephyr: Kernel Event" + status: approved + description: > + The system shall implement an event object supporting bitmask-based signaling between threads and ISRs. + tags: [zephyr, upstream, event] + fields: + priority: must + source: "reqmgmt/event.sdoc ZEP-SYRS-EV" + + - id: ZEP-SRS-EV-1 + type: stakeholder-req + title: "Zephyr: Event Bitmask Post and Wait" + status: approved + description: > + The Zephyr RTOS shall provide an event object where threads can post (OR) event bits and wait for specific bits to be set. + tags: [zephyr, upstream, event] + fields: + priority: must + source: "reqmgmt/event.sdoc ZEP-SRS-EV-1" + links: + - type: derives-from + target: ZEP-SYRS-EV + - type: satisfies + target: SYSREQ-EV-001 + + - id: ZEP-SRS-EV-2 + type: stakeholder-req + title: "Zephyr: Event ANY/ALL Matching Modes" + status: approved + description: > + The Zephyr RTOS shall support two wait modes: K_EVENT_WAIT_ANY (unblock when any requested bit is set) and K_EVENT_WAIT_ALL (unblock only when all requested bits are set). + tags: [zephyr, upstream, event] + fields: + priority: must + source: "reqmgmt/event.sdoc ZEP-SRS-EV-2" + links: + - type: derives-from + target: ZEP-SYRS-EV + - type: satisfies + target: SYSREQ-EV-001 + + - id: ZEP-SRS-EV-3 + type: stakeholder-req + title: "Zephyr: Event Blocking Wait with Timeout" + status: approved + description: > + The Zephyr RTOS shall allow threads to block on an event with a configurable timeout, returning an error code if the requested events are not received within the specified time. + tags: [zephyr, upstream, event] + fields: + priority: must + source: "reqmgmt/event.sdoc ZEP-SRS-EV-3" + links: + - type: derives-from + target: ZEP-SYRS-EV + - type: satisfies + target: SYSREQ-EV-001 + + # ── Timeout ────────────────────────────────────────────────────────────── + + - id: ZEP-SYRS-TO + type: stakeholder-req + title: "Zephyr: Timeout Subsystem" + status: approved + description: > + The system shall implement a timeout subsystem for tracking absolute deadlines and managing time-based blocking operations. + tags: [zephyr, upstream, timeout] + fields: + priority: must + source: "reqmgmt/timeout.sdoc ZEP-SYRS-TO" + + - id: ZEP-SRS-TO-1 + type: stakeholder-req + title: "Zephyr: Timeout Deadline Tracking" + status: approved + description: > + The Zephyr RTOS shall track timeout deadlines as absolute tick values and maintain a sorted list of pending timeouts for efficient expiry processing. + tags: [zephyr, upstream, timeout] + fields: + priority: must + source: "reqmgmt/timeout.sdoc ZEP-SRS-TO-1" + links: + - type: derives-from + target: ZEP-SYRS-TO + - type: satisfies + target: SYSREQ-TO-001 + + - id: ZEP-SRS-TO-2 + type: stakeholder-req + title: "Zephyr: Timeout Overflow Protection" + status: approved + description: > + The Zephyr RTOS shall handle tick counter overflow correctly, ensuring that timeout arithmetic remains valid across the full range of the system tick counter. + tags: [zephyr, upstream, timeout] + fields: + priority: must + source: "reqmgmt/timeout.sdoc ZEP-SRS-TO-2" + links: + - type: derives-from + target: ZEP-SYRS-TO + - type: satisfies + target: SYSREQ-TO-001 + + # ── Timeslice ──────────────────────────────────────────────────────────── + + - id: ZEP-SYRS-TS + type: stakeholder-req + title: "Zephyr: Timeslice Subsystem" + status: approved + description: > + The system shall implement time-slice enforcement for preemptive round-robin scheduling among equal-priority threads. + tags: [zephyr, upstream, timeslice] + fields: + priority: must + source: "reqmgmt/timeslice.sdoc ZEP-SYRS-TS" + + - id: ZEP-SRS-TS-1 + type: stakeholder-req + title: "Zephyr: Time Quantum Enforcement" + status: approved + description: > + The Zephyr RTOS shall enforce a configurable time quantum (slice duration) per thread, rotating the current thread to the end of its priority queue when the slice expires. + tags: [zephyr, upstream, timeslice] + fields: + priority: must + source: "reqmgmt/timeslice.sdoc ZEP-SRS-TS-1" + links: + - type: derives-from + target: ZEP-SYRS-TS + - type: satisfies + target: SYSREQ-TS-001 + + - id: ZEP-SRS-TS-2 + type: stakeholder-req + title: "Zephyr: Cooperative Thread Exemption from Timeslicing" + status: approved + description: > + The Zephyr RTOS shall exempt cooperative-priority threads (priority < 0) from time-slice preemption, allowing them to run until they voluntarily yield or block. + tags: [zephyr, upstream, timeslice] + fields: + priority: must + source: "reqmgmt/timeslice.sdoc ZEP-SRS-TS-2" + links: + - type: derives-from + target: ZEP-SYRS-TS + - type: satisfies + target: SYSREQ-TS-001 + + # ── Work ───────────────────────────────────────────────────────────────── + + - id: ZEP-SYRS-WK + type: stakeholder-req + title: "Zephyr: Work Queue" + status: approved + description: > + The system shall implement a work queue subsystem for deferred execution of work items in thread context. + tags: [zephyr, upstream, work] + fields: + priority: must + source: "reqmgmt/work.sdoc ZEP-SYRS-WK" + + - id: ZEP-SRS-WK-1 + type: stakeholder-req + title: "Zephyr: Deferred Execution via Work Items" + status: approved + description: > + The Zephyr RTOS shall provide a mechanism to submit work items for deferred execution in a dedicated work queue thread context. + tags: [zephyr, upstream, work] + fields: + priority: must + source: "reqmgmt/work.sdoc ZEP-SRS-WK-1" + links: + - type: derives-from + target: ZEP-SYRS-WK + - type: satisfies + target: SYSREQ-WK-001 + + - id: ZEP-SRS-WK-2 + type: stakeholder-req + title: "Zephyr: Delayed Work Submission" + status: approved + description: > + The Zephyr RTOS shall support scheduling work items for submission after a specified delay, allowing deferred-deferred execution patterns. + tags: [zephyr, upstream, work] + fields: + priority: must + source: "reqmgmt/work.sdoc ZEP-SRS-WK-2" + links: + - type: derives-from + target: ZEP-SYRS-WK + - type: satisfies + target: SYSREQ-WK-001 + + - id: ZEP-SRS-WK-3 + type: stakeholder-req + title: "Zephyr: Work Item Cancellation" + status: approved + description: > + The Zephyr RTOS shall provide a mechanism to cancel a pending or delayed work item, preventing its execution if it has not yet started running. + tags: [zephyr, upstream, work] + fields: + priority: must + source: "reqmgmt/work.sdoc ZEP-SRS-WK-3" + links: + - type: derives-from + target: ZEP-SYRS-WK + - type: satisfies + target: SYSREQ-WK-001 + + # ── MemSlab ────────────────────────────────────────────────────────────── + + - id: ZEP-SYRS-MS + type: stakeholder-req + title: "Zephyr: Memory Slab Allocator" + status: approved + description: > + The system shall implement a fixed-size block memory allocator for deterministic memory allocation. + tags: [zephyr, upstream, mem-slab] + fields: + priority: must + source: "reqmgmt/mem_slab.sdoc ZEP-SYRS-MS" + + - id: ZEP-SRS-MS-1 + type: stakeholder-req + title: "Zephyr: Fixed-Size Block Allocation" + status: approved + description: > + The Zephyr RTOS shall provide a memory slab allocator that manages a pool of equal-size memory blocks, returning a block on allocation and accepting a block on free. + tags: [zephyr, upstream, mem-slab] + fields: + priority: must + source: "reqmgmt/mem_slab.sdoc ZEP-SRS-MS-1" + links: + - type: derives-from + target: ZEP-SYRS-MS + - type: satisfies + target: SYSREQ-MS-001 + + - id: ZEP-SRS-MS-2 + type: stakeholder-req + title: "Zephyr: Memory Slab Blocking Allocation with Timeout" + status: approved + description: > + The Zephyr RTOS shall allow threads to block when allocating from an exhausted memory slab, with a configurable timeout after which an error is returned. + tags: [zephyr, upstream, mem-slab] + fields: + priority: must + source: "reqmgmt/mem_slab.sdoc ZEP-SRS-MS-2" + links: + - type: derives-from + target: ZEP-SYRS-MS + - type: satisfies + target: SYSREQ-MS-001 + + - id: ZEP-SRS-MS-3 + type: stakeholder-req + title: "Zephyr: Memory Slab Bounded Pool" + status: approved + description: > + The Zephyr RTOS shall enforce that the number of allocated blocks never exceeds the configured pool capacity, maintaining the invariant 0 <= num_used <= num_blocks. + tags: [zephyr, upstream, mem-slab] + fields: + priority: must + source: "reqmgmt/mem_slab.sdoc ZEP-SRS-MS-3" + links: + - type: derives-from + target: ZEP-SYRS-MS + - type: satisfies + target: SYSREQ-MS-001 + + # ── KHeap ──────────────────────────────────────────────────────────────── + + - id: ZEP-SYRS-KH + type: stakeholder-req + title: "Zephyr: Kernel Heap" + status: approved + description: > + The system shall implement a kernel heap allocator supporting dynamic memory allocation with blocking wait and alignment control. + tags: [zephyr, upstream, kheap] + fields: + priority: must + source: "reqmgmt/kheap.sdoc ZEP-SYRS-KH" + + - id: ZEP-SRS-KH-1 + type: stakeholder-req + title: "Zephyr: Dynamic Heap Allocation" + status: approved + description: > + The Zephyr RTOS shall provide a heap allocator supporting k_heap_alloc for variable-size allocation with optional blocking wait when memory is unavailable. + tags: [zephyr, upstream, kheap] + fields: + priority: must + source: "reqmgmt/kheap.sdoc ZEP-SRS-KH-1" + links: + - type: derives-from + target: ZEP-SYRS-KH + - type: satisfies + target: SYSREQ-KH-001 + + - id: ZEP-SRS-KH-2 + type: stakeholder-req + title: "Zephyr: Aligned Heap Allocation" + status: approved + description: > + The Zephyr RTOS shall provide k_heap_aligned_alloc for allocating memory with a specified alignment, ensuring the returned pointer satisfies the requested alignment constraint. + tags: [zephyr, upstream, kheap] + fields: + priority: must + source: "reqmgmt/kheap.sdoc ZEP-SRS-KH-2" + links: + - type: derives-from + target: ZEP-SYRS-KH + - type: satisfies + target: SYSREQ-KH-001 + + # ── Mempool ────────────────────────────────────────────────────────────── + + - id: ZEP-SYRS-MP + type: stakeholder-req + title: "Zephyr: Memory Pool" + status: approved + description: > + The system shall implement a memory pool providing fixed-block allocation with bounded capacity tracking. + tags: [zephyr, upstream, mempool] + fields: + priority: must + source: "reqmgmt/mempool.sdoc ZEP-SYRS-MP" + + - id: ZEP-SRS-MP-1 + type: stakeholder-req + title: "Zephyr: Memory Pool Management" + status: approved + description: > + The Zephyr RTOS shall provide a memory pool that tracks allocated and free block counts, ensuring the conservation invariant (allocated + free == capacity) holds at all times. + tags: [zephyr, upstream, mempool] + fields: + priority: must + source: "reqmgmt/mempool.sdoc ZEP-SRS-MP-1" + links: + - type: derives-from + target: ZEP-SYRS-MP + - type: satisfies + target: SYSREQ-MP-001 + + - id: ZEP-SRS-MP-2 + type: stakeholder-req + title: "Zephyr: Memory Pool Block Size Classes" + status: approved + description: > + The Zephyr RTOS shall support memory pools with fixed block sizes, where all blocks within a pool are of identical size to ensure O(1) allocation and deallocation. + tags: [zephyr, upstream, mempool] + fields: + priority: must + source: "reqmgmt/mempool.sdoc ZEP-SRS-MP-2" + links: + - type: derives-from + target: ZEP-SYRS-MP + - type: satisfies + target: SYSREQ-MP-001 + + # ── Fatal ──────────────────────────────────────────────────────────────── + + - id: ZEP-SYRS-FT + type: stakeholder-req + title: "Zephyr: Fatal Error Handling" + status: approved + description: > + The system shall implement fatal error classification and recovery decision logic for safe system shutdown. + tags: [zephyr, upstream, fatal] + fields: + priority: must + source: "reqmgmt/fatal.sdoc ZEP-SYRS-FT" + + - id: ZEP-SRS-FT-1 + type: stakeholder-req + title: "Zephyr: Fatal Error Classification" + status: approved + description: > + The Zephyr RTOS shall classify fatal errors into distinct reason codes (CPU exception, oops, panic, stack overflow, kernel oops) to enable appropriate recovery or halt decisions. + tags: [zephyr, upstream, fatal] + fields: + priority: must + source: "reqmgmt/fatal.sdoc ZEP-SRS-FT-1" + links: + - type: derives-from + target: ZEP-SYRS-FT + - type: satisfies + target: SYSREQ-FT-001 + + - id: ZEP-SRS-FT-2 + type: stakeholder-req + title: "Zephyr: System Halt on Unrecoverable Error" + status: approved + description: > + The Zephyr RTOS shall halt the system when a fatal error occurs in ISR context or when the faulting thread is marked essential, as recovery is not possible in these cases. + tags: [zephyr, upstream, fatal] + fields: + priority: must + source: "reqmgmt/fatal.sdoc ZEP-SRS-FT-2" + links: + - type: derives-from + target: ZEP-SYRS-FT + - type: satisfies + target: SYSREQ-FT-001 + + # ── Dynamic ────────────────────────────────────────────────────────────── + + - id: ZEP-SYRS-DY + type: stakeholder-req + title: "Zephyr: Dynamic Thread Creation" + status: approved + description: > + The system shall implement dynamic thread creation with stack pool management for runtime thread provisioning. + tags: [zephyr, upstream, dynamic] + fields: + priority: must + source: "reqmgmt/dynamic.sdoc ZEP-SYRS-DY" + + - id: ZEP-SRS-DY-1 + type: stakeholder-req + title: "Zephyr: Dynamic Thread Creation" + status: approved + description: > + The Zephyr RTOS shall provide a mechanism to create threads dynamically at runtime, allocating stack memory from a pre-configured stack pool. + tags: [zephyr, upstream, dynamic] + fields: + priority: must + source: "reqmgmt/dynamic.sdoc ZEP-SRS-DY-1" + links: + - type: derives-from + target: ZEP-SYRS-DY + - type: satisfies + target: SYSREQ-DY-001 + + - id: ZEP-SRS-DY-2 + type: stakeholder-req + title: "Zephyr: Dynamic Thread Stack Pool Management" + status: approved + description: > + The Zephyr RTOS shall manage a bounded pool of thread stacks, enforcing the invariant that the number of active dynamic threads never exceeds the pool maximum. + tags: [zephyr, upstream, dynamic] + fields: + priority: must + source: "reqmgmt/dynamic.sdoc ZEP-SRS-DY-2" + links: + - type: derives-from + target: ZEP-SYRS-DY + - type: satisfies + target: SYSREQ-DY-001 + + # ── SMP ────────────────────────────────────────────────────────────────── + + - id: ZEP-SYRS-SM + type: stakeholder-req + title: "Zephyr: SMP CPU Management" + status: approved + description: > + The system shall implement SMP CPU lifecycle management with global lock coordination for multi-processor operation. + tags: [zephyr, upstream, smp] + fields: + priority: must + source: "reqmgmt/smp.sdoc ZEP-SYRS-SM" + + - id: ZEP-SRS-SM-1 + type: stakeholder-req + title: "Zephyr: SMP CPU Lifecycle" + status: approved + description: > + The Zephyr RTOS shall manage CPU lifecycle transitions (init, start, stop, resume) while maintaining the invariant that the number of active CPUs is bounded by [1, max_cpus]. + tags: [zephyr, upstream, smp] + fields: + priority: must + source: "reqmgmt/smp.sdoc ZEP-SRS-SM-1" + links: + - type: derives-from + target: ZEP-SYRS-SM + - type: satisfies + target: SYSREQ-SM-001 + + - id: ZEP-SRS-SM-2 + type: stakeholder-req + title: "Zephyr: SMP Global Lock" + status: approved + description: > + The Zephyr RTOS shall provide a global SMP lock mechanism ensuring mutual exclusion across CPUs, with lock/unlock/release semantics and correct nesting behavior. + tags: [zephyr, upstream, smp] + fields: + priority: must + source: "reqmgmt/smp.sdoc ZEP-SRS-SM-2" + links: + - type: derives-from + target: ZEP-SYRS-SM + - type: satisfies + target: SYSREQ-SM-001 + + # ── Thread Lifecycle ───────────────────────────────────────────────────── + + - id: ZEP-SYRS-TL + type: stakeholder-req + title: "Zephyr: Thread Lifecycle" + status: approved + description: > + The system shall implement thread lifecycle management including creation, starting, aborting, and joining with proper state tracking. + tags: [zephyr, upstream, thread] + fields: + priority: must + source: "reqmgmt/thread.sdoc ZEP-SYRS-TL" + + - id: ZEP-SRS-TL-1 + type: stakeholder-req + title: "Zephyr: Thread Create and Start" + status: approved + description: > + The Zephyr RTOS shall provide k_thread_create to initialize a thread with a stack, entry point, priority, and options, supporting both immediate and delayed start. + tags: [zephyr, upstream, thread] + fields: + priority: must + source: "reqmgmt/thread.sdoc ZEP-SRS-TL-1" + links: + - type: derives-from + target: ZEP-SYRS-TL + - type: satisfies + target: SYSREQ-TL-001 + + - id: ZEP-SRS-TL-2 + type: stakeholder-req + title: "Zephyr: Thread Abort and Join" + status: approved + description: > + The Zephyr RTOS shall provide k_thread_abort to terminate a thread with cleanup and k_thread_join to block the calling thread until the target thread terminates. + tags: [zephyr, upstream, thread] + fields: + priority: must + source: "reqmgmt/thread.sdoc ZEP-SRS-TL-2" + links: + - type: derives-from + target: ZEP-SYRS-TL + - type: satisfies + target: SYSREQ-TL-001 + + # ── Scheduler ──────────────────────────────────────────────────────────── + + - id: ZEP-SYRS-SC + type: stakeholder-req + title: "Zephyr: Priority Scheduler" + status: approved + description: > + The system shall implement a priority-based preemptive scheduler with run queue management and cooperative thread support. + tags: [zephyr, upstream, sched] + fields: + priority: must + source: "reqmgmt/sched.sdoc ZEP-SYRS-SC" + + - id: ZEP-SRS-SC-1 + type: stakeholder-req + title: "Zephyr: Priority-Based Scheduling" + status: approved + description: > + The Zephyr RTOS shall schedule threads based on priority, always selecting the highest-priority ready thread for execution via the run queue. + tags: [zephyr, upstream, sched] + fields: + priority: must + source: "reqmgmt/sched.sdoc ZEP-SRS-SC-1" + links: + - type: derives-from + target: ZEP-SYRS-SC + - type: satisfies + target: SYSREQ-SC-001 + + - id: ZEP-SRS-SC-2 + type: stakeholder-req + title: "Zephyr: Preemption Policy" + status: approved + description: > + The Zephyr RTOS shall preempt the current thread when a higher-priority thread becomes ready, unless the current thread is cooperative or has the preemption lock set. + tags: [zephyr, upstream, sched] + fields: + priority: must + source: "reqmgmt/sched.sdoc ZEP-SRS-SC-2" + links: + - type: derives-from + target: ZEP-SYRS-SC + - type: satisfies + target: SYSREQ-SC-001 + + - id: ZEP-SRS-SC-3 + type: stakeholder-req + title: "Zephyr: Cooperative Thread Protection" + status: approved + description: > + The Zephyr RTOS shall protect cooperative-priority threads from preemption, ensuring they run until they voluntarily yield, block, or terminate. + tags: [zephyr, upstream, sched] + fields: + priority: must + source: "reqmgmt/sched.sdoc ZEP-SRS-SC-3" + links: + - type: derives-from + target: ZEP-SYRS-SC + - type: satisfies + target: SYSREQ-SC-001 + From 22072518e6e8620b68ab3c509b48d540dda244a4 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 20 Mar 2026 07:39:22 +0100 Subject: [PATCH 14/16] fix(error): align error codes with Zephyr's minimal libc errno.h ENOMSG, ETIMEDOUT, ECANCELED, EOVERFLOW, and EADDRINUSE used Linux values instead of Zephyr's. This caused msgq boundary tests to fail: Rust returned -42 (Linux ENOMSG) but Zephyr tests expect -35. Fixed all five mismatched constants in both src/error.rs and plain/src/error.rs to match zephyr/lib/libc/minimal/include/errno.h. Co-Authored-By: Claude Opus 4.6 (1M context) --- plain/src/error.rs | 10 +++++----- src/error.rs | 10 +++++----- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/plain/src/error.rs b/plain/src/error.rs index 02309c6..63075c9 100644 --- a/plain/src/error.rs +++ b/plain/src/error.rs @@ -9,18 +9,18 @@ pub const EAGAIN: i32 = -11; pub const EPERM: i32 = -1; pub const ENOMEM: i32 = -12; pub const EPIPE: i32 = -32; -pub const ENOMSG: i32 = -42; -pub const ETIMEDOUT: i32 = -110; -pub const ECANCELED: i32 = -125; +pub const ENOMSG: i32 = -35; +pub const ETIMEDOUT: i32 = -116; +pub const ECANCELED: i32 = -140; /// No space left on device / no free slots. pub const ENOSPC: i32 = -28; /// No such entry / not found. pub const ENOENT: i32 = -2; /// Value too large (arithmetic overflow). -pub const EOVERFLOW: i32 = -75; +pub const EOVERFLOW: i32 = -139; /// Bad file descriptor / object not found or type mismatch. pub const EBADF: i32 = -9; /// Address already in use / object already initialized. -pub const EADDRINUSE: i32 = -98; +pub const EADDRINUSE: i32 = -112; /// Success return value. pub const OK: i32 = 0; diff --git a/src/error.rs b/src/error.rs index 159fe1d..259e913 100644 --- a/src/error.rs +++ b/src/error.rs @@ -14,19 +14,19 @@ pub const EAGAIN: i32 = -11; pub const EPERM: i32 = -1; pub const ENOMEM: i32 = -12; pub const EPIPE: i32 = -32; -pub const ENOMSG: i32 = -42; -pub const ETIMEDOUT: i32 = -110; -pub const ECANCELED: i32 = -125; +pub const ENOMSG: i32 = -35; +pub const ETIMEDOUT: i32 = -116; +pub const ECANCELED: i32 = -140; /// No space left on device / no free slots. pub const ENOSPC: i32 = -28; /// No such entry / not found. pub const ENOENT: i32 = -2; /// Value too large (arithmetic overflow). -pub const EOVERFLOW: i32 = -75; +pub const EOVERFLOW: i32 = -139; /// Bad file descriptor / object not found or type mismatch. pub const EBADF: i32 = -9; /// Address already in use / object already initialized. -pub const EADDRINUSE: i32 = -98; +pub const EADDRINUSE: i32 = -112; /// Success return value. pub const OK: i32 = 0; From cbb6cc8fe979a573087419cef70102eed1016025 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 20 Mar 2026 07:39:46 +0100 Subject: [PATCH 15/16] fix(pipe): check direct-copy completion at top of read loop After a reader wakes from a direct copy by a writer, buf.used may already satisfy the request. The decision struct conversion moved the buf.used == len check inside the READ_OK/WAKE_WRITER branches, so when the loop re-entered and Rust returned READ_PEND (because the ring buffer was empty), the reader hung forever despite having all its data. Add buf.used >= len guard at the top of the for(;;) loop, matching the unconditional check in upstream Zephyr's k_pipe_read. This also fixes the semaphore test_sem_multi_take_timeout_diff_sem hang, which used a pipe for inter-thread result reporting. Co-Authored-By: Claude Opus 4.6 (1M context) --- zephyr/gale_pipe.c | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/zephyr/gale_pipe.c b/zephyr/gale_pipe.c index 04048b1..8af7eb3 100644 --- a/zephyr/gale_pipe.c +++ b/zephyr/gale_pipe.c @@ -221,6 +221,14 @@ int z_impl_k_pipe_read(struct k_pipe *pipe, uint8_t *data, size_t len, k_timeout SYS_PORT_TRACING_OBJ_FUNC_ENTER(k_pipe, read, pipe, data, len, timeout); for (;;) { + /* After waking from direct copy, buf.used may already + * satisfy the request — check before asking Rust. + */ + if (buf.used >= len) { + rc = buf.used; + break; + } + /* Extract: gather kernel state */ uint32_t used = ring_buf_size_get(&pipe->buf); uint32_t capacity = ring_buf_capacity_get(&pipe->buf); From d05c0a6b3ae586de69ea9a131e6c1dc3560fda6e Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 20 Mar 2026 07:40:07 +0100 Subject: [PATCH 16/16] fix(pipe): wake writers for zero-size pipes in read decide gale_k_pipe_read_decide had a guard (size > 0) that prevented WAKE_WRITER from ever being returned for zero-size pipes. Upstream Zephyr wakes writers unconditionally when pipe_full() (space == 0), which is always true for zero-size pipes. Without this wake, the reader pends and no writer ever runs copy_to_pending_readers. Remove the size > 0 guard so the condition becomes used >= size, which for zero-size pipes is 0 >= 0 = true. This lets writers copy data directly to readers via the swap_data mechanism. Co-Authored-By: Claude Opus 4.6 (1M context) --- ffi/src/lib.rs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/ffi/src/lib.rs b/ffi/src/lib.rs index cc0d031..aac590b 100644 --- a/ffi/src/lib.rs +++ b/ffi/src/lib.rs @@ -1340,7 +1340,10 @@ pub extern "C" fn gale_k_pipe_read_decide( new_used: used, }; } - if size > 0 && used >= size && has_writer != 0 { + if used >= size && has_writer != 0 { + // Buffer full (or zero-size pipe): wake writers so they can + // copy data directly to us. For zero-size pipes size==0 and + // used==0, so this path is the only way to trigger the writer. let n = if request_len <= used { request_len } else { used }; #[allow(clippy::arithmetic_side_effects)] let nu = used - n;