Struct AtomicU16 

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

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

Implementations

impl AtomicU16

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

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<AtomicU16>>) -> (u16, Ghost<SyncView>)

Wrapper for std::sync::atomic::AtomicU16::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<AtomicU16>>, 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: u16, new: u16, f: Ghost<F>, ) -> Result<u16, u16>

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

Wrapper for std::sync::atomic::AtomicU16::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: u16, new: u16, f: Ghost<F>, ) -> Result<u16, u16>

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

Wrapper for std::sync::atomic::AtomicU16::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>) -> u16

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

Wrapper for std::sync::atomic::AtomicU16::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: u16, f: Ghost<F>)

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

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

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

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

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

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 AtomicU16

type Value = FMap<Int, (u16, 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.