Struct ThreadToken 

pub struct ThreadToken(/* private fields */);

A special token asserting the liveness of a given thread.

You can create one by giving up a Tokens containing the THREAD_TOKEN namespace.

For now, it has only one special property: it can be used to express that the number of threads is bounded, in particular it is less than Self::max_live_threads. This might also be used in the future to carry thread ids.

Implementations

impl ThreadToken

pub fn max_live_threads() -> Int

Maximum number of threads that can be running simultaneously.

logic(opaque)

ensures

result < usize::MAX@ / 2

pub fn get_thread_token<'a>(tokens: Tokens<'a>) -> &'a mut Self

Get a temporary thread token, that asserts that the current thread is still alive.

To ensure that there is only one such token per thread, you need to temporarily give a Tokens object containing the THREAD_TOKEN namespace.

requires

tokens.contains(THREAD_TOKEN())

ghost

pub fn bound_thread_number(thread_tokens: &Seq<Self>)

Ghost lemma, to bound the total number of threads.

We are certain that it is impossible to spawn more than Self::max_live_threads threads at the same time ; and, each ThreadToken is associated to exactly one live thread.

ghost

ensures

thread_tokens.len() <= Self::max_live_threads()