Struct SpinLock Copy item path

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

§Verification Design

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. 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. When the lock guard is dropped, the ghost permission is transferred back to the spin lock.

§Invariant

The SpinLock is internally represented by a struct SpinLockInner that contains an AtomicBool and a PCell to hold the protected data. We present its formally verified version and invariant below.

The lock field is extended with a PointsTo<T> 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, thereby ensuring exclusive access to the protected data. The val field is a PCell<T>, which behaves like UnsafeCell<T> used in the Asterinas mainline, but only allows verified access through the ghost permission.

When the internal AtomicBool is true, the permission has been transferred to a SpinLockGuard and no one else can acquire the lock. When it is false, the permission to access the PCell<T> is stored in the lock, and it must match the val’s id.

struct_with_invariants! {
struct SpinLockInner<T> {
   lock: AtomicBool<_,Option<PointsTo<T>>,_>,
   val: PCell<T>,
}

closed spec fn wf(self) -> bool {
   invariant on lock with (val) is (v:bool, g:Option<PointsTo<T>>) {
       match g {
           None => v == true,
           Some(perm) => perm.id() == val.id() && !v
       }
   }
}
}

Note: The invariant is encapsulated in type_inv 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.

§Safety

There are no data races.

§Functional Correctness

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