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    /// Public well-formedness predicate for external wrappers.
152    pub closed spec fn wf(self) -> bool {
153        self.type_inv()
154    }
155
156    /// Encapsulates the invariant described in the *Invariant* section of [`SpinLock`].
157    #[verifier::type_invariant]
158    pub closed spec fn type_inv(self) -> bool{
159        self.inner.type_inv()
160    }
161}
162
163/*
164impl<T: ?Sized> SpinLock<T, PreemptDisabled> {
165    /// Converts the guard behavior from disabling preemption to disabling IRQs.
166    pub fn disable_irq(&self) -> &SpinLock<T, LocalIrqDisabled> {
167        let ptr = self as *const SpinLock<T, PreemptDisabled>;
168        let ptr = ptr as *const SpinLock<T, LocalIrqDisabled>;
169        // SAFETY:
170        // 1. The types `SpinLock<T, PreemptDisabled>`, `SpinLockInner<T>` and `SpinLock<T,
171        //    IrqDisabled>` have the same memory layout guaranteed by `#[repr(transparent)]`.
172        // 2. The specified memory location can be borrowed as an immutable reference for the
173        //    specified lifetime.
174        unsafe { &*ptr }
175    }
176}*/
177
178#[verus_verify]
179impl<T /*: ?Sized */, G: SpinGuardian> SpinLock<T, G> {
180    /// Acquires the spin lock.
181    ///
182    /// # Verified Properties
183    /// ## Safety
184    /// There are no data races. The lock ensures exclusive access to the protected data.
185    /// ## Preconditions
186    /// None. (The invariant of `SpinLock` always holds internally.)
187    /// ## Postconditions
188    /// The returned `SpinLockGuard` satisfies its type invariant:
189    /// - An exclusive permission to access the protected data is held by the guard.
190    /// - The guard's permission matches the lock's internal cell ID.
191    /// ## Key Verification Step
192    /// When the internal atomic compare-and-exchange operation in `acquire_lock` succeeds,
193    /// the ghost permission is simultaneously extracted from the lock.
194    /// ```rust
195    /// atomic_with_ghost!  {
196    ///    self.inner.lock => compare_exchange(false, true);
197    ///    returning res;
198    ///    ghost cell_perm => {
199    ///     // Extract the ghost permission when the lock is successfully acquired
200    ///     if res is Ok {
201    ///            perm = Some(cell_perm.tracked_take());
202    ///        }
203    ///    }
204    ///}.is_ok()
205    /// ```
206    #[verus_spec]
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 mut perm: PointsTo<T> = arbitrary_cell_pointsto();
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            v_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    #[verus_spec]
235    pub fn try_lock(&self) -> Option<SpinLockGuard<'_, T, G>> {
236        let inner_guard = G::guard();
237        proof_decl!{
238            let tracked mut perm: Option<PointsTo<T>> = None;
239        }
240        if #[verus_spec(with => Tracked(perm))] self.try_acquire_lock() {
241            let lock_guard = SpinLockGuard {
242                lock: self,
243                guard: inner_guard,
244                v_perm: Tracked(perm.tracked_unwrap()),
245            };
246            return Some(lock_guard);
247        }
248        None
249    }
250
251    /*
252    /// Returns a mutable reference to the underlying data.
253    ///
254    /// This method is zero-cost: By holding a mutable reference to the lock, the compiler has
255    /// already statically guaranteed that access to the data is exclusive.
256    pub fn get_mut(&mut self) -> &mut T {
257        self.inner.val.get_mut()
258    }*/
259
260    /// Acquires the spin lock, otherwise busy waiting
261    #[verus_spec(ret =>
262        with
263            -> perm: Tracked<PointsTo<T>>,
264        ensures
265            perm@.id() == self.inner.val.id(),
266            )]
267    #[verifier::exec_allows_no_decreases_clause]
268    fn acquire_lock(&self) {
269        proof_decl!{
270            let tracked mut perm: Option<PointsTo<T>> = None;
271        }
272        proof!{ use_type_invariant(self);}
273        #[verus_spec(
274            invariant self.type_inv(),
275        )]
276        while !#[verus_spec(with => Tracked(perm))]self.try_acquire_lock() {
277            core::hint::spin_loop();
278        }
279
280        proof_decl!{
281            let tracked mut perm = perm.tracked_unwrap();
282        }
283        // VERUS LIMITATION： Explicit return value to bind the ghost permission return value
284        #[verus_spec(with |= Tracked(perm))]
285        ()
286    }
287
288    #[verus_spec(ret =>
289        with
290            -> perm: Tracked<Option<PointsTo<T>>>,
291        ensures
292            ret && perm@ is Some && perm@ -> Some_0.id() == self.inner.val.id() || !ret && perm@ is None,
293            )]
294    fn try_acquire_lock(&self) -> bool {
295        /*self.inner
296            .lock
297            .compare_exchange(false, true, Ordering::Acquire, Ordering::Relaxed)
298            .is_ok()*/
299        proof_decl!{
300            let tracked mut perm: Option<PointsTo<T>> = None;
301        }
302        proof!{ use_type_invariant(self);}
303        proof_with!{ |= Tracked(perm)}
304        atomic_with_ghost!  {
305            self.inner.lock => compare_exchange(false, true);
306            returning res;
307            ghost cell_perm => {
308                if res is Ok {
309                    perm = Some(cell_perm.tracked_take());
310                }
311            }
312        }.is_ok()
313    }
314
315    #[verus_spec(
316        with
317            Tracked(perm): Tracked<PointsTo<T>>,
318        requires
319            perm.id() == self.inner.val.id(),
320    )]
321    fn release_lock(&self) {
322        proof!{
323            use_type_invariant(self);
324        }
325        //self.inner.lock.store(false, Ordering::Release);
326        atomic_with_ghost!{
327            self.inner.lock => store(false);
328            ghost cell_perm => {
329                cell_perm = Some(perm);
330            }
331        }
332    }
333}
334
335
336/*
337impl<T: ?Sized + fmt::Debug, G> fmt::Debug for SpinLock<T, G> {
338    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
339        fmt::Debug::fmt(&self.inner.val, f)
340    }
341}*/
342
343// SAFETY: Only a single lock holder is permitted to access the inner data of Spinlock.
344#[verifier::external]
345unsafe impl<T: Send, G> Send for SpinLock<T, G> {}
346#[verifier::external]
347unsafe impl<T: Send, G> Sync for SpinLock<T, G> {}
348
349/// A guard that provides exclusive access to the data protected by a [`SpinLock`].
350///
351/// # Verified Properties
352/// ## Verification Design
353/// The guard is extended with a ghost permission field `v_perm` that
354/// holds the ghost permission ([`PointsTo<T>`](https://verus-lang.github.io/verus/verusdoc/vstd/cell/pcell/struct.PointsTo.html))
355/// This permission grants exclusive ownership of the protected data and enables verified access to the `PCell<T>`.
356///
357///
358/// ## Invariant
359/// The guard maintains a type invariant ensuring that its ghost permission's ID matches
360/// the lock's internal cell ID. This guarantees that the permission corresponds to the
361/// correct protected data.
362///
363/// ```rust
364/// #[verifier::type_invariant]
365///    spec fn type_inv(self) -> bool{
366///        self.lock.cell_id() == self.v_perm@.id()
367///    }
368/// ```
369///
370/// *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.
371/// It internally holds at all steps during the method executions and is **NOT** exposed in the public APIs' pre- and post-conditions.
372#[verifier::reject_recursive_types(T)]
373#[verifier::reject_recursive_types(G)]
374#[clippy::has_significant_drop]
375#[must_use]
376#[verus_verify]
377pub struct SpinLockGuard<'a, T /*: ?Sized*/, G: SpinGuardian> {
378    guard: G::Guard,
379    lock: &'a SpinLock<T, G>,
380    /// Ghost permission for verification
381    v_perm: Tracked<PointsTo<T>>,
382}
383
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.v_perm@.id()
389    }
390
391    /// The value stored in the lock.
392    pub closed spec fn value(self) -> T {
393        *self.v_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#[verus_verify]
409impl<T: /*?Sized*/, G: SpinGuardian> Deref for SpinLockGuard<'_, T, G> {
410    type Target = T;
411
412    #[verus_spec(returns self.view())]
413    fn deref(&self) -> &T {
414        proof_decl! {
415            let tracked read_perm = self.v_perm.borrow();
416        }
417        proof!{
418            use_type_invariant(self);
419        }
420        // unsafe { &*self.lock.inner.val.get() }
421        // The internal implementation of `PCell<T>::borrow` is exactly unsafe { &(*(*self.ucell).get()) },
422        // and here we verify that we have the permission to call `borrow`.
423        self.lock.inner.val.borrow(Tracked(read_perm))
424    }
425}
426
427
428#[verus_verify]
429impl<T: /* ?Sized */, G: SpinGuardian> DerefMut for SpinLockGuard<'_, T, G> {
430    #[verus_spec(ret =>
431        ensures
432            final(self).view() == *final(ret),
433    )]
434    fn deref_mut(&mut self) -> &mut Self::Target
435    {
436        proof!{
437            use_type_invariant(&*self);
438        }
439        // unsafe { &mut *self.lock.inner.val.get() }
440        pcell_borrow_mut(&self.lock.inner.val, &mut self.v_perm)
441    }
442}
443}
444
445/* impl<T: ?Sized, G: SpinGuardian> Drop for SpinLockGuard<'_, T, G> {
446    fn drop(&mut self) {
447        self.lock.release_lock();
448    }
449}
450
451impl<T: ?Sized + fmt::Debug, G: SpinGuardian> fmt::Debug for SpinLockGuard<'_, T, G> {
452    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
453        fmt::Debug::fmt(&**self, f)
454    }
455}*/
456
457#[verus_verify]
458impl<T: ?Sized, G: SpinGuardian> !Send for SpinLockGuard<'_, T, G> {}
459
460#[verifier::external]
461// SAFETY: `SpinLockGuard` can be shared between tasks/threads in same CPU.
462// As `lock()` is only called when there are no race conditions caused by interrupts.
463unsafe impl<T: Sync, G: SpinGuardian> Sync for SpinLockGuard<'_, T, G> {}
ostd/sync/spin.rs

ostd/sync/
spin.rs
