Struct Committer 

pub struct Committer<C: PermTarget, T, Load, Store>(/* private fields */);

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

Note: For load-only accesses, 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<C: PermTarget, T, Load, Store> Committer<C, T, Load, Store>

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 timestamp(self) -> Timestamp

Timestamp of the latest load, before any store.

This is used for an update operation.

logic(opaque)

pub fn val_load(self) -> T

Value read from the atomic operation.

logic(opaque)

pub fn val_store(self) -> T

Value written by the atomic operation.

logic(opaque)

pub fn shot_store(self) -> bool

Status of the committer

logic(opaque)

pub fn hist_inv(self, other: Self) -> bool

logic(open, inline)

self.ward() == other.ward()
    && self.val_load() == other.val_load()
    && self.val_store() == other.val_store()
    && self.timestamp() == other.timestamp()

impl<C, T, Store> Committer<C, T, Relaxed, Store>

where C: PermTarget<Value<'static> = FMap<Timestamp, (T, SyncView)>> + HasTimestamp + 'static,

pub fn shoot_load( &self, own: &Perm<C>, sync_view: &mut SyncView, ) -> AcquireSyncView

‘Shoot’ the committer

This does the read on the atomic in ghost code.

requires

!self.shot_store()

requires

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

ensures

*sync_view <= ^sync_view

ensures

self.ward().get_timestamp(*sync_view) <= self.timestamp()

ensures

self.timestamp() <= self.ward().get_timestamp(^sync_view)

ensures

own.val().get(self.timestamp()) == Some((self.val_load(), result@))

terminates

ghost

impl<C, T, Store> Committer<C, T, Acquire, Store>

where C: PermTarget<Value<'static> = FMap<Timestamp, (T, SyncView)>> + HasTimestamp + 'static,

pub fn shoot_load(&self, own: &Perm<C>, sync_view: &mut SyncView)

‘Shoot’ the committer

This does the read on the atomic in ghost code.

requires

!self.shot_store()

requires

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

ensures

*sync_view <= ^sync_view

ensures

self.ward().get_timestamp(*sync_view) <= self.timestamp()

ensures

self.timestamp() <= self.ward().get_timestamp(^sync_view)

ensures

match own.val().get(self.timestamp()) {
    Some((v, v_view)) => v == self.val_load() && v_view <= ^sync_view,
    None => false
}

terminates

ghost

impl<C, Store> Committer<C, C::Value<'static>, SeqCst, Store>

where C: PermTarget,

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

‘Shoot’ the committer

This does the read on the atomic in ghost code.

requires

!self.shot_store()

requires

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

ensures

self.val_load() == own.val()

terminates

ghost

impl<C, T, Load> Committer<C, T, Load, Relaxed>

where C: PermTarget<Value<'static> = FMap<Timestamp, (T, SyncView)>> + HasTimestamp + 'static,

pub fn shoot_store( &mut self, own: &mut Perm<C>, sync_view: &mut SyncView, rel_view: ReleaseSyncView, )

‘Shoot’ the committer (Relaxed)

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

requires

!(*self).shot_store()

requires

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

ensures

(*self).hist_inv(^self)

ensures

(^self).shot_store()

ensures

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

ensures

*sync_view <= ^sync_view

ensures

(*self).ward().get_timestamp(*sync_view) <= self.timestamp()

ensures

self.timestamp() < (*self).ward().get_timestamp(^sync_view)

ensures

(*own).val().get(self.timestamp() + 1) == None

ensures

(^own).val() == (*own).val().insert(self.timestamp() + 1, ((*self).val_store(), rel_view@))

terminates

ghost

impl<C, T, Load> Committer<C, T, Load, Release>

where C: PermTarget<Value<'static> = FMap<Timestamp, (T, SyncView)>> + HasTimestamp + 'static,

pub fn shoot_store(&mut self, own: &mut Perm<C>, sync_view: &mut SyncView)

‘Shoot’ the committer

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

requires

!(*self).shot_store()

requires

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

ensures

(*self).hist_inv(^self)

ensures

(^self).shot_store()

ensures

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

ensures

*sync_view <= ^sync_view

ensures

(*self).ward().get_timestamp(*sync_view) <= self.timestamp()

ensures

self.timestamp() < (*self).ward().get_timestamp(^sync_view)

ensures

(*own).val().get(self.timestamp() + 1) == None

ensures

(^own).val() == (*own).val().insert(self.timestamp() + 1, ((*self).val_store(), ^sync_view))

terminates

ghost

impl<C, Load> Committer<C, C::Value<'static>, Load, SeqCst>

where C: PermTarget,

pub fn shoot_store(&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_store()

requires

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

ensures

(*self).hist_inv(^self)

ensures

(^self).shot_store()

ensures

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

ensures

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

terminates

ghost