Struct AtomicBool 

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

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

Implementations

impl AtomicBool

pub fn new(val: bool) -> (Self, Ghost<Perm<AtomicBool>>)

ensures

result.1.val() == val

ensures

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

terminates

pub fn into_inner(self, own: Ghost<Perm<AtomicBool>>) -> bool

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

requires

self == *own.ward()

ensures

result == own.val()

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

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

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

The load and the store are always sequentially consistent.

requires

forall<c: &mut Committer<Self, $type, ordering::SeqCst, ordering::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, ordering::SeqCst, ordering::None>>
    !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, ordering::SeqCst, ordering::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, ordering::SeqCst, ordering::None>>
            !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: bool, new: bool, f: Ghost<F>, ) -> Result<bool, bool>

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

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

The load and the store are always sequentially consistent.

requires

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

ensures

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

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

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

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

The load is always sequentially consistent.

requires

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

ensures

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

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

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

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

The store is always sequentially consistent.

requires

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

Trait Implementations

impl PermTarget for AtomicBool

type Value<'a> = bool where Self: 'a

Value managed by the type.

type PermPayload = ()

Variance, objectiveness and sizeness 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.