creusot_std/std/
thread.rs

1use crate::{ghost::invariant::Tokens, prelude::*};
2use ::std::thread::{self, JoinHandle, ScopedJoinHandle};
3
4/// Extension trait for [`JoinHandle`].
5pub trait JoinHandleExt<T> {
6    /// Predicate that specifies the valid return results for the handle.
7    #[logic]
8    fn valid_result(self, x: T) -> bool;
9
10    /// This function is a wrapper `self.join().unwrap()`.
11    ///
12    /// This function panics only on stack-overflow or OOM on the spawned thread.
13    // NOTE: This is a way to avoid ::std::thread::Result, which:
14    //  - contains a dyn;
15    //  - we don't know how to handle the Err case in Creusot.
16    #[ensures(self.valid_result(result))]
17    fn join_unwrap(self) -> T;
18}
19
20impl<T> JoinHandleExt<T> for JoinHandle<T> {
21    #[logic(opaque)]
22    fn valid_result(self, _x: T) -> bool {
23        dead
24    }
25
26    #[ensures(self.valid_result(result))]
27    #[trusted]
28    fn join_unwrap(self) -> T {
29        self.join().unwrap()
30    }
31}
32
33impl<T> JoinHandleExt<T> for ScopedJoinHandle<'_, T> {
34    #[logic(opaque)]
35    fn valid_result(self, _x: T) -> bool {
36        dead
37    }
38
39    #[ensures(self.valid_result(result))]
40    #[trusted]
41    fn join_unwrap(self) -> T {
42        self.join().unwrap()
43    }
44}
45
46extern_spec! {
47    impl<T> JoinHandle<T> {
48        #[ensures(true)] // no spec, but you can call this if you want
49        fn is_finished(&self) -> bool;
50    }
51
52    impl<T> ScopedJoinHandle<'_, T> {
53        #[ensures(true)] // no spec, but you can call this if you want
54        fn is_finished(&self) -> bool;
55    }
56}
57
58/// Creusot wrapper around [`std::thread::spawn`].
59///
60/// The only difference is that the closure gives access to a fresh token object
61#[requires(forall<t: Ghost<Tokens>> (forall<ns> t.contains(ns)) ==> f.precondition((t,)))]
62#[ensures(exists<t: Ghost<Tokens>> (forall<ns> t.contains(ns)) && forall<r> result.valid_result(r) ==> f.postcondition_once((t,), r))]
63#[trusted]
64pub fn spawn<F, T>(f: F) -> JoinHandle<T>
65where
66    F: FnOnce(Ghost<Tokens>) -> T + Send + 'static,
67    T: Send + 'static,
68{
69    ::std::thread::spawn(|| f(Tokens::new()))
70}
71
72/// Creusot's replacement for [`Scope`].
73pub struct Scope<'scope, 'env: 'scope> {
74    inner: &'scope thread::Scope<'scope, 'env>,
75}
76
77impl<'scope, 'env: 'scope> Scope<'scope, 'env> {
78    #[requires(forall<t: Ghost<Tokens>> (forall<ns> t.contains(ns)) ==> f.precondition((t,)))]
79    #[ensures(exists<t: Ghost<Tokens>> (forall<ns> t.contains(ns)) && forall<r> result.valid_result(r) ==> f.postcondition_once((t,), r))]
80    #[trusted]
81    pub fn spawn<F, T>(&mut self, f: F) -> ScopedJoinHandle<'scope, T>
82    where
83        F: FnOnce(Ghost<Tokens>) -> T + Send + 'scope,
84        T: Send + 'scope,
85    {
86        self.inner.spawn(|| f(Tokens::new()))
87    }
88}
89
90/// Creusot wrapper around [`std::thread::scope`].
91#[requires(forall<s> inv(s) ==> f.precondition((s,)))]
92#[ensures(exists<s> inv(s) && f.postcondition_once((s,),result))]
93#[trusted]
94pub fn scope<'env, F, T>(f: F) -> T
95where
96    F: for<'scope> FnOnce(&mut Scope<'scope, 'env>) -> T,
97{
98    ::std::thread::scope(|s| f(&mut Scope { inner: s }))
99}
creusot_std/std/thread.rs

creusot_std/std/
thread.rs
