Module rcu_read_lease 

Unbounded fractional read leases for delayed reclamation.

An owner-side accumulator stores one linear resource in Verus’ Leaf-style storage protocol. Each reader-held lease receives half of the accumulator’s current rational fraction, so the number of outstanding leases has no fixed integer bound. Reclamation can recover the resource only after all leases have been returned and the accumulator fraction is whole.

Structs

RcuActiveReadLeaseRecord

Registry-held accounting record paired with one outstanding reader lease.

RcuLeaseAccumulator

Owner-side fractional accumulator for one delayed-reclamation resource.

RcuReadLease

Reader-held fractional permission split from an RcuLeaseAccumulator.

RcuReadLeaseRegistry

Authoritative allocation-indexed registry for physical read permissions.

RcuRegisteredReadLease

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

Functions

active_lease_fraction

lease_accumulator_reclaims_after_returns