diff --git a/ostd/src/sync/rwlock.rs b/ostd/src/sync/rwlock.rs index 64a3266ad..27dc0613d 100644 --- a/ostd/src/sync/rwlock.rs +++ b/ostd/src/sync/rwlock.rs @@ -3,7 +3,7 @@ use vstd::atomic_ghost::*; use vstd::cell::{self, pcell::*, CellId}; use vstd::prelude::*; use vstd::resource::Loc; -use vstd_extra::resource::ghost_resource::{count::*, csum::*, excl::*, tokens::*}; +use vstd_extra::resource::ghost_resource::{acq_rel_rwlock::*, count::*, csum::*, excl::*, tokens::*}; use vstd_extra::sum::*; use vstd_extra::{prelude::*, resource}; @@ -43,37 +43,15 @@ exec const V_MAX_READ_RETRACT_FRACS: u64 } /// The token reserved in the lock when the write permission is given out. -type NoPerm = EmptyCount>; +type NoPerm = AcqRelNoPerm>; /// Half of the permission for read access, one for `RwLockUpgradeableGuard` and the other for all `RwLockReadGuard`s. -type HalfPerm = Count>; +type HalfPerm = AcqRelHalfPerm>; /// The permission for read access can be further split into `MAX_READER` pieces. -type ReadPerm = (HalfPerm, OneLeftKnowledge, NoPerm, 3>); - -tracked struct RwPerms { - /// This token tracks whether the write permission is given out. If it is `Left`, it stores the knowledge that - /// there are active readers because the existence of `HalfPerm` resource for read access. - /// If it is `Right`, we know there is an active writer and there is no active reader, because there is a `NoPerm` - /// indicating the absence of `PointsTo`. - core_token: SumResource, NoPerm, 3>, - /// The permission to retract a `READER` count. Its total quantity tracks the gap between - /// the number of `try_read` increments recorded in the lock atomic and the number of active - /// `RwLockReadGuard`s (created and ongoing creation that will succeed) represented by `read_guard_token`. - /// It can be splited up to `V_MAX_READ_RETRACT_FRACS:= 2 * MAX_READER` pieces, - /// which allows at most `2*MAX_READER - 1` `try_read` attempts that will fail to acquire the lock. - read_retract_token: TokenResource, - /// The permission to retract the set of `UPGRADEABLE_READER` bit. - upread_retract_token: Option, - /// Tracks whether there is a live `RwLockUpgradeableGuard`, also stores half of the permission for read access. - upreader_guard_token: Option, NoPerm, 3>>, - /// Tracks the number of live `RwLockReadGuard`s. If it is `Left`, it stores the remaining read permissions. - /// If it is `Right`, it stores an empty token indicating the permission has been given out. - read_guard_token: Sum< - CountResource, MAX_READER_U64>, - EmptyCount, MAX_READER_U64>, - >, -} +type ReadPerm = AcqRelReadPerm>; + +type RwPerms = AcqRelRwPerms, MAX_READER_U64, V_MAX_READ_RETRACT_FRACS>; ghost struct RwId { core_token_id: Loc, @@ -238,6 +216,11 @@ closed spec fn wf(self) -> bool { &&& 0 <= active_read_guards <= reader_bits <= total_reader_bits // The core invariant of `RwLock`: there are no simultaneous active writers and readers. &&& !(active_writer && (active_read_guards + if active_upgrade_guard { 1int } else { 0 }) > 0) + // Standalone acquire-release PCM mirrors the abstract protocol state. + &&& g.pcm.value() == g.abstract_pcm() + // Abstract weak-memory state: release advances the published phase, + // acquire imports it. This is the proof-level acquire/release model. + &&& g.wm.wf(g.phase) &&& g.core_token.id() == v_id@.core_token_id &&& g.core_token.wf() &&& g.core_token.is_left() ==> { @@ -380,6 +363,7 @@ impl RwLock { let tracked read_guard_token = CountResource::, MAX_READER_U64>::alloc( (read_half_cell_perm, left_token), ); + let tracked pcm = vstd::resource::pcm::Resource::alloc(AcqRelRwPCM::elem(0, 0, 0, 0, 0, 0)); let ghost v_id = RwId { frac_id, core_token_id: core_token.id(), @@ -388,11 +372,19 @@ impl RwLock { read_guard_token_id: read_guard_token.id(), }; let tracked perms = RwPerms { + pcm, core_token, read_retract_token, upread_retract_token: Some(upread_retract_token), upreader_guard_token: Some(upreader_guard_token), read_guard_token: Sum::Left(read_guard_token), + phase: 0, + wm: AcqRelWm::init(), + core_token_id: v_id.core_token_id, + frac_id: v_id.frac_id, + read_retract_token_id: v_id.read_retract_token_id, + upread_retract_token_id: v_id.upread_retract_token_id, + read_guard_token_id: v_id.read_guard_token_id, }; Self { @@ -493,9 +485,11 @@ impl RwLock { let tracked mut tmp = g.read_guard_token.tracked_take_left(); read_token = Some(tmp.split_one()); g.read_guard_token = Sum::Left(tmp); + g.acquire_wm(); } else { retract_read_token = Some(g.read_retract_token.split_one()); } + g.sync_pcm(); } ); if lock & (WRITER | MAX_READER | BEING_UPGRADED) == 0 { @@ -517,6 +511,8 @@ impl RwLock { lemma_consts_properties_value(next_usize); lemma_consts_properties_prev_next(prev_usize, next_usize); g.read_retract_token.combine(retract_read_token.tracked_unwrap()); + g.release_wm(); + g.sync_pcm(); } ); None @@ -566,6 +562,8 @@ impl RwLock { guard_perm = Some(pointsto); g.core_token.change_to_right(empty); guard_token = Some(g.core_token.split_one_right_knowledge()); + g.acquire_wm(); + g.sync_pcm(); } } ).is_ok() { @@ -605,10 +603,12 @@ impl RwLock { lemma_consts_properties_prev_next(prev, next); if prev & (WRITER | UPGRADEABLE_READER) == 0 { upgrade_guard_token = Some(g.upreader_guard_token.tracked_take()); + g.acquire_wm(); } else if prev & (WRITER | UPGRADEABLE_READER) == WRITER { retract_upgrade_token = Some(g.upread_retract_token.tracked_take()); } + g.sync_pcm(); } ) & (WRITER | UPGRADEABLE_READER); @@ -637,6 +637,8 @@ impl RwLock { else{ g.upread_retract_token= retract_upgrade_token; } + g.release_wm(); + g.sync_pcm(); } ); } @@ -813,6 +815,8 @@ impl RwLockReadGuard<'_, T, G> { let tracked mut tmp = g.read_guard_token.tracked_take_left(); tmp.combine(token); g.read_guard_token = Sum::Left(tmp); + g.release_wm(); + g.sync_pcm(); } ); } @@ -944,6 +948,8 @@ impl RwLockWriteGuard<'_, T, G> { (read_half_cell_perm, left_token), ); g.read_guard_token = Sum::Left(read_guard_token); + g.release_wm(); + g.sync_pcm(); } }; } @@ -1015,6 +1021,7 @@ impl<'a, T /*: ?Sized*/ , G: SpinGuardian> RwLockUpgradeableGuard<'a, T, G> { update prev -> next; ghost g => { lemma_consts_properties_prev_next(prev, next); + g.acquire_wm(); } ); loop { @@ -1079,6 +1086,9 @@ impl<'a, T /*: ?Sized*/ , G: SpinGuardian> RwLockUpgradeableGuard<'a, T, G> { g.core_token.change_to_right(empty); write_guard_token = Some(g.core_token.split_one_right_knowledge()); retract_upgrade_token = Some(g.upread_retract_token.tracked_take()); + g.acquire_wm(); + g.release_wm(); + g.sync_pcm(); } else { err_upread_guard_token = Some(upread_guard_token); } @@ -1101,6 +1111,8 @@ impl<'a, T /*: ?Sized*/ , G: SpinGuardian> RwLockUpgradeableGuard<'a, T, G> { token.validate_with_other(g.upread_retract_token.tracked_borrow()); } g.upread_retract_token = Some(token); + g.release_wm(); + g.sync_pcm(); } ); Ok( @@ -1172,6 +1184,8 @@ impl RwLockUpgradeableGuard<'_, T, G> { } else { g.upreader_guard_token= Some(guard_token); } + g.release_wm(); + g.sync_pcm(); } ); } diff --git a/vstd_extra/src/resource/ghost_resource/acq_rel_rwlock.rs b/vstd_extra/src/resource/ghost_resource/acq_rel_rwlock.rs new file mode 100644 index 000000000..bd8ee72f0 --- /dev/null +++ b/vstd_extra/src/resource/ghost_resource/acq_rel_rwlock.rs @@ -0,0 +1,705 @@ +//! Acquire-release ghost resources for reader-writer lock verification. +//! +//! This module packages the Leaf-style resources used to verify a reader-writer +//! lock into one reusable permission carrier. The executable acquire/release +//! semantics are still provided by the lock's atomics; this carrier records the +//! ownership transfer facts that each successful acquire, failed acquire +//! rollback, release, and upgrade path must maintain. + +use crate::resource::ghost_resource::{count::*, csum::*, excl::*, tokens::*}; +use crate::sum::*; +use vstd::modes::tracked_swap; +use vstd::prelude::*; +use vstd::resource::algebra::ResourceAlgebra; +use vstd::resource::pcm::{PCM, Resource as PcmResource}; +use vstd::resource::relations::frame_preserving_update; + +verus! { + +/// A single-location abstract weak-memory view. +/// +/// This is not a full RC11 timestamp map. It is the part needed by the rwlock +/// proof: release operations publish a monotonically increasing clock, and +/// acquire operations import the currently published clock. +pub ghost struct AcqRelView { + pub clock: nat, +} + +impl AcqRelView { + pub open spec fn init() -> Self { + AcqRelView { clock: 0 } + } + + pub open spec fn leq(self, other: Self) -> bool { + self.clock <= other.clock + } + + pub open spec fn join(self, other: Self) -> Self { + if self.clock <= other.clock { + other + } else { + self + } + } +} + +/// Abstract release/acquire state for one synchronization location. +pub ghost struct AcqRelWm { + pub released: AcqRelView, + pub acquired: AcqRelView, +} + +impl AcqRelWm { + pub open spec fn init() -> Self { + AcqRelWm { released: AcqRelView::init(), acquired: AcqRelView::init() } + } + + pub open spec fn wf(self, phase: nat) -> bool { + &&& self.released.clock == phase + &&& self.acquired.leq(self.released) + } + + pub open spec fn acquire(self) -> Self { + AcqRelWm { released: self.released, acquired: self.acquired.join(self.released) } + } + + pub open spec fn release(self) -> Self { + AcqRelWm { + released: AcqRelView { clock: self.released.clock + 1 }, + acquired: self.acquired, + } + } +} + +/// Standalone PCM carrier for acquire-release reader-writer lock protocols. +/// +/// `Elem` is an authoritative abstract state for the lock protocol. The PCM is +/// exclusive except for `Unit`, so changing one valid authoritative state into +/// another is frame-preserving: no non-unit frame can coexist with an `Elem`. +pub ghost enum AcqRelRwPCM { + Unit, + Elem { + readers: nat, + upreaders: nat, + writers: nat, + pending_read_fails: nat, + pending_upread_fails: nat, + phase: nat, + }, + Invalid, +} + +impl AcqRelRwPCM< + MAX_READERS, + READ_RETRACT, +> { + pub open spec fn elem( + readers: nat, + upreaders: nat, + writers: nat, + pending_read_fails: nat, + pending_upread_fails: nat, + phase: nat, + ) -> Self { + AcqRelRwPCM::Elem { + readers, + upreaders, + writers, + pending_read_fails, + pending_upread_fails, + phase, + } + } + + pub open spec fn wf_counts( + readers: nat, + upreaders: nat, + writers: nat, + pending_read_fails: nat, + pending_upread_fails: nat, + ) -> bool { + &&& readers <= MAX_READERS + &&& upreaders <= 1 + &&& writers <= 1 + &&& pending_read_fails <= READ_RETRACT + &&& pending_upread_fails <= 1 + &&& upreaders + pending_upread_fails <= 1 + &&& writers > 0 ==> readers == 0 && upreaders == 0 + } + + pub open spec fn readers(self) -> nat + recommends + self is Elem, + { + self->readers + } + + pub open spec fn upreaders(self) -> nat + recommends + self is Elem, + { + self->upreaders + } + + pub open spec fn writers(self) -> nat + recommends + self is Elem, + { + self->writers + } + + pub open spec fn pending_read_fails(self) -> nat + recommends + self is Elem, + { + self->pending_read_fails + } + + pub open spec fn pending_upread_fails(self) -> nat + recommends + self is Elem, + { + self->pending_upread_fails + } + + pub open spec fn phase(self) -> nat + recommends + self is Elem, + { + self->phase + } +} + +impl ResourceAlgebra for AcqRelRwPCM< + MAX_READERS, + READ_RETRACT, +> { + open spec fn valid(self) -> bool { + match self { + AcqRelRwPCM::Unit => true, + AcqRelRwPCM::Elem { + readers, + upreaders, + writers, + pending_read_fails, + pending_upread_fails, + phase: _, + } => Self::wf_counts( + readers, + upreaders, + writers, + pending_read_fails, + pending_upread_fails, + ), + AcqRelRwPCM::Invalid => false, + } + } + + open spec fn op(a: Self, b: Self) -> Self { + match (a, b) { + (AcqRelRwPCM::Invalid, _) => AcqRelRwPCM::Invalid, + (_, AcqRelRwPCM::Invalid) => AcqRelRwPCM::Invalid, + (AcqRelRwPCM::Unit, x) => x, + (x, AcqRelRwPCM::Unit) => x, + (AcqRelRwPCM::Elem { .. }, AcqRelRwPCM::Elem { .. }) => AcqRelRwPCM::Invalid, + } + } + + proof fn valid_op(a: Self, b: Self) { + } + + proof fn commutative(a: Self, b: Self) { + } + + proof fn associative(a: Self, b: Self, c: Self) { + } +} + +impl PCM for AcqRelRwPCM< + MAX_READERS, + READ_RETRACT, +> { + open spec fn unit() -> Self { + AcqRelRwPCM::Unit + } + + proof fn op_unit(self) { + } + + proof fn unit_valid() { + } +} + +pub proof fn lemma_acq_rel_rw_pcm_phase_update< + const MAX_READERS: u64, + const READ_RETRACT: u64, +>( + readers: nat, + upreaders: nat, + writers: nat, + pending_read_fails: nat, + pending_upread_fails: nat, + old_phase: nat, + new_phase: nat, +) + requires + AcqRelRwPCM::::elem( + readers, + upreaders, + writers, + pending_read_fails, + pending_upread_fails, + new_phase, + ).valid(), + ensures + frame_preserving_update::>( + AcqRelRwPCM::::elem( + readers, + upreaders, + writers, + pending_read_fails, + pending_upread_fails, + old_phase, + ), + AcqRelRwPCM::::elem( + readers, + upreaders, + writers, + pending_read_fails, + pending_upread_fails, + new_phase, + ), + ), +{ + lemma_acq_rel_rw_pcm_state_update( + AcqRelRwPCM::::elem( + readers, + upreaders, + writers, + pending_read_fails, + pending_upread_fails, + old_phase, + ), + AcqRelRwPCM::::elem( + readers, + upreaders, + writers, + pending_read_fails, + pending_upread_fails, + new_phase, + ), + ); +} + +pub proof fn lemma_acq_rel_rw_pcm_release_read_update< + const MAX_READERS: u64, + const READ_RETRACT: u64, +>( + readers: nat, + upreaders: nat, + pending_read_fails: nat, + pending_upread_fails: nat, + old_phase: nat, + new_phase: nat, +) + requires + readers > 0, + AcqRelRwPCM::::elem( + (readers - 1) as nat, + upreaders, + 0, + pending_read_fails, + pending_upread_fails, + new_phase, + ).valid(), + ensures + frame_preserving_update::>( + AcqRelRwPCM::::elem( + readers, + upreaders, + 0, + pending_read_fails, + pending_upread_fails, + old_phase, + ), + AcqRelRwPCM::::elem( + (readers - 1) as nat, + upreaders, + 0, + pending_read_fails, + pending_upread_fails, + new_phase, + ), + ), +{ + lemma_acq_rel_rw_pcm_state_update( + AcqRelRwPCM::::elem( + readers, + upreaders, + 0, + pending_read_fails, + pending_upread_fails, + old_phase, + ), + AcqRelRwPCM::::elem( + (readers - 1) as nat, + upreaders, + 0, + pending_read_fails, + pending_upread_fails, + new_phase, + ), + ); +} + +pub proof fn lemma_acq_rel_rw_pcm_cancel_pending_read_update< + const MAX_READERS: u64, + const READ_RETRACT: u64, +>( + readers: nat, + upreaders: nat, + writers: nat, + pending_read_fails: nat, + pending_upread_fails: nat, + phase: nat, +) + requires + pending_read_fails > 0, + AcqRelRwPCM::::elem( + readers, + upreaders, + writers, + (pending_read_fails - 1) as nat, + pending_upread_fails, + phase, + ).valid(), + ensures + frame_preserving_update::>( + AcqRelRwPCM::::elem( + readers, + upreaders, + writers, + pending_read_fails, + pending_upread_fails, + phase, + ), + AcqRelRwPCM::::elem( + readers, + upreaders, + writers, + (pending_read_fails - 1) as nat, + pending_upread_fails, + phase, + ), + ), +{ + lemma_acq_rel_rw_pcm_state_update( + AcqRelRwPCM::::elem( + readers, + upreaders, + writers, + pending_read_fails, + pending_upread_fails, + phase, + ), + AcqRelRwPCM::::elem( + readers, + upreaders, + writers, + (pending_read_fails - 1) as nat, + pending_upread_fails, + phase, + ), + ); +} + +pub proof fn lemma_acq_rel_rw_pcm_state_update< + const MAX_READERS: u64, + const READ_RETRACT: u64, +>( + old_state: AcqRelRwPCM, + new_state: AcqRelRwPCM, +) + requires + old_state is Elem, + new_state.valid(), + ensures + frame_preserving_update::>( + old_state, + new_state, + ), +{ + assert forall|c: AcqRelRwPCM| + #![trigger + AcqRelRwPCM::::op(old_state, c), + AcqRelRwPCM::::op(new_state, c) + ] + AcqRelRwPCM::::op(old_state, c).valid() implies + AcqRelRwPCM::::op(new_state, c).valid() by { + match c { + AcqRelRwPCM::Unit => {}, + AcqRelRwPCM::Elem { .. } => {}, + AcqRelRwPCM::Invalid => {}, + } + } +} + +/// Token reserved in the lock while write permission is checked out. +pub type AcqRelNoPerm = EmptyCount; + +/// Half of the protected permission, shared by upread and read modes. +pub type AcqRelHalfPerm = Count; + +/// One read permission plus knowledge that the lock is in shared mode. +pub type AcqRelReadPerm = ( + AcqRelHalfPerm, + OneLeftKnowledge, AcqRelNoPerm, 3>, +); + +/// The authoritative acquire-release resource state stored under the lock +/// atomic invariant. +pub tracked struct AcqRelRwPerms { + /// Standalone PCM mirror of the abstract acquire-release state. + pub pcm: PcmResource>, + /// Shared-vs-writer mode and the resource owner for the protected value. + pub core_token: SumResource, AcqRelNoPerm, 3>, + /// Rollback budget for failed read attempts that have already incremented + /// the concrete reader bits. + pub read_retract_token: TokenResource, + /// Rollback token for the failed upread path that transiently set the + /// concrete upread bit. + pub upread_retract_token: Option, + /// The unique live upgradeable-reader token, when it is stored in the lock. + pub upreader_guard_token: Option< + OneLeftOwner, AcqRelNoPerm, 3>, + >, + /// Pool of read guard permissions, or an empty marker while a writer owns + /// the protected resource. + pub read_guard_token: Sum< + CountResource, MAX_READERS>, + EmptyCount, MAX_READERS>, + >, + /// Ghost publication phase. Each release may advance this value; acquire + /// paths carry tokens from the phase they observed. + pub phase: nat, + pub ghost wm: AcqRelWm, + pub ghost core_token_id: vstd::resource::Loc, + pub ghost frac_id: vstd::resource::Loc, + pub ghost read_retract_token_id: vstd::resource::Loc, + pub ghost upread_retract_token_id: vstd::resource::Loc, + pub ghost read_guard_token_id: vstd::resource::Loc, +} + +impl AcqRelRwPerms< + R, + MAX_READERS, + READ_RETRACT, +> { + /// Construct the initial shared-mode resource state from full ownership of + /// the protected resource. + pub proof fn alloc(tracked resource: R) -> (tracked result: Self) + requires + MAX_READERS > 0, + READ_RETRACT > 0, + ensures + result.pcm.value() == result.abstract_pcm(), + result.core_token_id() == result.core_token.id(), + result.read_retract_token_id() == result.read_retract_token.id(), + result.upread_retract_token is Some, + result.upread_retract_token_id() == result.upread_retract_token->0.id(), + result.read_guard_token is Left, + result.read_guard_token_id() == result.read_guard_token.left().id(), + result.core_token.wf(), + result.core_token.is_left(), + !result.core_token.is_resource_owner(), + result.core_token.frac() == 1, + result.read_retract_token.wf(), + result.read_retract_token.is_full(), + result.upread_retract_token->0.wf(), + result.upreader_guard_token is Some, + result.upreader_guard_token->0.id() == result.core_token_id(), + result.upreader_guard_token->0.has_resource(), + result.upreader_guard_token->0.resource().id() == result.frac_id(), + result.upreader_guard_token->0.resource().resource() == resource, + result.upreader_guard_token->0.resource().frac() == 1, + result.upreader_guard_token->0.wf(), + result.read_guard_token.left().wf(), + result.read_guard_token.left().id() == result.read_guard_token_id(), + result.read_guard_token.left().not_empty(), + result.read_guard_token.left().resource().0.id() == result.frac_id(), + result.read_guard_token.left().resource().0.resource() == resource, + result.read_guard_token.left().resource().0.frac() == 1, + result.read_guard_token.left().resource().1.id() == result.core_token_id(), + result.phase == 0, + result.wm.wf(result.phase), + { + let tracked mut full_perm = Count::::new(resource); + let tracked read_half_perm = full_perm.split(1int); + let ghost frac_id = full_perm.id(); + let tracked mut core_token = SumResource::alloc_left(full_perm); + let tracked read_retract_token = TokenResource::::alloc(()); + let tracked upread_retract_token = UniqueToken::alloc(()); + let tracked upreader_guard_token = core_token.split_one_left_owner(); + let tracked left_token = core_token.split_one_left_knowledge(); + let tracked read_guard_token = CountResource::, MAX_READERS>::alloc( + (read_half_perm, left_token), + ); + let tracked pcm = PcmResource::alloc(AcqRelRwPCM::::elem(0, 0, 0, 0, 0, 0)); + AcqRelRwPerms { + pcm, + core_token, + read_retract_token, + upread_retract_token: Some(upread_retract_token), + upreader_guard_token: Some(upreader_guard_token), + read_guard_token: Sum::Left(read_guard_token), + phase: 0, + wm: AcqRelWm::init(), + core_token_id: core_token.id(), + frac_id, + read_retract_token_id: read_retract_token.id(), + upread_retract_token_id: upread_retract_token.id(), + read_guard_token_id: read_guard_token.id(), + } + } + + pub closed spec fn core_token_id(self) -> vstd::resource::Loc { + self.core_token_id + } + + pub closed spec fn frac_id(self) -> vstd::resource::Loc { + self.frac_id + } + + pub closed spec fn read_retract_token_id(self) -> vstd::resource::Loc { + self.read_retract_token_id + } + + pub closed spec fn upread_retract_token_id(self) -> vstd::resource::Loc { + self.upread_retract_token_id + } + + pub closed spec fn read_guard_token_id(self) -> vstd::resource::Loc { + self.read_guard_token_id + } + + pub open spec fn active_readers(self) -> nat { + if self.read_guard_token is Left { + ((MAX_READERS as int) - self.read_guard_token.left().frac()) as nat + } else { + 0nat + } + } + + pub open spec fn active_upreaders(self) -> nat { + if !self.core_token.is_right() && self.upreader_guard_token is None { + 1nat + } else { + 0nat + } + } + + pub open spec fn active_writers(self) -> nat { + if self.core_token.is_right() { + 1nat + } else { + 0nat + } + } + + pub open spec fn pending_read_fails(self) -> nat { + ((READ_RETRACT as int) - self.read_retract_token.frac()) as nat + } + + pub open spec fn pending_upread_fails(self) -> nat { + if self.upread_retract_token is None { + 1nat + } else { + 0nat + } + } + + pub open spec fn abstract_pcm(self) -> AcqRelRwPCM { + AcqRelRwPCM::::elem( + self.active_readers(), + self.active_upreaders(), + self.active_writers(), + self.pending_read_fails(), + self.pending_upread_fails(), + self.phase, + ) + } + + pub proof fn sync_pcm(tracked &mut self) + requires + old(self).pcm.value() is Elem, + old(self).abstract_pcm().valid(), + ensures + final(self).pcm.loc() == old(self).pcm.loc(), + final(self).pcm.value() == old(self).abstract_pcm(), + final(self).core_token == old(self).core_token, + final(self).read_retract_token == old(self).read_retract_token, + final(self).upread_retract_token == old(self).upread_retract_token, + final(self).upreader_guard_token == old(self).upreader_guard_token, + final(self).read_guard_token == old(self).read_guard_token, + final(self).phase == old(self).phase, + final(self).wm == old(self).wm, + final(self).core_token_id == old(self).core_token_id, + final(self).frac_id == old(self).frac_id, + final(self).read_retract_token_id == old(self).read_retract_token_id, + final(self).upread_retract_token_id == old(self).upread_retract_token_id, + final(self).read_guard_token_id == old(self).read_guard_token_id, + { + let new_state = self.abstract_pcm(); + let tracked mut old_pcm = self.pcm.extract(); + lemma_acq_rel_rw_pcm_state_update(old_pcm.value(), new_state); + let tracked mut new_pcm = old_pcm.update(new_state); + tracked_swap(&mut self.pcm, &mut new_pcm); + } + + pub proof fn acquire_wm(tracked &mut self) + requires + old(self).wm.wf(old(self).phase), + ensures + final(self).wm == old(self).wm.acquire(), + final(self).phase == old(self).phase, + final(self).wm.wf(final(self).phase), + final(self).pcm == old(self).pcm, + final(self).core_token == old(self).core_token, + final(self).read_retract_token == old(self).read_retract_token, + final(self).upread_retract_token == old(self).upread_retract_token, + final(self).upreader_guard_token == old(self).upreader_guard_token, + final(self).read_guard_token == old(self).read_guard_token, + final(self).core_token_id == old(self).core_token_id, + final(self).frac_id == old(self).frac_id, + final(self).read_retract_token_id == old(self).read_retract_token_id, + final(self).upread_retract_token_id == old(self).upread_retract_token_id, + final(self).read_guard_token_id == old(self).read_guard_token_id, + { + self.wm = self.wm.acquire(); + } + + pub proof fn release_wm(tracked &mut self) + requires + old(self).wm.wf(old(self).phase), + ensures + final(self).wm == old(self).wm.release(), + final(self).phase == old(self).phase + 1, + final(self).wm.wf(final(self).phase), + final(self).pcm == old(self).pcm, + final(self).core_token == old(self).core_token, + final(self).read_retract_token == old(self).read_retract_token, + final(self).upread_retract_token == old(self).upread_retract_token, + final(self).upreader_guard_token == old(self).upreader_guard_token, + final(self).read_guard_token == old(self).read_guard_token, + final(self).core_token_id == old(self).core_token_id, + final(self).frac_id == old(self).frac_id, + final(self).read_retract_token_id == old(self).read_retract_token_id, + final(self).upread_retract_token_id == old(self).upread_retract_token_id, + final(self).read_guard_token_id == old(self).read_guard_token_id, + { + self.phase = self.phase + 1; + self.wm = self.wm.release(); + } +} + +} // verus! diff --git a/vstd_extra/src/resource/ghost_resource/mod.rs b/vstd_extra/src/resource/ghost_resource/mod.rs index d49207558..796add6e8 100644 --- a/vstd_extra/src/resource/ghost_resource/mod.rs +++ b/vstd_extra/src/resource/ghost_resource/mod.rs @@ -1,4 +1,5 @@ //! Ghost resources available for use in proofs. +pub mod acq_rel_rwlock; pub mod count; pub mod csum; pub mod excl;