vstd/thread.rs
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!