Struct PAtomicI64 

pub struct PAtomicI64 { /* private fields */ }

Implementations

impl PAtomicI64

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

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 i64, perm: Tracked<&PointsTo<i64>>) -> ret : i64

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 i64, Tracked(perm): Tracked<&mut PointsTo<i64>>, v: i64, ) -> ret : i64

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 PAtomicI64

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

pub const exec fn new(i: i64) -> res : (PAtomicI64, Tracked<PermissionI64>)

ensures

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

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

requires

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

ensures

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

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

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 PermissionI64>, current: i64, new: i64, ) -> ret : Result<i64, i64>

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 PermissionI64>, current: i64, new: i64, ) -> ret : Result<i64, i64>

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 PermissionI64>, v: i64) -> ret : i64

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<PermissionI64>) -> ret : i64

requires

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

ensures

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

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

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 == i64_specs::wrapping_add(old(perm).view().value, n),

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

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 == i64_specs::wrapping_sub(old(perm).view().value, n),

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

requires

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

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

old(perm).view().value + n <= (<i64>::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 PermissionI64>, n: i64, ) -> ret : i64

requires

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

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

old(perm).view().value - n <= <i64>::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 PermissionI64>, n: i64, ) -> ret : i64

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 PermissionI64>, n: i64, ) -> ret : i64

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 PermissionI64>, n: i64, ) -> ret : i64

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 PermissionI64>, n: i64, ) -> ret : i64

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 PermissionI64>, n: i64, ) -> ret : i64

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 PermissionI64>, n: i64, ) -> ret : i64

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