stdlib.sync

Synchronization Primitives

Generated from v0.65.7. 7 source files, 148 documented symbols.

atomics.xi

type AtomicInt

AtomicInt - a lock-free atomically accessed signed integer.

Field	Type
ptr	*Int

fn atomic_int_new(init: Int) -> AtomicInt

Create an atomic integer initialised to init. Params: init - the initial value. Returns: a new atomic integer holding init. Complexity: O(1).

• Postcondition: result.ptr != null

fn atomic_load(a: &AtomicInt) -> Int

Atomically read the current value. Params: a - the atomic integer. Returns: the current value. Complexity: O(1). Thread-safe.

• Precondition: a.ptr != null

fn atomic_store(a: &mut AtomicInt, value: Int)

Atomically write a new value. Params: a - the atomic integer; value - the new value. Complexity: O(1). Thread-safe.

• Precondition: a.ptr != null

fn atomic_add(a: &mut AtomicInt, delta: Int) -> Int

Atomically add delta and return the new value. Params: a - the atomic integer; delta - the increment. Returns: the value after the addition. Complexity: O(1). Thread-safe.

• Precondition: a.ptr != null

fn atomic_sub(a: &mut AtomicInt, delta: Int) -> Int

Atomically subtract delta and return the new value. Params: a - the atomic integer; delta - the decrement. Returns: the value after the subtraction. Complexity: O(1). Thread-safe.

• Precondition: a.ptr != null

fn atomic_fetch_add(a: &mut AtomicInt, delta: Int) -> Int

Atomically add delta and return the old value. Params: a - the atomic integer; delta - the increment. Returns: the value before the addition. Complexity: O(1). Thread-safe.

• Precondition: a.ptr != null

fn atomic_fetch_sub(a: &mut AtomicInt, delta: Int) -> Int

Atomically subtract delta and return the old value. Params: a - the atomic integer; delta - the decrement. Returns: the value before the subtraction. Complexity: O(1). Thread-safe.

• Precondition: a.ptr != null

fn atomic_swap(a: &mut AtomicInt, value: Int) -> Int

Atomically store value and return the old value. Params: a - the atomic integer; value - the new value. Returns: the value before the store. Complexity: O(1). Thread-safe.

• Precondition: a.ptr != null

fn atomic_compare_exchange(a: &mut AtomicInt, expected: Int, new: Int) -> Bool

Store new if the value equals expected. Params: a - the atomic integer; expected - the value to compare against; new - the value to store on match. Returns: true if the exchange was performed. Complexity: O(1). Thread-safe.

• Precondition: a.ptr != null

type AtomicBool

AtomicBool - a lock-free atomically accessed boolean.

Field	Type
ptr	*Int

fn atomic_bool_new(init: Bool) -> AtomicBool

Create an atomic boolean initialised to init. Params: init - the initial value. Returns: a new atomic boolean holding init. Complexity: O(1).

• Postcondition: result.ptr != null

fn atomic_bool_load(a: &AtomicBool) -> Bool

Atomically read the current value. Params: a - the atomic boolean. Returns: the current value. Complexity: O(1). Thread-safe.

• Precondition: a.ptr != null

fn atomic_bool_store(a: &mut AtomicBool, value: Bool)

Atomically write a new value. Params: a - the atomic boolean; value - the new value. Complexity: O(1). Thread-safe.

• Precondition: a.ptr != null

fn atomic_bool_swap(a: &mut AtomicBool, value: Bool) -> Bool

Atomically store value and return the old value. Params: a - the atomic boolean; value - the new value. Returns: the value before the store. Complexity: O(1). Thread-safe.

• Precondition: a.ptr != null

type AtomicPtr

AtomicPtr - a lock-free atomically accessed raw pointer.

Field	Type
ptr	*Int

fn atomic_ptr_new[T](ptr: Int) -> AtomicPtr

Create an atomic pointer from an address. Params: ptr - the address to store. Returns: a new atomic pointer holding ptr. Complexity: O(1).

• Postcondition: result.ptr != null

fn atomic_ptr_load(a: &AtomicPtr) -> Int

Atomically read the current address. Params: a - the atomic pointer. Returns: the current address. Complexity: O(1). Thread-safe.

• Precondition: a.ptr != null

fn atomic_ptr_store(a: &mut AtomicPtr, ptr: Int)

Atomically write a new address. Params: a - the atomic pointer; ptr - the new address. Complexity: O(1). Thread-safe.

• Precondition: a.ptr != null

---

---

---

barrier.xi

type SyncBarrier

SyncBarrier (the stub's Barrier) - a reusable rendezvous for N threads.

Field	Type
guard	*Int
count	Int
waiting	*Int
generation	*Int

fn barrier_new(count: Int) -> SyncBarrier

Create a barrier for count threads. Params: count - the number of threads that must arrive to release. Returns: a new barrier. A non-positive count is clamped to 1. Complexity: O(1).

• Postcondition: result.count >= 1

fn barrier_wait(b: &mut SyncBarrier) -> Bool

Block until all threads arrive; true for the last arriver. Params: b - the barrier. Returns: true when this call releases the barrier (the last arriver), false for the other waiters. Complexity: O(1) per poll; blocks until all threads arrive.

• Precondition: b.guard != null
• Precondition: b.waiting != null
• Precondition: b.generation != null

fn barrier_count(b: &SyncBarrier) -> Int

The configured thread count. Params: b - the barrier. Returns: the number of threads the barrier was created for. Complexity: O(1).

• Postcondition: result >= 1

fn barrier_reset(b: &mut SyncBarrier)

Reset the waiting counter to zero. Params: b - the barrier. Complexity: O(1). Not safe for concurrent use with active waiters.

• Precondition: b.waiting != null

fn barrier_is_ready(b: &SyncBarrier) -> Bool

True if every thread has arrived. Params: b - the barrier. Returns: whether the current cycle is complete (all threads arrived). Complexity: O(1).

• Precondition: b.waiting != null

---

---

---

channel.xi

type Channel

Channel[T] - a generic message queue; capacity 0 means unbounded. data is raw element storage, len the queued count, alloc_cap the allocated slots, cap the configured maximum (0 = unbounded).

Field	Type
data	*UInt8
len	Int
alloc_cap	Int
cap	Int
closed	Bool

fn channel_new[T](capacity: Int) -> Channel[T]

Create a channel with the given capacity (0 = unbounded). Params: capacity - maximum queued items, or 0 for unbounded. Returns: a new empty open channel. Complexity: O(1).

• Postcondition: (capacity < 0) => (result.cap == 0)
• Postcondition: (capacity >= 0) => (result.cap == capacity)
• Postcondition: result.closed == false

fn channel_send[T](ch: &mut Channel[T], item: T) -> Result[Unit, Str]

Enqueue item, blocking on a full bounded channel; error if closed. Params: ch - the channel; item - the value to send. Returns: Ok(()) on success, Err("channel closed") if closed. Complexity: O(1) per poll; blocks while the channel is full.

• Postcondition: result is Err(_) => ch.closed == true

fn channel_try_send[T](ch: &mut Channel[T], item: T) -> Bool

Enqueue without blocking; false if full or closed. Params: ch - the channel; item - the value to send. Returns: true if queued, false if the channel is full or closed. Complexity: O(1). Never blocks.

• Postcondition: result => ch.cap == 0 || ch.len <= ch.cap
• Postcondition: !result => ch.closed || (ch.cap > 0 && ch.len >= ch.cap)

fn channel_recv[T](ch: &mut Channel[T]) -> Option[T]

Dequeue the next item, blocking when empty; None if closed. Params: ch - the channel. Returns: Some(item) in FIFO order, None if closed and drained. Complexity: O(n) shift per pop; blocks while empty.

• Postcondition: result is None => ch.closed == true && ch.len == 0

fn channel_try_recv[T](ch: &mut Channel[T]) -> Option[T]

Dequeue without blocking; None if empty or closed. Params: ch - the channel. Returns: Some(item) in FIFO order, None if empty or closed. Complexity: O(n) shift per pop. Never blocks.

• Postcondition: result is None => ch.len == 0

fn channel_close[T](ch: &mut Channel[T])

Mark the channel closed; pending sends fail, queued items stay readable. Params: ch - the channel. Complexity: O(1).

• Postcondition: ch.closed == true

fn channel_is_closed[T](ch: &Channel[T]) -> Bool

True if the channel is closed. Params: ch - the channel. Returns: whether the channel was closed. Complexity: O(1).

• Postcondition: result == ch.closed

fn channel_len[T](ch: &Channel[T]) -> Int

Number of items currently queued. Params: ch - the channel. Returns: the queue length. Complexity: O(1).

• Postcondition: result >= 0

fn channel_capacity[T](ch: &Channel[T]) -> Int

Configured capacity; 0 for unbounded. Params: ch - the channel. Returns: the capacity configured at creation. Complexity: O(1).

• Postcondition: result >= 0

fn channel_select[T](chs: &Vec[Channel[T]]) -> Option[Int]

Block until one channel is ready; returns its index. Params: chs - the channels to watch. Returns: Some(index) of the first channel with a queued item, or None if every channel is closed and drained. Complexity: O(n) per poll; blocks while no channel is ready.

• Postcondition: result is Some(_) => result.value >= 0 && result.value < chs.len()

type ChannelHandle

ChannelHandle[T] - a copyable Int-addressed handle to a heap-allocated Channel[T] cell. The address is non-zero for a live handle.

Field	Type
addr	Int

fn channel_open[T](capacity: Int) -> ChannelHandle[T]

Allocate a channel cell and return its copyable handle. Params: capacity - maximum queued items, or 0 for unbounded; negative values are clamped to 0. Returns: a handle with a non-zero address to a new empty open channel. Thread safety: the caller must serialize all handle operations externally. Complexity: O(1).

• Postcondition: result.addr != 0

fn channel_handle_try_send[T](h: ChannelHandle[T], item: T) -> Bool

Enqueue without blocking; false if the channel is full or closed. Params: h - the handle; item - the value to send. Returns: true if queued, false if full or closed. Thread safety: caller must hold the external lock for h. Complexity: O(1). Never blocks.

• Precondition: h.addr != 0
• Postcondition: result == false => channel_handle_is_closed(h) || (channel_handle_capacity(h) > 0 && channel_handle_len(h) >= channel_handle_capacity(h))

fn channel_handle_try_recv[T](h: ChannelHandle[T]) -> Option[T]

Dequeue without blocking; None if the channel is empty (closed or open). Params: h - the handle. Returns: Some(item) in FIFO order, or None when empty. Thread safety: caller must hold the external lock for h. Complexity: O(n) shift per pop. Never blocks.

• Precondition: h.addr != 0
• Postcondition: result is None => channel_handle_len(h) == 0

fn channel_handle_close[T](h: ChannelHandle[T])

Mark the channel closed; queued items stay readable. Params: h - the handle. Thread safety: caller must hold the external lock for h. Complexity: O(1).

• Precondition: h.addr != 0
• Postcondition: channel_handle_is_closed(h) == true

fn channel_handle_is_closed[T](h: ChannelHandle[T]) -> Bool

True if the channel is closed. Params: h - the handle. Returns: whether the channel was closed. Thread safety: caller must hold the external lock for h. Complexity: O(1).

• Precondition: h.addr != 0

fn channel_handle_len[T](h: ChannelHandle[T]) -> Int

Number of items currently queued. Params: h - the handle. Returns: the queue length (>= 0). Thread safety: caller must hold the external lock for h. Complexity: O(1).

• Precondition: h.addr != 0
• Postcondition: result >= 0

fn channel_handle_capacity[T](h: ChannelHandle[T]) -> Int

Configured capacity; 0 for unbounded. Params: h - the handle. Returns: the capacity configured at channel_open (>= 0). Thread safety: caller must hold the external lock for h. Complexity: O(1).

• Precondition: h.addr != 0
• Postcondition: result >= 0

fn channel_handle_free[T](h: ChannelHandle[T])

Drain the channel and deallocate its element buffer and cell. Params: h - the handle. Thread safety: caller must hold the external lock for h; call exactly once, after every thread using the handle has been joined, and never concurrently with another handle operation. Copies of the handle are dangling after this call. Complexity: O(n) drain + O(1) deallocation.

• Precondition: h.addr != 0

---

---

---

condvar.xi

type SyncCondvar

SyncCondvar (the stub's Condvar) - a condition variable paired with a mutex.

Field	Type
notified	*Int

fn condvar_new() -> SyncCondvar

Create a new condition variable. Returns: a condvar with a zero notify count. Complexity: O(1).

• Postcondition: result.notified != null

fn condvar_wait(cv: SyncCondvar, m: SyncMutex)

Atomically release m and block until notified. Params: cv - the condition variable; m - the mutex guarding the state. Re-acquires m before returning. Complexity: O(1) per poll; blocks until a notify.

• Precondition: cv.notified != null
• Precondition: m.locked != null

fn condvar_wait_timeout(cv: SyncCondvar, m: SyncMutex, ms: Int) -> Bool

Wait with a timeout; true if notified. Params: cv - the condition variable; m - the mutex; ms - timeout in milliseconds (clamped to >= 0). Returns: true if notified before the timeout, false on timeout. Re-acquires m before returning. Complexity: O(ms) polls, each sleeping up to 1 ms.

• Precondition: cv.notified != null
• Precondition: m.locked != null

fn condvar_notify_one(cv: SyncCondvar)

Wake one waiting thread. Params: cv - the condition variable. Complexity: O(1).

• Precondition: cv.notified != null

fn condvar_notify_all(cv: SyncCondvar)

Wake all waiting threads. Params: cv - the condition variable. Complexity: O(1).

• Precondition: cv.notified != null

---

---

---

mutex.xi

type SyncMutex

SyncMutex (the stub's Mutex) - an owned mutual exclusion primitive.

Field	Type
locked	*Int

fn mutex_new() -> SyncMutex

Create a new unlocked mutex. Returns: a mutex whose locked state is false. Complexity: O(1).

• Postcondition: result.locked != null

fn mutex_lock(m: &mut SyncMutex)

Block until the mutex is acquired. Params: m - the mutex. Complexity: O(1) per poll; spins with 1 ms sleeps while contended.

• Precondition: m.locked != null

fn mutex_try_lock(m: &mut SyncMutex) -> Bool

Attempt a non-blocking acquire. Params: m - the mutex. Returns: true if the mutex was acquired, false if it is already held. Complexity: O(1). Never blocks.

• Precondition: m.locked != null

fn mutex_unlock(m: &mut SyncMutex)

Release a held mutex. Params: m - the mutex. Complexity: O(1).

• Precondition: m.locked != null

fn mutex_is_locked(m: &SyncMutex) -> Bool

True if the mutex is currently held. Params: m - the mutex. Returns: whether the mutex is locked by any thread. Complexity: O(1).

• Precondition: m.locked != null

fn mutex_into_inner(m: &mut SyncMutex) -> Int

Consume the mutex and return the raw handle. Params: m - the mutex (consumed). Returns: the address of the atomic owner flag as an integer. Complexity: O(1). Frees the flag storage.

• Precondition: m.locked != null

---

---

---

rwlock.xi

type SyncRwLock

SyncRwLock (the stub's RwLock) - a reader-writer lock protecting shared data.

Field	Type
guard	*Int
readers	*Int
writer	*Int

fn rwlock_new() -> SyncRwLock

Create an unlocked reader-writer lock. Returns: a new lock with no readers and no writer. Complexity: O(1).

• Postcondition: result.guard != null
• Postcondition: result.readers != null
• Postcondition: result.writer != null

fn rwlock_read_lock(l: &mut SyncRwLock)

Acquire a shared read lock, blocking for writers. Params: l - the lock. Complexity: O(1) per poll; blocks while a writer holds the lock.

• Precondition: l.guard != null
• Precondition: l.writer != null

fn rwlock_read_try_lock(l: &mut SyncRwLock) -> Bool

Acquire a read lock without blocking. Params: l - the lock. Returns: true if the read lock was acquired, false if a writer holds it. Complexity: O(1). Never blocks.

• Precondition: l.guard != null
• Precondition: l.writer != null

fn rwlock_read_unlock(l: &mut SyncRwLock)

Release a held read lock. Params: l - the lock. Complexity: O(1).

• Precondition: l.guard != null
• Precondition: l.readers != null

fn rwlock_write_lock(l: &mut SyncRwLock)

Acquire the exclusive write lock, blocking. Params: l - the lock. Complexity: O(1) per poll; blocks while readers are active.

• Precondition: l.guard != null
• Precondition: l.readers != null
• Precondition: l.writer != null

fn rwlock_write_try_lock(l: &mut SyncRwLock) -> Bool

Acquire the write lock without blocking. Params: l - the lock. Returns: true if the write lock was acquired, false if the lock is held. Complexity: O(1). Never blocks.

• Precondition: l.guard != null
• Precondition: l.readers != null
• Precondition: l.writer != null

fn rwlock_write_unlock(l: &mut SyncRwLock)

Release a held write lock. Params: l - the lock. Complexity: O(1).

• Precondition: l.guard != null
• Precondition: l.writer != null

fn rwlock_is_write_locked(l: &SyncRwLock) -> Bool

True if the lock is held for writing. Params: l - the lock. Returns: whether a writer currently holds the lock. Complexity: O(1).

• Precondition: l.writer != null

fn rwlock_into_inner(l: &mut SyncRwLock) -> Int

Consume the lock and return the raw handle. Params: l - the lock (consumed). Returns: the address of the writer cell as an integer. Complexity: O(1). Frees the state storage.

• Precondition: l.guard != null
• Precondition: l.readers != null
• Precondition: l.writer != null

---

---

---

sync.xi

type Mutex

=== Mutex ===

Field	Type
inner	*UInt8
data	*T

fn new[T](value: T) -> Mutex[T]

Create an unlocked mutex holding value.

• Postcondition: result.inner != null
• Postcondition: result.data != null

fn lock[T](self: Self) -> MutexGuard[T]

Block until the lock is acquired; returns the guard.

• Postcondition: result.mutex.inner == inner
• Postcondition: result.mutex.data == data

fn try_lock[T](self: Self) -> Option[MutexGuard[T]]

Non-blocking lock attempt; None when already locked.

• Precondition: inner != null

fn into_inner[T](self: Self) -> T

Consume the mutex and return the value.

• Precondition: inner != null
• Precondition: data != null

type MutexGuard

RAII guard holding the mutex lock.

Field	Type
mutex	Mutex[T]

fn get[T](self: Self) -> T

Read the guarded value.

• Precondition: mutex.data != null

fn get_mut[T](self: Self) -> T

Mutable access to the guarded value (returns it by value).

• Precondition: mutex.data != null

fn drop[T](self: Self)

Release the lock.

• Precondition: mutex.inner != null

type RwLock

=== RwLock ===

Field	Type
inner	*UInt8
rcond	*UInt8
wcond	*UInt8
data	*T
state	*Int

fn new[T](data: T) -> RwLock[T]

Create an unlocked read-write lock holding data.

• Postcondition: result.inner != null
• Postcondition: result.rcond != null
• Postcondition: result.wcond != null
• Postcondition: result.data != null
• Postcondition: result.state != null

fn read[T](self: Self) -> ReadGuard[T]

Acquire a shared read guard (blocks while a writer holds the lock).

• Precondition: inner != null
• Precondition: state != null

fn write[T](self: Self) -> WriteGuard[T]

Acquire an exclusive write guard.

• Precondition: inner != null
• Precondition: wcond != null
• Precondition: state != null

fn try_read[T](self: Self) -> Option[ReadGuard[T]]

Non-blocking shared read; None when a writer holds the lock.

• Precondition: inner != null
• Precondition: state != null

fn try_write[T](self: Self) -> Option[WriteGuard[T]]

Non-blocking exclusive write; None when the lock is held.

• Precondition: inner != null
• Precondition: state != null

type ReadGuard

RAII guard for shared read access.

Field	Type
lock	RwLock[T]

fn get[T](self: Self) -> T

Read the guarded value.

• Precondition: lock.data != null

fn drop[T](self: Self)

Release the shared read lock.

• Precondition: lock.inner != null
• Precondition: lock.state != null

type WriteGuard

RAII guard for exclusive write access.

Field	Type
lock	RwLock[T]

fn get[T](self: Self) -> T

Read the guarded value.

• Precondition: lock.data != null

fn get_mut[T](self: Self) -> T

Mutable access to the guarded value (returns it by value).

• Precondition: lock.data != null

fn drop[T](self: Self)

Release the exclusive lock.

• Precondition: lock.inner != null
• Precondition: lock.state != null

type Condvar

=== Condvar ===

Field	Type
inner	*UInt8

fn new() -> Condvar

Create a condition variable.

• Postcondition: result.inner != null

fn wait[T](self: Self, guard: MutexGuard[T]) -> MutexGuard[T]

Wait for a notification, releasing and re-acquiring the mutex.

• Precondition: inner != null
• Precondition: guard.mutex.inner != null

fn notify_one(self: Self)

Wake one waiting thread.

• Precondition: inner != null

fn notify_all(self: Self)

Wake all waiting threads.

• Precondition: inner != null

type Once

=== Once ===

Field	Type
inner	*UInt8
state	*Int

fn new() -> Once

Create a one-shot initializer.

• Postcondition: result.inner != null
• Postcondition: result.state != null

fn call_once(self: Self, f: fn() -> Unit)

Run f exactly once; later calls return immediately.

• Precondition: inner != null
• Precondition: state != null

fn is_completed(self: Self) -> Bool

True when the initializer already ran.

• Precondition: state != null

type Barrier

=== Barrier ===

Field	Type
inner	*UInt8
cond	*UInt8
count	Int
waiting	*Int
generation	*Int

Invariants: - count > 0

fn new(n: Int) -> Barrier

Create a barrier for n threads (n is clamped to at least 1).

• Precondition: n > 0

fn wait(self: Self)

Block until n threads arrive, then release them together.

• Precondition: inner != null
• Precondition: cond != null
• Precondition: waiting != null
• Precondition: generation != null

type Arc

=== Arc (Atomic Reference Counted) ===

Field	Type
ptr	*ArcInner[T]

Invariants: - ptr != null => (*ptr).count >= 1

type ArcInner

Control block behind Arc: atomic strong count plus the value.

Field	Type
count	*Int
value	T

fn new[T](value: T) -> Arc[T]

Allocate a shared-ownership pointer with strong count 1.

• Postcondition: result.strong_count() == 1

fn clone[T](self: Self) -> Arc[T]

Increment the strong count and return a second handle.

• Precondition: ptr != null
• Postcondition: strong_count() == strong_count()@pre + 1

fn get[T](self: Self) -> T

Read the shared value (by value).

• Precondition: ptr != null

fn strong_count[T](self: Self) -> Int

Current strong count (atomic).

• Precondition: ptr != null
• Postcondition: result >= 1

fn ptr_eq[T, U](self: Self, other: &Arc[U]) -> Bool

True when both handles point at the same control block.

• Precondition: true

fn drop[T](self: Self)

Decrement the strong count; free when it reaches zero.

• Precondition: ptr != null

fn deref[T](self: Self) -> &T

Generated summary: Method; Takes no arguments; returns &T. No source comment yet.

• Precondition: ptr != null
• Postcondition: true

fn as_ref[T](self: Self) -> &T

Generated summary: Method; Takes no arguments; returns &T. No source comment yet.

• Precondition: ptr != null

type AtomicBool

=== AtomicBool -- real atomic operations ===

Field	Type
ptr	*Int

fn new(val: Bool) -> AtomicBool

Create an atomic bool.

• Postcondition: result.ptr != null

fn load(self: Self) -> Bool

Current value with acquire ordering.

• Precondition: ptr != null

fn store(self: Self, val: Bool)

Store with release ordering.

• Precondition: ptr != null

fn swap(self: Self, val: Bool) -> Bool

Atomically replace the value, returning the previous one.

• Precondition: ptr != null

fn compare_exchange(self: Self, current: Bool, new: Bool) -> Bool

Set to new when the value equals current; true on success.

• Precondition: ptr != null

type AtomicInt

=== AtomicInt -- real atomic operations ===

Field	Type
ptr	*Int

fn new(val: Int) -> AtomicInt

Create an atomic Int.

• Postcondition: result.ptr != null

fn load(self: Self) -> Int

Current value with acquire ordering.

• Precondition: ptr != null

fn store(self: Self, val: Int) -> AtomicInt

Store with release ordering; returns the atomic.

• Precondition: ptr != null

fn fetch_add(self: Self, val: Int) -> Int

Atomically add, returning the previous value.

• Precondition: ptr != null

fn fetch_sub(self: Self, val: Int) -> Int

Atomically subtract, returning the previous value.

• Precondition: ptr != null

fn swap(self: Self, val: Int) -> Int

Atomically replace, returning the previous value.

• Precondition: ptr != null

fn compare_exchange(self: Self, current: Int, new: Int) -> Bool

Set to new when the value equals current; true on success.

• Precondition: ptr != null

type Semaphore

A simple counting semaphore backed by an integer counter. Non-blocking: acquire returns false if no permits are available. Thread-safety: NOT atomic -- use Mutex[Semaphore] for shared access.

Field	Type
count	Int
max	Int

fn sem_new(permits: Int) -> Semaphore

Creates a new semaphore with permits initial available permits. Complexity: O(1).

• Postcondition: result.count == permits
• Postcondition: result.max == permits

fn sem_try_acquire(s: &mut Semaphore) -> Bool

Attempts to acquire one permit. Returns true on success, false if none available. Non-blocking. Complexity: O(1).

• Postcondition: (result == false) => (s.count <= 0)

fn sem_acquire(s: &mut Semaphore) -> Bool

Alias for sem_try_acquire. Non-blocking. Complexity: O(1).

• Postcondition: (result == false) => (s.count <= 0)

fn sem_release(s: &mut Semaphore)

Releases one permit back to the semaphore, up to the maximum. Complexity: O(1).

• Precondition: s.count <= s.max

fn sem_available(s: &Semaphore) -> Int

Returns the number of currently available permits. Complexity: O(1).

• Postcondition: result == s.count

fn barrier_new(n: Int) -> Barrier

Creates a new barrier for n threads. Wraps Barrier.new. Complexity: O(1).

• Precondition: n > 0
• Postcondition: result.count == n

fn barrier_wait(b: &mut Barrier) -> Bool

Waits at the barrier. Returns true when this thread is the last to arrive and the barrier releases all waiters. Returns false otherwise. Complexity: O(1) lock operations; blocks until all threads arrive.

• Precondition: b.inner != null
• Precondition: b.cond != null
• Precondition: b.waiting != null
• Precondition: b.generation != null

fn barrier_reset(b: &mut Barrier)

Resets the barrier waiting count to zero (best-effort). Complexity: O(1). Not safe for concurrent use with active waiters.

• Precondition: b.waiting != null

type CountDownLatch

A simple count-down latch for synchronisation. Thread-safety: NOT atomic -- use Mutex[CountDownLatch] for shared access.

Field	Type
remaining	Int

fn cdl_new(n: Int) -> CountDownLatch

Creates a new count-down latch initialised to n. Complexity: O(1).

• Postcondition: result.remaining == n

fn cdl_count_down(l: &mut CountDownLatch)

Decrements the latch counter by one. Does nothing if already zero. Complexity: O(1).

• Postcondition: l.remaining == l.remaining@pre || l.remaining == l.remaining@pre - 1
• Postcondition: l.remaining >= 0

fn cdl_is_zero(l: &CountDownLatch) -> Bool

Returns true if the latch has reached zero. Complexity: O(1).

• Postcondition: (l.remaining == 0) => (result == true)
• Postcondition: (l.remaining != 0) => (result == false)

fn cdl_wait_spin(l: &mut CountDownLatch)

Spins until the latch reaches zero. Yields the thread between checks. Complexity: O(remaining) busy-wait iterations.

• Postcondition: l.remaining <= 0

fn atomic_load(ai: &AtomicInt) -> Int

Atomically loads the current value. Direct FFI access. Complexity: O(1). Thread-safe.

• Precondition: ai.ptr != null

fn atomic_store(ai: &mut AtomicInt, v: Int)

Atomically stores a new value. Direct FFI access. Complexity: O(1). Thread-safe.

• Precondition: ai.ptr != null

fn atomic_add(ai: &mut AtomicInt, v: Int) -> Int

Atomically adds v to the value. Returns the new value. Complexity: O(1). Thread-safe.

• Precondition: ai.ptr != null

fn atomic_sub(ai: &mut AtomicInt, v: Int) -> Int

Atomically subtracts v from the value. Returns the new value. Complexity: O(1). Thread-safe.

• Precondition: ai.ptr != null

fn atomic_exchange(ai: &mut AtomicInt, v: Int) -> Int

Atomically swaps the value and returns the old value. Complexity: O(1). Thread-safe.

• Precondition: ai.ptr != null

fn atomic_compare_exchange(ai: &mut AtomicInt, expected: Int, new: Int) -> Bool

Atomically compares and exchanges. Stores new if current value equals expected. Returns true if the exchange was performed. Complexity: O(1). Thread-safe.

• Precondition: ai.ptr != null

fn atomic_fetch_add(ai: &mut AtomicInt, v: Int) -> Int

Atomically adds v and returns the OLD value. Complexity: O(1). Thread-safe.

• Precondition: ai.ptr != null

fn atomic_fetch_sub(ai: &mut AtomicInt, v: Int) -> Int

Atomically subtracts v and returns the OLD value. Complexity: O(1). Thread-safe.

• Precondition: ai.ptr != null

---

---