ostd/sync/
mutex.rs

1// SPDX-License-Identifier: MPL-2.0
2use vstd::atomic_ghost::*;
3use vstd::cell::{
4    self,
5    pcell::{self, *},
6};
7use vstd::prelude::*;
8use vstd_extra::prelude::*;
9use vstd_extra::resource::ghost_resource::excl::*;
10
11use alloc::sync::Arc;
12use core::{
13    cell::UnsafeCell,
14    fmt,
15    ops::{Deref, DerefMut},
16    sync::atomic::Ordering,
17};
18
19use super::WaitQueue;
20
21verus! {
22
23struct_with_invariants! {
24
25/// A mutex with waitqueue.
26pub struct Mutex<T  /* : ?Sized */ > {
27    lock: AtomicBool<_, Option<PointsTo<T>>, _>,
28    queue: WaitQueue,
29    // val: UnsafeCell<T>,
30    val: PCell<T>,
31}
32
33closed spec fn wf(self) -> bool {
34    invariant on lock with (val) is (v: bool, g: Option<PointsTo<T>>) {
35        let active_guard = g is None;
36        &&& v <==> active_guard
37        &&& g is Some ==> g->0.id() == val.id()
38    }
39}
40}
41
42impl<T> Mutex<T> {
43    pub closed spec fn cell_id(self) -> cell::CellId {
44        self.val.id()
45    }
46
47    #[verifier::type_invariant]
48    pub closed spec fn type_inv(self) -> bool {
49        self.wf()
50    }
51
52    /// Creates a new mutex.
53    pub const fn new(val: T) -> Self {
54        let (val, Tracked(perm)) = PCell::new(val);
55        Self {
56            lock: AtomicBool::new(
57                Ghost(val),
58                false,
59                Tracked(Some(perm)),
60            ),
61            queue: WaitQueue::new(),
62            val: val,
63        }
64    }
65}
66
67#[verus_verify]
68impl<T  /* : ?Sized */ > Mutex<T> {
69    /// Acquires the mutex.
70    ///
71    /// This method runs in a block way until the mutex can be acquired.
72    #[track_caller]
73    pub fn lock(&self) -> MutexGuard<'_, T> {
74        self.queue.wait_until(|| self.try_lock())
75    }
76
77    /// Tries to acquire the mutex immediately.
78    #[verus_spec(ret =>
79        ensures
80            ret is Some ==> ret->0.rel_mutex(*self),
81    )]
82    pub fn try_lock(&self) -> Option<MutexGuard<'_, T>> {
83        // Cannot be reduced to `then_some`, or the possible dropping of the temporary
84        // guard will cause an unexpected unlock.
85        // SAFETY: The lock is successfully acquired when creating the guard.
86        proof_decl! {
87            let tracked mut locked_state: Option<PointsTo<T>> = None;
88        }
89        {#[verus_spec(with => Tracked(locked_state))] self.acquire_lock()}.then(
90            || -> (ret: MutexGuard<T>)
91                requires
92                    locked_state is Some,
93                    locked_state -> Some_0.id() == self.cell_id(),
94                ensures
95                    ret.rel_mutex(*self),
96                {unsafe { proof_with!{Tracked(locked_state.tracked_unwrap())}; MutexGuard::new(self) }})
97    }
98
99    /* /// Returns a mutable reference to the underlying data.
100    ///
101    /// This method is zero-cost: By holding a mutable reference to the lock, the compiler has
102    /// already statically guaranteed that access to the data is exclusive.
103    #[verifier::external_body]
104    pub fn get_mut(&mut self) -> &mut T {
105        self.val.get_mut()
106    } */
107
108    /// Releases the mutex and wake up one thread which is blocked on this mutex.
109    #[verus_spec(
110        with
111            Tracked(perm): Tracked<PointsTo<T>>,
112        requires
113            perm.id() == self.cell_id(),
114    )]
115    fn unlock(&self)
116    {
117        proof_with!(Tracked(perm));
118        self.release_lock();
119        self.queue.wake_one();
120    }
121
122    #[verus_spec(ret =>
123        with
124            -> locked_state: Tracked<Option<PointsTo<T>>>,
125        ensures
126            ret ==> locked_state@ is Some && locked_state@->0.id() == self.cell_id(),
127            !ret ==> locked_state@ is None,
128    )]
129    fn acquire_lock(&self) -> bool {
130        proof_decl! {
131            let tracked mut locked_state: Option<PointsTo<T>> = None;
132        }
133        proof! {
134            use_type_invariant(self);
135        }
136        proof_with! { |= Tracked(locked_state) }
137        atomic_with_ghost! {
138            self.lock => compare_exchange(false, true);
139            returning res;
140            ghost perms => {
141                if res is Ok {
142                    let tracked perm = perms.tracked_take();
143                    locked_state = Some(perm);
144                }
145            }
146        }.is_ok()
147    }
148
149    #[verus_spec(
150        with
151            Tracked(perm): Tracked<PointsTo<T>>,
152        requires
153            perm.id() == self.cell_id(),
154    )]
155    fn release_lock(&self)
156    {
157        proof! {
158            use_type_invariant(self);
159        }
160        atomic_with_ghost! {
161            self.lock => store(false);
162            ghost perms => {
163                perms = Some(perm);
164            }
165        }
166    }
167}
168
169/* impl<T: /* ?Sized +  */fmt::Debug> fmt::Debug for Mutex<T> {
170    #[verifier::external_body]
171    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
172        fmt::Debug::fmt(&self.val, f)
173    }
174} */
175#[verifier::external]
176unsafe impl<T: /*?Sized + */Send> Send for Mutex<T> {}
177#[verifier::external]
178unsafe impl<T: /*?Sized + */Send> Sync for Mutex<T> {}
179
180/// A guard that provides exclusive access to the data protected by a [`Mutex`].
181#[verifier::reject_recursive_types(T)]
182#[clippy::has_significant_drop]
183#[must_use]
184#[verus_verify]
185pub struct MutexGuard<'a, T  /* : ?Sized */ > {
186    mutex: &'a Mutex<T>,
187    tracked_perm: Tracked<PointsTo<T>>,
188}
189
190impl<'a, T  /* : ?Sized */ > MutexGuard<'a, T> {
191    #[verifier::type_invariant]
192    closed spec fn type_inv(self) -> bool {
193        self.tracked_perm@.id() == self.mutex.cell_id()
194    }
195
196    /// The value stored in the mutex.
197    pub closed spec fn value(self) -> T {
198        *self.tracked_perm@.value()
199    }
200
201    /// The value stored in the mutex. It is an alias of `Self::value`.
202    pub open spec fn view(self) -> T {
203        self.value()
204    }
205
206    pub closed spec fn rel_mutex(self, mutex: Mutex<T>) -> bool {
207        *self.mutex == mutex
208    }
209}
210
211#[verus_verify]
212impl<'a, T  /* : ?Sized */ > MutexGuard<'a, T> {
213    /// # Safety
214    ///
215    /// The caller must ensure that the given reference of [`Mutex`] lock has been successfully acquired
216    /// in the current context. When the created [`MutexGuard`] is dropped, it will unlock the [`Mutex`].
217    #[verus_spec(ret =>
218        with
219            Tracked(perm): Tracked<PointsTo<T>>,
220        requires
221            perm.id() == mutex.cell_id(),
222        ensures
223            ret.rel_mutex(*mutex),
224    )]
225    unsafe fn new(mutex: &'a Mutex<T>) -> (r: MutexGuard<'a, T>)
226    {
227        MutexGuard { mutex, tracked_perm: Tracked(perm) }
228    }
229}
230
231#[verus_verify]
232impl<T/* : ?Sized */> Deref for MutexGuard<'_, T> {
233    type Target = T;
234
235    #[verus_spec(returns self.view())]
236    fn deref(&self) -> &Self::Target {
237        proof! {
238            use_type_invariant(self);
239        }
240        // unsafe { &*self.mutex.val.get() }
241        self.mutex.val.borrow(Tracked(self.tracked_perm.borrow()))
242    }
243}
244
245#[verus_verify]
246impl<T/* : ?Sized */> DerefMut for MutexGuard<'_, T> {
247    #[verus_spec(ret =>
248        ensures
249            final(self).view() == *final(ret),
250            old(self).view() == *ret,
251    )]
252    fn deref_mut(&mut self) -> &mut Self::Target
253    {
254        proof!{
255            use_type_invariant(&*self);
256        }
257        //unsafe { &mut *self.mutex.val.get() }
258        self.mutex.val.borrow_mut(Tracked(&mut *self.tracked_perm))
259    }
260}
261
262/* impl<T  /* : ?Sized */ > Drop for MutexGuard<'_, T> {
263    fn drop(&mut self)
264    {
265        self.mutex.unlock();
266    }
267} */
268
269impl<T: /* ?Sized*/ > MutexGuard<'_, T> {
270    /// VERUS LIMITATION: We implement `drop` and call it manually because Verus's support for `Drop` is incomplete for now.
271    #[verus_spec]
272    pub fn drop(self) {
273        proof!{use_type_invariant(&self);}
274        proof_with!(self.tracked_perm);
275        self.mutex.unlock();
276    }
277}
278
279/* impl<T: /* ?Sized + */ fmt::Debug> fmt::Debug for MutexGuard<'_, T> {
280    #[verifier::external_body]
281    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
282        fmt::Debug::fmt(&**self, f)
283    }
284} */
285
286impl<T  /* : ?Sized */ > !Send for MutexGuard<'_, T> {}
287
288#[verifier::external]
289unsafe impl<T: /*?Sized +*/ Sync> Sync for MutexGuard<'_, T> {}
290
291#[verus_verify]
292impl<'a, T  /* : ?Sized */ > MutexGuard<'a, T> {
293    /// Returns the [`Mutex`] associated with this guard.
294    #[verus_spec(ret =>
295        ensures
296            guard.rel_mutex(*ret),
297    )]
298    pub fn get_lock(guard: &MutexGuard<'a, T>) -> &'a Mutex<T> {
299        guard.mutex
300    }
301}
302
303} // verus!
304#[cfg(ktest)]
305mod test {
306    use super::*;
307    use crate::prelude::*;
308
309    // A regression test for a bug fixed in [#1279](https://github.com/asterinas/asterinas/pull/1279).
310    #[ktest]
311    fn test_mutex_try_lock_does_not_unlock() {
312        let lock = Mutex::new(0);
313        assert!(!lock.lock.load(Ordering::Relaxed));
314
315        // A successful lock
316        let guard1 = lock.lock();
317        assert!(lock.lock.load(Ordering::Relaxed));
318
319        // A failed `try_lock` won't drop the lock
320        assert!(lock.try_lock().is_none());
321        assert!(lock.lock.load(Ordering::Relaxed));
322
323        // Ensure the lock is held until here
324        drop(guard1);
325    }
326}
ostd/sync/mutex.rs

ostd/sync/
mutex.rs
