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 used for the atomic operation. For a load operation, this is the timestamp of the value read. For a store operation, this is the predecessor of the timestamp of the value written.

The use of the predecessor for store operations allows us to use the same logical function for the timestamp for both the load and the store in a read-modify-write operation. Indeed, in the case of a read-modify-write operation, the timestamp of the store is the successor of the timestamp of the load.

logic(opaque)

pub fn val_load_logic(self) -> T

Value read from the atomic operation.

logic(opaque)

pub fn val_load(&self) -> T

Value read from the atomic operation.

ghost

ensures

#[logic_alias(self.val_load_logic())]

pub fn val_store_logic(self) -> T

Value written by the atomic operation.

logic(opaque)

pub fn val_store(&self) -> T

Value written by the atomic operation.

ghost

ensures

#[logic_alias(self.val_store_logic())]

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 = FMap<Timestamp, (T, SyncView)>> + HasTimestamp,

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().lookup(self.timestamp()) == Some((self.val_load(), result@))

ghost

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

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

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().lookup(self.timestamp()) {
    Some((v, v_view)) => v == self.val_load() && v_view <= ^sync_view,
    None => false
}

ghost

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

where C: PermTarget, C::Value: Sized,

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()

ghost

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

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

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().lookup(self.timestamp() + 1) == None

ensures

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

ghost

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

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

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().lookup(self.timestamp() + 1) == None

ensures

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

ghost

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

where C: PermTarget, C::Value: Sized,

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()

ghost