Struct AtomicU64 

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

Creusot wrapper around [std::sync::atomic::$atomic_type] Creusot wrapper around std::sync::atomic::AtomicU64.

Implementations

impl AtomicU64

pub fn new(val: u64) -> (Self, Ghost<Perm<AtomicU64>>)

ensures

result.1.val() == val

ensures

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

terminates

pub fn into_inner(self, own: Ghost<Perm<AtomicU64>>) -> u64

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

requires

self == *own.ward()

ensures

result == own.val()

pub fn compare_exchange<F>( &self, current: u64, new: u64, f: Ghost<F>, ) -> Result<u64, u64>

where F: FnGhost + FnOnce(Result<&mut Committer<Self, u64, SeqCst, SeqCst>, &Committer<Self, u64, SeqCst, ()>>),

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

The load and the store are always sequentially consistent.

requires

forall<c: &mut Committer<Self, $type, SeqCst, SeqCst>>
    !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, SeqCst, ()>>
    !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, SeqCst, SeqCst>>
            !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, SeqCst, ()>>
            !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>( &self, current: u64, new: u64, f: Ghost<F>, ) -> Result<u64, u64>

where F: FnGhost + FnOnce(Result<&mut Committer<Self, u64, SeqCst, SeqCst>, &Committer<Self, u64, SeqCst, ()>>),

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

The load and the store are always sequentially consistent.

requires

forall<c: &mut Committer<Self, $type, SeqCst, SeqCst>>
    !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, SeqCst, ()>>
    !c.shot_store() ==> c.ward() == *self ==>
    f.precondition((Err(c),))

ensures

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

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

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

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

The load is always sequentially consistent.

requires

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

ensures

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

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

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

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

The store is always sequentially consistent.

requires

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

impl AtomicU64

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

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

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

The load and the store are always sequentially consistent.

requires

forall<c: &mut Committer<Self, $int_type, SeqCst, SeqCst>>
    !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, SeqCst, SeqCst>>
    !c.shot_store() && c.ward() == *self && c.val_store() == val + c.val_load() &&
    c.val_load() == result && f.postcondition_once((c,), ())

Trait Implementations

impl PermTarget for AtomicU64

type Value = u64

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.