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; // TODO: [VL] Rename valid_result.
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    mod std {
48        mod thread {
49            impl<T> JoinHandle<T> {
50                #[ensures(true)] // no spec, but you can call this if you want
51                fn is_finished(&self) -> bool;
52            }
53
54            impl<T> ScopedJoinHandle<'_, T> {
55                #[ensures(true)] // no spec, but you can call this if you want
56                fn is_finished(&self) -> bool;
57            }
58        }
59    }
60}
61
62/// Creusot wrapper around [`std::thread::spawn`].
63///
64/// The only difference is that the closure gives access to a fresh token object
65#[requires(forall<t: Ghost<Tokens>> (forall<ns> t.contains(ns)) ==> f.precondition((t,)))]
66#[ensures(exists<t: Ghost<Tokens>> (forall<ns> t.contains(ns)) && forall<r> result.valid_result(r) ==> f.postcondition_once((t,), r))]
67#[trusted]
68pub fn spawn<F, T>(f: F) -> JoinHandle<T>
69where
70    F: FnOnce(Ghost<Tokens>) -> T + Send + 'static,
71    T: Send + 'static,
72{
73    ::std::thread::spawn(|| f(Tokens::new()))
74}
75
76/// Creusot's replacement for [`Scope`].
77pub struct Scope<'scope, 'env: 'scope> {
78    inner: &'scope thread::Scope<'scope, 'env>,
79}
80
81impl<'scope, 'env: 'scope> Scope<'scope, 'env> {
82    #[requires(forall<t: Ghost<Tokens>> (forall<ns> t.contains(ns)) ==> f.precondition((t,)))]
83    #[ensures(exists<t: Ghost<Tokens>> (forall<ns> t.contains(ns)) && forall<r> result.valid_result(r) ==> f.postcondition_once((t,), r))]
84    #[trusted]
85    pub fn spawn<F, T>(&mut self, f: F) -> ScopedJoinHandle<'scope, T>
86    where
87        F: FnOnce(Ghost<Tokens>) -> T + Send + 'scope,
88        T: Send + 'scope,
89    {
90        self.inner.spawn(|| f(Tokens::new()))
91    }
92}
93
94/// Creusot wrapper around [`std::thread::scope`].
95#[requires(forall<s> inv(s) ==> f.precondition((s,)))]
96#[ensures(exists<s> inv(s) && f.postcondition_once((s,),result))]
97#[trusted]
98pub fn scope<'env, F, T>(f: F) -> T
99where
100    F: for<'scope> FnOnce(&mut Scope<'scope, 'env>) -> T,
101{
102    ::std::thread::scope(|s| f(&mut Scope { inner: s }))
103}
creusot_std/std/thread.rs

creusot_std/std/
thread.rs
