Struct RcuReadLeaseRegistry 

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

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

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

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.

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

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

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.

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.

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

recommends

self.contains(key),

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

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

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

pub closed spec fn next_lease(self) -> nat

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

recommends

self.active_ids().contains(lease_id),

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.

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.

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
    }
}

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
    }

}

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.

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.

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.

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.