Although Verus does not yet support breaking type invariants, we have already encountered some subtleties in how type invariants interact with Drop, which deserve careful consideration.
Example
The RwLockUpgradeableGuard is a read handle that can be upgraded to a RwLockWriteGuard:
pub struct RwLockUpgradeableGuard<'a, T/*: ?Sized*/, G: SpinGuardian> {
guard: G::Guard,
inner: &'a RwLock<T, G>,
v_perm: Tracked<RwFrac<T>>,
v_token: Tracked<UpreaderGuardToken>,
}
Its v_perm field represents a fractional PointsTo permission, and its type invariant relates this permission to the lock so that an immutable reference can be safely obtained. In the RwLock’s atomic state, the existence of such a guard is represented by the UPGRADEABLE_GUARD bit. The v_token field grants the permission required to manipulate that bit.
impl<'a, T, G: SpinGuardian> RwLockUpgradeableGuard<'a, T, G> {
#[verifier::type_invariant]
pub closed spec fn type_inv(self) -> bool {
&&& self.inner.cell_perm_id() == self.v_perm@.id()
&&& self.inner.cell_id() == self.v_perm@.resource().id()
&&& self.v_perm@.frac() == 1
}
}
Normal Drop Behaviour
Dropping this guard in the normal case is straightforward. We simply return both permissions to the lock while executing
atomic_with_ghost!(
self.inner.lock => fetch_sub(UPGRADEABLE_READER);
);
Dropping a broken-type-invariant
The interesting case arises when upgrading a RwLockUpgradeableGuard to a RwWriteGuard via RwLockUpgradeableGuard::try_upgrade. The implementation first performs
let res = atomic_with_ghost!(
inner.lock => compare_exchange(
UPGRADEABLE_READER | BEING_UPGRADED,
WRITER | UPGRADEABLE_READER
);
);
If the operation succeeds, it then calls RwLockUpgradeableGuard::drop, which subtracts the UPGRADEABLE_GUARD bit to reach a clean WRITER state, and finally returns a RwLockWriteGuard.
However, this leads to an issue. If we call drop under the type invariant of RwLockUpgradeableGuard, we are required to return the fractional permission stored in v_perm, while we need the full permission to construct a write guard.
If, instead of calling drop, we directly execute fetch_sub (which is exactly equivalent from the perspective of the executable code), the verification works smoothly. In this case, we can consume the fractional permission during the earlier compare_exchange step to obtain the full permission, and we do not need to return the fractional permission during the fetch_sub.
The key insight is that we do not need to preserve the type invariant when calling drop in this scenario. Since the guard is about to be dropped, no reference can be obtained from it, and therefore, maintaining the invariant at that point is unnecessary. Beyond the issue of temporarily breaking the type invariant, a potentially more significant problem is that the same operation is used for two different ghost resource transitions: one that returns the fractional permission and one that does not.
Although Verus does not yet support breaking type invariants, we have already encountered some subtleties in how type invariants interact with
Drop, which deserve careful consideration.Example
The
RwLockUpgradeableGuardis a read handle that can be upgraded to aRwLockWriteGuard:Its
v_permfield represents a fractionalPointsTopermission, and its type invariant relates this permission to thelockso that an immutable reference can be safely obtained. In theRwLock’s atomic state, the existence of such a guard is represented by theUPGRADEABLE_GUARDbit. Thev_tokenfield grants the permission required to manipulate that bit.Normal Drop Behaviour
Dropping this guard in the normal case is straightforward. We simply return both permissions to the lock while executing
Dropping a broken-type-invariant
The interesting case arises when upgrading a
RwLockUpgradeableGuardto aRwWriteGuardviaRwLockUpgradeableGuard::try_upgrade. The implementation first performsIf the operation succeeds, it then calls
RwLockUpgradeableGuard::drop, which subtracts theUPGRADEABLE_GUARDbit to reach a cleanWRITERstate, and finally returns aRwLockWriteGuard.However, this leads to an issue. If we call
dropunder the type invariant ofRwLockUpgradeableGuard, we are required to return the fractional permission stored inv_perm, while we need the full permission to construct awrite guard.If, instead of calling
drop, we directly executefetch_sub(which is exactly equivalent from the perspective of the executable code), the verification works smoothly. In this case, we can consume the fractional permission during the earliercompare_exchangestep to obtain the full permission, and we do not need to return the fractional permission during thefetch_sub.The key insight is that we do not need to preserve the type invariant when calling drop in this scenario. Since the guard is about to be dropped, no reference can be obtained from it, and therefore, maintaining the invariant at that point is unnecessary. Beyond the issue of temporarily breaking the type invariant, a potentially more significant problem is that the same operation is used for two different ghost resource transitions: one that returns the fractional permission and one that does not.