Struct AtomicPtr 

pub struct AtomicPtr<T>(/* private fields */);

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

Implementations

impl<T> AtomicPtr<T>

pub fn new(val: *mut T) -> (Self, Ghost<Perm<AtomicPtr<T>>>)

ensures

result.1.val() == val

ensures

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

terminates

pub fn into_inner(self, own: Ghost<Perm<AtomicPtr<T>>>) -> *mut T

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

requires

self == *own.ward()

ensures

result == own.val()

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

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

Wrapper for std::sync::atomic::AtomicPtr::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: *mut T, new: *mut T, f: Ghost<F>, ) -> Result<*mut T, *mut T>

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

Wrapper for std::sync::atomic::AtomicPtr::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>) -> *mut T

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

Wrapper for std::sync::atomic::AtomicPtr::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: *mut T, f: Ghost<F>)

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

Wrapper for std::sync::atomic::AtomicPtr::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<T> PermTarget for AtomicPtr<T>

type Value<'a> = *mut T 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.