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

vstd/
atomic.rs
