Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1,328 changes: 1,327 additions & 1 deletion artifacts/zephyr_upstream_reqs.yaml

Large diffs are not rendered by default.

26 changes: 26 additions & 0 deletions ffi/include/gale_event.h
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
43 changes: 43 additions & 0 deletions ffi/include/gale_fifo.h
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
43 changes: 43 additions & 0 deletions ffi/include/gale_lifo.h
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
24 changes: 24 additions & 0 deletions ffi/include/gale_mbox.h
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
26 changes: 26 additions & 0 deletions ffi/include/gale_mem_slab.h
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
34 changes: 34 additions & 0 deletions ffi/include/gale_msgq.h
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
46 changes: 46 additions & 0 deletions ffi/include/gale_mutex.h
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
34 changes: 34 additions & 0 deletions ffi/include/gale_pipe.h
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
23 changes: 23 additions & 0 deletions ffi/include/gale_queue.h
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
27 changes: 27 additions & 0 deletions ffi/include/gale_stack.h
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading
Loading