ostd/sync/
atomic_data.rs

1use core::ops::Deref;
2
3use vstd::{predicate::Predicate, prelude::*};
4use vstd_extra::ownership::Inv;
5
6use super::{RwLockReadGuard, SpinGuardian};
7
8verus! {
9
10/// A structure that combines some data with a permission to access it.
11///
12/// For example, in `aster_common` we can see a lot of structs with
13/// its `owner` associated. E.g., `MetaSlotOwner` is the owner of
14/// `MetaSlot`. This struct can be used to represent such a combination
15/// because now the permission is no longer exclusively owner by some
16/// specific CPU and is "shared" among multiple threads via atomic
17/// operations.
18///
19/// This struct is especially useful when used in conjunction with
20/// synchronization primitives like [`Once`], where we want to ensure that
21/// the data is initialized only once and the permission is preserved
22/// throughout the lifetime of the data.
23///
24/// # Examples
25///
26/// ```rust,ignore
27///  struct MyData {
28///     pub foo: u32,
29///     pub bar: u32,
30///  }
31///
32/// tracked struct MyDataWithOwner {
33///    pub baz: nat,
34///    pub quz: Seq<int>,
35/// }
36///
37/// impl Inv for MyData {
38///     // inv...
39/// }
40///
41/// impl Predicate<MyData> for MyDataWithOwner {
42///    #[verifier::inline]
43///    open spec fn inv_with(self, v: MyData) -> bool {
44///         &&& self.baz == v.foo as nat
45///         &&& self.quz.len() == v.bar as nat
46///    }
47/// }
48///
49/// type Data = AtomicDataWithOwner<MyData, MyDataWithOwner>;
50/// ```
51#[repr(transparent)]
52#[allow(repr_transparent_non_zst_fields)]
53pub struct AtomicDataWithOwner<V, Own> {
54    /// The underlying data.
55    pub data: V,
56    /// The permission to access the data.
57    pub permission: Tracked<Own>,
58}
59
60impl<'a, V, Own, G: SpinGuardian> RwLockReadGuard<'a, crate::sync::AtomicDataWithOwner<V, Own>, G> {
61    /// Borrows the tracked permission stored in an [`AtomicDataWithOwner`].
62    #[verifier::external_body]
63    pub proof fn atomic_permission(tracked &self) -> (tracked permission: &'a Own)
64        returns
65            self@.permission@,
66    {
67        unimplemented!()
68    }
69}
70
71impl<V, Own> Deref for AtomicDataWithOwner<V, Own> {
72    type Target = V;
73
74    #[inline]
75    #[verus_spec(returns self.data)]
76    fn deref(&self) -> &Self::Target {
77        &self.data
78    }
79}
80
81impl<V, Own> AtomicDataWithOwner<V, Own> {
82    #[inline]
83    pub fn new(data: V, permission: Tracked<Own>) -> Self {
84        Self { data, permission }
85    }
86}
87
88impl<V, Own> !Copy for AtomicDataWithOwner<V, Own> {
89
90}
91
92impl<V, Own> !Clone for AtomicDataWithOwner<V, Own> {
93
94}
95
96impl<V, Own: Predicate<V>> Inv for AtomicDataWithOwner<V, Own> {
97    #[verifier::inline]
98    open spec fn inv(self) -> bool {
99        &&& self.permission.predicate(self.data)
100    }
101}
102
103impl<T, Own> View for AtomicDataWithOwner<T, Own> {
104    type V = T;
105
106    #[verifier::inline]
107    open spec fn view(&self) -> Self::V {
108        self.data
109    }
110}
111
112} // verus!
ostd/sync/atomic_data.rs

ostd/sync/
atomic_data.rs
