Struct AtomicU8 

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

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

Implementations

impl AtomicU8

pub fn new(val: u8) -> (Self, Ghost<Perm<AtomicU8>>)

ensures

result.1.val() == val

ensures

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

terminates

pub fn into_inner(self, own: Ghost<Perm<AtomicU8>>) -> u8

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

requires

self == *own.ward()

ensures

result == own.val()

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

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

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

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

Wrapper for std::sync::atomic::AtomicU8::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>) -> u8

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

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

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

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

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

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

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

type Value = u8

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.