Struct LoadCommitter 

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

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

Note: this committer has no observable effect on ghost ressources. Thus, it is optional to shoot it, and nothing prevent the user from shooting it several times.

Implementations

impl<T, C: Container<Value = FMap<Timestamp, (T, SyncView)>> + HasTimestamp> LoadCommitter<T, C>

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].

logic(opaque)

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

‘Shoot’ the committer

This does the read on the atomic in ghost code.

requires

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

ensures

(*view).le_log(^view)

ensures

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

ensures

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

ensures

match own.val().get(result) {
    Some((v, v_view)) => v == self.val() && v_view.le_log(^view),
    None => false
}

terminates

ghost