ostd/specs/task/
cpu_core.rs

1// SPDX-License-Identifier: MPL-2.0
2//! Proof model for ownership of one CPU's local resources.
3//!
4//! A [`CpuCoreOwner`] permanently owns the CPU-local resources assigned to one
5//! logical CPU. Scheduling changes only the owner's `current_task`; it never
6//! transfers those resources to the task. Runtime CPU-local access temporarily
7//! opens the owner into a linear [`CpuCoreOwnerHandle`] and its typed local
8//! state, then restores that state before returning the owner to the scheduler.
9use vstd::{prelude::*, resource::Loc};
10use vstd_extra::resource::ghost_resource::excl::ExclusiveGhost;
11
12use crate::specs::task::cpu_local::CpuLocalAuth;
13
14use core::marker::PhantomData;
15
16use crate::cpu::CpuId;
17
18verus! {
19
20/// Logical scheduling state carried by a CPU-local resource owner.
21pub ghost struct CpuCoreOwnerView {
22    /// Stable logical CPU represented by this core.
23    pub cpu: CpuId,
24    /// Task currently executing on this core, or `None` while the core is idle.
25    pub current_task: Option<Loc>,
26    /// Ordered identities of the CPU-local resources assigned to this core.
27    pub locals_key: Seq<Loc>,
28}
29
30/// A typed collection of resources that belongs permanently to one CPU.
31///
32/// Implementations may aggregate any number of differently typed CPU-local
33/// points-to resources in a tracked struct. The predicate must state that all
34/// resources in the aggregate belong to `cpu`. `local_key` must faithfully and
35/// stably list their identities: changing, replacing, reordering, adding, or
36/// removing a resource must change the key.
37pub trait CpuCoreLocalState {
38    spec fn belongs_to_cpu(self, cpu: CpuId) -> bool;
39
40    /// Ordered identities of the resources comprising this local state.
41    ///
42    /// The key must remain unchanged while the payload is detached from its
43    /// core. Ordering makes two same-typed fields distinguishable.
44    spec fn local_key(self) -> Seq<Loc>;
45}
46
47impl CpuCoreLocalState for () {
48    open spec fn belongs_to_cpu(self, _cpu: CpuId) -> bool {
49        true
50    }
51
52    open spec fn local_key(self) -> Seq<Loc> {
53        Seq::empty()
54    }
55}
56
57impl<A: CpuCoreLocalState, B: CpuCoreLocalState> CpuCoreLocalState for (A, B) {
58    open spec fn belongs_to_cpu(self, cpu: CpuId) -> bool {
59        self.0.belongs_to_cpu(cpu) && self.1.belongs_to_cpu(cpu)
60    }
61
62    open spec fn local_key(self) -> Seq<Loc> {
63        self.0.local_key() + self.1.local_key()
64    }
65}
66
67/// Linear identity and scheduling state left while CPU-local resources are
68/// temporarily being accessed.
69///
70/// A handle cannot be duplicated. Restoring a [`CpuCoreOwner`] requires
71/// returning a local-state aggregate of the same type, with the same ordered
72/// resource identities, whose resources all belong to this handle's CPU.
73pub tracked struct CpuCoreOwnerHandle<L: CpuCoreLocalState> {
74    state: ExclusiveGhost<CpuCoreOwnerView>,
75    marker: PhantomData<L>,
76}
77
78/// Scheduler-owned proof state for one CPU's local resources.
79///
80/// `L` is deliberately generic instead of type-erased. A subsystem can define
81/// a tracked aggregate containing all CPU-local resources it needs and use that
82/// aggregate as the owner's payload.
83pub tracked struct CpuCoreOwner<L: CpuCoreLocalState> {
84    handle: CpuCoreOwnerHandle<L>,
85    locals: L,
86}
87
88impl<L: CpuCoreLocalState> View for CpuCoreOwnerHandle<L> {
89    type V = CpuCoreOwnerView;
90
91    closed spec fn view(&self) -> Self::V {
92        self.state.view()
93    }
94}
95
96impl<L: CpuCoreLocalState> View for CpuCoreOwner<L> {
97    type V = CpuCoreOwnerView;
98
99    closed spec fn view(&self) -> Self::V {
100        self.handle@
101    }
102}
103
104impl<L: CpuCoreLocalState> CpuCoreOwnerHandle<L> {
105    /// Unique identity of this core resource.
106    pub closed spec fn id(&self) -> Loc {
107        self.state.id()
108    }
109
110    /// Stable CPU represented by this handle.
111    pub closed spec fn cpu(&self) -> CpuId {
112        self@.cpu
113    }
114
115    /// Task currently running on this CPU.
116    pub closed spec fn current_task(&self) -> Option<Loc> {
117        self@.current_task
118    }
119
120    /// Whether no task is currently associated with this core.
121    pub open spec fn is_idle(&self) -> bool {
122        self.current_task() is None
123    }
124
125    /// Internal validity of the exclusive core state.
126    pub closed spec fn wf(&self) -> bool {
127        self.state.wf()
128    }
129
130    /// Ordered resource identities expected when restoring the core.
131    pub closed spec fn expected_locals_key(&self) -> Seq<Loc> {
132        self@.locals_key
133    }
134
135    /// Restores a complete core after a temporary CPU-local access.
136    pub proof fn tracked_restore(tracked self, tracked locals: L) -> (tracked res: CpuCoreOwner<L>)
137        requires
138            self.wf(),
139            locals.belongs_to_cpu(self.cpu()),
140            locals.local_key() == self.expected_locals_key(),
141        ensures
142            res.id() == self.id(),
143            res@ == self@,
144            res.wf(),
145            res.locals() == locals,
146            res.locals().local_key() == self.expected_locals_key(),
147    {
148        CpuCoreOwner { handle: self, locals }
149    }
150}
151
152impl<L: CpuCoreLocalState> CpuCoreOwner<L> {
153    /// Creates an idle core with its permanent CPU-local resource aggregate.
154    pub proof fn new(cpu: CpuId, tracked locals: L) -> (tracked res: Self)
155        requires
156            locals.belongs_to_cpu(cpu),
157        ensures
158            res.cpu() == cpu,
159            res.is_idle(),
160            res.wf(),
161            res.locals() == locals,
162    {
163        let ghost locals_key = locals.local_key();
164        let tracked state = ExclusiveGhost::alloc(
165            CpuCoreOwnerView { cpu, current_task: None, locals_key },
166        );
167        let tracked handle = CpuCoreOwnerHandle { state, marker: PhantomData };
168        CpuCoreOwner { handle, locals }
169    }
170
171    /// Unique identity of this core resource.
172    pub closed spec fn id(&self) -> Loc {
173        self.handle.id()
174    }
175
176    /// Stable CPU represented by this core.
177    pub closed spec fn cpu(&self) -> CpuId {
178        self@.cpu
179    }
180
181    /// Task currently running on this CPU.
182    pub closed spec fn current_task(&self) -> Option<Loc> {
183        self@.current_task
184    }
185
186    /// Whether no task is currently associated with this core.
187    pub open spec fn is_idle(&self) -> bool {
188        self.current_task() is None
189    }
190
191    /// CPU-local resource aggregate permanently assigned to this core.
192    pub closed spec fn locals(&self) -> L {
193        self.locals
194    }
195
196    /// Ordered identities of the CPU-local resources assigned to this core.
197    pub closed spec fn locals_key(&self) -> Seq<Loc> {
198        self.handle.expected_locals_key()
199    }
200
201    /// The core identity is valid and every local resource belongs to its CPU.
202    pub closed spec fn wf(&self) -> bool {
203        &&& self.handle.wf()
204        &&& self.locals().belongs_to_cpu(self.cpu())
205        &&& self.locals().local_key() == self.locals_key()
206    }
207
208    /// Associates a task with an idle CPU core.
209    pub proof fn tracked_schedule_in(tracked &mut self, task: Loc)
210        requires
211            old(self).wf(),
212            old(self).is_idle(),
213        ensures
214            final(self).id() == old(self).id(),
215            final(self).cpu() == old(self).cpu(),
216            final(self).current_task() == Some(task),
217            final(self).locals() == old(self).locals(),
218            final(self).locals_key() == old(self).locals_key(),
219            final(self).wf(),
220    {
221        let ghost next = CpuCoreOwnerView {
222            cpu: self.cpu(),
223            current_task: Some(task),
224            locals_key: self.locals_key(),
225        };
226        self.handle.state.update(next);
227    }
228
229    /// Makes this CPU idle and returns the task that was running on it.
230    pub proof fn tracked_schedule_out(tracked &mut self) -> (task: Loc)
231        requires
232            old(self).wf(),
233            !old(self).is_idle(),
234        ensures
235            old(self).current_task() == Some(task),
236            final(self).id() == old(self).id(),
237            final(self).cpu() == old(self).cpu(),
238            final(self).is_idle(),
239            final(self).locals() == old(self).locals(),
240            final(self).locals_key() == old(self).locals_key(),
241            final(self).wf(),
242    {
243        let task = self.current_task()->0;
244        let ghost next = CpuCoreOwnerView {
245            cpu: self.cpu(),
246            current_task: None,
247            locals_key: self.locals_key(),
248        };
249        self.handle.state.update(next);
250        task
251    }
252
253    /// Temporarily separates the typed CPU-local state from the core handle.
254    ///
255    /// The caller may update the returned resources, but must eventually call
256    /// [`CpuCoreOwnerHandle::tracked_restore`] with resources that still
257    /// belong to this CPU.
258    pub proof fn tracked_open(tracked self) -> (tracked res: (CpuCoreOwnerHandle<L>, L))
259        requires
260            self.wf(),
261        ensures
262            res.0.id() == self.id(),
263            res.0@ == self@,
264            res.0.wf(),
265            res.0.expected_locals_key() == self.locals_key(),
266            res.1 == self.locals(),
267            res.1.belongs_to_cpu(res.0.cpu()),
268            res.1.local_key() == res.0.expected_locals_key(),
269    {
270        (self.handle, self.locals)
271    }
272}
273
274/// Regression proof that a CPU-local points-to resource remains owned by the
275/// same core across scheduling and a temporary local-state access.
276proof fn cpu_core_owns_cpu_local_points_to<V>(initial: Map<CpuId, V>, cpu: CpuId, new_value: V)
277    requires
278        initial.contains_key(cpu),
279{
280    let tracked (mut auth, mut points_to_set) = CpuLocalAuth::new(initial);
281    let tracked points_to = points_to_set.tracked_take(cpu);
282    let tracked mut core = CpuCoreOwner::new(cpu, points_to);
283
284    let ghost task = auth.id();
285    core.tracked_schedule_in(task);
286    let tracked (handle, mut points_to) = core.tracked_open();
287    assert(handle.cpu() == cpu);
288    assert(handle.current_task() == Some(task));
289
290    points_to.tracked_update(&mut auth, new_value);
291    let tracked mut core = handle.tracked_restore(points_to);
292    assert(core.cpu() == cpu);
293    assert(core.current_task() == Some(task));
294
295    let finished_task = core.tracked_schedule_out();
296    assert(finished_task == task);
297    assert(core.is_idle());
298}
299
300} // verus!
ostd/specs/task/cpu_core.rs

ostd/specs/task/
cpu_core.rs
