Type Alias vstd::rwlock::FieldType_RwLock_cell

pub type FieldType_RwLock_cell<V> = PCell<V>;

Aliased Type

struct FieldType_RwLock_cell<V> { /* private fields */ }

Implementations

impl<V> PCell<V>

pub fn id(&self) -> CellId

// verusdoc_special_attr modes
// { "fn_mode": "uninterp", "ret_mode": "Default", "param_modes": ["Default"], "broadcast": false, "ret_name": "" }

A unique ID for the cell.

pub const fn empty() -> (PCell<V>, Tracked<PointsTo<V>>)

// verusdoc_special_attr modes
// { "fn_mode": "exec", "ret_mode": "Default", "param_modes": [], "broadcast": false, "ret_name": "pt" }

// verusdoc_special_attr ensures
pt.1@@ === pcell_points![pt.0.id() => MemContents::Uninit],

Return an empty (“uninitialized”) cell.

pub const fn new(v: V) -> (PCell<V>, Tracked<PointsTo<V>>)

// verusdoc_special_attr modes
// { "fn_mode": "exec", "ret_mode": "Default", "param_modes": ["Default"], "broadcast": false, "ret_name": "pt" }

// verusdoc_special_attr ensures
pt.1@@ === pcell_points![pt.0.id() => MemContents::Init(v)],

pub fn put(&self, verus_tmp_perm: Tracked<&mut PointsTo<V>>, v: V)

// verusdoc_special_attr modes
// { "fn_mode": "exec", "ret_mode": "Default", "param_modes": ["Default","Default","Default"], "broadcast": false, "ret_name": "" }

// verusdoc_special_attr requires
old(perm)@ === pcell_points![self.id() => MemContents::Uninit],

// verusdoc_special_attr ensures
perm@ === pcell_points![self.id() => MemContents::Init(v)],

pub fn take(&self, verus_tmp_perm: Tracked<&mut PointsTo<V>>) -> V

// verusdoc_special_attr modes
// { "fn_mode": "exec", "ret_mode": "Default", "param_modes": ["Default","Default"], "broadcast": false, "ret_name": "v" }

// verusdoc_special_attr requires
self.id() === old(perm)@.pcell,

// verusdoc_special_attr requires
old(perm).is_init(),

// verusdoc_special_attr ensures
perm.id() === old(perm)@.pcell,

// verusdoc_special_attr ensures
perm.mem_contents() === MemContents::Uninit,

// verusdoc_special_attr ensures
v === old(perm).value(),

pub fn replace(&self, verus_tmp_perm: Tracked<&mut PointsTo<V>>, in_v: V) -> V

// verusdoc_special_attr modes
// { "fn_mode": "exec", "ret_mode": "Default", "param_modes": ["Default","Default","Default"], "broadcast": false, "ret_name": "out_v" }

// verusdoc_special_attr requires
self.id() === old(perm)@.pcell,

// verusdoc_special_attr requires
old(perm).is_init(),

// verusdoc_special_attr ensures
perm.id() === old(perm)@.pcell,

// verusdoc_special_attr ensures
perm.mem_contents() === MemContents::Init(in_v),

// verusdoc_special_attr ensures
out_v === old(perm).value(),

pub fn borrow<'a>(&'a self, verus_tmp_perm: Tracked<&'a PointsTo<V>>) -> &'a V

// verusdoc_special_attr modes
// { "fn_mode": "exec", "ret_mode": "Default", "param_modes": ["Default","Default"], "broadcast": false, "ret_name": "v" }

// verusdoc_special_attr requires
self.id() === perm@.pcell,

// verusdoc_special_attr requires
perm.is_init(),

// verusdoc_special_attr ensures
*v === perm.value(),

pub fn into_inner(self, verus_tmp_perm: Tracked<PointsTo<V>>) -> V

// verusdoc_special_attr modes
// { "fn_mode": "exec", "ret_mode": "Default", "param_modes": ["Default","Default"], "broadcast": false, "ret_name": "v" }

// verusdoc_special_attr requires
self.id() === perm@.pcell,

// verusdoc_special_attr requires
perm.is_init(),

// verusdoc_special_attr ensures
v === perm.value(),

impl<V: Copy> PCell<V>

pub fn write(&self, verus_tmp_perm: Tracked<&mut PointsTo<V>>, in_v: V)

// verusdoc_special_attr modes
// { "fn_mode": "exec", "ret_mode": "Default", "param_modes": ["Default","Default","Default"], "broadcast": false, "ret_name": "" }

// verusdoc_special_attr requires
self.id() === old(perm)@.pcell,

// verusdoc_special_attr requires
old(perm).is_init(),

// verusdoc_special_attr ensures
perm.id() === old(perm)@.pcell,

// verusdoc_special_attr ensures
perm.mem_contents() === MemContents::Init(in_v),

Trait Implementations

impl<T> Send for PCell<T>

impl<T> Sync for PCell<T>

PCell is always safe to Send or Sync. Rather, it is the PointsTo object where Send and Sync matter. (It doesn’t matter if you move the bytes to another thread if you can’t access them.)