Struct PAtomicIsize 

pub struct PAtomicIsize { /* private fields */ }

Implementations

impl PAtomicIsize

pub exec fn from_ptr_store( ptr: *mut isize, value: isize, Tracked(perm): Tracked<&mut PointsTo<isize>>, )

requires

old(perm).ptr() == ptr,

ensures

value == final(perm).value(),

old(perm).ptr() == final(perm).ptr(),

final(perm).is_init(),

Store a value via a raw pointer using atomic store.

This is useful if a user wants to implement lockless algorithm for a struct where elements are linked through pointers. In that case, PointsTo<$value_ty> might be stored in AtomicInvariant.

The specification is similar to raw_ptr::ptr_mut_ref, but the implementation is atomic and so we can mark it as verifier::atomic, and so it can be used in open_atomic_invariant!.

pub exec fn from_ptr_load(ptr: *mut isize, perm: Tracked<&PointsTo<isize>>) -> ret : isize

requires

perm.ptr() == ptr,

perm.is_init(),

ensures

ret == perm.value(),

Create a copy of the value via atomic load.

pub exec fn from_ptr_swap( ptr: *mut isize, Tracked(perm): Tracked<&mut PointsTo<isize>>, v: isize, ) -> ret : isize

requires

ptr == old(perm).ptr(),

old(perm).is_init(),

ensures

final(perm).value() == v,

final(perm).is_init(),

old(perm).value() == ret,

ptr == final(perm).ptr(),

Swap the value via atomic swap.

The swap reads the old value, so the memory must already be initialized; it writes v, so it is initialized on return.

impl PAtomicIsize

pub uninterp spec fn id(&self) -> int

pub const exec fn new(i: isize) -> res : (PAtomicIsize, Tracked<PermissionIsize>)

ensures

equal(
    res.1@.view(),
    PermissionDataIsize {
        patomic: res.0.id(),
        value: i,
    },
),

pub exec fn load(&self, Tracked(perm): Tracked<&PermissionIsize>) -> ret : isize

requires

equal(self.id(), perm.view().patomic),

ensures

equal(perm.view().value, ret),

pub exec fn store(&self, Tracked(perm): Tracked<&mut PermissionIsize>, v: isize)

requires

equal(self.id(), old(perm).view().patomic),

ensures

equal(final(perm).view().value, v) && equal(self.id(), final(perm).view().patomic),

pub exec fn compare_exchange( &self, Tracked(perm): Tracked<&mut PermissionIsize>, current: isize, new: isize, ) -> ret : Result<isize, isize>

requires

equal(self.id(), old(perm).view().patomic),

ensures

equal(self.id(), final(perm).view().patomic)
    && match ret {
        Result::Ok(r) => {
            current == old(perm).view().value && equal(final(perm).view().value, new)
                && equal(r, old(perm).view().value)
        }
        Result::Err(r) => {
            current != old(perm).view().value
                && equal(final(perm).view().value, old(perm).view().value)
                && equal(r, old(perm).view().value)
        }
    },

pub exec fn compare_exchange_weak( &self, Tracked(perm): Tracked<&mut PermissionIsize>, current: isize, new: isize, ) -> ret : Result<isize, isize>

requires

equal(self.id(), old(perm).view().patomic),

ensures

equal(self.id(), final(perm).view().patomic)
    && match ret {
        Result::Ok(r) => {
            current == old(perm).view().value && equal(final(perm).view().value, new)
                && equal(r, old(perm).view().value)
        }
        Result::Err(r) => {
            equal(final(perm).view().value, old(perm).view().value)
                && equal(r, old(perm).view().value)
        }
    },

pub exec fn swap( &self, Tracked(perm): Tracked<&mut PermissionIsize>, v: isize, ) -> ret : isize

requires

equal(self.id(), old(perm).view().patomic),

ensures

equal(final(perm).view().value, v) && equal(old(perm).view().value, ret)
    && equal(self.id(), final(perm).view().patomic),

pub exec fn into_inner(self, Tracked(perm): Tracked<PermissionIsize>) -> ret : isize

requires

equal(self.id(), perm.view().patomic),

ensures

equal(perm.view().value, ret),

pub exec fn fetch_add_wrapping( &self, Tracked(perm): Tracked<&mut PermissionIsize>, n: isize, ) -> ret : isize

requires

equal(self.id(), old(perm).view().patomic),

ensures

equal(old(perm).view().value, ret),

final(perm).view().patomic == old(perm).view().patomic,

final(perm).view().value as int == isize_specs::wrapping_add(old(perm).view().value, n),

pub exec fn fetch_sub_wrapping( &self, Tracked(perm): Tracked<&mut PermissionIsize>, n: isize, ) -> ret : isize

requires

equal(self.id(), old(perm).view().patomic),

ensures

equal(old(perm).view().value, ret),

final(perm).view().patomic == old(perm).view().patomic,

final(perm).view().value as int == isize_specs::wrapping_sub(old(perm).view().value, n),

pub exec fn fetch_add( &self, Tracked(perm): Tracked<&mut PermissionIsize>, n: isize, ) -> ret : isize

requires

equal(self.id(), old(perm).view().patomic),

(<isize>::MIN as int) <= old(perm).view().value + n,

old(perm).view().value + n <= (<isize>::MAX as int),

ensures

equal(old(perm).view().value, ret),

final(perm).view().patomic == old(perm).view().patomic,

final(perm).view().value == old(perm).view().value + n,

pub exec fn fetch_sub( &self, Tracked(perm): Tracked<&mut PermissionIsize>, n: isize, ) -> ret : isize

requires

equal(self.id(), old(perm).view().patomic),

(<isize>::MIN as int) <= old(perm).view().value - n,

old(perm).view().value - n <= <isize>::MAX as int,

ensures

equal(old(perm).view().value, ret),

final(perm).view().patomic == old(perm).view().patomic,

final(perm).view().value == old(perm).view().value - n,

pub exec fn fetch_and( &self, Tracked(perm): Tracked<&mut PermissionIsize>, n: isize, ) -> ret : isize

requires

equal(self.id(), old(perm).view().patomic),

ensures

equal(old(perm).view().value, ret),

final(perm).view().patomic == old(perm).view().patomic,

final(perm).view().value == (old(perm).view().value & n),

pub exec fn fetch_or( &self, Tracked(perm): Tracked<&mut PermissionIsize>, n: isize, ) -> ret : isize

requires

equal(self.id(), old(perm).view().patomic),

ensures

equal(old(perm).view().value, ret),

final(perm).view().patomic == old(perm).view().patomic,

final(perm).view().value == (old(perm).view().value | n),

pub exec fn fetch_xor( &self, Tracked(perm): Tracked<&mut PermissionIsize>, n: isize, ) -> ret : isize

requires

equal(self.id(), old(perm).view().patomic),

ensures

equal(old(perm).view().value, ret),

final(perm).view().patomic == old(perm).view().patomic,

final(perm).view().value == (old(perm).view().value ^ n),

pub exec fn fetch_nand( &self, Tracked(perm): Tracked<&mut PermissionIsize>, n: isize, ) -> ret : isize

requires

equal(self.id(), old(perm).view().patomic),

ensures

equal(old(perm).view().value, ret),

final(perm).view().patomic == old(perm).view().patomic,

final(perm).view().value == !(old(perm).view().value & n),

pub exec fn fetch_max( &self, Tracked(perm): Tracked<&mut PermissionIsize>, n: isize, ) -> ret : isize

requires

equal(self.id(), old(perm).view().patomic),

ensures

equal(old(perm).view().value, ret),

final(perm).view().patomic == old(perm).view().patomic,

final(perm).view().value
    == (if old(perm).view().value > n { old(perm).view().value } else { n }),

pub exec fn fetch_min( &self, Tracked(perm): Tracked<&mut PermissionIsize>, n: isize, ) -> ret : isize

requires

equal(self.id(), old(perm).view().patomic),

ensures

equal(old(perm).view().value, ret),

final(perm).view().patomic == old(perm).view().patomic,

final(perm).view().value
    == (if old(perm).view().value < n { old(perm).view().value } else { n }),