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.

Dyn Compatibility

This trait is dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

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>