vstd/
atomic.rs

1#![allow(unused_imports)]
2
3use core::sync::atomic::{
4    AtomicBool, AtomicI8, AtomicI16, AtomicI32, AtomicIsize, AtomicPtr, AtomicU8, AtomicU16,
5    AtomicU32, AtomicUsize, Ordering,
6};
7
8#[cfg(target_has_atomic = "64")]
9use core::sync::atomic::{AtomicI64, AtomicU64};
10
11use super::modes::*;
12use super::pervasive::*;
13use super::prelude::*;
14use super::view::*;
15use super::wrapping::*;
16
17macro_rules! make_unsigned_integer_atomic {
18    ($at_ident:ident, $p_ident:ident, $p_data_ident:ident, $rust_ty: ty, $value_ty: ty, $modname:ident) => {
19        atomic_types!($at_ident, $p_ident, $p_data_ident, $rust_ty, $value_ty);
20        #[cfg_attr(verus_keep_ghost, verus::internal(verus_macro))]
21        impl $at_ident {
22            atomic_common_methods!($at_ident, $p_ident, $p_data_ident, $rust_ty, $value_ty, []);
23            atomic_integer_methods!($at_ident, $p_ident, $rust_ty, $value_ty, $modname);
24        }
25    };
26}
27
28macro_rules! make_signed_integer_atomic {
29    ($at_ident:ident, $p_ident:ident, $p_data_ident:ident, $rust_ty: ty, $value_ty: ty, $modname:ident) => {
30        atomic_types!($at_ident, $p_ident, $p_data_ident, $rust_ty, $value_ty);
31        #[cfg_attr(verus_keep_ghost, verus::internal(verus_macro))]
32        impl $at_ident {
33            atomic_common_methods!($at_ident, $p_ident, $p_data_ident, $rust_ty, $value_ty, []);
34            atomic_integer_methods!($at_ident, $p_ident, $rust_ty, $value_ty, $modname);
35        }
36    };
37}
38
39macro_rules! make_bool_atomic {
40    ($at_ident:ident, $p_ident:ident, $p_data_ident:ident, $rust_ty: ty, $value_ty: ty) => {
41        atomic_types!($at_ident, $p_ident, $p_data_ident, $rust_ty, $value_ty);
42        #[cfg_attr(verus_keep_ghost, verus::internal(verus_macro))]
43        impl $at_ident {
44            atomic_common_methods!($at_ident, $p_ident, $p_data_ident, $rust_ty, $value_ty, []);
45            atomic_bool_methods!($at_ident, $p_ident, $rust_ty, $value_ty);
46        }
47    };
48}
49
50macro_rules! atomic_types {
51    ($at_ident:ident, $p_ident:ident, $p_data_ident:ident, $rust_ty: ty, $value_ty: ty) => {
52        verus! {
53
54        #[verifier::external_body] /* vattr */
55        pub struct $at_ident {
56            ato: $rust_ty,
57        }
58
59        #[verifier::external_body] /* vattr */
60        pub tracked struct $p_ident {
61            no_copy: NoCopy,
62            unused: $value_ty,
63        }
64
65        pub ghost struct $p_data_ident {
66            pub patomic: int,
67            pub value: $value_ty,
68        }
69
70        impl $p_ident {
71            #[verifier::external_body] /* vattr */
72            pub uninterp spec fn view(self) -> $p_data_ident;
73
74            pub open spec fn is_for(&self, patomic: $at_ident) -> bool {
75                self.view().patomic == patomic.id()
76            }
77
78            pub open spec fn points_to(&self, v: $value_ty) -> bool {
79                self.view().value == v
80            }
81
82            #[verifier::inline]
83            pub open spec fn value(&self) -> $value_ty {
84                self.view().value
85            }
86
87            #[verifier::inline]
88            pub open spec fn id(&self) -> AtomicCellId {
89                self.view().patomic
90            }
91        }
92
93        }
94    };
95}
96
97macro_rules! atomic_types_generic {
98    ($at_ident:ident, $p_ident:ident, $p_data_ident:ident, $rust_ty: ty, $value_ty: ty) => {
99        verus! {
100
101        #[verifier::accept_recursive_types(T)]
102        #[verifier::external_body] /* vattr */
103        pub struct $at_ident <T> {
104            ato: $rust_ty,
105        }
106
107        #[verifier::accept_recursive_types(T)]
108        #[verifier::external_body] /* vattr */
109        pub tracked struct $p_ident <T> {
110            no_copy: NoCopy,
111            unusued: $value_ty,
112        }
113
114        #[verifier::accept_recursive_types(T)]
115        pub ghost struct $p_data_ident <T> {
116            pub patomic: int,
117            pub value: $value_ty,
118        }
119
120        impl<T> $p_ident <T> {
121            #[verifier::external_body] /* vattr */
122            pub uninterp spec fn view(self) -> $p_data_ident <T>;
123
124            pub open spec fn is_for(&self, patomic: $at_ident <T>) -> bool {
125                self.view().patomic == patomic.id()
126            }
127
128            pub open spec fn points_to(&self, v: $value_ty) -> bool {
129                self.view().value == v
130            }
131
132            #[verifier::inline]
133            pub open spec fn value(&self) -> $value_ty {
134                self.view().value
135            }
136
137            #[verifier::inline]
138            pub open spec fn id(&self) -> AtomicCellId {
139                self.view().patomic
140            }
141        }
142
143        }
144    };
145}
146
147pub type AtomicCellId = int;
148
149macro_rules! atomic_common_methods {
150    ($at_ident: ty, $p_ident: ty, $p_data_ident: ty, $rust_ty: ty, $value_ty: ty, [ $($addr:tt)* ]) => {
151        verus_impl!{
152
153        pub uninterp spec fn id(&self) -> int;
154
155        #[inline(always)]
156        #[verifier::external_body] /* vattr */
157        pub const fn new(i: $value_ty) -> (res: ($at_ident, Tracked<$p_ident>))
158            ensures
159                equal(res.1@.view(), $p_data_ident{ patomic: res.0.id(), value: i }),
160        {
161            let p = $at_ident { ato: <$rust_ty>::new(i) };
162            (p, Tracked::assume_new())
163        }
164
165        #[inline(always)]
166        #[verifier::external_body] /* vattr */
167        #[verifier::atomic] /* vattr */
168        pub fn load(&self, Tracked(perm): Tracked<&$p_ident>) -> (ret: $value_ty)
169            requires
170                equal(self.id(), perm.view().patomic),
171            ensures equal(perm.view().value, ret),
172            opens_invariants none
173            no_unwind
174        {
175            self.ato.load(Ordering::SeqCst)
176        }
177
178        #[inline(always)]
179        #[verifier::external_body] /* vattr */
180        #[verifier::atomic] /* vattr */
181        pub fn store(&self, Tracked(perm): Tracked<&mut $p_ident>, v: $value_ty)
182            requires
183                equal(self.id(), old(perm).view().patomic),
184            ensures equal(final(perm).view().value, v) && equal(self.id(), final(perm).view().patomic),
185            opens_invariants none
186            no_unwind
187        {
188            self.ato.store(v, Ordering::SeqCst)
189        }
190
191        #[inline(always)]
192        #[verifier::external_body] /* vattr */
193        #[verifier::atomic] /* vattr */
194        pub fn compare_exchange(&self, Tracked(perm): Tracked<&mut $p_ident>, current: $value_ty, new: $value_ty) -> (ret: Result<$value_ty, $value_ty>)
195            requires
196                equal(self.id(), old(perm).view().patomic),
197            ensures
198                equal(self.id(), final(perm).view().patomic)
199                && match ret {
200                    Result::Ok(r) =>
201                           current $($addr)* == old(perm).view().value $($addr)*
202                        && equal(final(perm).view().value, new)
203                        && equal(r, old(perm).view().value),
204                    Result::Err(r) =>
205                           current $($addr)* != old(perm).view().value $($addr)*
206                        && equal(final(perm).view().value, old(perm).view().value)
207                        && equal(r, old(perm).view().value),
208                },
209            opens_invariants none
210            no_unwind
211        {
212            self.ato.compare_exchange(current, new, Ordering::SeqCst, Ordering::SeqCst)
213        }
214
215        #[inline(always)]
216        #[verifier::external_body] /* vattr */
217        #[verifier::atomic] /* vattr */
218        pub fn compare_exchange_weak(&self, Tracked(perm): Tracked<&mut $p_ident>, current: $value_ty, new: $value_ty) -> (ret: Result<$value_ty, $value_ty>)
219            requires
220                equal(self.id(), old(perm).view().patomic),
221            ensures
222                equal(self.id(), final(perm).view().patomic)
223                && match ret {
224                    Result::Ok(r) =>
225                           current $($addr)* == old(perm).view().value $($addr)*
226                        && equal(final(perm).view().value, new)
227                        && equal(r, old(perm).view().value),
228                    Result::Err(r) =>
229                           equal(final(perm).view().value, old(perm).view().value)
230                        && equal(r, old(perm).view().value),
231                },
232            opens_invariants none
233            no_unwind
234        {
235            self.ato.compare_exchange_weak(current, new, Ordering::SeqCst, Ordering::SeqCst)
236        }
237
238        #[inline(always)]
239        #[verifier::external_body] /* vattr */
240        #[verifier::atomic] /* vattr */
241        pub fn swap(&self, Tracked(perm): Tracked<&mut $p_ident>, v: $value_ty) -> (ret: $value_ty)
242            requires
243                equal(self.id(), old(perm).view().patomic),
244            ensures
245                   equal(final(perm).view().value, v)
246                && equal(old(perm).view().value, ret)
247                && equal(self.id(), final(perm).view().patomic),
248            opens_invariants none
249            no_unwind
250        {
251            self.ato.swap(v, Ordering::SeqCst)
252        }
253
254        #[inline(always)]
255        #[verifier::external_body] /* vattr */
256        pub fn into_inner(self, Tracked(perm): Tracked<$p_ident>) -> (ret: $value_ty)
257            requires
258                equal(self.id(), perm.view().patomic),
259            ensures equal(perm.view().value, ret),
260            opens_invariants none
261            no_unwind
262        {
263            self.ato.into_inner()
264        }
265
266        }
267    };
268}
269
270macro_rules! atomic_integer_methods {
271    ($at_ident:ident, $p_ident:ident, $rust_ty: ty, $value_ty: ty, $modname:ident) => {
272        verus_impl!{
273
274        // Note that wrapping-on-overflow is the defined behavior for fetch_add and fetch_sub
275        // for Rust's atomics (in contrast to ordinary arithmetic)
276
277        #[inline(always)]
278        #[verifier::external_body] /* vattr */
279        #[verifier::atomic] /* vattr */
280        pub fn fetch_add_wrapping(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
281            requires equal(self.id(), old(perm).view().patomic),
282            ensures
283                equal(old(perm).view().value, ret),
284                final(perm).view().patomic == old(perm).view().patomic,
285                final(perm).view().value as int == $modname::wrapping_add(old(perm).view().value, n),
286            opens_invariants none
287            no_unwind
288        {
289            self.ato.fetch_add(n, Ordering::SeqCst)
290        }
291
292        #[inline(always)]
293        #[verifier::external_body] /* vattr */
294        #[verifier::atomic] /* vattr */
295        pub fn fetch_sub_wrapping(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
296            requires equal(self.id(), old(perm).view().patomic),
297            ensures
298                equal(old(perm).view().value, ret),
299                final(perm).view().patomic == old(perm).view().patomic,
300                final(perm).view().value as int == $modname::wrapping_sub(old(perm).view().value, n),
301            opens_invariants none
302            no_unwind
303        {
304            self.ato.fetch_sub(n, Ordering::SeqCst)
305        }
306
307        // fetch_add and fetch_sub are more natural in the common case that you
308        // don't expect wrapping
309
310        #[inline(always)]
311        #[verifier::atomic] /* vattr */
312        pub fn fetch_add(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
313            requires
314                equal(self.id(), old(perm).view().patomic),
315                (<$value_ty>::MIN as int) <= old(perm).view().value + n,
316                old(perm).view().value + n <= (<$value_ty>::MAX as int),
317            ensures
318                equal(old(perm).view().value, ret),
319                final(perm).view().patomic == old(perm).view().patomic,
320                final(perm).view().value == old(perm).view().value + n,
321            opens_invariants none
322            no_unwind
323        {
324            self.fetch_add_wrapping(Tracked(&mut *perm), n)
325        }
326
327        #[inline(always)]
328        #[verifier::atomic] /* vattr */
329        pub fn fetch_sub(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
330            requires
331                equal(self.id(), old(perm).view().patomic),
332                (<$value_ty>::MIN as int) <= old(perm).view().value - n,
333                old(perm).view().value - n <= <$value_ty>::MAX as int,
334            ensures
335                equal(old(perm).view().value, ret),
336                final(perm).view().patomic == old(perm).view().patomic,
337                final(perm).view().value == old(perm).view().value - n,
338            opens_invariants none
339            no_unwind
340        {
341            self.fetch_sub_wrapping(Tracked(&mut *perm), n)
342        }
343
344        #[inline(always)]
345        #[verifier::external_body] /* vattr */
346        #[verifier::atomic] /* vattr */
347        pub fn fetch_and(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
348            requires equal(self.id(), old(perm).view().patomic),
349            ensures
350                equal(old(perm).view().value, ret),
351                final(perm).view().patomic == old(perm).view().patomic,
352                final(perm).view().value == (old(perm).view().value & n),
353            opens_invariants none
354            no_unwind
355        {
356            self.ato.fetch_and(n, Ordering::SeqCst)
357        }
358
359        #[inline(always)]
360        #[verifier::external_body] /* vattr */
361        #[verifier::atomic] /* vattr */
362        pub fn fetch_or(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
363            requires equal(self.id(), old(perm).view().patomic),
364            ensures
365                equal(old(perm).view().value, ret),
366                final(perm).view().patomic == old(perm).view().patomic,
367                final(perm).view().value == (old(perm).view().value | n),
368            opens_invariants none
369            no_unwind
370        {
371            self.ato.fetch_or(n, Ordering::SeqCst)
372        }
373
374        #[inline(always)]
375        #[verifier::external_body] /* vattr */
376        #[verifier::atomic] /* vattr */
377        pub fn fetch_xor(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
378            requires equal(self.id(), old(perm).view().patomic),
379            ensures
380                equal(old(perm).view().value, ret),
381                final(perm).view().patomic == old(perm).view().patomic,
382                final(perm).view().value == (old(perm).view().value ^ n),
383            opens_invariants none
384            no_unwind
385        {
386            self.ato.fetch_xor(n, Ordering::SeqCst)
387        }
388
389        #[inline(always)]
390        #[verifier::external_body] /* vattr */
391        #[verifier::atomic] /* vattr */
392        pub fn fetch_nand(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
393            requires equal(self.id(), old(perm).view().patomic),
394            ensures
395                equal(old(perm).view().value, ret),
396                final(perm).view().patomic == old(perm).view().patomic,
397                final(perm).view().value == !(old(perm).view().value & n),
398            opens_invariants none
399            no_unwind
400        {
401            self.ato.fetch_nand(n, Ordering::SeqCst)
402        }
403
404        #[inline(always)]
405        #[verifier::external_body] /* vattr */
406        #[verifier::atomic] /* vattr */
407        pub fn fetch_max(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
408            requires equal(self.id(), old(perm).view().patomic),
409            ensures
410                equal(old(perm).view().value, ret),
411                final(perm).view().patomic == old(perm).view().patomic,
412                final(perm).view().value == (if old(perm).view().value > n { old(perm).view().value } else { n }),
413            opens_invariants none
414            no_unwind
415        {
416            self.ato.fetch_max(n, Ordering::SeqCst)
417        }
418
419        #[inline(always)]
420        #[verifier::external_body] /* vattr */
421        #[verifier::atomic] /* vattr */
422        pub fn fetch_min(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
423            requires equal(self.id(), old(perm).view().patomic),
424            ensures
425                equal(old(perm).view().value, ret),
426                final(perm).view().patomic == old(perm).view().patomic,
427                final(perm).view().value == (if old(perm).view().value < n { old(perm).view().value } else { n }),
428            opens_invariants none
429            no_unwind
430        {
431            self.ato.fetch_min(n, Ordering::SeqCst)
432        }
433
434        }
435    };
436}
437
438macro_rules! atomic_bool_methods {
439    ($at_ident:ident, $p_ident:ident, $rust_ty: ty, $value_ty: ty) => {
440        verus!{
441
442        #[inline(always)]
443        #[verifier::external_body] /* vattr */
444        #[verifier::atomic] /* vattr */
445        pub fn fetch_and(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
446            requires
447                equal(self.id(), old(perm).view().patomic),
448            ensures
449                   equal(old(perm).view().value, ret)
450                && final(perm).view().patomic == old(perm).view().patomic
451                && final(perm).view().value == (old(perm).view().value && n),
452            opens_invariants none
453            no_unwind
454        {
455            self.ato.fetch_and(n, Ordering::SeqCst)
456        }
457
458        #[inline(always)]
459        #[verifier::external_body] /* vattr */
460        #[verifier::atomic] /* vattr */
461        pub fn fetch_or(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
462            requires
463                equal(self.id(), old(perm).view().patomic),
464            ensures
465                  equal(old(perm).view().value, ret)
466                && final(perm).view().patomic == old(perm).view().patomic
467                && final(perm).view().value == (old(perm).view().value || n),
468            opens_invariants none
469            no_unwind
470        {
471            self.ato.fetch_or(n, Ordering::SeqCst)
472        }
473
474        #[inline(always)]
475        #[verifier::external_body] /* vattr */
476        #[verifier::atomic] /* vattr */
477        pub fn fetch_xor(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
478            requires
479                equal(self.id(), old(perm).view().patomic),
480            ensures
481                equal(old(perm).view().value, ret)
482                && final(perm).view().patomic == old(perm).view().patomic
483                && final(perm).view().value == ((old(perm).view().value && !n) || (!old(perm).view().value && n)),
484            opens_invariants none
485            no_unwind
486        {
487            self.ato.fetch_xor(n, Ordering::SeqCst)
488        }
489
490        #[inline(always)]
491        #[verifier::external_body] /* vattr */
492        #[verifier::atomic] /* vattr */
493        pub fn fetch_nand(&self, Tracked(perm): Tracked<&mut $p_ident>, n: $value_ty) -> (ret: $value_ty)
494            requires
495                equal(self.id(), old(perm).view().patomic),
496            ensures
497                equal(old(perm).view().value, ret)
498                && final(perm).view().patomic == old(perm).view().patomic
499                && final(perm).view().value == !(old(perm).view().value && n),
500            opens_invariants none
501            no_unwind
502        {
503            self.ato.fetch_nand(n, Ordering::SeqCst)
504        }
505
506        }
507    };
508}
509
510make_bool_atomic!(PAtomicBool, PermissionBool, PermissionDataBool, AtomicBool, bool);
511
512make_unsigned_integer_atomic!(PAtomicU8, PermissionU8, PermissionDataU8, AtomicU8, u8, u8_specs);
513make_unsigned_integer_atomic!(
514    PAtomicU16,
515    PermissionU16,
516    PermissionDataU16,
517    AtomicU16,
518    u16,
519    u16_specs
520);
521make_unsigned_integer_atomic!(
522    PAtomicU32,
523    PermissionU32,
524    PermissionDataU32,
525    AtomicU32,
526    u32,
527    u32_specs
528);
529
530#[cfg(target_has_atomic = "64")]
531make_unsigned_integer_atomic!(
532    PAtomicU64,
533    PermissionU64,
534    PermissionDataU64,
535    AtomicU64,
536    u64,
537    u64_specs
538);
539make_unsigned_integer_atomic!(
540    PAtomicUsize,
541    PermissionUsize,
542    PermissionDataUsize,
543    AtomicUsize,
544    usize,
545    usize_specs
546);
547
548make_signed_integer_atomic!(PAtomicI8, PermissionI8, PermissionDataI8, AtomicI8, i8, i8_specs);
549make_signed_integer_atomic!(
550    PAtomicI16,
551    PermissionI16,
552    PermissionDataI16,
553    AtomicI16,
554    i16,
555    i16_specs
556);
557make_signed_integer_atomic!(
558    PAtomicI32,
559    PermissionI32,
560    PermissionDataI32,
561    AtomicI32,
562    i32,
563    i32_specs
564);
565
566#[cfg(target_has_atomic = "64")]
567make_signed_integer_atomic!(
568    PAtomicI64,
569    PermissionI64,
570    PermissionDataI64,
571    AtomicI64,
572    i64,
573    i64_specs
574);
575make_signed_integer_atomic!(
576    PAtomicIsize,
577    PermissionIsize,
578    PermissionDataIsize,
579    AtomicIsize,
580    isize,
581    isize_specs
582);
583
584atomic_types_generic!(PAtomicPtr, PermissionPtr, PermissionDataPtr, AtomicPtr<T>, *mut T);
585
586#[cfg_attr(verus_keep_ghost, verifier::verus_macro)]
587impl<T> PAtomicPtr<T> {
588    atomic_common_methods!(
589        PAtomicPtr::<T>,
590        PermissionPtr::<T>,
591        PermissionDataPtr::<T>,
592        AtomicPtr::<T>,
593        *mut T,
594        [ .view().addr ]
595    );
596}
597
598impl<X, Y, Pred> core::fmt::Debug for AtomicUpdate<X, Y, Pred> {
599    fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
600        f.debug_struct("AtomicUpdate").finish_non_exhaustive()
601    }
602}
603
604/// Mark the `AtomicUpdate` as `Send` if both `X` and `Y` are also `Send`.
605///
606/// # SAFETY
607/// While the `AtomicUpdate` is only a stand-in for a stack of nested callback functions,
608/// when the AU is moved to another thread, e.g. by moving it in and out of an atomic invariant,
609/// it allows resources to cross thread boundaries with it,
610/// so we must ensure the AU is only `Send` when `X: Send` and `Y: Send`.
611///
612/// The predicate type we generate as part of the atomic specification only contains
613/// a ghost copy of function arguments, and ghost-mode data is always fine to move between threads.
614/// There is no need to restrict it, as it is safe by construction.
615unsafe impl<X: Send, Y: Send, Pred> Send for AtomicUpdate<X, Y, Pred> {}
616
617/// Unconditionally mark the `AtomicUpdate` as `Sync`.
618///
619/// # SAFETY
620/// A shared reference to an `AtomicUpdate` is pretty much useless.
621/// The only thing the user can do with an AU is open it, which requires full ownership.
622/// All methods provided by this type are spec-mode,
623/// meaning they can already be used with a much weaker ghost copy of the AU.
624unsafe impl<X, Y, Pred> Sync for AtomicUpdate<X, Y, Pred> {}
625
626verus! {
627
628/// The **atomic update (AU)** is a ghost object which encapsulates the linearization point of a logically atomic function.
629///
630/// Logical atomicity is a proof technique that allows us to treat a function as if it was atomic, i.e. as if it evaluates in a single atomic step, even though it might perform multiple `exec`-mode operations internally.
631/// The key idea is that a logically atomic function contains a **linearization point (LP)**, that is, a point in the function which updates the state of the program in a single atomic step of computation.
632/// We specify the behavior of such a function by describing the state of the program at four distinct points in time, specifically:
633/// - **(private pre)** at the start of the function,
634/// - **(atomic pre)** just before the linearization point,
635/// - **(atomic post)** just after the linearization point,
636/// - **(private post)** at the end of the function.
637/// ```
638///                        linearization point
639///                                 🠗
640/// ├──────────────────────────────┤●├─────────────────────────┤
641///  private                 atomic   atomic            private
642///  pre                        pre   post                 post
643/// ```
644/// The `AtomicUpdate` ghost object is the central abstraction for our implementation if logical atomicity, as it encapsulates the behavior of the function at the linearization point.
645/// The atomic update is declared by the atomic specification, it is constructed by the atomic function call (i.e. the "client"), and it is opened/destructed at the linearization point of the logically atomic function (i.e. the "library").
646#[verifier::reject_recursive_types(X)]
647#[verifier::reject_recursive_types(Y)]
648#[verifier::reject_recursive_types(Pred)]
649#[verifier::external_body]
650pub struct AtomicUpdate<X, Y, Pred> {
651    pred: Pred,
652    _dummy: core::marker::PhantomData<fn (fn (X) -> Y)>,
653    _not_send_sync: core::marker::PhantomData<*const ()>,
654}
655
656impl<X, Y, Pred> AtomicUpdate<X, Y, Pred> {
657    /// The predicate of the atomic update.
658    ///
659    /// See [`UpdatePredicate`] for more information.
660    #[rustc_diagnostic_item = "verus::vstd::atomic::AtomicUpdate::pred"]
661    pub uninterp spec fn pred(self) -> Pred;
662
663    /// A prophesy variable which indicates that an atomic update has been resolved.
664    ///
665    /// Initially, the value of this function is unknown, i.e. we can neither prove that it is `true` or `false`.
666    /// Once the atomic update has been committed using the [`try_open_atomic_update`] macro, we learn that `au.resolves()` is `true`.
667    ///
668    /// We must be able to prove that `au.resolves()` when the logically atomic function exits.
669    #[rustc_diagnostic_item = "verus::vstd::atomic::AtomicUpdate::resolves"]
670    pub uninterp spec fn resolves(self) -> bool;
671
672    /// A prophesy variable for the input value of the atomic update.
673    ///
674    /// When the atomic update is committed, this variable is resolved to the input value of the atomic update.
675    /// This variable is used internally in the (private) postcondition of the logically atomic function.
676    #[rustc_diagnostic_item = "verus::vstd::atomic::AtomicUpdate::input"]
677    pub uninterp spec fn input(self) -> X;
678
679    /// A prophesy variable for the output value of the atomic update.
680    ///
681    /// When the atomic update is committed, this variable is resolved to the output value of the atomic update.
682    /// This variable is used internally in the (private) postcondition of the logically atomic function.
683    #[rustc_diagnostic_item = "verus::vstd::atomic::AtomicUpdate::output"]
684    pub uninterp spec fn output(self) -> Y;
685}
686
687impl<X, Y, Pred: UpdatePredicate<X, Y>> AtomicUpdate<X, Y, Pred> {
688    #[rustc_diagnostic_item = "verus::vstd::atomic::AtomicUpdate::req"]
689    pub open spec fn req(self, x: X) -> bool {
690        self.pred().req(x)
691    }
692
693    #[rustc_diagnostic_item = "verus::vstd::atomic::AtomicUpdate::ens"]
694    pub open spec fn ens(self, x: X, y: Y) -> bool {
695        self.pred().ens(x, y)
696    }
697
698    #[rustc_diagnostic_item = "verus::vstd::atomic::AtomicUpdate::outer_mask"]
699    pub open spec fn outer_mask(self) -> ISet<int> {
700        self.pred().outer_mask()
701    }
702
703    #[rustc_diagnostic_item = "verus::vstd::atomic::AtomicUpdate::inner_mask"]
704    pub open spec fn inner_mask(self) -> ISet<int> {
705        self.pred().inner_mask()
706    }
707}
708
709#[cfg(verus_keep_ghost)]
710#[rustc_diagnostic_item = "verus::vstd::atomic::pred_args"]
711#[doc(hidden)]
712pub uninterp spec fn pred_args<Pred, Args>(pred: Pred) -> Args;
713
714/// Trait used to specify the update predicate for the [`AtomicUpdate`].
715///
716/// This trait is implemented automatically by Verus when a logically atomic function is defined.
717/// ```
718/// exec fn function(px: PX) -> (py: PY)
719///     atomically (atomic_update) {
720///         type PredType,
721///
722///         (ax: AX) -> (ay: AY),
723///
724///         requires atomic_pre(px, ax),
725///         ensures atomic_post(px, ax, ay),
726///
727///         outer_mask Eo,
728///         inner_mask Ei,
729///     },
730///     requires private_pre(px),
731///     ensures private_post(px, ax, ay, py),
732/// ```
733/// The above code snipped generates (roughly) the type and trait implementation below.
734/// ```
735/// struct PredType { px: Ghost<PX> }
736///
737/// impl UpdatePredicate<AX, AY> for PredType {
738///     open spec fn req(self, x: X)       -> bool { atomic_pre  }
739///     open spec fn ens(self, x: X, y: Y) -> bool { atomic_post }
740///
741///     open spec fn outer_mask(self) -> ISet<int> { Eo }
742///     open spec fn inner_mask(self) -> ISet<int> { Ei }
743/// }
744/// ```
745pub trait UpdatePredicate<X, Y>: Sized {
746    /// The atomic pre-condition.
747    spec fn req(self, x: X) -> bool;
748
749    /// The atomic post-condition.
750    spec fn ens(self, x: X, y: Y) -> bool;
751
752    /// The outer mask of the atomic update.
753    open spec fn outer_mask(self) -> ISet<int> {
754        ISet::empty()
755    }
756
757    /// The inner mask of the atomic update.
758    open spec fn inner_mask(self) -> ISet<int> {
759        ISet::empty()
760    }
761}
762
763/// The control flow corresponding to the atomic update output.
764pub enum UpdateControlFlow {
765    /// The update output value indicates that the atomic update has been committed.
766    ///
767    /// This means [`try_open_atomic_update`] will consume the atomic update (i.e. return `Ok(())`),
768    /// and the atomic function call has to `break`.
769    Commit,
770    /// The update output value indicates that the atomic update has been aborted.
771    ///
772    /// This means [`try_open_atomic_update`] will give back the atomic update (i.e. return `Err(Tracked(au))`),
773    /// and the atomic function call has to `continue`.
774    Abort,
775}
776
777impl UpdateControlFlow {
778    pub open spec fn is_commit(self) -> bool {
779        match self {
780            UpdateControlFlow::Commit => true,
781            UpdateControlFlow::Abort => false,
782        }
783    }
784
785    pub open spec fn is_abort(self) -> bool {
786        !self.is_commit()
787    }
788}
789
790pub trait UpdateTry {
791    spec fn branch(self) -> UpdateControlFlow;
792}
793
794impl<T, E> UpdateTry for Result<T, E> {
795    open spec fn branch(self) -> UpdateControlFlow {
796        match self {
797            Ok(_) => UpdateControlFlow::Commit,
798            Err(_) => UpdateControlFlow::Abort,
799        }
800    }
801}
802
803/// A trivial wrapper type which indicates a commit.
804///
805/// This is useful for logically atomic functions which do not require an abort case.
806#[derive(Debug)]
807pub struct Commit<T>(pub T);
808
809impl<T> Commit<T> {
810    pub proof fn get(tracked self) -> (tracked out: T)
811        ensures
812            self@ == out,
813    {
814        self.0
815    }
816}
817
818impl<T> View for Commit<T> {
819    type V = T;
820
821    #[verifier::inline]
822    open spec fn view(&self) -> T {
823        self.0
824    }
825}
826
827impl<T> UpdateTry for Commit<T> {
828    open spec fn branch(self) -> UpdateControlFlow {
829        UpdateControlFlow::Commit
830    }
831}
832
833impl UpdateTry for () {
834    open spec fn branch(self) -> UpdateControlFlow {
835        UpdateControlFlow::Commit
836    }
837}
838
839#[cfg(verus_keep_ghost)]
840#[rustc_diagnostic_item = "verus::vstd::atomic::branch_bool"]
841#[doc(hidden)]
842pub open spec fn branch_bool<T: UpdateTry>(this: T) -> bool {
843    this.branch().is_commit()
844}
845
846// Definition for atomic function call
847#[cfg(verus_keep_ghost)]
848#[rustc_diagnostic_item = "verus::vstd::atomic::atomically"]
849#[doc(hidden)]
850#[verifier::external]
851pub fn atomically<X, Y: UpdateTry, P: UpdatePredicate<X, Y>>(
852    _body: impl FnOnce(fn (X) -> Y, Ghost<AtomicUpdate<X, Y, P>>),
853) -> AtomicUpdate<X, Y, P> {
854    arbitrary()
855}
856
857// Definitions for `try_open_atomic_update` macro
858#[doc(hidden)]
859pub struct BlockGuard<T> {
860    _inner: core::marker::PhantomData<T>,
861}
862
863#[cfg(verus_keep_ghost)]
864#[doc(hidden)]
865#[verifier::external]  /* vattr */
866pub fn bind_lifetime_internal<'a, X: 'a, Y, P>(
867    _block_guard: &'a BlockGuard<AtomicUpdate<X, Y, P>>,
868) -> X {
869    unimplemented!()
870}
871
872#[cfg(verus_keep_ghost)]
873#[rustc_diagnostic_item = "verus::vstd::atomic::try_open_atomic_update_begin"]
874#[doc(hidden)]
875#[verifier::external]  /* vattr */
876pub fn try_open_atomic_update_begin<X, Y: UpdateTry, P: UpdatePredicate<X, Y>>(
877    _atomic_update: AtomicUpdate<X, Y, P>,
878) -> BlockGuard<AtomicUpdate<X, Y, P>> {
879    unimplemented!()
880}
881
882#[cfg(verus_keep_ghost)]
883#[rustc_diagnostic_item = "verus::vstd::atomic::try_open_atomic_update_end"]
884#[doc(hidden)]
885#[verifier::external]  /* vattr */
886pub fn try_open_atomic_update_end<X, Y: UpdateTry, P: UpdatePredicate<X, Y>>(
887    _guard: BlockGuard<AtomicUpdate<X, Y, P>>,
888    _y: Tracked<Y>,
889) -> Tracked<Result<(), AtomicUpdate<X, Y, P>>> {
890    unimplemented!()
891}
892
893// Macro definitions
894#[macro_export]
895macro_rules! open_atomic_update {
896    ($($tail:tt)*) => {
897        {
898            let _ = ::verus_builtin_macros::verus_exec_open_au_macro_exprs!(
899                $crate::atomic::try_open_atomic_update_internal!(
900                    $($tail)*, @EXEC, au_commit_wrap_exec
901                )
902            );
903        }
904    };
905}
906
907#[macro_export]
908macro_rules! open_atomic_update_in_proof {
909    ($($tail:tt)*) => {
910        {
911            let _ = ::verus_builtin_macros::verus_ghost_open_au_macro_exprs!(
912                $crate::atomic::try_open_atomic_update_internal!(
913                    $($tail)*, @PROOF, au_commit_wrap_proof
914                )
915            );
916        }
917    };
918}
919
920#[macro_export]
921macro_rules! peek_atomic_update {
922    ($($tail:tt)*) => {
923        {
924            #[verifier::exec]
925            let err_au = ::verus_builtin_macros::verus_exec_open_au_macro_exprs!(
926                $crate::atomic::try_open_atomic_update_internal!(
927                    $($tail)*, @EXEC, au_abort_wrap_exec
928                )
929            );
930
931            match () {
932                #[cfg(verus_keep_ghost_body)]
933                _ => $crate::atomic::au_abort_unwrap_exec(err_au),
934
935                #[cfg(not(verus_keep_ghost_body))]
936                _ => ::verus_builtin::Tracked::assume_new_fallback(|| ::core::unreachable!()),
937            }
938        }
939    };
940}
941
942#[macro_export]
943macro_rules! peek_atomic_update_in_proof {
944    ($($tail:tt)*) => {
945        {
946            #[verifier::proof]
947            let err_au = ::verus_builtin_macros::verus_ghost_open_au_macro_exprs!(
948                $crate::atomic::try_open_atomic_update_internal!(
949                    $($tail)*, @PROOF, au_abort_wrap_proof
950                )
951            );
952
953            match () {
954                #[cfg(verus_keep_ghost_body)]
955                _ => $crate::atomic::au_abort_unwrap_proof(err_au),
956
957                #[cfg(not(verus_keep_ghost_body))]
958                _ => ::verus_builtin::Tracked::assume_new_fallback(|| ::core::unreachable!()),
959            }
960        }
961    };
962}
963
964#[macro_export]
965macro_rules! try_open_atomic_update {
966    ($($tail:tt)*) => {
967        ::verus_builtin_macros::verus_exec_open_au_macro_exprs!(
968            $crate::atomic::try_open_atomic_update_internal!($($tail)*)
969        )
970    };
971}
972
973#[macro_export]
974macro_rules! try_open_atomic_update_in_proof {
975    ($($tail:tt)*) => {
976        ::verus_builtin_macros::verus_ghost_open_au_macro_exprs!(
977            $crate::atomic::try_open_atomic_update_internal!($($tail)*)
978        )
979    };
980}
981
982#[macro_export]
983macro_rules! try_open_atomic_update_internal {
984    ($au:expr, $x:pat => $body:block, @EXEC, $wrap_fn:ident) => {
985        $crate::atomic::try_open_atomic_update_internal!($au, $x => {
986            #[verifier::exec]
987            let v = $body;
988
989            match () {
990                #[cfg(verus_keep_ghost_body)]
991                _ => $crate::atomic::$wrap_fn(v),
992
993                #[cfg(not(verus_keep_ghost_body))]
994                _ => ::verus_builtin::Tracked::assume_new_fallback(|| ::core::unreachable!()),
995            }
996        })
997    };
998
999    ($au:expr, $x:pat => $body:block, @PROOF, $wrap_fn:ident) => {
1000        $crate::atomic::try_open_atomic_update_internal!($au, $x => {
1001            #[verifier::proof]
1002            let v = $body;
1003
1004            match () {
1005                #[cfg(verus_keep_ghost_body)]
1006                _ => $crate::atomic::$wrap_fn(v),
1007
1008                #[cfg(not(verus_keep_ghost_body))]
1009                _ => ::verus_builtin::Tracked::assume_new_fallback(|| ::core::unreachable!()),
1010            }
1011        })
1012    };
1013
1014    ($au:expr, $x:pat => $body:block) => {
1015        #[cfg_attr(verus_keep_ghost, verifier::open_au_block)] /* vattr */ {
1016            #[cfg(verus_keep_ghost_body)]
1017            let guard = $crate::atomic::try_open_atomic_update_begin($au);
1018            #[cfg(verus_keep_ghost_body)]
1019            let $x = $crate::atomic::bind_lifetime_internal(&guard);
1020            let res = $body;
1021
1022            match res {
1023                #[cfg(verus_keep_ghost_body)]
1024                res => $crate::atomic::try_open_atomic_update_end(guard, res),
1025
1026                #[cfg(not(verus_keep_ghost_body))]
1027                _ => ::verus_builtin::Tracked::assume_new_fallback(|| ::core::unreachable!()),
1028            }
1029        }
1030    };
1031}
1032
1033#[doc(hidden)]
1034pub use {try_open_atomic_update_internal};
1035pub use {
1036    open_atomic_update,
1037    open_atomic_update_in_proof,
1038    peek_atomic_update,
1039    peek_atomic_update_in_proof,
1040    try_open_atomic_update,
1041    try_open_atomic_update_in_proof,
1042};
1043
1044impl<T> PAtomicPtr<T> {
1045    #[inline(always)]
1046    #[verifier::external_body]  /* vattr */
1047    #[verifier::atomic]  /* vattr */
1048    #[cfg(any(verus_keep_ghost, feature = "strict_provenance_atomic_ptr"))]
1049    pub fn fetch_and(&self, Tracked(perm): Tracked<&mut PermissionPtr<T>>, n: usize) -> (ret:
1050        *mut T)
1051        requires
1052            equal(self.id(), old(perm).view().patomic),
1053        ensures
1054            equal(old(perm).view().value, ret),
1055            final(perm).view().patomic == old(perm).view().patomic,
1056            final(perm).view().value@.addr == (old(perm).view().value@.addr & n),
1057            final(perm).view().value@.provenance == old(perm).view().value@.provenance,
1058            final(perm).view().value@.metadata == old(perm).view().value@.metadata,
1059        opens_invariants none
1060        no_unwind
1061    {
1062        self.ato.fetch_and(n, Ordering::SeqCst)
1063    }
1064
1065    #[inline(always)]
1066    #[verifier::external_body]  /* vattr */
1067    #[verifier::atomic]  /* vattr */
1068    #[cfg(any(verus_keep_ghost, feature = "strict_provenance_atomic_ptr"))]
1069    pub fn fetch_xor(&self, Tracked(perm): Tracked<&mut PermissionPtr<T>>, n: usize) -> (ret:
1070        *mut T)
1071        requires
1072            equal(self.id(), old(perm).view().patomic),
1073        ensures
1074            equal(old(perm).view().value, ret),
1075            final(perm).view().patomic == old(perm).view().patomic,
1076            final(perm).view().value@.addr == (old(perm).view().value@.addr ^ n),
1077            final(perm).view().value@.provenance == old(perm).view().value@.provenance,
1078            final(perm).view().value@.metadata == old(perm).view().value@.metadata,
1079        opens_invariants none
1080        no_unwind
1081    {
1082        self.ato.fetch_xor(n, Ordering::SeqCst)
1083    }
1084
1085    #[inline(always)]
1086    #[verifier::external_body]  /* vattr */
1087    #[verifier::atomic]  /* vattr */
1088    #[cfg(any(verus_keep_ghost, feature = "strict_provenance_atomic_ptr"))]
1089    pub fn fetch_or(&self, Tracked(perm): Tracked<&mut PermissionPtr<T>>, n: usize) -> (ret: *mut T)
1090        requires
1091            equal(self.id(), old(perm).view().patomic),
1092        ensures
1093            equal(old(perm).view().value, ret),
1094            final(perm).view().patomic == old(perm).view().patomic,
1095            final(perm).view().value@.addr == (old(perm).view().value@.addr | n),
1096            final(perm).view().value@.provenance == old(perm).view().value@.provenance,
1097            final(perm).view().value@.metadata == old(perm).view().value@.metadata,
1098        opens_invariants none
1099        no_unwind
1100    {
1101        self.ato.fetch_or(n, Ordering::SeqCst)
1102    }
1103}
1104
1105} // verus!
vstd/atomic.rs

vstd/
atomic.rs
