Struct Committer 

pub struct Committer<C: Container<Value: Sized>>(/* private fields */);

Wrapper around a single atomic operation, where multiple ghost steps can be performed.

Implementations

impl<C: Container<Value: Sized>> Committer<C>

pub fn shot(self) -> bool

Status of the committer

logic(opaque)

pub fn ward(self) -> C

Identity of the committer

This is used so that we can only use the committer with the right [AtomicOwn].

logic(opaque)

pub fn old_value(self) -> C::Value

Value held by the [AtomicOwn], before the [shoot].

logic(opaque)

pub fn new_value(self) -> C::Value

Value held by the [AtomicOwn], after the [shoot].

logic(opaque)

pub fn shoot(&mut self, own: &mut Perm<C>)

‘Shoot’ the committer

This does the write on the atomic in ghost code, and can only be called once.

requires

!self.shot()

requires

self.ward() == *own.ward()

ensures

(^self).shot()

ensures

(^own).ward() == (*own).ward()

ensures

*(*own).val() == (*self).old_value()

ensures

*(^own).val() == (*self).new_value()

terminates

ghost