ostd/sync/
mutex.rs

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

ostd/sync/
mutex.rs
