Skip to main content

RcuRegisteredReadLease

vstd_extra::rcu_read_lease

Struct RcuRegisteredReadLease 

Source 
pub struct RcuRegisteredReadLease<K, T> { /* private fields */ }
Expand description

Reader-held lease registered under an allocation key and a unique lease ID.

The private lease_id names the matching RcuActiveReadLeaseRecord in the authoritative RcuReadLeaseRegistry. Returning this lease must consume that exact record, so it cannot be returned to another allocation that happens to store an equal resource.

Implementations§

Source§

impl<K, T> RcuRegisteredReadLease<K, T>

Source

pub closed spec fn lease_id(self) -> nat

Source

pub closed spec fn key(self) -> K

Source

pub closed spec fn accumulator_id(self) -> Loc

Source

pub closed spec fn resource(self) -> T

Source

pub closed spec fn fraction(self) -> real

Source

pub proof fn tracked_borrow(tracked &self) -> tracked resource : &T

ensures
*resource == self.resource(),

Borrows the protected resource while this registered lease remains live.

Auto Trait Implementations§

§

impl<K, T> Freeze for RcuRegisteredReadLease<K, T>
where K: Freeze,

§

impl<K, T> RefUnwindSafe for RcuRegisteredReadLease<K, T>
where K: RefUnwindSafe, T: RefUnwindSafe,

§

impl<K, T> Send for RcuRegisteredReadLease<K, T>
where K: Send, T: Send + Sync,

§

impl<K, T> Sync for RcuRegisteredReadLease<K, T>
where K: Sync, T: Sync + Send,

§

impl<K, T> Unpin for RcuRegisteredReadLease<K, T>
where K: Unpin, T: Unpin,

§

impl<K, T> UnsafeUnpin for RcuRegisteredReadLease<K, T>
where K: UnsafeUnpin,

§

impl<K, T> UnwindSafe for RcuRegisteredReadLease<K, T>
where K: UnwindSafe, T: UnwindSafe,

Blanket Implementations§

Source§

impl<T> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<T> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

§

impl<T, VERUS_SPEC__A> FromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: From<T>,

§

fn obeys_from_spec() -> bool

§

fn from_spec(v: T) -> VERUS_SPEC__A

Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

§

impl<T, VERUS_SPEC__A> IntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: Into<T>,

§

fn obeys_into_spec() -> bool

§

fn into_spec(self) -> T

§

impl<T, U> IntoSpecImpl<U> for T
where U: From<T>,

§

fn obeys_into_spec() -> bool

§

fn into_spec(self) -> U

Source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
§

impl<T, VERUS_SPEC__A> TryFromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryFrom<T>,

§

fn obeys_try_from_spec() -> bool

§

fn try_from_spec( v: T, ) -> Result<VERUS_SPEC__A, <VERUS_SPEC__A as TryFrom<T>>::Error>

Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.
§

impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryInto<T>,

§

fn obeys_try_into_spec() -> bool

§

fn try_into_spec(self) -> Result<T, <VERUS_SPEC__A as TryInto<T>>::Error>

§

impl<T, U> TryIntoSpecImpl<U> for T
where U: TryFrom<T>,

§

fn obeys_try_into_spec() -> bool

§

fn try_into_spec(self) -> Result<U, <U as TryFrom<T>>::Error>

§

impl<A> SpecEq<&A> for A
where A: ?Sized,

§

impl<A> SpecEq<&mut A> for A
where A: ?Sized,

§

impl<A> SpecEq<A> for A
where A: ?Sized,

§

impl<A> SpecEq<Ghost<A>> for A

§

impl<A> SpecEq<Tracked<A>> for A