Struct RcuLeaseAccumulator 

pub struct RcuLeaseAccumulator<T> { /* private fields */ }

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

Implementations

impl<T> RcuLeaseAccumulator<T>

pub proof fn new(tracked resource: T) -> tracked res : Self

ensures

res.resource() == resource,

res.fraction() == 1real,

Stores resource and creates a whole read accumulator.

pub closed spec fn id(self) -> Loc

Storage-protocol identity shared by this accumulator and all of its leases.

pub closed spec fn resource(self) -> T

The resource retained in storage while read leases exist.

pub closed spec fn fraction(self) -> real

Rational fraction currently accumulated by the owner.

pub proof fn split_lease(tracked &mut self) -> tracked lease : RcuReadLease<T>

ensures

final(self).id() == old(self).id(),

final(self).resource() == old(self).resource(),

lease.id() == old(self).id(),

lease.resource() == old(self).resource(),

final(self).fraction() == old(self).fraction() / 2real,

lease.fraction() == old(self).fraction() / 2real,

Splits a fresh lease without imposing a fixed reader capacity.

pub proof fn return_lease(tracked &mut self, tracked lease: RcuReadLease<T>)

requires

old(self).id() == lease.id(),

ensures

final(self).id() == old(self).id(),

final(self).resource() == old(self).resource(),

final(self).resource() == lease.resource(),

final(self).fraction() == old(self).fraction() + lease.fraction(),

Returns one lease to its originating accumulator.

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

requires

self.fraction() == 1real,

ensures

resource == self.resource(),

Recovers the stored resource after every lease has returned.

pub proof fn lemma_fraction_bounded(tracked &self)

ensures

0real < self.fraction() <= 1real,

Establishes the valid range of the accumulated rational fraction.