Struct SpinLockGuard 

pub struct SpinLockGuard<'a, T, G: SpinGuardian, I: ResourceInvariant<T> = TrivialResourceInvariant> { /* private fields */ }

A guard that provides exclusive access to the data protected by a SpinLock.

Verified Properties

Verification Design

The guard is extended with tracked fields holding both the ghost permission (PointsTo<T>) and the user-supplied tracked resource. The permission grants exclusive ownership of the protected data and enables verified access to the PCell<T>.

Invariant

The guard maintains a type invariant ensuring that its ghost permission’s ID matches the lock’s internal cell ID. This guarantees that the permission corresponds to the correct protected data.

#[verifier::type_invariant]
   spec fn type_inv(self) -> bool{
       self.lock.cell_id() == self.tracked_perm@.id()
   }

Note: The invariant is encapsulated using the #[verifier::type_invariant] mechanism. It internally holds at all steps during the method executions and is NOT exposed in the public APIs’ pre- and post-conditions.

Implementations

impl<'a, T, G: SpinGuardian, I: ResourceInvariant<T>> SpinLockGuard<'a, T, G, I>

pub closed spec fn value(self) -> T

The value stored in the lock.

pub closed spec fn resource(self) -> I::Resource

The tracked resource associated with the protected value.

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

The immutable user constant associated with the guarded spin lock.

pub open spec fn view(self) -> T

{ self.value() }

The value stored in the lock. It is an alias of Self::value.

pub proof fn tracked_borrow_mut_resource(tracked &mut self) -> tracked resource : &mut I::Resource

ensures

*resource == old(self).resource(),

final(self).resource() == *final(resource),

final(self).value() == old(self).value(),

final(self).constant() == old(self).constant(),

Mutably borrows the user-supplied tracked resource.

impl<'a, T, G: SpinGuardian, I: ResourceInvariant<T>> SpinLockGuard<'a, T, G, I>

pub exec fn drop(self)

requires

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

VERUS LIMITATION: We implement drop and call it manually because Verus’s support for Drop is incomplete for now.

Trait Implementations

impl<T, G: SpinGuardian, I: ResourceInvariant<T>> Deref for SpinLockGuard<'_, T, G, I>

exec fn deref(&self) -> &T

returns

self.view(),

type Target = T

The resulting type after dereferencing.

impl<T, G: SpinGuardian, I: ResourceInvariant<T>> DerefMut for SpinLockGuard<'_, T, G, I>

exec fn deref_mut(&mut self) -> ret : &mut Self::Target

ensures

final(self).view() == *final(ret),

old(self).view() == *ret,

final(self).resource() == old(self).resource(),

final(self).constant() == old(self).constant(),

impl<T: ?Sized, G: SpinGuardian, I: ResourceInvariant<T>> !Send for SpinLockGuard<'_, T, G, I>

impl<T: Sync, G: SpinGuardian, I: ResourceInvariant<T>> Sync for SpinLockGuard<'_, T, G, I>