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

ostd/specs/task/
cpu_local.rs
