Record Condvarpub

Source

:record(pub) Condvar
  .id (Int 0..)

Description

Condition variable paired with a Mutex. Opaque handle — the field .id holds a host-managed identifier. Spec declares unique; the attribute is dropped here alongside the guard-type locality caveat (divergence #1) to keep the WP-F1 partial compile-clean.

Fields

.id Int(0..)

Implementations

impl Condvar

.condvar-notify-all ( Condvar → Condvar )

Wake every task currently blocked in .wait on this Condvar. Renamed from .notify-all for the same reason as .condvar-notify-one.

.condvar-notify-one ( Condvar → Condvar )

Wake at most one task currently blocked in .wait. With zero waiters this is a no-op. Renamed from spec-exact .notify-one to .condvar-notify-one to avoid colliding with a future trait method of the same name (matches .mutex-lock / .barrier-wait pattern — see sync.si divergence #4).

.wait ( Condvar (MutexGuard a) → Condvar (MutexGuard a) )

Atomically release the paired guard, block until woken, then re-acquire the guard before returning. Spec signature carries +Executor; omitted for the partial stub. Stays stubbed in the WP-F1 followup because Rust's Condvar::wait needs a live MutexGuard, and the guard record currently wraps a by-value copy of the locked scalar rather than a real RAII borrow (see sync module header divergence #3). Lands with the :dispose runtime wiring.