Struct AtomicDataWithOwner 

pub struct AtomicDataWithOwner<V, I: SimpleResourceInvariant<V>> {
    pub data: V,
    pub permission: Tracked<I::Resource>,
}

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>,
}

ghost struct MyDataInvariant;

impl SimpleResourceInvariant<MyData> for MyDataInvariant {

    type Resource = MyDataWithOwner;

    open spec fn inv(value: MyData, resource: MyDataWithOwner) -> bool {
        &&& resource.baz == value.foo
        &&& resource.quz.len() == value.bar
    }
}

type Data = AtomicDataWithOwner<MyData, MyDataInvariant>;

Fields

data: V

The underlying data.

permission: Tracked<I::Resource>

The permission to access the data.

Implementations

impl<V, I: SimpleResourceInvariant<V>> AtomicDataWithOwner<V, I>

pub exec fn new( data: V, permission: Tracked<I::Resource>, Ghost(_pred): Ghost<I>, ) -> Self

requires

I::inv(data, permission@),

Trait Implementations

impl<V, I: SimpleResourceInvariant<V>> !Clone for AtomicDataWithOwner<V, I>

impl<V, I: SimpleResourceInvariant<V>> !Copy for AtomicDataWithOwner<V, I>

impl<V, I: SimpleResourceInvariant<V>> Deref for AtomicDataWithOwner<V, I>

exec fn deref(&self) -> &Self::Target

returns

self.data,

type Target = V

The resulting type after dereferencing.

impl<V, I: SimpleResourceInvariant<V>> Inv for AtomicDataWithOwner<V, I>

open spec fn inv(self) -> bool

{ I::inv(self.data, self.permission@) }

impl<T, I: SimpleResourceInvariant<T>> View for AtomicDataWithOwner<T, I>

open spec fn view(&self) -> Self::V

{ self.data }

type V = T