Struct SpinLock 

pub struct SpinLock<T, G, I: ResourceInvariant<T> = TrivialResourceInvariant> { /* private fields */ }

A spin lock.

Guard behavior

The type `G’ specifies the guard behavior of the spin lock. While holding the lock,

• if G is [PreemptDisabled], preemption is disabled;
• if G is LocalIrqDisabled, local IRQs are disabled.

The G can also be provided by other crates other than ostd, if it behaves similar like [PreemptDisabled] or LocalIrqDisabled.

The guard behavior can be temporarily upgraded from [PreemptDisabled] to LocalIrqDisabled using the disable_irq method.

Verified properties

Ownership model

The lock field extends [AtomicBool] with a [PointsTo<T>] permission and a user-supplied tracked resource. These two resources are bundled in SpinLockResource and stored as the atomic ghost state while the lock is available:

tracked struct SpinLockResource<T, I: ResourceInvariant<T>> {
    perm: PointsTo<T>,
    resource: I::Resource,
}

struct SpinLockInner<T, I: ResourceInvariant<T>> {
    lock: AtomicBool<_, Option<SpinLockResource<T, I>>, _>,
    val: PCell<T>,
    ghost_resource_constant: Ghost<<I as ResourceInvariant<T>>::Constant>,
}

When the lock bit is false, the atomic ghost state is Some, the permission refers to val, and the protected value satisfies the user ResourceInvariant. Acquiring the lock changes the bit to true and transfers the complete SpinLockResource to the guard, leaving None in the atomic ghost state. Releasing the guard restores the resource invariant and returns the bundle to the lock.

The immutable resource constant remains available through ghost_resource_constant even while the tracked resource is owned by a guard. The complete relationship is encapsulated as a Verus type invariant; public operations expose only the permissions and resource-invariant facts needed by their callers.

Safety

There are no data races.

Functional Correctness

• At most one user can hold the lock at the same time.

Implementations

impl<T, G, I: ResourceInvariant<T>> SpinLock<T, G, I>

pub const exec fn new( val: T, Ghost(resource_constant): Ghost<I::Constant>, Tracked(resource): Tracked<I::Resource>, ) -> res : Self

requires

I::inv(resource_constant, val, resource),

ensures

res.constant() == resource_constant,

Creates a new spin lock.

Verified Properties

Safety

This function is written in safe Rust and there is no undefined behavior.

Preconditions

None.

Postconditions

• The function will not panic.
• The created spin lock satisfies the invariant.

impl<T, G, I: ResourceInvariant<T>> SpinLock<T, G, I>

pub closed spec fn cell_id(self) -> CellId

Returns the unique CellId of the internal PCell<T>.

pub closed spec fn constant(self) -> I::Constant

The immutable constant associated with the resource invariant.

pub closed spec fn wf(self) -> bool

Public well-formedness predicate for external wrappers.

pub closed spec fn type_inv(self) -> bool

Encapsulates the invariant described in the Invariant section of SpinLock.

impl<T, G: SpinGuardian, I: ResourceInvariant<T>> SpinLock<T, G, I>

pub exec fn lock(&self) -> ret : SpinLockGuard<'_, T, G, I>

ensures

ret.constant() == self.constant(),

I::inv(ret.constant(), ret.value(), ret.resource()),

Acquires the spin lock.

Verified Properties

Safety

There are no data races. The lock ensures exclusive access to the protected data.

Preconditions

None. (The invariant of SpinLock always holds internally.)

Postconditions

The returned SpinLockGuard satisfies its type invariant and the user-supplied resource invariant:

• An exclusive permission to access the protected data is held by the guard.
• The guard’s permission matches the lock’s internal cell ID.
• The protected value and tracked resource satisfy the resource invariant.

Key Verification Step

When the internal atomic compare-and-exchange operation in acquire_lock succeeds, the ghost permission and user resource are simultaneously extracted from the lock.

atomic_with_ghost!  {
   self.inner.lock => compare_exchange(false, true);
   returning res;
   ghost lock_resource => {
    // Extract the resources when the lock is successfully acquired.
    if res is Ok {
           resource = Some(lock_resource.tracked_take());
       }
   }
}.is_ok()

pub exec fn try_lock(&self) -> ret : Option<SpinLockGuard<'_, T, G, I>>

ensures

ret is Some
    ==> {
        &&& ret->0.constant() == self.constant()
        &&& I::inv(ret->0.constant(), ret->0.value(), ret->0.resource())

    },

Tries acquiring the spin lock immediately.

Verified Properties

Safety

There are no data races. The lock ensures exclusive access to the protected data.

Preconditions

None. (The invariant of SpinLock always holds internally.)

Postconditions

If Some(guard) is returned, it satisfies its type invariant:

• An exclusive permission to access the protected data is held by the guard.
• The guard’s permission matches the lock’s internal cell ID.

Trait Implementations

impl<T: Send, G, I: ResourceInvariant<T>> Send for SpinLock<T, G, I>

where I::Resource: Send,

impl<T: Send, G, I: ResourceInvariant<T>> Sync for SpinLock<T, G, I>

where I::Resource: Send,