ostd/sync/
mutex.rs

1// SPDX-License-Identifier: MPL-2.0
2use vstd::{
3    atomic_ghost::*,
4    cell::{
5        self,
6        pcell::{self, *},
7    },
8    prelude::*,
9};
10use vstd_extra::{prelude::*, resource::ghost_resource::excl::*};
11
12use super::WaitQueue;
13use alloc::sync::Arc;
14use core::{
15    cell::UnsafeCell,
16    fmt,
17    ops::{Deref, DerefMut},
18    sync::atomic::Ordering,
19};
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    ///
110    /// # Safety
111    ///
112    /// The caller must ensure that it has acquired the lock.
113    #[verus_spec(
114        with
115            Tracked(perm): Tracked<PointsTo<T>>,
116        requires
117            perm.id() == self.cell_id(),
118    )]
119    unsafe fn unlock(&self)
120    {
121        // SAFETY: The safety is upheld by the caller.
122        unsafe {
123            proof_with!(Tracked(perm));
124            self.release_lock();
125        }
126        self.queue.wake_one();
127    }
128
129    #[verus_spec(ret =>
130        with
131            -> locked_state: Tracked<Option<PointsTo<T>>>,
132        ensures
133            ret ==> locked_state@ is Some && locked_state@->0.id() == self.cell_id(),
134            !ret ==> locked_state@ is None,
135    )]
136    fn acquire_lock(&self) -> bool {
137        proof_decl! {
138            let tracked mut locked_state: Option<PointsTo<T>> = None;
139        }
140        proof! {
141            use_type_invariant(self);
142        }
143        proof_with! { |= Tracked(locked_state) }
144        atomic_with_ghost! {
145            self.lock => compare_exchange(false, true);
146            returning res;
147            ghost perms => {
148                if res is Ok {
149                    let tracked perm = perms.tracked_take();
150                    locked_state = Some(perm);
151                }
152            }
153        }.is_ok()
154    }
155
156    /// # Safety
157    ///
158    /// The caller must ensure that it has acquired the lock.
159    #[verus_spec(
160        with
161            Tracked(perm): Tracked<PointsTo<T>>,
162        requires
163            perm.id() == self.cell_id(),
164    )]
165    unsafe fn release_lock(&self)
166    {
167        proof! {
168            use_type_invariant(self);
169        }
170        atomic_with_ghost! {
171            self.lock => store(false);
172            ghost perms => {
173                perms = Some(perm);
174            }
175        }
176    }
177}
178
179/* impl<T: /* ?Sized +  */fmt::Debug> fmt::Debug for Mutex<T> {
180    #[verifier::external_body]
181    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
182        fmt::Debug::fmt(&self.val, f)
183    }
184} */
185#[verifier::external]
186unsafe impl<T: /*?Sized + */Send> Send for Mutex<T> {}
187#[verifier::external]
188unsafe impl<T: /*?Sized + */Send> Sync for Mutex<T> {}
189
190/// A guard that provides exclusive access to the data protected by a [`Mutex`].
191#[verifier::reject_recursive_types(T)]
192#[clippy::has_significant_drop]
193#[must_use]
194#[verus_verify]
195pub struct MutexGuard<'a, T  /* : ?Sized */ > {
196    mutex: &'a Mutex<T>,
197    tracked_perm: Tracked<PointsTo<T>>,
198}
199
200impl<'a, T  /* : ?Sized */ > MutexGuard<'a, T> {
201    #[verifier::type_invariant]
202    closed spec fn type_inv(self) -> bool {
203        self.tracked_perm@.id() == self.mutex.cell_id()
204    }
205
206    /// The value stored in the mutex.
207    pub closed spec fn value(self) -> T {
208        *self.tracked_perm@.value()
209    }
210
211    /// The value stored in the mutex. It is an alias of `Self::value`.
212    pub open spec fn view(self) -> T {
213        self.value()
214    }
215
216    pub closed spec fn rel_mutex(self, mutex: Mutex<T>) -> bool {
217        *self.mutex == mutex
218    }
219}
220
221#[verus_verify]
222impl<'a, T  /* : ?Sized */ > MutexGuard<'a, T> {
223    /// # Safety
224    ///
225    /// The caller must ensure that the given reference of [`Mutex`] lock has been successfully acquired
226    /// in the current context. When the created [`MutexGuard`] is dropped, it will unlock the [`Mutex`].
227    #[verus_spec(ret =>
228        with
229            Tracked(perm): Tracked<PointsTo<T>>,
230        requires
231            perm.id() == mutex.cell_id(),
232        ensures
233            ret.rel_mutex(*mutex),
234    )]
235    unsafe fn new(mutex: &'a Mutex<T>) -> (r: MutexGuard<'a, T>)
236    {
237        MutexGuard { mutex, tracked_perm: Tracked(perm) }
238    }
239}
240
241#[verus_verify]
242impl<T/* : ?Sized */> Deref for MutexGuard<'_, T> {
243    type Target = T;
244
245    #[verus_spec(returns self.view())]
246    fn deref(&self) -> &Self::Target {
247        proof! {
248            use_type_invariant(self);
249        }
250        // unsafe { &*self.mutex.val.get() }
251        self.mutex.val.borrow(Tracked(self.tracked_perm.borrow()))
252    }
253}
254
255#[verus_verify]
256impl<T/* : ?Sized */> DerefMut for MutexGuard<'_, T> {
257    #[verus_spec(ret =>
258        ensures
259            final(self).view() == *final(ret),
260            old(self).view() == *ret,
261    )]
262    fn deref_mut(&mut self) -> &mut Self::Target
263    {
264        proof!{
265            use_type_invariant(&*self);
266        }
267        //unsafe { &mut *self.mutex.val.get() }
268        self.mutex.val.borrow_mut(Tracked(&mut *self.tracked_perm))
269    }
270}
271
272/* impl<T  /* : ?Sized */ > Drop for MutexGuard<'_, T> {
273    fn drop(&mut self)
274    {
275        // SAFETY: The mutex is locked.
276        unsafe { self.mutex.unlock() };
277    }
278} */
279
280impl<T: /* ?Sized*/ > MutexGuard<'_, T> {
281    /// VERUS LIMITATION: We implement `drop` and call it manually because Verus's support for `Drop` is incomplete for now.
282    #[verus_spec]
283    pub fn drop(self) {
284        proof!{use_type_invariant(&self);}
285        // SAFETY: The mutex is locked.
286        unsafe {
287            proof_with!(self.tracked_perm);
288            self.mutex.unlock();
289        }
290    }
291}
292
293/* impl<T: /* ?Sized + */ fmt::Debug> fmt::Debug for MutexGuard<'_, T> {
294    #[verifier::external_body]
295    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
296        fmt::Debug::fmt(&**self, f)
297    }
298} */
299
300impl<T  /* : ?Sized */ > !Send for MutexGuard<'_, T> {}
301
302#[verifier::external]
303unsafe impl<T: /*?Sized +*/ Sync> Sync for MutexGuard<'_, T> {}
304
305#[verus_verify]
306impl<'a, T  /* : ?Sized */ > MutexGuard<'a, T> {
307    /// Returns the [`Mutex`] associated with this guard.
308    #[verus_spec(ret =>
309        ensures
310            guard.rel_mutex(*ret),
311    )]
312    pub fn get_lock(guard: &MutexGuard<'a, T>) -> &'a Mutex<T> {
313        guard.mutex
314    }
315}
316
317} // verus!
318#[cfg(ktest)]
319mod test {
320    use super::*;
321    use crate::prelude::*;
322
323    // A regression test for a bug fixed in [#1279](https://github.com/asterinas/asterinas/pull/1279).
324    #[ktest]
325    fn test_mutex_try_lock_does_not_unlock() {
326        let lock = Mutex::new(0);
327        assert!(!lock.lock.load(Ordering::Relaxed));
328
329        // A successful lock
330        let guard1 = lock.lock();
331        assert!(lock.lock.load(Ordering::Relaxed));
332
333        // A failed `try_lock` won't drop the lock
334        assert!(lock.try_lock().is_none());
335        assert!(lock.lock.load(Ordering::Relaxed));
336
337        // Ensure the lock is held until here
338        drop(guard1);
339    }
340}
ostd/sync/mutex.rs

ostd/sync/
mutex.rs
