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.

[hiroki-chen]

Thanks for the clarification! In this case the two abstraction indeed server different purposes and it seems that none of each could substituate the other one. But I still think naming it SpinLockPredicate loses its generality because conceptually this predicate can be used in any locks.

In the longer term, we can nevertheless extract the shared invariant part or adapter to reduce the overlaps between atomic data owner and the lock predicates.

[rikosellic]

@dybolo According to the name of SpinLockPredicate, I assume that it will be a predicate type, so implementors of the trait will just be empty structs, and SpinLockPredicate::inv should not have a self argument. But after investigating the WaitQueue example, I find that the predicate actually stores a ghost_id to link the ghost states when the tracked P::state is moved to the guard. This works, but it seems a bit ugly. Since the ghost_id will never change, its usage looks very much like the constant method provided by LocalInvariant or AtomicInvariant. Can we just build the whole infrastructure upon AtomicInvariant? Then we only need to add a P in the type system, and Ghost<P> is not required anymore.

[dybolo]

@dybolo According to the name of SpinLockPredicate, I assume that it will be a predicate type, so implementors of the trait will just be empty structs, and SpinLockPredicate::inv should not have a self argument. But after investigating the WaitQueue example, I find that the predicate actually stores a ghost_id to link the ghost states when the tracked P::state is moved to the guard. This works, but it seems a bit ugly. Since the ghost_id will never change, its usage looks very much like the constant method provided by LocalInvariant or AtomicInvariant. Can we just build the whole infrastructure upon AtomicInvariant? Then we only need to add a P in the type system, and Ghost<P> is not required anymore.

I tried addressing this in the new commit. I made the lock's AtomicBool constant and predicate explicit. The lock stores the ghost_id together with the protected cell ID in the atomic invariant constant, so Ghost<P> is no longer needed. Consequently, WakersPredicate is now empty, and its immutable ghost_id is passed as the lock’s constant and exposed through SpinLock::constant().

Please let me know if this matches what you had in mind or if you’d prefer a different approach.

[hiroki-chen]

@dybolo According to the name of SpinLockPredicate, I assume that it will be a predicate type, so implementors of the trait will just be empty structs, and SpinLockPredicate::inv should not have a self argument. But after investigating the WaitQueue example, I find that the predicate actually stores a ghost_id to link the ghost states when the tracked P::state is moved to the guard. This works, but it seems a bit ugly. Since the ghost_id will never change, its usage looks very much like the constant method provided by LocalInvariant or AtomicInvariant. Can we just build the whole infrastructure upon AtomicInvariant? Then we only need to add a P in the type system, and Ghost<P> is not required anymore.

I tried addressing this in the new commit. I made the lock's AtomicBool constant and predicate explicit. The lock stores the ghost_id together with the protected cell ID in the atomic invariant constant, so Ghost<P> is no longer needed. Consequently, WakersPredicate is now empty, and its immutable ghost_id is passed as the lock’s constant and exposed through SpinLock::constant().

Please let me know if this matches what you had in mind or if you’d prefer a different approach.

oh i think @rikosellic meant that "GhostAuthVar" looks redundant because AtomicU32 can be parameterized by a K (a constant) that may carry the "ghost_id" you want.

[dybolo]

@dybolo According to the name of SpinLockPredicate, I assume that it will be a predicate type, so implementors of the trait will just be empty structs, and SpinLockPredicate::inv should not have a self argument. But after investigating the WaitQueue example, I find that the predicate actually stores a ghost_id to link the ghost states when the tracked P::state is moved to the guard. This works, but it seems a bit ugly. Since the ghost_id will never change, its usage looks very much like the constant method provided by LocalInvariant or AtomicInvariant. Can we just build the whole infrastructure upon AtomicInvariant? Then we only need to add a P in the type system, and Ghost<P> is not required anymore.

I tried addressing this in the new commit. I made the lock's AtomicBool constant and predicate explicit. The lock stores the ghost_id together with the protected cell ID in the atomic invariant constant, so Ghost<P> is no longer needed. Consequently, WakersPredicate is now empty, and its immutable ghost_id is passed as the lock’s constant and exposed through SpinLock::constant().
Please let me know if this matches what you had in mind or if you’d prefer a different approach.

oh i think @rikosellic meant that "GhostAuthVar" looks redundant because AtomicU32 can be parameterized by a K (a constant) that may carry the "ghost_id" you want.

I still think that the GhostAuthVar is necessary because it is what makes sure that num_wakers is equal to the size of the vector inside the spinlock when we don't have the guard. Carrying only the ghost ID in AtomicU32’s constant identifies the relation, but would not prevent the counter and queue length from being updated independently, nor give us a resource-based proof that they remain synchronized.

With the GhostVarAuth/GhostVar pair, the authoritative half is tied to num_wakers and the mirror half is tied to wakers.len(). Only during the critical session we can update the vector and the halves. Updating the ghost value requires both halves, the update then changes them together. When leaving the critical section we know that the new half value also matches with the number of elements left inside the vector.

[hiroki-chen]

@dybolo According to the name of SpinLockPredicate, I assume that it will be a predicate type, so implementors of the trait will just be empty structs, and SpinLockPredicate::inv should not have a self argument. But after investigating the WaitQueue example, I find that the predicate actually stores a ghost_id to link the ghost states when the tracked P::state is moved to the guard. This works, but it seems a bit ugly. Since the ghost_id will never change, its usage looks very much like the constant method provided by LocalInvariant or AtomicInvariant. Can we just build the whole infrastructure upon AtomicInvariant? Then we only need to add a P in the type system, and Ghost<P> is not required anymore.

I tried addressing this in the new commit. I made the lock's AtomicBool constant and predicate explicit. The lock stores the ghost_id together with the protected cell ID in the atomic invariant constant, so Ghost<P> is no longer needed. Consequently, WakersPredicate is now empty, and its immutable ghost_id is passed as the lock’s constant and exposed through SpinLock::constant().
Please let me know if this matches what you had in mind or if you’d prefer a different approach.

oh i think @rikosellic meant that "GhostAuthVar" looks redundant because AtomicU32 can be parameterized by a K (a constant) that may carry the "ghost_id" you want.

I still think that the GhostAuthVar is necessary because it is what makes sure that num_wakers is equal to the size of the vector inside the spinlock when we don't have the guard. Carrying only the ghost ID in AtomicU32’s constant identifies the relation, but would not prevent the counter and queue length from being updated independently, nor give us a resource-based proof that they remain synchronized.

With the GhostVarAuth/GhostVar pair, the authoritative half is tied to num_wakers and the mirror half is tied to wakers.len(). Only during the critical session we can update the vector and the halves. Updating the ghost value requires both halves, the update then changes them together. When leaving the critical section we know that the new half value also matches with the number of elements left inside the vector.

AFAIK, if you encode a constant K into AtomicU32 you may able to establish invariants with the invariant on () with () so theoretically we can encode such length constraints into it but I haven't tried it yet. If this is not feasible then a GhostAuthVar looks good.

[rikosellic]

@dybolo's GhostVarAuth design looks reasonable to me. I'm still thinking whether this design can be abstracted or rebased on AtomicInvariant so that it can be migrated to other synchronization primitives. I will try it myself first.

[hiroki-chen]

Wait for @rikosellic

[rikosellic]

@dybolo Your new design generally looks good to me. I just made some small changes:

• Rename SpinLockPredicate to ResourceInvariant and move it into vstd_extra since this mechanism is not specific to SpinLock.
• Simply track the constant as a ghost field in SpinLockInner and delete SpinLockConstant and SpinLockAtomicPredicate because they can be handled with struct_with_invariants!
• Remove the special SpinLock::new for trivial predicates, and rename new_with_pred back to new and use it everywhere. We prefer adding new verification arguments rather than adding new APIs.

@hiroki-chen @dybolo The constant is actually not a critical part of the resource, we can just keep it separately in the lock. AtomicDataWithOwner and SpinLockResource are the same thing then, since one can refactor the current AtomicDataWithOwner<V, Own> into

AtomicDataWithOwner<V, I: ResourceInvariant<V>>

This is even more expressive because one can define different invariants for different types of owners.

Anyway, this is a good improvement. Thanks for your contributions!

[rikosellic]

@hiroki-chen Please review the latest change!

[hiroki-chen]

For what it's worth, I can try if Once can reuse this design