Current Theory
The Verus concurrency theory is inspired by Iris, extended by Leaf to support general read-only shared permissions.
Leaf's core innovation lies in introducing a protocol monoid that represents the shared read-only permission of a storage monoid (a ghost resource). This mechanism serves as a foundation for instantiating classic permission models such as fractional or counting permissions. You can find the Verus implementation here: storage_protocol and Frac permission.
For a concrete example, please refer to the verified RwLock implementation. It utilizes the fractional permission of the underlying memory access permission and binds it to an atomic invariant, a standard operation in Iris. Consequently, the try_read and try_write methods can access this atomic invariant, yielding read and write guards bound to &self.
Limitation
However, consider the following API:
impl RwLock<T> {
fn get(&mut self) -> &T // &mut T seems also correct
｛
unsafe{ &*self.val.as_ptr()}; //Here self.val is a Cell
｝
}
Because the method takes &mut self, the Rust lifetime checker ensures that there cannot be any outstanding read or write handles. Therefore, this API is perfectly consistent with try_read and try_write. However, Verus can not verify it for two reasons:
- We need a mutable guard (ghost monoid) for the
PointsTo permission (storage monoid), so that we can obtain &mut PointsTo from the guard. This crosses a theory boundary that is not considered in Leaf, confirmed in this Zulip discussion.
- We cannot bind the mutable guard to the atomic. This appears to be an orthogonal issue.
Current Theory
The Verus concurrency theory is inspired by Iris, extended by Leaf to support general read-only shared permissions.
Leaf's core innovation lies in introducing a protocol monoid that represents the shared read-only permission of a storage monoid (a ghost resource). This mechanism serves as a foundation for instantiating classic permission models such as fractional or counting permissions. You can find the Verus implementation here:
storage_protocolandFracpermission.For a concrete example, please refer to the verified
RwLockimplementation. It utilizes the fractional permission of the underlying memory access permission and binds it to an atomic invariant, a standard operation in Iris. Consequently, thetry_readandtry_writemethods can access this atomic invariant, yielding read and write guards bound to&self.Limitation
However, consider the following API:
Because the method takes &mut self, the Rust lifetime checker ensures that there cannot be any outstanding read or write handles. Therefore, this API is perfectly consistent with
try_readandtry_write. However, Verus can not verify it for two reasons:PointsTopermission (storage monoid), so that we can obtain&mut PointsTofrom the guard. This crosses a theory boundary that is not considered in Leaf, confirmed in this Zulip discussion.