Struct AtomicInvariant 

pub struct AtomicInvariant<T>(/* private fields */);

A shareable invariant for atomic accesses between threads.

If you need sequentially consistent accesses, use AtomicInvariant.

If you do not need to share the invariant across threads, see NonAtomicInvariant.

Implementations

impl<T: Protocol> AtomicInvariant<T>

pub fn new(value: Ghost<T>, namespace: Snapshot<Namespace>) -> Ghost<Self>

Construct a AtomicInvariant

Parameters

• value: the actual data contained in the invariant. Use Self::open to access it. Also called the ‘private’ part of the invariant.
• namespace: the namespace of the invariant. This is required to avoid opening the same invariant twice.

requires

value.protocol()

ensures

result.public() == value.public()

ensures

result.namespace() == *namespace

terminates

ghost

pub fn namespace(self) -> Namespace

Get the namespace associated with this invariant.

logic(opaque)

pub fn public(self) -> T::Public

Get the ‘public’ part of this invariant.

logic(opaque)

pub fn into_inner(self) -> T

Gives the actual invariant held by the AtomicInvariant.

ensures

result.public() == self.public() && result.protocol()

terminates

ghost

pub fn open<A>( &self, tokens: Tokens<'_>, f: impl FnGhost + for<'a> FnOnce(&'a mut T) -> A, ) -> A

Open the invariant to get the data stored inside.

This will call the closure f with the inner data. You must restore the contained Protocol before returning from the closure.

NOTE: This function can only be called from ghost code, because atomic invariants are always wrapped in Ghost. This guarantees atomicity.

requires

tokens.contains(self.namespace())

requires

forall<t: &mut T> t.public() == self.public() && t.protocol() && inv(t) ==>
    f.precondition((t,)) &&
    // f must restore the invariant
    (forall<res: A> f.postcondition_once((t,), res) ==> (^t).public() == self.public() && (^t).protocol())

ensures

exists<t: &mut T> t.public() == self.public() && t.protocol() && inv(t) &&
    f.postcondition_once((t,), result)

terminates

ghost

Trait Implementations

impl<T: Send> Send for AtomicInvariant<T>

impl<T: Send + Objective> Sync for AtomicInvariant<T>