Struct PAtomicU8 

pub struct PAtomicU8 { /* private fields */ }

Implementations

impl PAtomicU8

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

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

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

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 PAtomicU8

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

pub const exec fn new(i: u8) -> res : (PAtomicU8, Tracked<PermissionU8>)

ensures

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

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

requires

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

ensures

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

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

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 PermissionU8>, current: u8, new: u8, ) -> ret : Result<u8, u8>

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 PermissionU8>, current: u8, new: u8, ) -> ret : Result<u8, u8>

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 PermissionU8>, v: u8) -> ret : u8

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<PermissionU8>) -> ret : u8

requires

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

ensures

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

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

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

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

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

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

requires

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

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

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

requires

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

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

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

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 PermissionU8>, n: u8) -> ret : u8

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 PermissionU8>, n: u8) -> ret : u8

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 PermissionU8>, n: u8, ) -> ret : u8

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 PermissionU8>, n: u8) -> ret : u8

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 PermissionU8>, n: u8) -> ret : u8

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