ostd/sync/
spin.rs

1// SPDX-License-Identifier: MPL-2.0
2use vstd::atomic_ghost::*;
3use vstd::cell::{self, pcell::*};
4use vstd::prelude::*;
5use vstd_extra::prelude::*;
6
7use core::{
8    cell::UnsafeCell,
9    fmt,
10    marker::PhantomData,
11    ops::{Deref, DerefMut},
12    //    sync::atomic::{AtomicBool, Ordering},
13};
14
15use super::{guard::SpinGuardian, LocalIrqDisabled /*, PreemptDisabled*/};
16//use crate::task::atomic_mode::AsAtomicModeGuard;
17
18/// A spin lock.
19///
20/// # Guard behavior
21///
22/// The type `G' specifies the guard behavior of the spin lock. While holding the lock,
23/// - if `G` is [`PreemptDisabled`], preemption is disabled;
24/// - if `G` is [`LocalIrqDisabled`], local IRQs are disabled.
25///
26/// The `G` can also be provided by other crates other than ostd,
27/// if it behaves similar like [`PreemptDisabled`] or [`LocalIrqDisabled`].
28///
29/// The guard behavior can be temporarily upgraded from [`PreemptDisabled`] to
30/// [`LocalIrqDisabled`] using the [`disable_irq`] method.
31///
32/// [`disable_irq`]: Self::disable_irq
33///
34/// # Verified Properties
35/// ## Verification Design
36/// To verify the correctness of spin lock, we use a ghost permission (i.e., not present in executable Rust). Only the owner of this permission can access the protected data in the cell.
37/// When [`lock`] or [`try_lock`] succeeds, the ghost permission is transferred to the lock guard and given to the user for accessing the protected data.
38/// When the lock guard is dropped, the ghost permission is transferred back to the spin lock.
39///
40/// [`lock`]: Self::lock
41/// [`try_lock`]: Self::try_lock
42///
43/// ## Invariant
44/// The `SpinLock` is internally represented by a struct `SpinLockInner` that contains an `AtomicBool` and a `PCell` to hold the protected data.
45/// We present its formally verified version and invariant below.
46///
47/// The `lock` field is extended with a [`PointsTo<T>`](https://verus-lang.github.io/verus/verusdoc/vstd/cell/pcell/struct.PointsTo.html)
48/// ghost permission to track the ownership of the protected data. This ghost permission is also checked by Rust's ownership and borrowing rules and cannot be duplicated,
49/// thereby ensuring exclusive access to the protected data.
50/// The `val` field is a [`PCell<T>`](https://verus-lang.github.io/verus/verusdoc/vstd/cell/pcell/struct.PCell.html), which behaves like [`UnsafeCell<T>`](https://doc.rust-lang.org/std/cell/struct.UnsafeCell.html) used in the Asterinas mainline, but
51/// only allows verified access through the ghost permission.
52///
53/// When the internal `AtomicBool` is `true`, the permission has been transferred to a `SpinLockGuard` and no one else can acquire the lock.
54/// When it is `false`, the permission to access the `PCell<T>` is stored in the lock, and it must match the `val`'s id.
55/// ```rust
56/// struct_with_invariants! {
57/// struct SpinLockInner<T> {
58///    lock: AtomicBool<_,Option<PointsTo<T>>,_>,
59///    val: PCell<T>,
60/// }
61///
62/// closed spec fn wf(self) -> bool {
63///    invariant on lock with (val) is (v:bool, g:Option<PointsTo<T>>) {
64///        match g {
65///            None => v == true,
66///            Some(perm) => perm.id() == val.id() && !v
67///        }
68///    }
69/// }
70/// }
71/// ```
72///
73/// *Note*: The invariant is encapsulated in [`type_inv`] using the [`#[verifier::type_invariant]`](https://verus-lang.github.io/verus/guide/reference-type-invariants.html?highlight=type_#declaring-a-type-invariant) mechanism.
74/// It internally holds at all steps during the method executions and is **NOT** exposed in the public APIs' pre- and post-conditions.
75///
76/// ## Safety
77/// There are no data races.
78///
79/// ## Functional Correctness
80/// - At most one user can hold the lock at the same time.
81///
82/// [`type_inv`]: Self::type_inv
83#[repr(transparent)]
84#[verus_verify]
85//pub struct SpinLock<T: ?Sized, G = PreemptDisabled> {
86pub struct SpinLock<T, G> {
87    phantom: PhantomData<G>,
88    /// Only the last field of a struct may have a dynamically sized type.
89    /// That's why SpinLockInner is put in the last field.
90    inner: SpinLockInner<T>,
91}
92
93struct_with_invariants! {
94struct SpinLockInner<T> {
95    lock: AtomicBool<_,Option<PointsTo<T>>,_>,
96    val: PCell<T>, //TODO: Waiting the new PCell that supports ?Sized
97    //val: UnsafeCell<T>,
98}
99
100closed spec fn wf(self) -> bool {
101    invariant on lock with (val) is (v:bool, g:Option<PointsTo<T>>) {
102        match g {
103            None => v == true,
104            Some(perm) => perm.id() == val.id() && !v
105        }
106    }
107}
108}
109
110verus! {
111impl<T> SpinLockInner<T>
112{
113    #[verifier::type_invariant]
114    closed spec fn type_inv(self) -> bool{
115        self.wf()
116    }
117}
118
119impl<T, G> SpinLock<T, G> {
120    /// Creates a new spin lock.
121    ///
122    /// # Verified Properties
123    /// ## Safety
124    /// This function is written in safe Rust and there is no undefined behavior.
125    /// ## Preconditions
126    /// None.
127    /// ## Postconditions
128    /// - The function will not panic.
129    /// - The created spin lock satisfies the invariant.
130    pub const fn new(val: T) -> Self
131    {
132        let (val, Tracked(perm)) = PCell::new(val);
133        let lock_inner = SpinLockInner {
134            lock: AtomicBool::new(Ghost(val),false,Tracked(Some(perm))),
135            //val: UnsafeCell::new(val),
136            val: val,
137        };
138        Self {
139            phantom: PhantomData,
140            inner: lock_inner,
141        }
142    }
143}
144
145impl<T,G> SpinLock<T,G>
146{
147    /// Returns the unique [`CellId`](https://verus-lang.github.io/verus/verusdoc/vstd/cell/struct.CellId.html) of the internal `PCell<T>`.
148    pub closed spec fn cell_id(self) -> cell::CellId {
149        self.inner.val.id()
150    }
151
152    /// Public well-formedness predicate for external wrappers.
153    pub closed spec fn wf(self) -> bool {
154        self.type_inv()
155    }
156
157    /// Encapsulates the invariant described in the *Invariant* section of [`SpinLock`].
158    #[verifier::type_invariant]
159    pub closed spec fn type_inv(self) -> bool{
160        self.inner.type_inv()
161    }
162}
163
164/*
165impl<T: ?Sized> SpinLock<T, PreemptDisabled> {
166    /// Converts the guard behavior from disabling preemption to disabling IRQs.
167    pub fn disable_irq(&self) -> &SpinLock<T, LocalIrqDisabled> {
168        let ptr = self as *const SpinLock<T, PreemptDisabled>;
169        let ptr = ptr as *const SpinLock<T, LocalIrqDisabled>;
170        // SAFETY:
171        // 1. The types `SpinLock<T, PreemptDisabled>`, `SpinLockInner<T>` and `SpinLock<T,
172        //    IrqDisabled>` have the same memory layout guaranteed by `#[repr(transparent)]`.
173        // 2. The specified memory location can be borrowed as an immutable reference for the
174        //    specified lifetime.
175        unsafe { &*ptr }
176    }
177}*/
178
179#[verus_verify]
180impl<T /*: ?Sized */, G: SpinGuardian> SpinLock<T, G> {
181    /// Acquires the spin lock.
182    ///
183    /// # Verified Properties
184    /// ## Safety
185    /// There are no data races. The lock ensures exclusive access to the protected data.
186    /// ## Preconditions
187    /// None. (The invariant of `SpinLock` always holds internally.)
188    /// ## Postconditions
189    /// The returned `SpinLockGuard` satisfies its type invariant:
190    /// - An exclusive permission to access the protected data is held by the guard.
191    /// - The guard's permission matches the lock's internal cell ID.
192    /// ## Key Verification Step
193    /// When the internal atomic compare-and-exchange operation in `acquire_lock` succeeds,
194    /// the ghost permission is simultaneously extracted from the lock.
195    /// ```rust
196    /// atomic_with_ghost!  {
197    ///    self.inner.lock => compare_exchange(false, true);
198    ///    returning res;
199    ///    ghost cell_perm => {
200    ///     // Extract the ghost permission when the lock is successfully acquired
201    ///     if res is Ok {
202    ///            perm = Some(cell_perm.tracked_take());
203    ///        }
204    ///    }
205    ///}.is_ok()
206    /// ```
207    pub fn lock(&self) -> SpinLockGuard<'_, T, G> {
208        // Notice the guard must be created before acquiring the lock.
209        proof!{ use_type_invariant(self);}
210        proof_decl!{
211            let tracked perm: PointsTo<T>;
212        }
213        let inner_guard = G::guard();
214        proof_with! {=> Tracked(perm)}
215        self.acquire_lock();
216        SpinLockGuard {
217            lock: self,
218            guard: inner_guard,
219            tracked_perm: Tracked(perm),
220        }
221    }
222
223    /// Tries acquiring the spin lock immediately.
224    ///
225    /// # Verified Properties
226    /// ## Safety
227    /// There are no data races. The lock ensures exclusive access to the protected data.
228    /// ## Preconditions
229    /// None. (The invariant of `SpinLock` always holds internally.)
230    /// ## Postconditions
231    /// If `Some(guard)` is returned, it satisfies its type invariant:
232    /// - An exclusive permission to access the protected data is held by the guard.
233    /// - The guard's permission matches the lock's internal cell ID.
234    pub fn try_lock(&self) -> Option<SpinLockGuard<'_, T, G>> {
235        let inner_guard = G::guard();
236        proof_decl!{
237            let tracked mut perm: Option<PointsTo<T>> = None;
238        }
239        if #[verus_spec(with => Tracked(perm))] self.try_acquire_lock() {
240            let lock_guard = SpinLockGuard {
241                lock: self,
242                guard: inner_guard,
243                tracked_perm: Tracked(perm.tracked_unwrap()),
244            };
245            return Some(lock_guard);
246        }
247        None
248    }
249
250    /*
251    /// Returns a mutable reference to the underlying data.
252    ///
253    /// This method is zero-cost: By holding a mutable reference to the lock, the compiler has
254    /// already statically guaranteed that access to the data is exclusive.
255    pub fn get_mut(&mut self) -> &mut T {
256        self.inner.val.get_mut()
257    }*/
258
259    /// Acquires the spin lock, otherwise busy waiting
260    #[verus_spec(ret =>
261        with
262            -> perm: Tracked<PointsTo<T>>,
263        ensures
264            perm@.id() == self.inner.val.id(),
265            )]
266    #[verifier::exec_allows_no_decreases_clause]
267    fn acquire_lock(&self) {
268        proof_decl!{
269            let tracked mut perm: Option<PointsTo<T>> = None;
270        }
271        proof!{ use_type_invariant(self);}
272        #[verus_spec(
273            invariant self.type_inv(),
274        )]
275        while !#[verus_spec(with => Tracked(perm))]self.try_acquire_lock() {
276            core::hint::spin_loop();
277        }
278
279        proof_decl!{
280            let tracked mut perm = perm.tracked_unwrap();
281        }
282        // VERUS LIMITATION： Explicit return value to bind the ghost permission return value
283        #[verus_spec(with |= Tracked(perm))]
284        ()
285    }
286
287    #[verus_spec(ret =>
288        with
289            -> perm: Tracked<Option<PointsTo<T>>>,
290        ensures
291            ret && perm@ is Some && perm@ -> Some_0.id() == self.inner.val.id() || !ret && perm@ is None,
292            )]
293    fn try_acquire_lock(&self) -> bool {
294        /*self.inner
295            .lock
296            .compare_exchange(false, true, Ordering::Acquire, Ordering::Relaxed)
297            .is_ok()*/
298        proof_decl!{
299            let tracked mut perm: Option<PointsTo<T>> = None;
300        }
301        proof!{ use_type_invariant(self);}
302        proof_with!{ |= Tracked(perm)}
303        atomic_with_ghost!  {
304            self.inner.lock => compare_exchange(false, true);
305            returning res;
306            ghost cell_perm => {
307                if res is Ok {
308                    perm = Some(cell_perm.tracked_take());
309                }
310            }
311        }.is_ok()
312    }
313
314    #[verus_spec(
315        with
316            Tracked(perm): Tracked<PointsTo<T>>,
317        requires
318            perm.id() == self.inner.val.id(),
319    )]
320    fn release_lock(&self) {
321        proof!{
322            use_type_invariant(self);
323        }
324        //self.inner.lock.store(false, Ordering::Release);
325        atomic_with_ghost!{
326            self.inner.lock => store(false);
327            ghost cell_perm => {
328                cell_perm = Some(perm);
329            }
330        }
331    }
332}
333}
334
335/*
336impl<T: ?Sized + fmt::Debug, G> fmt::Debug for SpinLock<T, G> {
337    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
338        fmt::Debug::fmt(&self.inner.val, f)
339    }
340}*/
341
342// SAFETY: Only a single lock holder is permitted to access the inner data of Spinlock.
343#[verifier::external]
344unsafe impl<T: Send, G> Send for SpinLock<T, G> {}
345#[verifier::external]
346unsafe impl<T: Send, G> Sync for SpinLock<T, G> {}
347
348/// A guard that provides exclusive access to the data protected by a [`SpinLock`].
349///
350/// # Verified Properties
351/// ## Verification Design
352/// The guard is extended with a ghost permission field `tracked_perm` that
353/// holds the ghost permission ([`PointsTo<T>`](https://verus-lang.github.io/verus/verusdoc/vstd/cell/pcell/struct.PointsTo.html))
354/// This permission grants exclusive ownership of the protected data and enables verified access to the `PCell<T>`.
355///
356///
357/// ## Invariant
358/// The guard maintains a type invariant ensuring that its ghost permission's ID matches
359/// the lock's internal cell ID. This guarantees that the permission corresponds to the
360/// correct protected data.
361///
362/// ```rust
363/// #[verifier::type_invariant]
364///    spec fn type_inv(self) -> bool{
365///        self.lock.cell_id() == self.tracked_perm@.id()
366///    }
367/// ```
368///
369/// *Note*: The invariant is encapsulated using the [`#[verifier::type_invariant]`](https://verus-lang.github.io/verus/guide/reference-type-invariants.html?highlight=type_#declaring-a-type-invariant) mechanism.
370/// It internally holds at all steps during the method executions and is **NOT** exposed in the public APIs' pre- and post-conditions.
371#[verifier::reject_recursive_types(T)]
372#[verifier::reject_recursive_types(G)]
373#[clippy::has_significant_drop]
374#[must_use]
375#[verus_verify]
376pub struct SpinLockGuard<'a, T /*: ?Sized*/, G: SpinGuardian> {
377    guard: G::Guard,
378    lock: &'a SpinLock<T, G>,
379    /// Ghost permission for verification
380    tracked_perm: Tracked<PointsTo<T>>,
381}
382
383verus! {
384impl<'a, T, G: SpinGuardian> SpinLockGuard<'a, T, G>
385{
386    #[verifier::type_invariant]
387    spec fn type_inv(self) -> bool{
388        self.lock.cell_id() == self.tracked_perm@.id()
389    }
390
391    /// The value stored in the lock.
392    pub closed spec fn value(self) -> T {
393        *self.tracked_perm@.value()
394    }
395
396    /// The value stored in the lock. It is an alias of `Self::value`.
397    pub open spec fn view(self) -> T {
398        self.value()
399    }
400}
401/*
402impl<T: ?Sized, G: SpinGuardian> AsAtomicModeGuard for SpinLockGuard<'_, T, G> {
403    fn as_atomic_mode_guard(&self) -> &dyn crate::task::atomic_mode::InAtomicMode {
404        self.guard.as_atomic_mode_guard()
405    }
406}*/
407
408// FIXME: fix when verus attribute syntax supports Tracked.
409#[verus_verify]
410impl<T: /*?Sized*/, G: SpinGuardian> Deref for SpinLockGuard<'_, T, G> {
411    type Target = T;
412
413    #[verus_spec(returns self.view())]
414    fn deref(&self) -> &T {
415        proof_decl! {
416            let tracked read_perm = self.tracked_perm.borrow();
417        }
418        proof!{
419            use_type_invariant(self);
420        }
421        // unsafe { &*self.lock.inner.val.get() }
422        // The internal implementation of `PCell<T>::borrow` is exactly unsafe { &(*(*self.ucell).get()) },
423        // and here we verify that we have the permission to call `borrow`.
424        self.lock.inner.val.borrow(Tracked(read_perm))
425    }
426}
427
428
429#[verus_verify]
430impl<T: /* ?Sized */, G: SpinGuardian> DerefMut for SpinLockGuard<'_, T, G> {
431    #[verus_spec(ret =>
432        ensures
433            final(self).view() == *final(ret),
434            old(self).view() == *ret,
435    )]
436    fn deref_mut(&mut self) -> &mut Self::Target
437    {
438        proof!{
439            use_type_invariant(&*self);
440        }
441        // unsafe { &mut *self.lock.inner.val.get() }
442        self.lock.inner.val.borrow_mut(Tracked(&mut *self.tracked_perm))
443    }
444}
445}
446
447/* impl<T: ?Sized, G: SpinGuardian> Drop for SpinLockGuard<'_, T, G> {
448    fn drop(&mut self) {
449        self.lock.release_lock();
450    }
451}
452*/
453
454#[verus_verify]
455impl<'a, T /*:?Sized */, G: SpinGuardian> SpinLockGuard<'a, T, G> {
456    /// VERUS LIMITATION: We implement `drop` and call it manually because Verus's support for `Drop` is incomplete for now.
457    #[verus_spec]
458    pub fn drop(self) {
459        proof! {use_type_invariant(&self);}
460        proof_with!(self.tracked_perm);
461        self.lock.release_lock();
462    }
463}
464
465/* impl<T: ?Sized + fmt::Debug, G: SpinGuardian> fmt::Debug for SpinLockGuard<'_, T, G> {
466    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
467        fmt::Debug::fmt(&**self, f)
468    }
469}*/
470
471#[verus_verify]
472impl<T: ?Sized, G: SpinGuardian> !Send for SpinLockGuard<'_, T, G> {}
473
474#[verifier::external]
475// SAFETY: `SpinLockGuard` can be shared between tasks/threads in same CPU.
476// As `lock()` is only called when there are no race conditions caused by interrupts.
477unsafe impl<T: Sync, G: SpinGuardian> Sync for SpinLockGuard<'_, T, G> {}
ostd/sync/spin.rs

ostd/sync/
spin.rs
