Struct CpuLocalPointsTo 

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

Exclusive ownership of one CPU’s entry in a CPU-local object.

Two live points-to resources associated with the same CpuLocalAuth necessarily refer to different CPUs. Holding this token does not by itself establish that the holder is currently executing on that CPU; the scheduler glue must additionally bind cpu() to its current-CPU token.

Implementations

impl<V> CpuLocalPointsTo<V>

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

Identity of the corresponding CpuLocalAuth.

pub closed spec fn cpu(&self) -> CpuId

CPU whose entry is owned by this points-to resource.

pub closed spec fn value(&self) -> V

Current logical value of this CPU’s entry.

pub proof fn lemma_agree(tracked &self, tracked auth: &CpuLocalAuth<V>)

requires

self.id() == auth.id(),

ensures

auth.cpus().contains(self.cpu()),

auth.value(self.cpu()) == self.value(),

Establishes agreement with the authoritative CPU-local contents.

pub proof fn tracked_update(tracked &mut self, tracked auth: &mut CpuLocalAuth<V>, value: V)

requires

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

ensures

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

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

final(self).value() == value,

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

final(auth).cpus() == old(auth).cpus(),

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

Updates this CPU’s logical value.

Other CPUs’ points-to resources remain disjoint and retain their values.

pub proof fn lemma_distinct(tracked &mut self, tracked other: &CpuLocalPointsTo<V>)

requires

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

ensures

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

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

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

final(self).cpu() != other.cpu(),

Two points-to resources belonging to one authority refer to distinct CPUs.

pub proof fn lemma_same_cpu_has_distinct_auth(tracked &mut self, tracked other: &CpuLocalPointsTo<V>)

requires

old(self).cpu() == other.cpu(),

ensures

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

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

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

final(self).id() != other.id(),

Two live points-to resources for the same CPU cannot belong to the same CPU-local authority.

Trait Implementations

impl<V> CpuCoreLocalState for CpuLocalPointsTo<V>

open spec fn belongs_to_cpu(self, cpu: CpuId) -> bool

{ self.cpu() == cpu }

open spec fn local_key(self) -> Seq<Loc>

{ seq![self.id()] }