Struct AtomicPtr 

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

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

Implementations

impl<T> AtomicPtr<T>

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

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>) -> *mut T

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

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

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

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

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

logic(open, inline)

self != other

type Value = FMap<Int, (*mut T, SyncView)>

impl<T> HasTimestamp for AtomicPtr<T>

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