Struct AtomicU64 

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

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

Implementations

impl AtomicU64

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

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

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

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

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

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

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

logic(open, inline)

self != other

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

impl HasTimestamp for AtomicU64

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