Struct AtomicU16 

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

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

Implementations

impl AtomicU16

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

ensures

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

ensures

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

terminates

pub fn load<F>(&self, f: Ghost<F>) -> u16

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

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

requires

forall<c: &LoadCommitter<$type, Self>> c.ward() == *self ==> f.precondition((c,))

ensures

exists<c: &LoadCommitter<$type, Self>>
    c.ward() == *self && c.val() == result && f.postcondition_once((c,), ())

pub fn store<F>(&self, val: u16, f: Ghost<F>)

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

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

requires

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

ensures

exists<c: &mut StoreCommitter<$type, Self>>
    !c.shot() && c.ward() == *self && c.val() == val &&
    f.postcondition_once((c,), ())

Trait Implementations

impl Container for AtomicU16

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

logic(open, inline)

self != other

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

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.le_log(y)

ensures

self.get_timestamp(x).le_log(self.get_timestamp(y))