Function creusot_contracts::std::thread::scope

pub fn scope<'env, F, T>(f: F) -> T
where
    F: for<'scope> FnOnce(&'scope Scope<'scope, 'env>) -> T,

Create a scope for spawning scoped threads.

The function passed to scope will be provided a Scope object, through which scoped threads can be spawned.

Unlike non-scoped threads, scoped threads can borrow non-'static data, as the scope guarantees all threads will be joined at the end of the scope.

All threads spawned within the scope that haven’t been manually joined will be automatically joined before this function returns.

Panics

If any of the automatically joined threads panicked, this function will panic.

If you want to handle panics from spawned threads, join them before the end of the scope.

Example

use std::thread;

let mut a = vec![1, 2, 3];
let mut x = 0;

thread::scope(|s| {
    s.spawn(|| {
        println!("hello from the first scoped thread");
        // We can borrow `a` here.
        dbg!(&a);
    });
    s.spawn(|| {
        println!("hello from the second scoped thread");
        // We can even mutably borrow `x` here,
        // because no other threads are using it.
        x += a[0] + a[2];
    });
    println!("hello from the main thread");
});

// After the scope, we can modify and access our variables again:
a.push(4);
assert_eq!(x, a.len());

Lifetimes

Scoped threads involve two lifetimes: 'scope and 'env.

The 'scope lifetime represents the lifetime of the scope itself. That is: the time during which new scoped threads may be spawned, and also the time during which they might still be running. Once this lifetime ends, all scoped threads are joined. This lifetime starts within the scope function, before f (the argument to scope) starts. It ends after f returns and all scoped threads have been joined, but before scope returns.

The 'env lifetime represents the lifetime of whatever is borrowed by the scoped threads. This lifetime must outlast the call to scope, and thus cannot be smaller than 'scope. It can be as small as the call to scope, meaning that anything that outlives this call, such as local variables defined right before the scope, can be borrowed by the scoped threads.

The 'env: 'scope bound is part of the definition of the Scope type.