Struct PAtomicU16 

pub struct PAtomicU16 { /* private fields */ }

Implementations

impl PAtomicU16

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

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

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

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 PAtomicU16

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

pub const exec fn new(i: u16) -> res : (PAtomicU16, Tracked<PermissionU16>)

ensures

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

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

requires

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

ensures

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

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

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 PermissionU16>, current: u16, new: u16, ) -> ret : Result<u16, u16>

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 PermissionU16>, current: u16, new: u16, ) -> ret : Result<u16, u16>

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 PermissionU16>, v: u16) -> ret : u16

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<PermissionU16>) -> ret : u16

requires

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

ensures

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

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

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

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

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

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

requires

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

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

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

requires

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

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

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

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 PermissionU16>, n: u16, ) -> ret : u16

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 PermissionU16>, n: u16, ) -> ret : u16

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 PermissionU16>, n: u16, ) -> ret : u16

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 PermissionU16>, n: u16, ) -> ret : u16

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 PermissionU16>, n: u16, ) -> ret : u16

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