vstd/
thread.rs

Help
1#![allow(unused_imports)]
2
3use super::pervasive::*;
4use core::marker;
5use verus_builtin::*;
6use verus_builtin_macros::*;
7
8verus! {
9
10/// Object returned by [`spawn()`](spawn) to allow thread joining.
11/// (Wrapper around [`std::thread::JoinHandle`](https://doc.rust-lang.org/std/thread/struct.JoinHandle.html).)
12///
13/// See the documentation of [`spawn()`](spawn) for more details.
14#[verifier::external_body]
15#[verifier::reject_recursive_types(Ret)]
16pub struct JoinHandle<Ret> {
17    handle: std::thread::JoinHandle<Ret>,
18}
19
20impl<Ret> JoinHandle<Ret> {
21    /// Predicate restricting the possible return values. This is determined by the
22    /// postcondition of the closure provided when calling `spawn()`.
23    pub uninterp spec fn predicate(&self, ret: Ret) -> bool;
24
25    /// Wait for a thread to complete.
26    #[verifier::external_body]
27    pub fn join(self) -> (r_result: Result<Ret, ()>)
28        ensures
29            match r_result {
30                Result::Ok(r) => self.predicate(r),
31                Result::Err(_) => true,
32            },
33    {
34        let res = std::panic::catch_unwind(
35            std::panic::AssertUnwindSafe(
36                ||
37                    {
38                        match self.handle.join() {
39                            Ok(v) => Ok(v),
40                            Err(_) => Err(()),
41                        }
42                    },
43            ),
44        );
45        match res {
46            Ok(res) => res,
47            Err(_) => {
48                println!("panic on join");
49                std::process::abort();
50            },
51        }
52    }
53}
54
55/// Spawns a thread. (Wrapper around [`std::thread::spawn`](https://doc.rust-lang.org/std/thread/fn.spawn.html).)
56///
57/// This takes as input a `FnOnce` closure with no arguments.
58/// The `spawn` returns a [`JoinHandle`], on which the client can call
59/// [`join()`](JoinHandle::join) to wait
60/// for the thread to complete. The return value of the closure is returned via `join()`.
61///
62/// The closure must be callable (i.e., its precondition must be satisfied)
63/// but it may have an arbitrary postcondition. The postcondition is passed through
64/// the `JoinHandle` via [`JoinHandle::predicate()`](JoinHandle::predicate).
65///
66/// ### Example
67///
68/// ```rust,ignore
69/// struct MyInteger {
70///     u: u64,
71/// }
72///
73/// fn main() {
74///     // Construct an object to pass into the thread.
75///     let my_int = MyInteger { u: 5 };
76///
77///     // Spawn a new thread.
78///     let join_handle = spawn(move || {
79///         ensures(|return_value: MyInteger|
80///             return_value.u == 20);
81///
82///         // Move the `my_int` object into the closure.
83///         let mut my_int_on_another_thread = my_int;
84///
85///         // Update its value.
86///         my_int_on_another_thread.u = 20;
87///
88///         // Return it.
89///         my_int_on_another_thread
90///     });
91///
92///     // Wait for the thread to finish its work.
93///     let result_my_int = join_handle.join();
94///
95///     match result_my_int {
96///         Result::Ok(my_int) => {
97///             // Obtain the `MyInteger` object that was passed
98///             // back from the spawned thread.
99///             // Assert that it has the right value.
100///             assert(my_int.u == 20);
101///         }
102///         Result::Err(_) => { }
103///     }
104/// }
105/// ```
106#[verifier::external_body]
107pub fn spawn<F, Ret>(f: F) -> (handle: JoinHandle<Ret>) where
108    F: FnOnce() -> Ret,
109    F: Send + 'static,
110    Ret: Send + 'static,
111
112    requires
113        f.requires(()),
114    ensures
115        forall|ret: Ret| #[trigger] handle.predicate(ret) ==> f.ensures((), ret),
116{
117    let res = std::panic::catch_unwind(
118        std::panic::AssertUnwindSafe(
119            ||
120                {
121                    let handle = std::thread::spawn(move || f());
122                    JoinHandle { handle }
123                },
124        ),
125    );
126    match res {
127        Ok(res) => res,
128        Err(_) => {
129            println!("panic on spawn");
130            std::process::abort();
131        },
132    }
133}
134
135/// Wrapper around Rust's
136/// [`ThreadId`](https://doc.rust-lang.org/std/thread/struct.ThreadId.html)
137/// object. This is an opaque type.
138// Note: Rust defines ThreadId as an opaque type. Rust guarantees that ThreadIds
139// will never be reused. There's also an `as_u64()` method, but it's unstable,
140// and right now it's not clear if it's going to have the same guarantee.
141// Regardless, it seems best to stick with Rust's opaque type here.
142#[verifier::external_body]
143pub struct ThreadId {
144    thread_id: std::thread::ThreadId,
145}
146
147/// Proof object that guarantees the owning thread has the given ThreadId.
148#[cfg(verus_keep_ghost)]
149#[verifier::external_body]
150pub tracked struct IsThread {}
151
152#[cfg(verus_keep_ghost)]
153impl !Sync for IsThread {
154
155}
156
157#[cfg(verus_keep_ghost)]
158impl !Send for IsThread {
159
160}
161
162// TODO: remove this when !Sync, !Send are supported by stable Rust
163#[cfg(not(verus_keep_ghost))]
164#[verifier::external_body]
165pub tracked struct IsThread {
166    _no_send_sync: core::marker::PhantomData<*const ()>,
167}
168
169impl IsThread {
170    pub uninterp spec fn view(&self) -> ThreadId;
171
172    /// Guarantees that any two `IsThread` objects on the same thread
173    /// will have the same ID.
174    pub axiom fn agrees(tracked self, tracked other: IsThread)
175        ensures
176            self@ == other@,
177    ;
178}
179
180#[verifier::external]
181impl Clone for IsThread {
182    #[cfg(verus_keep_ghost)]
183    fn clone(&self) -> Self {
184        IsThread {  }
185    }
186
187    #[cfg(not(verus_keep_ghost))]
188    fn clone(&self) -> Self {
189        IsThread { _no_send_sync: Default::default() }
190    }
191}
192
193impl Copy for IsThread {
194
195}
196
197/// Gets the current thread ID using Rust's [`Thread::id()`](https://doc.rust-lang.org/std/thread/struct.Thread.html#method.id)
198/// under the hood. Also returns a ghost object representing proof of being on this thread.
199#[verifier::external_body]
200pub fn thread_id() -> (res: (ThreadId, Tracked<IsThread>))
201    ensures
202        res.1@@ == res.0,
203{
204    let id: std::thread::ThreadId = std::thread::current().id();
205    let id = ThreadId { thread_id: id };
206    (id, Tracked::assume_new())
207}
208
209/// Returns _just_ the ghost object, without physically obtaining the thread ID.
210pub axiom fn ghost_thread_id() -> (tracked res: IsThread);
211
212/// Tracked object that makes any tracked object `Send` or `Sync`.
213/// Requires the client to prove that they are the correct thread in order to
214/// access the underlying object.
215#[verifier::external_body]
216#[verifier::accept_recursive_types(V)]
217tracked struct ThreadShareable<V> {
218    phantom: marker::PhantomData<V>,
219}
220
221#[verifier::external]
222unsafe impl<V> Sync for ThreadShareable<V> {
223
224}
225
226#[verifier::external]
227unsafe impl<V> Send for ThreadShareable<V> {
228
229}
230
231impl<V> ThreadShareable<V> {
232    pub uninterp spec fn view(&self) -> V;
233
234    pub uninterp spec fn id(&self) -> ThreadId;
235
236    /// Recover the inner value provide we are on the same thread.
237    pub axiom fn into(tracked self, tracked is_thread: IsThread) -> (tracked res: V)
238        requires
239            self.id() == is_thread@,
240        ensures
241            res == self@,
242    ;
243
244    /// Borrow the inner value provide we are on the same thread.
245    pub axiom fn borrow(tracked &self, tracked is_thread: IsThread) -> (tracked res: &V)
246        requires
247            self.id() == is_thread@,
248        ensures
249            *res == self@,
250    ;
251}
252
253impl<V: Send> ThreadShareable<V> {
254    /// Recover the inner value.
255    /// Unlike `into`, this has no thread requirement, but it does
256    /// require the inner type to be `Send`.
257    pub axiom fn send_into(tracked self) -> (tracked res: V)
258        ensures
259            res == self@,
260    ;
261}
262
263impl<V: Sync> ThreadShareable<V> {
264    /// Borrow the inner value.
265    /// Unlike `borrow`, this has no thread requirement, but it does
266    /// require the inner type to be `Sync`.
267    pub axiom fn sync_borrow(tracked &self) -> (tracked res: &V)
268        ensures
269            *res == self@,
270    ;
271}
272
273} // verus!
vstd/thread.rs

vstd/
thread.rs
