From 13234c7517d2b9d5fb889110850485de12e96c8d Mon Sep 17 00:00:00 2001 From: rikosellic <64517311+rikosellic@users.noreply.github.com> Date: Tue, 19 May 2026 16:25:23 +0800 Subject: [PATCH 1/2] Use `*mut` instead of `NonNull` in `NonNullPtr::ptr_perm_match`` --- ostd/src/sync/rcu/non_null/either.rs | 12 ++++++------ ostd/src/sync/rcu/non_null/mod.rs | 18 +++++++++--------- 2 files changed, 15 insertions(+), 15 deletions(-) diff --git a/ostd/src/sync/rcu/non_null/either.rs b/ostd/src/sync/rcu/non_null/either.rs index 49108bdcb..97b58defd 100644 --- a/ostd/src/sync/rcu/non_null/either.rs +++ b/ostd/src/sync/rcu/non_null/either.rs @@ -211,19 +211,19 @@ unsafe impl NonNullPtr for Either { } } - open spec fn ptr_perm_match(ptr: NonNull, perm: Self::Permission) -> bool { + open spec fn ptr_perm_match(ptr: *mut Self::Target, perm: Self::Permission) -> bool { let tag = 1usize << Self::ALIGN_BITS; match perm { Sum::Left(left) => { - &&& ptr.view_ptr_mut().addr() & tag == 0 + &&& ptr.addr() & tag == 0 &&& L::ptr_perm_match(ptr.cast(), left) }, Sum::Right(right) => { - let untagged_ptr = ptr.view_ptr_mut().with_addr((ptr.view_ptr_mut().addr() & !tag)); + let untagged_ptr = ptr.with_addr((ptr.addr() & !tag)); let right_nonnull = nonnull_from_ptr_mut_spec(untagged_ptr); - &&& ptr.view_ptr_mut().addr() & tag == tag - &&& (ptr.view_ptr_mut().addr() & !tag) != 0 - &&& R::ptr_perm_match(right_nonnull.cast(), right) + &&& ptr.addr() & tag == tag + &&& (ptr.addr() & !tag) != 0 + &&& R::ptr_perm_match(right_nonnull.cast().view_ptr_mut(), right) }, } } diff --git a/ostd/src/sync/rcu/non_null/mod.rs b/ostd/src/sync/rcu/non_null/mod.rs index 538ab5424..ef5d8afa6 100644 --- a/ostd/src/sync/rcu/non_null/mod.rs +++ b/ostd/src/sync/rcu/non_null/mod.rs @@ -58,7 +58,7 @@ pub unsafe trait NonNullPtr: Sized + 'static { /// VERUS LIMITATION: the #[verus_spec] attribute does not support `with` in trait yet. fn into_raw(self) -> ((res_ptr, perm): (NonNull, Tracked)) ensures - Self::ptr_perm_match(res_ptr, perm@), + Self::ptr_perm_match(res_ptr.view_ptr_mut(), perm@), self.rel_perm(perm@), perm@.inv(), res_ptr.view_ptr_mut().addr() % (1usize << Self::ALIGN_BITS) == 0, @@ -81,7 +81,7 @@ pub unsafe trait NonNullPtr: Sized + 'static { /// VERUS LIMITATION: the #[verus_spec] attribute does not support `with` in trait yet. unsafe fn from_raw(ptr: NonNull, perm: Tracked) -> (ret: Self) requires - Self::ptr_perm_match(ptr, perm@), + Self::ptr_perm_match(ptr.view_ptr_mut(), perm@), perm@.inv(), ensures ret.rel_perm(perm@), @@ -98,7 +98,7 @@ pub unsafe trait NonNullPtr: Sized + 'static { fn ref_as_raw(ptr_ref: Self::Ref<'_>) -> NonNull;*/ /// A specification function that constraints the nonnull pointer and the permission returned by `into_raw`. /// This design is to support the tagged pointer trick used in `Either`. - spec fn ptr_perm_match(ptr: NonNull, perm: Self::Permission) -> bool; + spec fn ptr_perm_match(ptr: *mut Self::Target, perm: Self::Permission) -> bool; /// A specification function that relates the original smart pointer and the permission. spec fn rel_perm(self, perm: Self::Permission) -> bool; @@ -142,7 +142,7 @@ pub unsafe trait NonNullPtrRef<'a>: NonNullPtr { unsafe fn raw_as_ref(raw: NonNull, perm: Tracked) -> (ret: Self::Ref) requires - Self::ptr_perm_match(raw, Self::ref_perm_view_permission(perm@)), + Self::ptr_perm_match(raw.view_ptr_mut(), Self::ref_perm_view_permission(perm@)), perm@.inv(), ensures Self::ref_rel_perm(ret, perm@), @@ -155,7 +155,7 @@ pub unsafe trait NonNullPtrRef<'a>: NonNullPtr { )) ensures Self::ref_rel_perm(ptr_ref, perm@), - Self::ptr_perm_match(res_ptr, Self::ref_perm_view_permission(perm@)), + Self::ptr_perm_match(res_ptr.view_ptr_mut(), Self::ref_perm_view_permission(perm@)), perm@.inv(), res_ptr.view_ptr_mut().addr() % (1usize << Self::ALIGN_BITS) == 0, ; @@ -273,8 +273,8 @@ unsafe impl NonNullPtr for Box { } } - open spec fn ptr_perm_match(ptr: NonNull, perm: Self::Permission) -> bool { - ptr.view_ptr_mut() == perm.ptr() + open spec fn ptr_perm_match(ptr: *mut Self::Target, perm: Self::Permission) -> bool { + ptr == perm.ptr() } open spec fn rel_perm(self, perm: Self::Permission) -> bool { @@ -404,8 +404,8 @@ unsafe impl NonNullPtr for Arc { } } - open spec fn ptr_perm_match(ptr: NonNull, perm: Self::Permission) -> bool { - ptr.view_ptr_mut() == perm.ptr() + open spec fn ptr_perm_match(ptr: *mut Self::Target, perm: Self::Permission) -> bool { + ptr == perm.ptr() } open spec fn rel_perm(self, perm: Self::Permission) -> bool { From 184a24a2983d5ce5d351023291cb7247c706c295 Mon Sep 17 00:00:00 2001 From: rikosellic <64517311+rikosellic@users.noreply.github.com> Date: Tue, 19 May 2026 16:48:34 +0800 Subject: [PATCH 2/2] RCU init --- ostd/src/sync/rcu/mod.rs | 31 +++++++++++++++++++++++++------ 1 file changed, 25 insertions(+), 6 deletions(-) diff --git a/ostd/src/sync/rcu/mod.rs b/ostd/src/sync/rcu/mod.rs index 08ae55659..5e07f8aec 100644 --- a/ostd/src/sync/rcu/mod.rs +++ b/ostd/src/sync/rcu/mod.rs @@ -1,18 +1,23 @@ // SPDX-License-Identifier: MPL-2.0 //! Read-copy update (RCU). -/* use core::{ + +use vstd::prelude::*; +use vstd::atomic_ghost::AtomicPtr; +use vstd_extra::prelude::*; + +use core::{ marker::PhantomData, mem::ManuallyDrop, ops::Deref, ptr::NonNull, - sync::atomic::{ + /*sync::atomic::{ AtomicPtr, Ordering::{AcqRel, Acquire}, - }, + },*/ }; use non_null::NonNullPtr; -use spin::once::Once; +/* use spin::once::Once; use self::monitor::RcuMonitor; use crate::task::{ @@ -22,6 +27,8 @@ use crate::task::{ mod monitor;*/ pub mod non_null; + +verus!{ /* /// A Read-Copy Update (RCU) cell for sharing a pointer between threads. /// @@ -105,25 +112,36 @@ pub struct RcuOption(RcuInner

); #[clippy::has_significant_drop] #[must_use] pub struct RcuOptionReadGuard<'a, P: NonNullPtr>(RcuReadGuardInner<'a, P>); - +*/ +struct_with_invariants!{ /// The inner implementation of both [`Rcu`] and [`RcuOption`]. struct RcuInner { - ptr: AtomicPtr<

::Target>, + ptr: AtomicPtr<

::Target,_ ,Option<

::Permission>, _>, // We want to implement Send and Sync explicitly. // Having a pointer field prevents them from being implemented // automatically by the compiler. _marker: PhantomData<*const P::Target>, } +closed spec fn wf(self) -> bool { + invariant on ptr with (_marker) is (p:*mut

::Target,g:Option<

::Permission>) { + g is Some ==> P::ptr_perm_match(p, g->0) + } +} +} + // SAFETY: It is apparent that if `P` is `Send`, then `Rcu

` is `Send`. +#[verifier::external] unsafe impl Send for RcuInner

where P: Send {} // SAFETY: To implement `Sync` for `Rcu

`, we need to meet two conditions: // 1. `P` must be `Sync` because `Rcu::get` allows concurrent access. // 2. `P` must be `Send` because `Rcu::update` may obtain an object // of `P` created on another thread. +#[verifier::external] unsafe impl Sync for RcuInner

where P: Send + Sync {} +/* impl RcuInner

{ const fn new_none() -> Self { Self { @@ -507,3 +525,4 @@ pub fn init() { RCU_MONITOR.call_once(RcuMonitor::new); } */ +} \ No newline at end of file