Struct Waiter 

pub struct Waiter { /* private fields */ }

A waiter that can put the current thread to sleep until it is woken up by the associated Waker.

By definition, a waiter belongs to the current thread, so it cannot be sent to another thread and its reference cannot be shared between threads.

Implementations

impl Waiter

pub closed spec fn rel_waker(self, waker: Arc<Waker>) -> bool

Checks if the input waker is the associated waker of the current waiter.

impl Waiter

pub exec fn new_pair() -> ret : (Self, Arc<Waker>)

ensures

ret.0.rel_waker(ret.1),

Creates a waiter and its associated Waker.

pub exec fn wait(&self)

Waits until the waiter is woken up by calling Waker::wake_up on the associated Waker.

This method returns immediately if the waiter has been woken since the end of the last call to this method (or since the waiter was created, if this method has not been called before). Otherwise, it puts the current thread to sleep until the waiter is woken up.

pub exec fn wait_until_or_cancelled<F, R, FCancel, E>( &self, cond: F, cancel_cond: FCancel, ) -> ret : Result<R, E>

where F: FnMut() -> Option<R>, FCancel: Fn() -> Result<(), E>,

requires

cond.requires(()),

cancel_cond.requires(()),

ensures

match ret {
    Ok(res) => cond.ensures((), Some(res)),
    Err(e) => cancel_cond.ensures((), Err(e)),
},

Waits until some condition is met or the cancel condition becomes true.

This method will return Ok(_) if the condition returns Some(_), and will stop waiting if the cancel condition returns Err(_). In this situation, this method will return the Err(_) generated by the cancel condition.

pub exec fn waker(&self) -> ret : Arc<Waker>

ensures

self.rel_waker(ret),

Gets the associated Waker of the current waiter.

pub exec fn task(&self) -> &Arc<Task>

Returns the task that the associated waker will attempt to wake up.

impl Waiter

pub exec fn drop(self)

VERUS LIMITATION: We implement drop and call it manually because Verus’s support for Drop is incomplete for now.

Trait Implementations

impl !Send for Waiter

impl !Sync for Waiter