ostd/sync/
mutex.rs

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

ostd/sync/
mutex.rs
