Struct PAtomicI64 

pub struct PAtomicI64 { /* private fields */ }

Implementations

impl PAtomicI64

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

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 fn from_ptr_load(ptr: *mut i64, perm: Tracked<&PointsTo<i64>>) -> i64

Create a copy of the value via atomic load.

pub fn from_ptr_swap( ptr: *mut i64, verus_tmp_perm: Tracked<&mut PointsTo<i64>>, v: i64, ) -> i64

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 const fn new(i: i64) -> (PAtomicI64, Tracked<PermissionI64>)

pub fn load(&self, verus_tmp_perm: Tracked<&PermissionI64>) -> i64

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

pub fn compare_exchange( &self, verus_tmp_perm: Tracked<&mut PermissionI64>, current: i64, new: i64, ) -> Result<i64, i64>

pub fn compare_exchange_weak( &self, verus_tmp_perm: Tracked<&mut PermissionI64>, current: i64, new: i64, ) -> Result<i64, i64>

pub fn swap(&self, verus_tmp_perm: Tracked<&mut PermissionI64>, v: i64) -> i64

pub fn into_inner(self, verus_tmp_perm: Tracked<PermissionI64>) -> i64

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

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

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

pub fn fetch_sub( &self, verus_tmp_perm: Tracked<&mut PermissionI64>, n: i64, ) -> i64

pub fn fetch_and( &self, verus_tmp_perm: Tracked<&mut PermissionI64>, n: i64, ) -> i64

pub fn fetch_or( &self, verus_tmp_perm: Tracked<&mut PermissionI64>, n: i64, ) -> i64

pub fn fetch_xor( &self, verus_tmp_perm: Tracked<&mut PermissionI64>, n: i64, ) -> i64

pub fn fetch_nand( &self, verus_tmp_perm: Tracked<&mut PermissionI64>, n: i64, ) -> i64

pub fn fetch_max( &self, verus_tmp_perm: Tracked<&mut PermissionI64>, n: i64, ) -> i64

pub fn fetch_min( &self, verus_tmp_perm: Tracked<&mut PermissionI64>, n: i64, ) -> i64