Skip to main content

RcuReadLeaseRegistry

vstd_extra::rcu_read_lease

Struct RcuReadLeaseRegistry 

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

Authoritative allocation-indexed registry for physical read permissions.

Each allocation keeps an owner-side RcuLeaseAccumulator. The registry also records every issued lease and removes its record only when the matching RcuRegisteredReadLease is returned. Its invariant says that the accumulator fraction plus all active reader fractions for an allocation is exactly one. Therefore proving that the allocation has no active record is sufficient to recover its stored resource.

Implementations§

Source§

impl<K, T, W> RcuReadLeaseRegistry<K, T, W>

Source

pub proof fn empty() -> tracked res : Self

ensures
res.wf(),
res.keys() == Set::<K>::empty(),
res.active_ids() == Set::<nat>::empty(),
res.next_lease() == 0,

Creates an empty tracked registry.

Source

pub closed spec fn keys(self) -> Set<K>

Source

pub closed spec fn contains(self, key: K) -> bool

Source

pub proof fn lemma_contains_iff_key(tracked &self, key: K)

ensures
self.contains(key) <==> self.keys().contains(key),

Relates keyed lookup to membership in the registry’s key set.

Source

pub proof fn lemma_all_contains_iff_keys(tracked &self)

ensures
forall |key: K| #[trigger] self.contains(key) <==> self.keys().contains(key),

Relates registry membership to the complete key set for all keys.

Source

pub closed spec fn accumulator(self, key: K) -> RcuLeaseAccumulator<T>

recommends
self.contains(key),
Source

pub closed spec fn active_ids(self) -> Set<nat>

Source

pub closed spec fn active_records(self) -> Map<nat, RcuActiveReadLeaseRecord<K, W>>

Ghost snapshot used to state the per-allocation accounting invariant.

Source

pub closed spec fn next_lease(self) -> nat

Source

pub closed spec fn active_record(self, lease_id: nat) -> RcuActiveReadLeaseRecord<K, W>

recommends
self.active_ids().contains(lease_id),
Source

pub proof fn tracked_borrow_active_witness(tracked &self, lease_id: nat) -> tracked witness : &W

requires
self.active_ids().contains(lease_id),
ensures
*witness == self.active_record(lease_id).witness(),

Borrows the client witness associated with one active lease.

The witness remains owned by the registry until the matching lease is returned. Reclamation proofs use this borrow to show that an allegedly active lease is incompatible with a completed grace period.

Source

pub proof fn tracked_borrow_active_witness_mut(tracked &mut self, lease_id: nat) -> tracked witness : &mut W

requires
old(self).active_ids().contains(lease_id),
ensures
*witness == old(self).active_record(lease_id).witness(),
final(self).keys() == old(self).keys(),
final(self).active_ids() == old(self).active_ids(),
final(self).next_lease() == old(self).next_lease(),
final(self).active_record(lease_id).key() == old(self).active_record(lease_id).key(),
final(self).active_record(lease_id).accumulator_id()
    == old(self).active_record(lease_id).accumulator_id(),
final(self).active_record(lease_id).fraction()
    == old(self).active_record(lease_id).fraction(),
final(self).active_record(lease_id).witness() == *final(witness),
forall |other: nat| {
    other != lease_id && old(self).active_ids().contains(other)
        ==> final(self).active_record(other) == old(self).active_record(other)
},

Mutably borrows an active witness while preserving the registry.

Resource-algebra validation may require a mutable receiver even when its postcondition leaves the witness unchanged.

Source

pub open spec fn has_active(self, key: K) -> bool

{
    exists |lease_id: nat| {
        self.active_ids().contains(lease_id) && self.active_record(lease_id).key() == key
    }
}
Source

pub open spec fn wf(self) -> bool

{
    &&& forall |lease_id: nat| {
        #[trigger] self.active_ids().contains(lease_id)
            ==> {
                let record = self.active_record(lease_id);
                &&& lease_id < self.next_lease()
                &&& self.contains(record.key())
                &&& record.accumulator_id() == self.accumulator(record.key()).id()
                &&& record.fraction() > 0real

            }
    }
    &&& forall |key: K| {
        #[trigger] self.contains(key)
            ==> self.accumulator(key).fraction()
                + active_lease_fraction(self.active_records(), key, self.next_lease())
                == 1real
    }

}
Source

pub proof fn insert(tracked &mut self, key: K, tracked resource: T)

requires
old(self).wf(),
!old(self).contains(key),
ensures
final(self).wf(),
final(self).keys() == old(self).keys().insert(key),
final(self).active_ids() == old(self).active_ids(),
final(self).next_lease() == old(self).next_lease(),
forall |lease_id: nat| {
    old(self).active_ids().contains(lease_id)
        ==> final(self).active_record(lease_id) == old(self).active_record(lease_id)
},
final(self).contains(key),
final(self).accumulator(key).resource() == resource,
final(self).accumulator(key).fraction() == 1real,
forall |other: K| {
    old(self).contains(other)
        ==> final(self).accumulator(other) == old(self).accumulator(other)
},

Registers one allocation and stores its complete ownership resource.

Source

pub proof fn split_lease( tracked &mut self, key: K, tracked witness: W, ) -> tracked lease : RcuRegisteredReadLease<K, T>

requires
old(self).wf(),
old(self).contains(key),
ensures
final(self).wf(),
final(self).keys() == old(self).keys(),
forall |candidate: K| (
    #[trigger] final(self).contains(candidate) == old(self).contains(candidate)
),
final(self).next_lease() == old(self).next_lease() + 1,
lease.lease_id() == old(self).next_lease(),
lease.key() == key,
final(self).active_ids() == old(self).active_ids().insert(lease.lease_id()),
final(self).active_record(lease.lease_id()).key() == key,
final(self).active_record(lease.lease_id()).accumulator_id() == lease.accumulator_id(),
final(self).active_record(lease.lease_id()).fraction() == lease.fraction(),
final(self).active_record(lease.lease_id()).witness() == witness,
forall |lease_id: nat| {
    old(self).active_ids().contains(lease_id)
        ==> final(self).active_record(lease_id) == old(self).active_record(lease_id)
},
lease.accumulator_id() == old(self).accumulator(key).id(),
lease.resource() == old(self).accumulator(key).resource(),
lease.fraction() == old(self).accumulator(key).fraction() / 2real,
final(self).accumulator(key).id() == old(self).accumulator(key).id(),
final(self).accumulator(key).resource() == old(self).accumulator(key).resource(),
final(self).accumulator(key).fraction() == old(self).accumulator(key).fraction() / 2real,
forall |other: K| {
    other != key && old(self).contains(other)
        ==> final(self).accumulator(other) == old(self).accumulator(other)
},

Splits a lease and installs its client witness in the active registry.

Source

pub proof fn return_lease(tracked &mut self, tracked lease: RcuRegisteredReadLease<K, T>) -> tracked witness : W

requires
old(self).wf(),
old(self).active_ids().contains(lease.lease_id()),
old(self).active_record(lease.lease_id()).key() == lease.key(),
old(self).active_record(lease.lease_id()).accumulator_id() == lease.accumulator_id(),
old(self).active_record(lease.lease_id()).fraction() == lease.fraction(),
ensures
final(self).wf(),
final(self).keys() == old(self).keys(),
forall |candidate: K| (
    #[trigger] final(self).contains(candidate) == old(self).contains(candidate)
),
final(self).next_lease() == old(self).next_lease(),
final(self).active_ids() == old(self).active_ids().remove(lease.lease_id()),
witness == old(self).active_record(lease.lease_id()).witness(),
forall |lease_id: nat| {
    lease_id != lease.lease_id() && old(self).active_ids().contains(lease_id)
        ==> final(self).active_record(lease_id) == old(self).active_record(lease_id)
},
final(self).accumulator(lease.key()).id() == old(self).accumulator(lease.key()).id(),
final(self).accumulator(lease.key()).resource()
    == old(self).accumulator(lease.key()).resource(),
final(self).accumulator(lease.key()).fraction()
    == old(self).accumulator(lease.key()).fraction() + lease.fraction(),
forall |other: K| {
    other != lease.key() && old(self).contains(other)
        ==> final(self).accumulator(other) == old(self).accumulator(other)
},

Returns one lease and removes exactly its matching active record.

Source

pub proof fn reclaim(tracked &mut self, key: K) -> tracked resource : T

requires
old(self).wf(),
old(self).contains(key),
!old(self).has_active(key),
ensures
final(self).wf(),
final(self).keys() == old(self).keys().remove(key),
final(self).active_ids() == old(self).active_ids(),
final(self).active_records() == old(self).active_records(),
final(self).next_lease() == old(self).next_lease(),
forall |lease_id: nat| {
    old(self).active_ids().contains(lease_id)
        ==> final(self).active_record(lease_id) == old(self).active_record(lease_id)
},
!final(self).contains(key),
resource == old(self).accumulator(key).resource(),
forall |other: K| {
    other != key && old(self).contains(other)
        ==> final(self).accumulator(other) == old(self).accumulator(other)
},

Recovers one allocation after a client proof rules out all active leases.

Auto Trait Implementations§

§

impl<K, T, W> Freeze for RcuReadLeaseRegistry<K, T, W>

§

impl<K, T, W> RefUnwindSafe for RcuReadLeaseRegistry<K, T, W>
where K: RefUnwindSafe, W: RefUnwindSafe, T: RefUnwindSafe,

§

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

§

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

§

impl<K, T, W> Unpin for RcuReadLeaseRegistry<K, T, W>
where K: Unpin, W: Unpin, T: Unpin,

§

impl<K, T, W> UnsafeUnpin for RcuReadLeaseRegistry<K, T, W>

§

impl<K, T, W> UnwindSafe for RcuReadLeaseRegistry<K, T, W>
where K: UnwindSafe, W: 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
§

impl<T> Conv for T

§

fn conv<T>(self) -> T
where Self: Into<T>,

Converts self into T using Into<T>. Read more
§

impl<T> FmtForward for T

§

fn fmt_binary(self) -> FmtBinary<Self>
where Self: Binary,

Causes self to use its Binary implementation when Debug-formatted.
§

fn fmt_display(self) -> FmtDisplay<Self>
where Self: Display,

Causes self to use its Display implementation when Debug-formatted.
§

fn fmt_lower_exp(self) -> FmtLowerExp<Self>
where Self: LowerExp,

Causes self to use its LowerExp implementation when Debug-formatted.
§

fn fmt_lower_hex(self) -> FmtLowerHex<Self>
where Self: LowerHex,

Causes self to use its LowerHex implementation when Debug-formatted.
§

fn fmt_octal(self) -> FmtOctal<Self>
where Self: Octal,

Causes self to use its Octal implementation when Debug-formatted.
§

fn fmt_pointer(self) -> FmtPointer<Self>
where Self: Pointer,

Causes self to use its Pointer implementation when Debug-formatted.
§

fn fmt_upper_exp(self) -> FmtUpperExp<Self>
where Self: UpperExp,

Causes self to use its UpperExp implementation when Debug-formatted.
§

fn fmt_upper_hex(self) -> FmtUpperHex<Self>
where Self: UpperHex,

Causes self to use its UpperHex implementation when Debug-formatted.
§

fn fmt_list(self) -> FmtList<Self>
where &'a Self: for<'a> IntoIterator,

Formats each item in a sequence. 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

§

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

§

fn pipe<R>(self, func: impl FnOnce(Self) -> R) -> R
where Self: Sized,

Pipes by value. This is generally the method you want to use. Read more
§

fn pipe_ref<'a, R>(&'a self, func: impl FnOnce(&'a Self) -> R) -> R
where R: 'a,

Borrows self and passes that borrow into the pipe function. Read more
§

fn pipe_ref_mut<'a, R>(&'a mut self, func: impl FnOnce(&'a mut Self) -> R) -> R
where R: 'a,

Mutably borrows self and passes that borrow into the pipe function. Read more
§

fn pipe_borrow<'a, B, R>(&'a self, func: impl FnOnce(&'a B) -> R) -> R
where Self: Borrow<B>, B: 'a + ?Sized, R: 'a,

Borrows self, then passes self.borrow() into the pipe function. Read more
§

fn pipe_borrow_mut<'a, B, R>( &'a mut self, func: impl FnOnce(&'a mut B) -> R, ) -> R
where Self: BorrowMut<B>, B: 'a + ?Sized, R: 'a,

Mutably borrows self, then passes self.borrow_mut() into the pipe function. Read more
§

fn pipe_as_ref<'a, U, R>(&'a self, func: impl FnOnce(&'a U) -> R) -> R
where Self: AsRef<U>, U: 'a + ?Sized, R: 'a,

Borrows self, then passes self.as_ref() into the pipe function.
§

fn pipe_as_mut<'a, U, R>(&'a mut self, func: impl FnOnce(&'a mut U) -> R) -> R
where Self: AsMut<U>, U: 'a + ?Sized, R: 'a,

Mutably borrows self, then passes self.as_mut() into the pipe function.
§

fn pipe_deref<'a, T, R>(&'a self, func: impl FnOnce(&'a T) -> R) -> R
where Self: Deref<Target = T>, T: 'a + ?Sized, R: 'a,

Borrows self, then passes self.deref() into the pipe function.
§

fn pipe_deref_mut<'a, T, R>( &'a mut self, func: impl FnOnce(&'a mut T) -> R, ) -> R
where Self: DerefMut<Target = T> + Deref, T: 'a + ?Sized, R: 'a,

Mutably borrows self, then passes self.deref_mut() into the pipe function.
§

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

§

impl<T> Tap for T

§

fn tap(self, func: impl FnOnce(&Self)) -> Self

Immutable access to a value. Read more
§

fn tap_mut(self, func: impl FnOnce(&mut Self)) -> Self

Mutable access to a value. Read more
§

fn tap_borrow<B>(self, func: impl FnOnce(&B)) -> Self
where Self: Borrow<B>, B: ?Sized,

Immutable access to the Borrow<B> of a value. Read more
§

fn tap_borrow_mut<B>(self, func: impl FnOnce(&mut B)) -> Self
where Self: BorrowMut<B>, B: ?Sized,

Mutable access to the BorrowMut<B> of a value. Read more
§

fn tap_ref<R>(self, func: impl FnOnce(&R)) -> Self
where Self: AsRef<R>, R: ?Sized,

Immutable access to the AsRef<R> view of a value. Read more
§

fn tap_ref_mut<R>(self, func: impl FnOnce(&mut R)) -> Self
where Self: AsMut<R>, R: ?Sized,

Mutable access to the AsMut<R> view of a value. Read more
§

fn tap_deref<T>(self, func: impl FnOnce(&T)) -> Self
where Self: Deref<Target = T>, T: ?Sized,

Immutable access to the Deref::Target of a value. Read more
§

fn tap_deref_mut<T>(self, func: impl FnOnce(&mut T)) -> Self
where Self: DerefMut<Target = T> + Deref, T: ?Sized,

Mutable access to the Deref::Target of a value. Read more
§

fn tap_dbg(self, func: impl FnOnce(&Self)) -> Self

Calls .tap() only in debug builds, and is erased in release builds.
§

fn tap_mut_dbg(self, func: impl FnOnce(&mut Self)) -> Self

Calls .tap_mut() only in debug builds, and is erased in release builds.
§

fn tap_borrow_dbg<B>(self, func: impl FnOnce(&B)) -> Self
where Self: Borrow<B>, B: ?Sized,

Calls .tap_borrow() only in debug builds, and is erased in release builds.
§

fn tap_borrow_mut_dbg<B>(self, func: impl FnOnce(&mut B)) -> Self
where Self: BorrowMut<B>, B: ?Sized,

Calls .tap_borrow_mut() only in debug builds, and is erased in release builds.
§

fn tap_ref_dbg<R>(self, func: impl FnOnce(&R)) -> Self
where Self: AsRef<R>, R: ?Sized,

Calls .tap_ref() only in debug builds, and is erased in release builds.
§

fn tap_ref_mut_dbg<R>(self, func: impl FnOnce(&mut R)) -> Self
where Self: AsMut<R>, R: ?Sized,

Calls .tap_ref_mut() only in debug builds, and is erased in release builds.
§

fn tap_deref_dbg<T>(self, func: impl FnOnce(&T)) -> Self
where Self: Deref<Target = T>, T: ?Sized,

Calls .tap_deref() only in debug builds, and is erased in release builds.
§

fn tap_deref_mut_dbg<T>(self, func: impl FnOnce(&mut T)) -> Self
where Self: DerefMut<Target = T> + Deref, T: ?Sized,

Calls .tap_deref_mut() only in debug builds, and is erased in release builds.
§

impl<T> TryConv for T

§

fn try_conv<T>(self) -> Result<T, Self::Error>
where Self: TryInto<T>,

Attempts to convert self into T using TryInto<T>. Read more
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>