From c642cd3a7556ba35944ba7cdc0d7507a7238652a Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Tue, 19 May 2026 16:58:07 +0800 Subject: [PATCH 1/3] prove: PCM for rwlock --- ostd/src/sync/rwlock.rs | 40 ++--- .../resource/ghost_resource/acq_rel_rwlock.rs | 146 ++++++++++++++++++ vstd_extra/src/resource/ghost_resource/mod.rs | 1 + 3 files changed, 159 insertions(+), 28 deletions(-) create mode 100644 vstd_extra/src/resource/ghost_resource/acq_rel_rwlock.rs diff --git a/ostd/src/sync/rwlock.rs b/ostd/src/sync/rwlock.rs index 64a3266ad..cdbefc965 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, @@ -393,6 +371,12 @@ impl RwLock { upread_retract_token: Some(upread_retract_token), upreader_guard_token: Some(upreader_guard_token), read_guard_token: Sum::Left(read_guard_token), + phase: 0, + 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 { 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..c102229f3 --- /dev/null +++ b/vstd_extra/src/resource/ghost_resource/acq_rel_rwlock.rs @@ -0,0 +1,146 @@ +//! 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::prelude::*; + +verus! { + +/// 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 { + /// 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 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.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, + { + 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), + ); + AcqRelRwPerms { + 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, + 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 + } +} + +} // 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; From 7abc463f5a13d7bddf8de526b0a5cb89b2904076 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Tue, 19 May 2026 17:27:31 +0800 Subject: [PATCH 2/3] prove: PCM for rwlock --- ostd/src/sync/rwlock.rs | 14 + .../resource/ghost_resource/acq_rel_rwlock.rs | 431 ++++++++++++++++++ 2 files changed, 445 insertions(+) diff --git a/ostd/src/sync/rwlock.rs b/ostd/src/sync/rwlock.rs index cdbefc965..a6a86a55c 100644 --- a/ostd/src/sync/rwlock.rs +++ b/ostd/src/sync/rwlock.rs @@ -216,6 +216,8 @@ 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() &&& g.core_token.id() == v_id@.core_token_id &&& g.core_token.wf() &&& g.core_token.is_left() ==> { @@ -358,6 +360,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(), @@ -366,6 +369,7 @@ 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), @@ -480,6 +484,7 @@ impl RwLock { } else { retract_read_token = Some(g.read_retract_token.split_one()); } + g.sync_pcm(); } ); if lock & (WRITER | MAX_READER | BEING_UPGRADED) == 0 { @@ -501,6 +506,7 @@ 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.sync_pcm(); } ); None @@ -550,6 +556,7 @@ impl RwLock { guard_perm = Some(pointsto); g.core_token.change_to_right(empty); guard_token = Some(g.core_token.split_one_right_knowledge()); + g.sync_pcm(); } } ).is_ok() { @@ -593,6 +600,7 @@ impl RwLock { else if prev & (WRITER | UPGRADEABLE_READER) == WRITER { retract_upgrade_token = Some(g.upread_retract_token.tracked_take()); } + g.sync_pcm(); } ) & (WRITER | UPGRADEABLE_READER); @@ -621,6 +629,7 @@ impl RwLock { else{ g.upread_retract_token= retract_upgrade_token; } + g.sync_pcm(); } ); } @@ -797,6 +806,7 @@ 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.sync_pcm(); } ); } @@ -928,6 +938,7 @@ impl RwLockWriteGuard<'_, T, G> { (read_half_cell_perm, left_token), ); g.read_guard_token = Sum::Left(read_guard_token); + g.sync_pcm(); } }; } @@ -1063,6 +1074,7 @@ 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.sync_pcm(); } else { err_upread_guard_token = Some(upread_guard_token); } @@ -1085,6 +1097,7 @@ 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.sync_pcm(); } ); Ok( @@ -1156,6 +1169,7 @@ impl RwLockUpgradeableGuard<'_, T, G> { } else { g.upreader_guard_token= Some(guard_token); } + 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 index c102229f3..282c0159a 100644 --- a/vstd_extra/src/resource/ghost_resource/acq_rel_rwlock.rs +++ b/vstd_extra/src/resource/ghost_resource/acq_rel_rwlock.rs @@ -9,9 +9,440 @@ use crate::resource::ghost_resource::{count::*, csum::*, excl::*, tokens::*}; use crate::sum::*; use vstd::prelude::*; +use vstd::resource::algebra::ResourceAlgebra; +use vstd::resource::pcm::PCM; +use vstd::resource::relations::frame_preserving_update; verus! { +/// Standalone PCM carrier for acquire-release reader-writer lock protocols. +/// +/// `Elem` counts the currently owned protocol fragments. `phase` is ghost +/// publication metadata: it composes monotonically but does not affect validity, +/// so phase-only updates are frame-preserving. +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 { + readers: ar, + upreaders: au, + writers: aw, + pending_read_fails: apr, + pending_upread_fails: apu, + phase: ap, + }, + AcqRelRwPCM::Elem { + readers: br, + upreaders: bu, + writers: bw, + pending_read_fails: bpr, + pending_upread_fails: bpu, + phase: bp, + }, + ) => AcqRelRwPCM::Elem { + readers: ar + br, + upreaders: au + bu, + writers: aw + bw, + pending_read_fails: apr + bpr, + pending_upread_fails: apu + bpu, + phase: ap + bp, + }, + } + } + + 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, +) + 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, + ), + ), +{ + assert forall|c: AcqRelRwPCM| + #![trigger + AcqRelRwPCM::::op( + AcqRelRwPCM::elem( + readers, + upreaders, + writers, + pending_read_fails, + pending_upread_fails, + old_phase, + ), + c, + ), + AcqRelRwPCM::::op( + AcqRelRwPCM::elem( + readers, + upreaders, + writers, + pending_read_fails, + pending_upread_fails, + new_phase, + ), + c, + ) + ] + AcqRelRwPCM::::op( + AcqRelRwPCM::elem( + readers, + upreaders, + writers, + pending_read_fails, + pending_upread_fails, + old_phase, + ), + c, + ).valid() implies AcqRelRwPCM::::op( + AcqRelRwPCM::elem( + readers, + upreaders, + writers, + pending_read_fails, + pending_upread_fails, + new_phase, + ), + c, + ).valid() by { + } +} + +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, + 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, + ), + ), +{ + assert forall|c: AcqRelRwPCM| + #![trigger + AcqRelRwPCM::::op( + AcqRelRwPCM::elem( + readers, + upreaders, + 0, + pending_read_fails, + pending_upread_fails, + old_phase, + ), + c, + ), + AcqRelRwPCM::::op( + AcqRelRwPCM::elem( + (readers - 1) as nat, + upreaders, + 0, + pending_read_fails, + pending_upread_fails, + new_phase, + ), + c, + ) + ] + AcqRelRwPCM::::op( + AcqRelRwPCM::elem( + readers, + upreaders, + 0, + pending_read_fails, + pending_upread_fails, + old_phase, + ), + c, + ).valid() implies AcqRelRwPCM::::op( + AcqRelRwPCM::elem( + (readers - 1) as nat, + upreaders, + 0, + pending_read_fails, + pending_upread_fails, + new_phase, + ), + c, + ).valid() by { + } +} + +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, + 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, + ), + ), +{ + assert forall|c: AcqRelRwPCM| + #![trigger + AcqRelRwPCM::::op( + AcqRelRwPCM::elem( + readers, + upreaders, + writers, + pending_read_fails, + pending_upread_fails, + phase, + ), + c, + ), + AcqRelRwPCM::::op( + AcqRelRwPCM::elem( + readers, + upreaders, + writers, + (pending_read_fails - 1) as nat, + pending_upread_fails, + phase, + ), + c, + ) + ] + AcqRelRwPCM::::op( + AcqRelRwPCM::elem( + readers, + upreaders, + writers, + pending_read_fails, + pending_upread_fails, + phase, + ), + c, + ).valid() implies AcqRelRwPCM::::op( + AcqRelRwPCM::elem( + readers, + upreaders, + writers, + (pending_read_fails - 1) as nat, + pending_upread_fails, + phase, + ), + c, + ).valid() by { + } +} + /// Token reserved in the lock while write permission is checked out. pub type AcqRelNoPerm = EmptyCount; From 502c0fbc7450b2ed7833467cd20dcde24e0fcf09 Mon Sep 17 00:00:00 2001 From: Marsman1996 Date: Tue, 19 May 2026 17:40:29 +0800 Subject: [PATCH 3/3] prove: weak memory model for rwlock --- ostd/src/sync/rwlock.rs | 16 + .../resource/ghost_resource/acq_rel_rwlock.rs | 472 +++++++++++------- 2 files changed, 316 insertions(+), 172 deletions(-) diff --git a/ostd/src/sync/rwlock.rs b/ostd/src/sync/rwlock.rs index a6a86a55c..27dc0613d 100644 --- a/ostd/src/sync/rwlock.rs +++ b/ostd/src/sync/rwlock.rs @@ -218,6 +218,9 @@ closed spec fn wf(self) -> bool { &&& !(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() ==> { @@ -376,6 +379,7 @@ impl RwLock { 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, @@ -481,6 +485,7 @@ 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()); } @@ -506,6 +511,7 @@ 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(); } ); @@ -556,6 +562,7 @@ 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(); } } @@ -596,6 +603,7 @@ 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()); @@ -629,6 +637,7 @@ impl RwLock { else{ g.upread_retract_token= retract_upgrade_token; } + g.release_wm(); g.sync_pcm(); } ); @@ -806,6 +815,7 @@ 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(); } ); @@ -938,6 +948,7 @@ 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(); } }; @@ -1010,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 { @@ -1074,6 +1086,8 @@ 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); @@ -1097,6 +1111,7 @@ 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(); } ); @@ -1169,6 +1184,7 @@ 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 index 282c0159a..bd8ee72f0 100644 --- a/vstd_extra/src/resource/ghost_resource/acq_rel_rwlock.rs +++ b/vstd_extra/src/resource/ghost_resource/acq_rel_rwlock.rs @@ -8,18 +8,74 @@ 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; +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` counts the currently owned protocol fragments. `phase` is ghost -/// publication metadata: it composes monotonically but does not affect validity, -/// so phase-only updates are frame-preserving. +/// `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 { @@ -145,31 +201,7 @@ impl ResourceAlgebra for AcqRel (_, AcqRelRwPCM::Invalid) => AcqRelRwPCM::Invalid, (AcqRelRwPCM::Unit, x) => x, (x, AcqRelRwPCM::Unit) => x, - ( - AcqRelRwPCM::Elem { - readers: ar, - upreaders: au, - writers: aw, - pending_read_fails: apr, - pending_upread_fails: apu, - phase: ap, - }, - AcqRelRwPCM::Elem { - readers: br, - upreaders: bu, - writers: bw, - pending_read_fails: bpr, - pending_upread_fails: bpu, - phase: bp, - }, - ) => AcqRelRwPCM::Elem { - readers: ar + br, - upreaders: au + bu, - writers: aw + bw, - pending_read_fails: apr + bpr, - pending_upread_fails: apu + bpu, - phase: ap + bp, - }, + (AcqRelRwPCM::Elem { .. }, AcqRelRwPCM::Elem { .. }) => AcqRelRwPCM::Invalid, } } @@ -210,9 +242,18 @@ pub proof fn lemma_acq_rel_rw_pcm_phase_update< 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( + AcqRelRwPCM::::elem( readers, upreaders, writers, @@ -220,7 +261,7 @@ pub proof fn lemma_acq_rel_rw_pcm_phase_update< pending_upread_fails, old_phase, ), - AcqRelRwPCM::elem( + AcqRelRwPCM::::elem( readers, upreaders, writers, @@ -230,53 +271,24 @@ pub proof fn lemma_acq_rel_rw_pcm_phase_update< ), ), { - assert forall|c: AcqRelRwPCM| - #![trigger - AcqRelRwPCM::::op( - AcqRelRwPCM::elem( - readers, - upreaders, - writers, - pending_read_fails, - pending_upread_fails, - old_phase, - ), - c, - ), - AcqRelRwPCM::::op( - AcqRelRwPCM::elem( - readers, - upreaders, - writers, - pending_read_fails, - pending_upread_fails, - new_phase, - ), - c, - ) - ] - AcqRelRwPCM::::op( - AcqRelRwPCM::elem( - readers, - upreaders, - writers, - pending_read_fails, - pending_upread_fails, - old_phase, - ), - c, - ).valid() implies AcqRelRwPCM::::op( - AcqRelRwPCM::elem( - readers, - upreaders, - writers, - pending_read_fails, - pending_upread_fails, - new_phase, - ), - c, - ).valid() by { - } + 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< @@ -292,9 +304,17 @@ pub proof fn lemma_acq_rel_rw_pcm_release_read_update< ) 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( + AcqRelRwPCM::::elem( readers, upreaders, 0, @@ -302,7 +322,7 @@ pub proof fn lemma_acq_rel_rw_pcm_release_read_update< pending_upread_fails, old_phase, ), - AcqRelRwPCM::elem( + AcqRelRwPCM::::elem( (readers - 1) as nat, upreaders, 0, @@ -312,53 +332,24 @@ pub proof fn lemma_acq_rel_rw_pcm_release_read_update< ), ), { - assert forall|c: AcqRelRwPCM| - #![trigger - AcqRelRwPCM::::op( - AcqRelRwPCM::elem( - readers, - upreaders, - 0, - pending_read_fails, - pending_upread_fails, - old_phase, - ), - c, - ), - AcqRelRwPCM::::op( - AcqRelRwPCM::elem( - (readers - 1) as nat, - upreaders, - 0, - pending_read_fails, - pending_upread_fails, - new_phase, - ), - c, - ) - ] - AcqRelRwPCM::::op( - AcqRelRwPCM::elem( - readers, - upreaders, - 0, - pending_read_fails, - pending_upread_fails, - old_phase, - ), - c, - ).valid() implies AcqRelRwPCM::::op( - AcqRelRwPCM::elem( - (readers - 1) as nat, - upreaders, - 0, - pending_read_fails, - pending_upread_fails, - new_phase, - ), - c, - ).valid() by { - } + 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< @@ -374,9 +365,17 @@ pub proof fn lemma_acq_rel_rw_pcm_cancel_pending_read_update< ) 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( + AcqRelRwPCM::::elem( readers, upreaders, writers, @@ -384,7 +383,7 @@ pub proof fn lemma_acq_rel_rw_pcm_cancel_pending_read_update< pending_upread_fails, phase, ), - AcqRelRwPCM::elem( + AcqRelRwPCM::::elem( readers, upreaders, writers, @@ -393,53 +392,55 @@ pub proof fn lemma_acq_rel_rw_pcm_cancel_pending_read_update< 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( - AcqRelRwPCM::elem( - readers, - upreaders, - writers, - pending_read_fails, - pending_upread_fails, - phase, - ), - c, - ), - AcqRelRwPCM::::op( - AcqRelRwPCM::elem( - readers, - upreaders, - writers, - (pending_read_fails - 1) as nat, - pending_upread_fails, - phase, - ), - c, - ) + AcqRelRwPCM::::op(old_state, c), + AcqRelRwPCM::::op(new_state, c) ] - AcqRelRwPCM::::op( - AcqRelRwPCM::elem( - readers, - upreaders, - writers, - pending_read_fails, - pending_upread_fails, - phase, - ), - c, - ).valid() implies AcqRelRwPCM::::op( - AcqRelRwPCM::elem( - readers, - upreaders, - writers, - (pending_read_fails - 1) as nat, - pending_upread_fails, - phase, - ), - c, - ).valid() by { + AcqRelRwPCM::::op(old_state, c).valid() implies + AcqRelRwPCM::::op(new_state, c).valid() by { + match c { + AcqRelRwPCM::Unit => {}, + AcqRelRwPCM::Elem { .. } => {}, + AcqRelRwPCM::Invalid => {}, + } } } @@ -458,6 +459,8 @@ pub type AcqRelReadPerm = ( /// 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 @@ -479,6 +482,7 @@ pub tracked struct AcqRelRwPerms AcqRelRwPerms< 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, @@ -526,6 +531,7 @@ impl AcqRelRwPerms< 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); @@ -538,13 +544,16 @@ impl AcqRelRwPerms< 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(), @@ -572,6 +581,125 @@ impl AcqRelRwPerms< 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!