Struct CpuCoreOwner 

pub struct CpuCoreOwner<L: CpuCoreLocalState> { /* private fields */ }

Scheduler-owned proof state for one CPU’s local resources.

L is deliberately generic instead of type-erased. A subsystem can define a tracked aggregate containing all CPU-local resources it needs and use that aggregate as the owner’s payload.

Implementations

impl<L: CpuCoreLocalState> CpuCoreOwner<L>

pub proof fn new(cpu: CpuId, tracked locals: L) -> tracked res : Self

requires

locals.belongs_to_cpu(cpu),

ensures

res.cpu() == cpu,

res.is_idle(),

res.wf(),

res.locals() == locals,

Creates an idle core with its permanent CPU-local resource aggregate.

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

Unique identity of this core resource.

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

Stable CPU represented by this core.

pub closed spec fn current_task(&self) -> Option<Loc>

Task currently running on this CPU.

pub open spec fn is_idle(&self) -> bool

{ self.current_task() is None }

Whether no task is currently associated with this core.

pub closed spec fn locals(&self) -> L

CPU-local resource aggregate permanently assigned to this core.

pub closed spec fn locals_key(&self) -> Seq<Loc>

Ordered identities of the CPU-local resources assigned to this core.

pub closed spec fn wf(&self) -> bool

The core identity is valid and every local resource belongs to its CPU.

pub proof fn tracked_schedule_in(tracked &mut self, task: Loc)

requires

old(self).wf(),

old(self).is_idle(),

ensures

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

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

final(self).current_task() == Some(task),

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

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

final(self).wf(),

Associates a task with an idle CPU core.

pub proof fn tracked_schedule_out(tracked &mut self) -> task : Loc

requires

old(self).wf(),

!old(self).is_idle(),

ensures

old(self).current_task() == Some(task),

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

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

final(self).is_idle(),

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

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

final(self).wf(),

Makes this CPU idle and returns the task that was running on it.

pub proof fn tracked_open(tracked self) -> tracked res : (CpuCoreOwnerHandle<L>, L)

requires

self.wf(),

ensures

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

res.0@ == self@,

res.0.wf(),

res.0.expected_locals_key() == self.locals_key(),

res.1 == self.locals(),

res.1.belongs_to_cpu(res.0.cpu()),

res.1.local_key() == res.0.expected_locals_key(),

Temporarily separates the typed CPU-local state from the core handle.

The caller may update the returned resources, but must eventually call CpuCoreOwnerHandle::tracked_restore with resources that still belong to this CPU.

Trait Implementations

impl<L: CpuCoreLocalState> View for CpuCoreOwner<L>

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

type V = CpuCoreOwnerView