ostd/specs/task/
cpu_local.rs

1// SPDX-License-Identifier: MPL-2.0
2//! Proof model for CPU-local state.
3//!
4//! A CPU-local object is modeled as one logical value for every CPU in its
5//! configured domain.
6//! [`CpuLocalAuth`] owns the authoritative map, while
7//! [`CpuLocalPointsTo`] is the exclusive points-to resource for one CPU's
8//! entry. Distinct CPUs therefore have independently owned resources and may
9//! operate on them concurrently.
10//!
11//! This module only defines the resource algebra used by CPU-local clients. It
12//! does not yet connect the resources to executable CPU-local storage,
13//! preemption guards, or scheduler transitions. Those layers should keep the
14//! authority in an invariant and transfer each points-to resource
15//! into the corresponding CPU core's proof state.
16use vstd::{
17    prelude::*,
18    resource::{
19        Loc,
20        map::{GhostMapAuth, GhostPointsTo, GhostSubmap},
21    },
22};
23
24use crate::specs::task::cpu_core::CpuCoreLocalState;
25
26use crate::cpu::CpuId;
27
28verus! {
29
30/// Authoritative logical contents of one CPU-local object.
31///
32/// The domain is fixed at allocation time. Updating a value requires both this
33/// authority and the matching [`CpuLocalPointsTo`], so the executable invariant
34/// cannot change a CPU's entry without its exclusive per-CPU permission.
35pub tracked struct CpuLocalAuth<V> {
36    auth: GhostMapAuth<CpuId, V>,
37}
38
39/// CPU-local points-to resources that have not yet been distributed.
40///
41/// A newly allocated model returns all resources in this collection. CPU setup
42/// can split them into individual [`CpuLocalPointsTo`] resources and install
43/// each resource in the corresponding CPU core's proof state.
44pub tracked struct CpuLocalPointsToSet<V> {
45    points_to: GhostSubmap<CpuId, V>,
46}
47
48/// Exclusive ownership of one CPU's entry in a CPU-local object.
49///
50/// Two live points-to resources associated with the same
51/// [`CpuLocalAuth`] necessarily refer to different CPUs. Holding this
52/// token does not by itself establish that the holder is currently executing
53/// on that CPU; the scheduler glue must additionally bind `cpu()` to its
54/// current-CPU token.
55pub tracked struct CpuLocalPointsTo<V> {
56    points_to: GhostPointsTo<CpuId, V>,
57}
58
59impl<V> CpuCoreLocalState for CpuLocalPointsTo<V> {
60    open spec fn belongs_to_cpu(self, cpu: CpuId) -> bool {
61        self.cpu() == cpu
62    }
63
64    open spec fn local_key(self) -> Seq<Loc> {
65        seq![self.id()]
66    }
67}
68
69impl<V> View for CpuLocalAuth<V> {
70    type V = Map<CpuId, V>;
71
72    closed spec fn view(&self) -> Self::V {
73        self.auth@
74    }
75}
76
77impl<V> View for CpuLocalPointsToSet<V> {
78    type V = Map<CpuId, V>;
79
80    closed spec fn view(&self) -> Self::V {
81        self.points_to@
82    }
83}
84
85impl<V> CpuLocalAuth<V> {
86    /// Allocates proof state for CPU-local contents described by `initial`.
87    ///
88    /// Allocation returns the authoritative state and exclusive ownership of
89    /// every points-to resource. No executable storage is allocated by this
90    /// proof function.
91    pub proof fn new(initial: Map<CpuId, V>) -> (tracked res: (
92        CpuLocalAuth<V>,
93        CpuLocalPointsToSet<V>,
94    ))
95        ensures
96            res.0.id() == res.1.id(),
97            res.0@ == initial,
98            res.1@ == initial,
99            res.0.cpus() == initial.dom(),
100            res.1.cpus() == initial.dom(),
101    {
102        let tracked (auth, points_to) = GhostMapAuth::new(initial);
103        (CpuLocalAuth { auth }, CpuLocalPointsToSet { points_to })
104    }
105
106    /// Identity shared by the authority and all of its points-to resources.
107    pub closed spec fn id(&self) -> Loc {
108        self.auth.id()
109    }
110
111    /// CPUs represented by this CPU-local object.
112    pub open spec fn cpus(&self) -> Set<CpuId> {
113        self@.dom()
114    }
115
116    /// The value currently associated with `cpu`.
117    pub open spec fn value(&self, cpu: CpuId) -> V
118        recommends
119            self.cpus().contains(cpu),
120    {
121        self@[cpu]
122    }
123
124    /// Whether this authority contains exactly the configured CPU set.
125    pub open spec fn covers(&self, cpus: Set<CpuId>) -> bool {
126        self.cpus() == cpus
127    }
128}
129
130impl<V> CpuLocalPointsToSet<V> {
131    /// Identity of the corresponding [`CpuLocalAuth`].
132    pub closed spec fn id(&self) -> Loc {
133        self.points_to.id()
134    }
135
136    /// CPUs whose exclusive points-to resources are still held here.
137    pub open spec fn cpus(&self) -> Set<CpuId> {
138        self@.dom()
139    }
140
141    /// Whether this collection currently owns `cpu`'s points-to resource.
142    pub open spec fn contains(&self, cpu: CpuId) -> bool {
143        self.cpus().contains(cpu)
144    }
145
146    /// Splits out exclusive ownership of one CPU's entry.
147    pub proof fn tracked_take(tracked &mut self, cpu: CpuId) -> (tracked res: CpuLocalPointsTo<V>)
148        requires
149            old(self).contains(cpu),
150        ensures
151            final(self).id() == old(self).id(),
152            res.id() == final(self).id(),
153            res.cpu() == cpu,
154            res.value() == old(self)@[cpu],
155            final(self)@ == old(self)@.remove(cpu),
156            final(self).cpus() == old(self).cpus().remove(cpu),
157    {
158        let tracked points_to = self.points_to.split_points_to(cpu);
159        let tracked res = CpuLocalPointsTo { points_to };
160        assert(res.value() == old(self)@[cpu]);
161        res
162    }
163
164    /// Returns an individual points-to resource to this collection.
165    pub proof fn tracked_return(tracked &mut self, tracked points_to: CpuLocalPointsTo<V>)
166        requires
167            old(self).id() == points_to.id(),
168            !old(self).contains(points_to.cpu()),
169        ensures
170            final(self).id() == old(self).id(),
171            final(self)@ == old(self)@.insert(points_to.cpu(), points_to.value()),
172            final(self).cpus() == old(self).cpus().insert(points_to.cpu()),
173    {
174        self.points_to.combine_points_to(points_to.points_to);
175    }
176}
177
178impl<V> CpuLocalPointsTo<V> {
179    /// Identity of the corresponding [`CpuLocalAuth`].
180    pub closed spec fn id(&self) -> Loc {
181        self.points_to.id()
182    }
183
184    /// CPU whose entry is owned by this points-to resource.
185    pub closed spec fn cpu(&self) -> CpuId {
186        self.points_to.key()
187    }
188
189    /// Current logical value of this CPU's entry.
190    pub closed spec fn value(&self) -> V {
191        self.points_to.value()
192    }
193
194    /// Establishes agreement with the authoritative CPU-local contents.
195    pub proof fn lemma_agree(tracked &self, tracked auth: &CpuLocalAuth<V>)
196        requires
197            self.id() == auth.id(),
198        ensures
199            auth.cpus().contains(self.cpu()),
200            auth.value(self.cpu()) == self.value(),
201    {
202        self.points_to.agree(&auth.auth);
203    }
204
205    /// Updates this CPU's logical value.
206    ///
207    /// Other CPUs' points-to resources remain disjoint and retain their values.
208    pub proof fn tracked_update(tracked &mut self, tracked auth: &mut CpuLocalAuth<V>, value: V)
209        requires
210            old(self).id() == old(auth).id(),
211        ensures
212            final(self).id() == old(self).id(),
213            final(self).cpu() == old(self).cpu(),
214            final(self).value() == value,
215            final(auth).id() == old(auth).id(),
216            final(auth).cpus() == old(auth).cpus(),
217            final(auth)@ == old(auth)@.insert(old(self).cpu(), value),
218    {
219        self.points_to.agree(&auth.auth);
220        let ghost cpu = self.cpu();
221        self.points_to.update(&mut auth.auth, value);
222        assert(auth@ == old(auth)@.insert(cpu, value));
223        assert(auth@.dom() == old(auth)@.dom());
224    }
225
226    /// Two points-to resources belonging to one authority refer to distinct CPUs.
227    pub proof fn lemma_distinct(tracked &mut self, tracked other: &CpuLocalPointsTo<V>)
228        requires
229            old(self).id() == other.id(),
230        ensures
231            final(self).id() == old(self).id(),
232            final(self).cpu() == old(self).cpu(),
233            final(self).value() == old(self).value(),
234            final(self).cpu() != other.cpu(),
235    {
236        self.points_to.disjoint(&other.points_to);
237    }
238
239    /// Two live points-to resources for the same CPU cannot belong to the same
240    /// CPU-local authority.
241    pub proof fn lemma_same_cpu_has_distinct_auth(
242        tracked &mut self,
243        tracked other: &CpuLocalPointsTo<V>,
244    )
245        requires
246            old(self).cpu() == other.cpu(),
247        ensures
248            final(self).id() == old(self).id(),
249            final(self).cpu() == old(self).cpu(),
250            final(self).value() == old(self).value(),
251            final(self).id() != other.id(),
252    {
253        if self.id() == other.id() {
254            self.points_to.disjoint(&other.points_to);
255        }
256    }
257}
258
259/// Regression proof for splitting, independently updating, and returning two
260/// CPU-local points-to resources.
261proof fn cpu_local_points_to_smoke_test<V>(
262    initial: Map<CpuId, V>,
263    cpu1: CpuId,
264    cpu2: CpuId,
265    new_value: V,
266)
267    requires
268        initial.contains_key(cpu1),
269        initial.contains_key(cpu2),
270        cpu1 != cpu2,
271{
272    let tracked (mut auth, mut points_to_set) = CpuLocalAuth::new(initial);
273    let tracked mut points_to1 = points_to_set.tracked_take(cpu1);
274    let tracked mut points_to2 = points_to_set.tracked_take(cpu2);
275
276    points_to1.lemma_distinct(&points_to2);
277    let ghost old_cpu2_value = points_to2.value();
278    points_to1.tracked_update(&mut auth, new_value);
279    points_to2.lemma_agree(&auth);
280    assert(points_to2.value() == old_cpu2_value);
281
282    points_to_set.tracked_return(points_to1);
283    points_to_set.tracked_return(points_to2);
284    assert(points_to_set.cpus() == initial.dom());
285}
286
287} // verus!
ostd/specs/task/cpu_local.rs

ostd/specs/task/
cpu_local.rs
