prove: WaitQueue num_wakers

[dybolo]

Verified that num_wakers in WaitQueue equals wakers length inside the SpinLock

Add support for user-supplied SpinLock invariants and use it to verify that WaitQueue::num_wakers matches the number of entries in its protected VecDeque whenever the spin lock is released.

Verification design

SpinLock now accepts a predicate type:

SpinLock<T, G, P>

where P: SpinLockPredicate<T> defines:

type State;

spec fn inv(self, value: T, state: Self::State) -> bool;

The lock’s atomic ghost state owns a SpinLockResource containing:

• The PointsTo<T> permission for the protected value.
• The user-supplied tracked state P::State.

The internal invariant has two states:

Unlocked:
    lock owns PointsTo<T> and P::State
    P::inv(value, state) must hold

Locked:
    guard owns PointsTo<T> and P::State
    P::inv may temporarily be broken

A successful lock() transfers both resources to the guard and ensures the predicate initially holds. Before SpinLockGuard::drop() can return the resources, the caller must restore the predicate.

Existing SpinLock users continue to use TrivialSpinLockPredicate, whose state is () and whose invariant is always true.

WaitQueue invariant

WaitQueue uses a pair of linked ghost tokens:

GhostVarAuth<int>   stored in num_wakers
GhostVar<int>       stored in the wakers spin lock

The spin-lock predicate establishes:

mirror.id() == predicate.id()
mirror@ == wakers@.len()

The num_wakers atomic invariant establishes:

auth.id() == wakers.predicate().id()
auth@ == num_wakers as int

Because GhostVarAuth and GhostVar with the same ID must agree:

num_wakers as int
    == auth@
    == mirror@
    == wakers.len()

This relationship is required whenever the spin lock is unlocked.

Queue updates

When adding or removing a waker:

1. Acquire the spin lock.
2. Modify the VecDeque.
3. Temporarily take the mirror token from the guard.
4. Open the num_wakers atomic invariant.
5. Use GhostVar agreement to relate the old counter to the old queue length.
6. Update the executable counter and both ghost tokens together.
7. Return the mirror token to the guard.
8. Drop the guard, which verifies that the mirror again equals the queue length.

For successful pop_front() operations, the queue invariant proves that the previous counter was positive. This removes the previous decrement assumptions.

Additional fixes

The change explicitly releases the manually-dropped spin-lock guard on all paths, including:

• Empty wake_one and wake_all paths.
• The end of enqueue.

Without these calls, the verified spin-lock implementation would remain locked because its ordinary Rust Drop implementation is currently disabled.

WaitQueue::is_empty is also verified directly and no longer requires #[verifier::external_body].

Verification

The following checks pass:

cargo dv verify --targets ostd -- --verify-only-module sync::wait
verification results: 18 verified, 0 errors

make
Verified ostd

Remaining limitations

This does not make all of wait.rs assumption-free. In particular:

• enqueue still assumes that num_wakers does not exceed u32::MAX.
• wake_all still assumes that num_woken does not overflow usize.
• Existing closure-related admit() calls remain.
• Scheduler-facing wait and wake operations still use external bodies.

[rikosellic]

I've skimmed through the code, and it looks very interesting. We are busy with other business for now, so we can only review the code closely next week. Please keep in touch!

[hiroki-chen]

Please also take a short look at ostd/stc/sync/atomic_data.rs that probably provides the functionalities you need in this PR. Although that might not be perfect:

#[repr(transparent)]
#[allow(repr_transparent_non_zst_fields)]
pub struct AtomicDataWithOwner<V, Own> {
    /// The underlying data.
    pub data: V,
    /// The permission to access the data.
    pub permission: Tracked<Own>,
}

You can also add prediate over it:

impl<V, Own: Predicate<V>> Inv for AtomicDataWithOwner<V, Own> {
    #[verifier::inline]
    open spec fn inv(self) -> bool {
        &&& self.permission.predicate(self.data)
    }
}

One thing I'm not sure is whether we'd favor a struct parameterized by V and its permission Own or a trait that could be used to bound sync primitives.

[dybolo]

Hi! Thank you for your feedback. I took a look at ostd/src/sync/atomic_data.rs.

Currently, the spin lock deliberately separates the stable predicate P from the linear state P::State, which is transferred to the guard. This keeps WakersPredicate::ghost_id accessible in WaitQueue for wf() through the lock while the GhostVar<int> mirror is temporarily owned by a guard.

To use AtomicDataWithOwner as the invariant-bearing lock resource would instead require the movable owner/state itself to implement Predicate<PointsTo<T>>, merging those two roles. The invariant P would need to move into P::State. Since P::State is transferred out of the lock when it is acquired, any predicate metadata stored there, such as WakersPredicate::ghost_id, would no longer remain accessible through the lock while a guard owns the state.



Please let me know if I have misunderstood the intended use of AtomicDataWithOwner here.