WaitQueue

Struct WaitQueue

pub struct WaitQueue { /* private fields */ }

Expand description

A wait queue.

One may wait on a wait queue to put its executing thread to sleep. Multiple threads may be the waiters of a wait queue. Other threads may invoke the wake-family methods of a wait queue to wake up one or many waiting threads.

Implementations§

impl WaitQueue

pub closed spec fn type_inv(self) -> bool

impl WaitQueue

pub const exec fn new() -> Self

Creates a new, empty wait queue.

pub exec fn wait_until<F, R>(&self, cond: F) -> ret : R
where F: FnMut() -> Option<R>,

requires

cond.requires(()),

ensures

cond.ensures((), Some(ret)),

Waits until some condition is met.

This method takes a closure that tests a user-given condition. The method only returns if the condition returns Some(_). A waker thread should first make the condition Some(_), then invoke the wake-family method. This ordering is important to ensure that waiter threads do not lose any wakeup notifications.

By taking a condition closure, this wait-wakeup mechanism becomes more efficient and robust.

pub exec fn wake_one(&self) -> r : bool

Wakes up one waiting thread, if there is one at the point of time when this method is called, returning whether such a thread was woken up.

pub exec fn wake_all(&self) -> r : usize

Wakes up all waiting threads, returning the number of threads that were woken up.

Trait Implementations§

impl Default for WaitQueue

exec fn default() -> Self

Auto Trait Implementations§

impl !Freeze for WaitQueue

impl !RefUnwindSafe for WaitQueue

impl Send for WaitQueue

impl Sync for WaitQueue

impl Unpin for WaitQueue

impl UnwindSafe for WaitQueue

Blanket Implementations§

impl<T> Any for T
where T: 'static + ?Sized,

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more

impl<T> Borrow<T> for T
where T: ?Sized,

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more

impl<T> BorrowMut<T> for T
where T: ?Sized,

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more

impl<T> From<T> for T

fn from(t: T) -> T

Returns the argument unchanged.

impl<T, VERUS_SPEC__A> FromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: From<T>,

fn obeys_from_spec() -> bool

fn from_spec(v: T) -> VERUS_SPEC__A

impl<T, U> Into<U> for T
where U: From<T>,

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

impl<T, VERUS_SPEC__A> IntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: Into<T>,

fn obeys_into_spec() -> bool

fn into_spec(self) -> T

impl<T, U> IntoSpecImpl<U> for T
where U: From<T>,

fn obeys_into_spec() -> bool

fn into_spec(self) -> U

impl<T, U> TryFrom<U> for T
where U: Into<T>,

type Error = Infallible

The type returned in the event of a conversion error.

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.

impl<T, VERUS_SPEC__A> TryFromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryFrom<T>,

fn obeys_try_from_spec() -> bool

fn try_from_spec( v: T, ) -> Result<VERUS_SPEC__A, <VERUS_SPEC__A as TryFrom<T>>::Error>

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.

impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryInto<T>,

fn obeys_try_into_spec() -> bool

fn try_into_spec(self) -> Result<T, <VERUS_SPEC__A as TryInto<T>>::Error>

impl<T, U> TryIntoSpecImpl<U> for T
where U: TryFrom<T>,

fn obeys_try_into_spec() -> bool

fn try_into_spec(self) -> Result<U, <U as TryFrom<T>>::Error>