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

ostd/sync/
spin.rs
