Trait CpuCoreLocalState 

pub trait CpuCoreLocalState {
    // Required methods
    spec fn belongs_to_cpu(self, cpu: CpuId) -> bool;
    spec fn local_key(self) -> Seq<Loc>;
}

A typed collection of resources that belongs permanently to one CPU.

Implementations may aggregate any number of differently typed CPU-local points-to resources in a tracked struct. The predicate must state that all resources in the aggregate belong to cpu. local_key must faithfully and stably list their identities: changing, replacing, reordering, adding, or removing a resource must change the key.

Required Methods

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

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

Ordered identities of the resources comprising this local state.

The key must remain unchanged while the payload is detached from its core. Ordering makes two same-typed fields distinguishable.

Implementations on Foreign Types

impl CpuCoreLocalState for ()

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

{ true }

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

{ Seq::empty() }

impl<A: CpuCoreLocalState, B: CpuCoreLocalState> CpuCoreLocalState for (A, B)

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

{ self.0.belongs_to_cpu(cpu) && self.1.belongs_to_cpu(cpu) }

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

{ self.0.local_key() + self.1.local_key() }

Implementors

impl<V> CpuCoreLocalState for CpuLocalPointsTo<V>