vstd_extra/
atomic_data.rs

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

vstd_extra/
atomic_data.rs
