Struct StoreCommitter 

pub struct StoreCommitter<T, C: Container<Value = FMap<Timestamp, (T, SyncView)>>>(/* private fields */);

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

Implementations

impl<T, C: Container<Value = FMap<Timestamp, (T, SyncView)>> + HasTimestamp> StoreCommitter<T, 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 val(self) -> T

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

logic(opaque)

pub fn shoot(&mut self, own: &mut Perm<C>, view: &mut SyncView) -> Timestamp

‘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

(*self).ward() == (^self).ward() && (*self).val() == (^self).val()

ensures

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

ensures

(*view).le_log(^view)

ensures

(*self).ward().get_timestamp(*view) < result

ensures

result <= (*self).ward().get_timestamp(^view)

ensures

(*own).val().get(result) == None

ensures

*(^own).val() == (*own).val().insert(result, ((*self).val(), (*view)))

terminates

ghost