Expand description
Proof model for CPU-local state.
A CPU-local object is modeled as one logical value for every CPU in its
configured domain.
CpuLocalAuth owns the authoritative map, while
CpuLocalPointsTo is the exclusive points-to resource for one CPU’s
entry. Distinct CPUs therefore have independently owned resources and may
operate on them concurrently.
This module only defines the resource algebra used by CPU-local clients. It does not yet connect the resources to executable CPU-local storage, preemption guards, or scheduler transitions. Those layers should keep the authority in an invariant and transfer each points-to resource into the corresponding CPU core’s proof state.
Structs§
- CpuLocal
Auth - Authoritative logical contents of one CPU-local object.
- CpuLocal
Points To - Exclusive ownership of one CPU’s entry in a CPU-local object.
- CpuLocal
Points ToSet - CPU-local points-to resources that have not yet been distributed.