Struct AtomicDataWithOwner Copy item path

A structure that combines some data with a permission to access it.

For example, in aster_common we can see a lot of structs with its owner associated. E.g., MetaSlotOwner is the owner of MetaSlot. This struct can be used to represent such a combination because now the permission is no longer exclusively owner by some specific CPU and is “shared” among multiple threads via atomic operations.

This struct is especially useful when used in conjunction with synchronization primitives like [Once], where we want to ensure that the data is initialized only once and the permission is preserved throughout the lifetime of the data.

§Examples

 struct MyData {
    pub foo: u32,
    pub bar: u32,
 }

tracked struct MyDataWithOwner {
   pub baz: nat,
   pub quz: Seq<int>,
}

impl Inv for MyData {
    // inv...
}

impl Predicate<MyData> for MyDataWithOwner {
   #[verifier::inline]
   open spec fn inv_with(self, v: MyData) -> bool {
        &&& self.baz == v.foo as nat
        &&& self.quz.len() == v.bar as nat
   }
}

type Data = AtomicDataWithOwner<MyData, MyDataWithOwner>;