Struct Committer 

pub struct Committer;

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

Implementations

impl Committer

pub fn shot(self) -> bool

Status of the committer

(opaque)

pub fn ward(self) -> AtomicI32

Identity of the committer

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

(opaque)

pub fn old_value(self) -> i32

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

(opaque)

pub fn new_value(self) -> i32

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

(opaque)

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

‘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