Struct AtomicI64 

pub struct AtomicI64(/* private fields */);

Creusot wrapper around std::sync::atomic::AtomicI64.

Implementations

impl AtomicI64

pub fn new( val: i64, sync_view: Ghost<&mut SyncView>, ) -> (Self, Ghost<Perm<AtomicI64>>)

ensures

result.1.val() == FMap::singleton(result.0.get_timestamp(^sync_view), (val, ^sync_view))

ensures

**sync_view <= ^sync_view

ensures

*result.1.ward() == result.0

terminates

pub fn into_inner(self, own: Ghost<Perm<AtomicI64>>) -> (i64, Ghost<SyncView>)

Wrapper for std::sync::atomic::AtomicI64::into_inner.

requires

self == *own.ward()

ensures

match own.val().lookup(self.get_timestamp(*result.1)) { Some((v, _)) => result.0 == v, None => false }

ensures

forall<t> match own.val().lookup(t) {
    Some((_, view)) => t <= self.get_timestamp(*result.1) && view <= *result.1,
    None => true
}

terminates

pub fn refresh( &mut self, own: Ghost<&mut Perm<AtomicI64>>, sync_view: Ghost<&mut SyncView>, )

Clear the old unusable history, thanks to the full ownership of the atomic.

requires

*self == *own.ward()

ensures

**sync_view <= ^sync_view

ensures

match (*own).val().lookup(self.get_timestamp(^sync_view)) {
    Some((v, _)) => (^own).val() == FMap::singleton(self.get_timestamp(^sync_view), (v, **sync_view)),
    None => false
}

ensures

forall<t> match own.val().lookup(t) {
    Some((_, view)) => t <= self.get_timestamp(^sync_view) && view <= ^sync_view,
    None => true
}

ensures

*self == ^self

terminates

pub fn compare_exchange<F, Success: UpdateOrdering, Failure: LoadOrdering>( &self, current: i64, new: i64, f: Ghost<F>, ) -> Result<i64, i64>

where F: FnGhost + FnOnce(Result<&mut Committer<Self, i64, Success::Load, Success::Store>, &Committer<Self, i64, Failure, ()>>),

Wrapper for std::sync::atomic::AtomicI64::compare_exchange.

The load and the store are always sequentially consistent.

requires

forall<c: &mut Committer<Self, $type, _, _>>
    !c.shot_store() ==> c.ward() == *self ==>
    c.val_load().deep_model() == current.deep_model() ==>
    c.val_store() == new ==>
    f.precondition((Ok(c),)) && (f.postcondition_once((Ok(c),), ()) ==> (^c).shot_store())

requires

forall<c: &Committer<Self, $type, _, _>>
    !c.shot_store() ==> c.ward() == *self ==>
    // NOTE: This following line is not present for `weak`
    c.val_load().deep_model() != current.deep_model() ==>
    f.precondition((Err(c),))

ensures

(exists<c: &mut Committer<Self, $type, _, _>>
    !c.shot_store() && c.ward() == *self &&
    c.val_load().deep_model() == current.deep_model() &&
    c.val_store() == new &&
    result == Ok(c.val_load()) &&
    f.postcondition_once((Ok(c),), ())) ||
(exists<c: &Committer<Self, $type, _, _>>
    !c.shot_store() && c.ward() == *self &&
    // NOTE: This following line is not present for `weak`
    c.val_load().deep_model() != current.deep_model() &&
    result == Err(c.val_load()) &&
    f.postcondition_once((Err(c),), ())
)

pub fn compare_exchange_weak<F, Success: UpdateOrdering, Failure: LoadOrdering>( &self, current: i64, new: i64, f: Ghost<F>, ) -> Result<i64, i64>

where F: FnGhost + FnOnce(Result<&mut Committer<Self, i64, Success::Load, Success::Store>, &Committer<Self, i64, Failure, ()>>),

Wrapper for std::sync::atomic::AtomicI64::compare_exchange_weak.

The load and the store are always sequentially consistent.

requires

forall<c: &mut Committer<Self, $type, _, _>>
    !c.shot_store() ==> c.ward() == *self ==>
    c.val_load().deep_model() == current.deep_model() ==>
    c.val_store() == new ==>
    f.precondition((Ok(c),)) && (f.postcondition_once((Ok(c),), ()) ==> (^c).shot_store())

requires

forall<c: &Committer<Self, $type, _, _>>
    !c.shot_store() ==> c.ward() == *self ==>
    f.precondition((Err(c),))

ensures

(exists<c: &mut Committer<Self, $type, _, _>>
    !c.shot_store() && c.ward() == *self &&
    c.val_load().deep_model() == current.deep_model() &&
    c.val_store() == new &&
    result == Ok(c.val_load()) &&
    f.postcondition_once((Ok(c),), ())) ||
(exists<c: &Committer<Self, $type, _, _>>
    !c.shot_store() && c.ward() == *self &&
    result == Err(c.val_load()) &&
    f.postcondition_once((Err(c),), ())
)

pub fn load<F, Load: LoadOrdering>(&self, f: Ghost<F>) -> i64

where F: FnGhost + FnOnce(&Committer<Self, i64, Load, ()>),

Wrapper for std::sync::atomic::AtomicI64::load.

requires

forall<c: &Committer<Self, $type, Load, ()>>
    !c.shot_store() ==> c.ward() == *self ==> f.precondition((c,))

ensures

exists<c: &Committer<Self, $type, Load, ()>>
    !c.shot_store() && c.ward() == *self && c.val_load() == result && f.postcondition_once((c,), ())

pub fn store<F, Store: StoreOrdering>(&self, val: i64, f: Ghost<F>)

where F: FnGhost + FnOnce(&mut Committer<Self, i64, (), Store>),

Wrapper for std::sync::atomic::AtomicI64::store.

requires

forall<c: &mut Committer<Self, $type, (), Store>>
    !c.shot_store() ==> c.ward() == *self ==> c.val_store() == val ==>
    f.precondition((c,)) && (f.postcondition_once((c,), ()) ==> (^c).shot_store())

ensures

exists<c: &mut Committer<Self, $type, (), Store>>
    !c.shot_store() && c.ward() == *self && c.val_store() == val &&
    f.postcondition_once((c,), ())

impl AtomicI64

pub fn fetch_add<F, Ord: UpdateOrdering>(&self, val: i64, f: Ghost<F>) -> i64

where F: FnGhost + FnOnce(&mut Committer<Self, i64, Ord::Load, Ord::Store>),

Wrapper for std::sync::atomic::AtomicI64::fetch_add.

requires

forall<c: &mut Committer<Self, $int_type, Ord::Load, Ord::Store>>
    !c.shot_store() ==> c.ward() == *self ==> c.val_store() == val + c.val_load() ==>
    f.precondition((c,)) && (f.postcondition_once((c,), ()) ==> (^c).shot_store())

ensures

exists<c: &mut Committer<Self, $int_type, Ord::Load, Ord::Store>>
    !c.shot_store() && c.ward() == *self && c.val_store() == val + c.val_load() &&
    c.val_load() == result && f.postcondition_once((c,), ())

Trait Implementations

impl HasTimestamp for AtomicI64

fn get_timestamp(self, _: SyncView) -> Timestamp

logic(opaque)

fn get_timestamp_monotonic(self, x: SyncView, y: SyncView)

logic(law)

requires

x <= y

ensures

self.get_timestamp(x) <= self.get_timestamp(y)

impl PermTarget for AtomicI64

type Value = FMap<Int, (i64, SyncView)>

Value managed by the type.

type Objectiveness = ()

Objectiveness parametrization for the Perm.

fn is_disjoint( &self, _self_val: &Self::Value, other: &Self, _other_val: &Self::Value, ) -> bool

Logical function that describes the behavior of Perm::disjoint_lemma.