creusot_std/ghost/
thread.rs

1//! Ghost tokens to reason about the number of threads.
2//!
3//! If you are looking to prove a concurrent algorithm, you might be more
4//! interested in [atomic invariants](crate::ghost::invariant::AtomicInvariant).
5
6use crate::{
7    ghost::invariant::{Tokens, declare_namespace},
8    prelude::*,
9};
10
11declare_namespace! { THREAD_TOKEN }
12
13/// A special token asserting the liveness of a given thread.
14///
15/// You can create one by giving up a [`Tokens`] containing the [`THREAD_TOKEN`]
16/// namespace.
17///
18/// For now, it has only one special property: it can be used to express
19/// that the number of threads is bounded, in particular it is less than
20/// [`Self::max_live_threads`]. This might also be used in the future to carry
21/// thread ids.
22#[opaque]
23#[allow(dead_code)]
24pub struct ThreadToken(());
25
26impl ThreadToken {
27    /// Maximum number of threads that can be running simultaneously.
28    #[trusted]
29    #[logic(opaque)]
30    #[ensures(result < usize::MAX@ / 2)]
31    pub fn max_live_threads() -> Int {
32        dead
33    }
34
35    /// Get a temporary thread token, that asserts that the current thread is
36    /// still alive.
37    ///
38    /// To ensure that there is only one such token per thread, you need to
39    /// temporarily give a `Tokens` object containing the [`THREAD_TOKEN`]
40    /// namespace.
41    #[trusted]
42    #[requires(tokens.contains(THREAD_TOKEN()))]
43    #[check(ghost)]
44    pub fn get_thread_token<'a>(#[allow(unused)] tokens: Tokens<'a>) -> &'a mut Self {
45        panic!("ghost only")
46    }
47
48    /// Ghost lemma, to bound the total number of threads.
49    ///
50    /// We are certain that it is impossible to spawn more than
51    /// [`Self::max_live_threads`] threads _at the same time_ ; and, each
52    /// `ThreadToken` is associated to exactly one _live_ thread.
53    #[check(ghost)]
54    #[trusted]
55    #[ensures(thread_tokens.len() <= Self::max_live_threads())]
56    #[allow(unused_variables)]
57    pub fn bound_thread_number(thread_tokens: &Seq<Self>) {}
58}
creusot_std/ghost/thread.rs

creusot_std/ghost/
thread.rs
