Function vstd::thread::spawn

source · 
pub exec fn spawn<F, Ret>(f: F) -> handle : JoinHandle<Ret>
where
    F: FnOnce() -> Ret + Send + 'static,
    Ret: Send + 'static,
Expand description
requires
f.requires(()),
ensures
forall |ret: Ret| #[trigger] handle.predicate(ret) ==> f.ensures((), ret),

Spawns a thread. (Wrapper around std::thread::spawn.)

This takes as input a FnOnce closure with no arguments. The spawn returns a JoinHandle, on which the client can call join() to wait for the thread to complete. The return value of the closure is returned via join().

The closure must be callable (i.e., its precondition must be satisfied) but it may have an arbitrary postcondition. The postcondition is passed through the JoinHandle via JoinHandle::predicate().

§Example

ⓘ
struct MyInteger {
    u: u64,
}

fn main() {
    // Construct an object to pass into the thread.
    let my_int = MyInteger { u: 5 };

    // Spawn a new thread.
    let join_handle = spawn(move || {
        ensures(|return_value: MyInteger|
            return_value.u == 20);

        // Move the `my_int` object into the closure.
        let mut my_int_on_another_thread = my_int;

        // Update its value.
        my_int_on_another_thread.u = 20;

        // Return it.
        my_int_on_another_thread
    });

    // Wait for the thread to finish its work.
    let result_my_int = join_handle.join();

    match result_my_int {
        Result::Ok(my_int) => {
            // Obtain the `MyInteger` object that was passed
            // back from the spawned thread.
            // Assert that it has the right value.
            assert(my_int.u == 20);
        }
        Result::Err(_) => { }
    }
}