Struct CpuLocalPointsToSet 

pub struct CpuLocalPointsToSet<V> { /* private fields */ }

CPU-local points-to resources that have not yet been distributed.

A newly allocated model returns all resources in this collection. CPU setup can split them into individual CpuLocalPointsTo resources and install each resource in the corresponding CPU core’s proof state.

Implementations

impl<V> CpuLocalPointsToSet<V>

pub closed spec fn id(&self) -> Loc

Identity of the corresponding CpuLocalAuth.

pub open spec fn cpus(&self) -> Set<CpuId>

{ self@.dom() }

CPUs whose exclusive points-to resources are still held here.

pub open spec fn contains(&self, cpu: CpuId) -> bool

{ self.cpus().contains(cpu) }

Whether this collection currently owns cpu’s points-to resource.

pub proof fn tracked_take(tracked &mut self, cpu: CpuId) -> tracked res : CpuLocalPointsTo<V>

requires

old(self).contains(cpu),

ensures

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

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

res.cpu() == cpu,

res.value() == old(self)@[cpu],

final(self)@ == old(self)@.remove(cpu),

final(self).cpus() == old(self).cpus().remove(cpu),

Splits out exclusive ownership of one CPU’s entry.

pub proof fn tracked_return(tracked &mut self, tracked points_to: CpuLocalPointsTo<V>)

requires

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

!old(self).contains(points_to.cpu()),

ensures

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

final(self)@ == old(self)@.insert(points_to.cpu(), points_to.value()),

final(self).cpus() == old(self).cpus().insert(points_to.cpu()),

Returns an individual points-to resource to this collection.

Trait Implementations

impl<V> View for CpuLocalPointsToSet<V>

closed spec fn view(&self) -> Self::V

type V = Map<CpuId, V>