#![allow(non_snake_case)]
#![allow(unused_imports)]
#![allow(non_shorthand_field_patterns)]
use super::atomic_ghost::*;
use super::cell::{CellId, PCell, PointsTo};
use super::invariant::InvariantPredicate;
use super::modes::*;
use super::multiset::*;
use super::prelude::*;
use super::set::*;
use core::marker::PhantomData;
#[cfg(verus_keep_ghost)]
use state_machines_macros::tokenized_state_machine_vstd;
#[cfg(verus_keep_ghost)]
tokenized_state_machine_vstd!(
RwLockToks<K, V, Pred: InvariantPredicate<K, V>> {
fields {
#[sharding(constant)]
pub k: K,
#[sharding(constant)]
pub pred: PhantomData<Pred>,
#[sharding(variable)]
pub flag_exc: bool,
#[sharding(variable)]
pub flag_rc: nat,
#[sharding(storage_option)]
pub storage: Option<V>,
#[sharding(option)]
pub pending_writer: Option<()>,
#[sharding(option)]
pub writer: Option<()>,
#[sharding(multiset)]
pub pending_reader: Multiset<()>,
#[sharding(multiset)]
pub reader: Multiset<V>,
}
init!{
initialize_full(k: K, t: V) {
require Pred::inv(k, t);
init k = k;
init pred = PhantomData;
init flag_exc = false;
init flag_rc = 0;
init storage = Option::Some(t);
init pending_writer = Option::None;
init writer = Option::None;
init pending_reader = Multiset::empty();
init reader = Multiset::empty();
}
}
#[inductive(initialize_full)]
fn initialize_full_inductive(post: Self, k: K, t: V) {
broadcast use group_multiset_axioms;
}
transition!{
acquire_read_start() {
update flag_rc = pre.flag_rc + 1;
add pending_reader += {()};
}
}
transition!{
acquire_read_end() {
require(pre.flag_exc == false);
remove pending_reader -= {()};
birds_eye let x: V = pre.storage.get_Some_0();
add reader += {x};
assert Pred::inv(pre.k, x);
}
}
transition!{
acquire_read_abandon() {
remove pending_reader -= {()};
assert(pre.flag_rc >= 1);
update flag_rc = (pre.flag_rc - 1) as nat;
}
}
transition!{
acquire_exc_start() {
require(pre.flag_exc == false);
update flag_exc = true;
add pending_writer += Some(());
}
}
transition!{
acquire_exc_end() {
require(pre.flag_rc == 0);
remove pending_writer -= Some(());
add writer += Some(());
birds_eye let x = pre.storage.get_Some_0();
withdraw storage -= Some(x);
assert Pred::inv(pre.k, x);
}
}
transition!{
release_exc(x: V) {
require Pred::inv(pre.k, x);
remove writer -= Some(());
update flag_exc = false;
deposit storage += Some(x);
}
}
property!{
read_guard(x: V) {
have reader >= {x};
guard storage >= Some(x);
}
}
property!{
read_match(x: V, y: V) {
have reader >= {x};
have reader >= {y};
assert(equal(x, y));
}
}
#[transition]
transition!{
release_shared(x: V) {
remove reader -= {x};
assert(pre.flag_rc >= 1) by {
assert(equal(pre.storage, Option::Some(x)));
};
update flag_rc = (pre.flag_rc - 1) as nat;
}
}
#[invariant]
pub fn exc_bit_matches(&self) -> bool {
(if self.flag_exc { 1 } else { 0 as int }) ==
(if self.pending_writer.is_Some() { 1 } else { 0 as int }) as int
+ (if self.writer.is_Some() { 1 } else { 0 as int }) as int
}
#[invariant]
pub fn count_matches(&self) -> bool {
self.flag_rc == self.pending_reader.count(())
+ self.reader.count(self.storage.get_Some_0())
}
#[invariant]
pub fn reader_agrees_storage(&self) -> bool {
forall |t: V| imply(#[trigger] self.reader.count(t) > 0,
equal(self.storage, Option::Some(t)))
}
#[invariant]
pub fn writer_agrees_storage(&self) -> bool {
imply(self.writer.is_Some(), self.storage.is_None())
}
#[invariant]
pub fn writer_agrees_storage_rev(&self) -> bool {
imply(self.storage.is_None(), self.writer.is_Some())
}
#[invariant]
pub fn sto_user_inv(&self) -> bool {
self.storage.is_some() ==> Pred::inv(self.k, self.storage.unwrap())
}
#[inductive(acquire_read_start)]
fn acquire_read_start_inductive(pre: Self, post: Self) {
broadcast use group_multiset_axioms;
}
#[inductive(acquire_read_end)]
fn acquire_read_end_inductive(pre: Self, post: Self) {
broadcast use group_multiset_axioms;
}
#[inductive(acquire_read_abandon)]
fn acquire_read_abandon_inductive(pre: Self, post: Self) {
broadcast use group_multiset_axioms;
}
#[inductive(acquire_exc_start)]
fn acquire_exc_start_inductive(pre: Self, post: Self) { }
#[inductive(acquire_exc_end)]
fn acquire_exc_end_inductive(pre: Self, post: Self) { }
#[inductive(release_exc)]
fn release_exc_inductive(pre: Self, post: Self, x: V) { }
#[inductive(release_shared)]
fn release_shared_inductive(pre: Self, post: Self, x: V) {
broadcast use group_multiset_axioms;
assert(equal(pre.storage, Option::Some(x)));
}
});
verus! {
pub trait RwLockPredicate<V>: Sized {
spec fn inv(self, v: V) -> bool;
}
impl<V> RwLockPredicate<V> for spec_fn(V) -> bool {
open spec fn inv(self, v: V) -> bool {
self(v)
}
}
ghost struct InternalPred<V, Pred> {
v: V,
pred: Pred,
}
impl<V, Pred: RwLockPredicate<V>> InvariantPredicate<(Pred, CellId), PointsTo<V>> for InternalPred<
V,
Pred,
> {
closed spec fn inv(k: (Pred, CellId), v: PointsTo<V>) -> bool {
v.view().pcell == k.1 && v.view().value.is_Some() && k.0.inv(v.view().value.get_Some_0())
}
}
struct_with_invariants_vstd!{
pub struct RwLock<V, Pred: RwLockPredicate<V>> {
cell: PCell<V>,
exc: AtomicBool<_, RwLockToks::flag_exc<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>, _>,
rc: AtomicU64<_, RwLockToks::flag_rc<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>, _>,
inst: Tracked<RwLockToks::Instance<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>>,
pred: Ghost<Pred>,
}
#[verifier::type_invariant]
spec fn wf(&self) -> bool {
invariant on exc with (inst) is (v: bool, g: RwLockToks::flag_exc<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>) {
g@.instance == inst@
&& g@.value == v
}
invariant on rc with (inst) is (v: u64, g: RwLockToks::flag_rc<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>) {
g@.instance == inst@
&& g@.value == v
}
predicate {
self.inst@.k() == (self.pred@, self.cell.id())
}
}
}
pub struct WriteHandle<'a, V, Pred: RwLockPredicate<V>> {
handle: Tracked<RwLockToks::writer<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>>,
perm: Tracked<PointsTo<V>>,
rwlock: &'a RwLock<V, Pred>,
}
pub struct ReadHandle<'a, V, Pred: RwLockPredicate<V>> {
handle: Tracked<RwLockToks::reader<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>>,
rwlock: &'a RwLock<V, Pred>,
}
impl<'a, V, Pred: RwLockPredicate<V>> WriteHandle<'a, V, Pred> {
#[verifier::type_invariant]
spec fn wf_write_handle(self) -> bool {
equal(self.perm@.view().pcell, self.rwlock.cell.id()) && self.perm@.view().value.is_None()
&& equal(self.handle@.view().instance, self.rwlock.inst@) && self.rwlock.wf()
}
pub closed spec fn rwlock(self) -> RwLock<V, Pred> {
*self.rwlock
}
pub fn release_write(self, t: V)
requires
self.rwlock().inv(t),
{
proof {
use_type_invariant(&self);
}
let WriteHandle { handle: Tracked(handle), perm: Tracked(mut perm), rwlock } = self;
self.rwlock.cell.put(Tracked(&mut perm), t);
atomic_with_ghost!(
&rwlock.exc => store(false);
ghost g =>
{
self.rwlock.inst.borrow().release_exc(perm, &mut g, perm, handle);
});
}
}
impl<'a, V, Pred: RwLockPredicate<V>> ReadHandle<'a, V, Pred> {
#[verifier::type_invariant]
spec fn wf_read_handle(self) -> bool {
equal(self.handle@.view().instance, self.rwlock.inst@)
&& self.handle@.view().key.view().value.is_Some() && equal(
self.handle@.view().key.view().pcell,
self.rwlock.cell.id(),
) && self.handle@.view().count == 1 && self.rwlock.wf()
}
pub closed spec fn view(self) -> V {
self.handle@.view().key.view().value.unwrap()
}
pub closed spec fn rwlock(self) -> RwLock<V, Pred> {
*self.rwlock
}
pub fn borrow<'b>(&'b self) -> (t: &'b V)
ensures
t == self.view(),
{
proof {
use_type_invariant(self);
}
let tracked perm = self.rwlock.inst.borrow().read_guard(
self.handle@.view().key,
self.handle.borrow(),
);
self.rwlock.cell.borrow(Tracked(&perm))
}
pub proof fn lemma_readers_match(
tracked read_handle1: &ReadHandle<V, Pred>,
tracked read_handle2: &ReadHandle<V, Pred>,
)
requires
read_handle1.rwlock() == read_handle2.rwlock(),
ensures
(equal(read_handle1.view(), read_handle2.view())),
{
use_type_invariant(read_handle1);
use_type_invariant(read_handle2);
read_handle1.rwlock.inst.borrow().read_match(
read_handle1.handle@.view().key,
read_handle2.handle@.view().key,
&read_handle1.handle.borrow(),
&read_handle2.handle.borrow(),
);
}
pub fn release_read(self) {
proof {
use_type_invariant(&self);
}
let ReadHandle { handle: Tracked(handle), rwlock } = self;
let _ =
atomic_with_ghost!(
&rwlock.rc => fetch_sub(1);
ghost g =>
{
rwlock.inst.borrow().release_shared(handle.view().key, &mut g, handle);
});
}
}
impl<V, Pred: RwLockPredicate<V>> RwLock<V, Pred> {
pub closed spec fn pred(&self) -> Pred {
self.pred@
}
pub open spec fn inv(&self, t: V) -> bool {
self.pred().inv(t)
}
pub fn new(t: V, Ghost(pred): Ghost<Pred>) -> (s: Self)
requires
pred.inv(t),
ensures
s.pred() == pred,
{
let (cell, Tracked(perm)) = PCell::<V>::new(t);
let tracked (Tracked(inst), Tracked(flag_exc), Tracked(flag_rc), _, _, _, _) =
RwLockToks::Instance::<
(Pred, CellId),
PointsTo<V>,
InternalPred<V, Pred>,
>::initialize_full((pred, cell.id()), perm, Option::Some(perm));
let inst = Tracked(inst);
let exc = AtomicBool::new(Ghost(inst), false, Tracked(flag_exc));
let rc = AtomicU64::new(Ghost(inst), 0, Tracked(flag_rc));
RwLock { cell, exc, rc, inst, pred: Ghost(pred) }
}
pub fn acquire_write(&self) -> (ret: (V, WriteHandle<V, Pred>))
ensures
({
let t = ret.0;
let write_handle = ret.1;
&&write_handle.rwlock() == *self && self.inv(t)
}),
{
proof {
use_type_invariant(self);
}
let mut done = false;
let tracked mut token: Option<
RwLockToks::pending_writer<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>,
> = Option::None;
while !done
invariant
done ==> token.is_Some() && equal(token.get_Some_0().view().instance, self.inst@),
self.wf(),
{
let result =
atomic_with_ghost!(
&self.exc => compare_exchange(false, true);
returning res;
ghost g =>
{
if res.is_Ok() {
token = Option::Some(self.inst.borrow().acquire_exc_start(&mut g));
}
});
done =
match result {
Result::Ok(_) => true,
_ => false,
};
}
loop
invariant
token.is_Some() && equal(token.get_Some_0().view().instance, self.inst@),
self.wf(),
{
let tracked mut perm_opt: Option<PointsTo<V>> = None;
let tracked mut handle_opt: Option<
RwLockToks::writer<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>,
> = None;
let result =
atomic_with_ghost!(
&self.rc => load();
returning res;
ghost g =>
{
if res == 0 {
let tracked tok = match token { Option::Some(t) => t, Option::None => proof_from_false() };
let tracked x = self.inst.borrow().acquire_exc_end(&g, tok);
token = None;
let tracked (_, Tracked(perm), Tracked(exc_handle)) = x;
perm_opt = Some(perm);
handle_opt = Some(exc_handle);
}
});
if result == 0 {
let tracked mut perm = match perm_opt {
Option::Some(t) => t,
Option::None => proof_from_false(),
};
let tracked handle = match handle_opt {
Option::Some(t) => t,
Option::None => proof_from_false(),
};
let t = self.cell.take(Tracked(&mut perm));
let write_handle = WriteHandle {
perm: Tracked(perm),
handle: Tracked(handle),
rwlock: self,
};
return (t, write_handle);
}
}
}
pub fn acquire_read(&self) -> (read_handle: ReadHandle<V, Pred>)
ensures
read_handle.rwlock() == *self,
self.inv(read_handle.view()),
{
proof {
use_type_invariant(self);
}
loop
invariant
self.wf(),
{
let val = atomic_with_ghost!(&self.rc => load(); ghost g => { });
let tracked mut token: Option<
RwLockToks::pending_reader<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>,
> = Option::None;
if val < 0xffff_ffff_ffff_ffff {
let result =
atomic_with_ghost!(
&self.rc => compare_exchange(val, val + 1);
returning res;
ghost g =>
{
if res.is_Ok() {
token = Option::Some(self.inst.borrow().acquire_read_start(&mut g));
}
});
match result {
Result::Ok(_) => {
let tracked mut handle_opt: Option<
RwLockToks::reader<(Pred, CellId), PointsTo<V>, InternalPred<V, Pred>>,
> = None;
let result =
atomic_with_ghost!(
&self.exc => load();
returning res;
ghost g =>
{
if res == false {
let tracked tok = match token { Option::Some(t) => t, Option::None => proof_from_false() };
let tracked x = self.inst.borrow().acquire_read_end(&g, tok);
token = None;
let tracked (_, Tracked(exc_handle)) = x;
handle_opt = Some(exc_handle);
}
});
if result == false {
let tracked handle = match handle_opt {
Option::Some(t) => t,
Option::None => proof_from_false(),
};
let read_handle = ReadHandle { handle: Tracked(handle), rwlock: self };
return read_handle;
} else {
let _ =
atomic_with_ghost!(
&self.rc => fetch_sub(1);
ghost g =>
{
let tracked tok = match token { Option::Some(t) => t, Option::None => proof_from_false() };
self.inst.borrow().acquire_read_abandon(&mut g, tok);
});
}
},
_ => {},
}
}
}
}
pub fn into_inner(self) -> (v: V)
ensures
self.inv(v),
{
let (v, _write_handle) = self.acquire_write();
v
}
}
}