Struct AtomicI8 

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

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

Implementations

impl AtomicI8

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

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<AtomicI8>>) -> (i8, Ghost<SyncView>)

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

requires

self == *own.ward()

ensures

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

ensures

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

terminates

pub fn refresh( &mut self, own: Ghost<&mut Perm<AtomicI8>>, 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().get(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().get(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: i8, new: i8, f: Ghost<F>, ) -> Result<i8, i8>

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

Wrapper for std::sync::atomic::AtomicI8::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

match result {
    Ok(result) => {
        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 == c.val_load() &&
            f.postcondition_once((Ok(c),), ())
    },
    Err(result) => {
       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 == c.val_load() &&
            f.postcondition_once((Err(c),), ())
    }
}

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

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

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

The load and the store are always sequentially consistent.

requires

forall<c: &mut Committer<Self, $type, _, _>> // TODO: [VL] Wrong permission here (Success == Ordering::RelAcq)
    !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

match result {
    Ok(result) => {
        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 == c.val_load() &&
            f.postcondition_once((Ok(c),), ())
    },
    Err(result) => {
       exists<c: &Committer<Self, $type, _, _>>
            !c.shot_store() && c.ward() == *self &&
            result == c.val_load() &&
            f.postcondition_once((Err(c),), ())
    }
}

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

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

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

requires

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

ensures

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

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

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

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

requires

forall<c: &mut Committer<Self, $type, ordering::None, 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, ordering::None, Store>>
    !c.shot_store() && c.ward() == *self && c.val_store() == val &&
    f.postcondition_once((c,), ())

impl AtomicI8

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

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

Wrapper for std::sync::atomic::AtomicI8::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 AtomicI8

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 AtomicI8

type Value<'a> = FMap<Int, (i8, SyncView)> where Self: 'a

Value managed by the type.

type PermPayload = ()

Variance, objectiveness and sizeness 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.