pub struct RwLock<V, Pred: RwLockPredicate<V>> { /* private fields */ }Expand description
A verified implementation of a reader-writer lock, implemented using atomics and a reference count.
When constructed, you can provide an invariant via the Pred parameter,
specifying the allowed values that can go in the lock.
Note that this specification does not verify the absence of dead-locks.
Examples
On construction of a lock, we can specify an invariant for the object that goes inside.
One way to do this is by providing a spec_fn, which implements the RwLockPredicate
trait.
fn example1() {
// We can create a lock with an invariant: `v == 5 || v == 13`.
// Thus only 5 or 13 can be stored in the lock.
let lock = RwLock::<u64, spec_fn(u64) -> bool>::new(5, Ghost(|v| v == 5 || v == 13));
let (val, write_handle) = lock.acquire_write();
assert(val == 5 || val == 13);
write_handle.release_write(13);
let read_handle1 = lock.acquire_read();
let read_handle2 = lock.acquire_read();
// We can take multiple read handles at the same time:
let val1 = read_handle1.borrow();
let val2 = read_handle2.borrow();
// RwLock has a lemma that both read handles have the same value:
proof { ReadHandle::lemma_readers_match(&read_handle1, &read_handle2); }
assert(*val1 == *val2);
read_handle1.release_read();
read_handle2.release_read();
}It’s often easier to implement the RwLockPredicate trait yourself. This way you can
have a configurable predicate without needing to work with higher-order functions.
struct FixedParity {
pub parity: int,
}
impl RwLockPredicate<u64> for FixedParity {
open spec fn inv(self, v: u64) -> bool {
v % 2 == self.parity
}
}
fn example2() {
// Create a lock that can only store even integers
let lock_even = RwLock::<u64, FixedParity>::new(20, Ghost(FixedParity { parity: 0 }));
// Create a lock that can only store odd integers
let lock_odd = RwLock::<u64, FixedParity>::new(23, Ghost(FixedParity { parity: 1 }));
let read_handle_even = lock_even.acquire_read();
let val_even = *read_handle_even.borrow();
assert(val_even % 2 == 0);
let read_handle_odd = lock_odd.acquire_read();
let val_odd = *read_handle_odd.borrow();
assert(val_odd % 2 == 1);
}Implementations§
source§impl<V, Pred: RwLockPredicate<V>> RwLock<V, Pred>
impl<V, Pred: RwLockPredicate<V>> RwLock<V, Pred>
sourcepub open spec fn inv(&self, t: V) -> bool
pub open spec fn inv(&self, t: V) -> bool
{ self.pred().inv(t) }Indicates if the value v can be stored in the lock. Per the definition,
it depends on [self.pred()], which is configured upon lock construction (RwLock::new).
sourcepub exec fn new(t: V, Ghost(pred): Ghost<Pred>) -> s : Self
pub exec fn new(t: V, Ghost(pred): Ghost<Pred>) -> s : Self
pred.inv(t),s.pred() == pred,sourcepub exec fn acquire_write(&self) -> ret : (V, WriteHandle<'_, V, Pred>)
pub exec fn acquire_write(&self) -> ret : (V, WriteHandle<'_, V, Pred>)
({
let t = ret.0;
let write_handle = ret.1;
&&write_handle.rwlock() == *self && self.inv(t)
}),Acquires an exclusive write-lock. To release it, use WriteHandle::release_write.
Warning: The lock is NOT released automatically when the handle
is dropped. You must call WriteHandle::release_write.
Verus does not check that lock is released.
sourcepub exec fn acquire_read(&self) -> read_handle : ReadHandle<'_, V, Pred>
pub exec fn acquire_read(&self) -> read_handle : ReadHandle<'_, V, Pred>
read_handle.rwlock() == *self,self.inv(read_handle.view()),Acquires a shared read-lock. To release it, use ReadHandle::release_read.
Warning: The lock is NOT released automatically when the handle
is dropped. You must call ReadHandle::release_read.
Verus does not check that lock is released.
sourcepub exec fn into_inner(self) -> v : V
pub exec fn into_inner(self) -> v : V
self.inv(v),Destroys the lock and returns the inner object. Note that this may deadlock if not all locks have been released.