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

ostd/specs/task/
cpu_core.rs
