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#[doc(hidden)]
737#[verifier::external_body]
738pub struct AtomicUpdateLifetimeMarker<'a> {
739    _marker: core::marker::PhantomData<fn (&'a ())>,
740}
741
742/// The **atomic update (AU)** is a ghost object which encapsulates the linearization point of a logically atomic function.
743///
744/// 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.
745/// 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.
746/// We specify the behavior of such a function by describing the state of the program at four distinct points in time, specifically:
747/// - **(private pre)** at the start of the function,
748/// - **(atomic pre)** just before the linearization point,
749/// - **(atomic post)** just after the linearization point,
750/// - **(private post)** at the end of the function.
751/// ```
752///                        linearization point
753///                                 🠗
754/// ├──────────────────────────────┤●├─────────────────────────┤
755///  private                 atomic   atomic            private
756///  pre                        pre   post                 post
757/// ```
758/// 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.
759/// 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").
760#[verifier::reject_recursive_types(X)]
761#[verifier::reject_recursive_types(Y)]
762#[verifier::reject_recursive_types(Pred)]
763#[verifier::external_body]
764pub struct AtomicUpdate<X, Y, Pred> {
765    pred: Pred,
766    _dummy: core::marker::PhantomData<fn (fn (X) -> Y)>,
767    _not_send_sync: core::marker::PhantomData<*const ()>,
768}
769
770impl<X, Y, Pred> AtomicUpdate<X, Y, Pred> {
771    /// The predicate of the atomic update.
772    ///
773    /// See [`UpdatePredicate`] for more information.
774    #[rustc_diagnostic_item = "verus::vstd::atomic::AtomicUpdate::pred"]
775    pub uninterp spec fn pred(self) -> Pred;
776
777    /// A prophesy variable which indicates that an atomic update has been resolved.
778    ///
779    /// Initially, the value of this function is unknown, i.e. we can neither prove that it is `true` or `false`.
780    /// Once the atomic update has been committed using the [`try_open_atomic_update`] macro, we learn that `au.resolves()` is `true`.
781    ///
782    /// We must be able to prove that `au.resolves()` when the logically atomic function exits.
783    #[rustc_diagnostic_item = "verus::vstd::atomic::AtomicUpdate::resolves"]
784    pub uninterp spec fn resolves(self) -> bool;
785
786    /// A prophesy variable for the input value of the atomic update.
787    ///
788    /// When the atomic update is committed, this variable is resolved to the input value of the atomic update.
789    /// This variable is used internally in the (private) postcondition of the logically atomic function.
790    #[rustc_diagnostic_item = "verus::vstd::atomic::AtomicUpdate::input"]
791    pub uninterp spec fn input(self) -> X;
792
793    /// A prophesy variable for the output value of the atomic update.
794    ///
795    /// When the atomic update is committed, this variable is resolved to the output value of the atomic update.
796    /// This variable is used internally in the (private) postcondition of the logically atomic function.
797    #[rustc_diagnostic_item = "verus::vstd::atomic::AtomicUpdate::output"]
798    pub uninterp spec fn output(self) -> Y;
799}
800
801impl<X, Y, Pred: UpdatePredicate<X, Y>> AtomicUpdate<X, Y, Pred> {
802    #[rustc_diagnostic_item = "verus::vstd::atomic::AtomicUpdate::req"]
803    pub open spec fn req(self, x: X) -> bool {
804        self.pred().req(x)
805    }
806
807    #[rustc_diagnostic_item = "verus::vstd::atomic::AtomicUpdate::ens"]
808    pub open spec fn ens(self, x: X, y: Y) -> bool {
809        self.pred().ens(x, y)
810    }
811
812    #[rustc_diagnostic_item = "verus::vstd::atomic::AtomicUpdate::outer_mask"]
813    pub open spec fn outer_mask(self) -> ISet<int> {
814        self.pred().outer_mask()
815    }
816
817    #[rustc_diagnostic_item = "verus::vstd::atomic::AtomicUpdate::inner_mask"]
818    pub open spec fn inner_mask(self) -> ISet<int> {
819        self.pred().inner_mask()
820    }
821}
822
823#[cfg(verus_keep_ghost)]
824#[rustc_diagnostic_item = "verus::vstd::atomic::pred_args"]
825#[doc(hidden)]
826pub uninterp spec fn pred_args<Pred, Args>(pred: Pred) -> Args;
827
828/// Trait used to specify the update predicate for the [`AtomicUpdate`].
829///
830/// This trait is implemented automatically by Verus when a logically atomic function is defined.
831/// ```
832/// exec fn function(px: PX) -> (py: PY)
833///     atomically (atomic_update) {
834///         type PredType,
835///
836///         (ax: AX) -> (ay: AY),
837///
838///         requires atomic_pre(px, ax),
839///         ensures atomic_post(px, ax, ay),
840///
841///         outer_mask Eo,
842///         inner_mask Ei,
843///     },
844///     requires private_pre(px),
845///     ensures private_post(px, ax, ay, py),
846/// ```
847/// The above code snipped generates (roughly) the type and trait implementation below.
848/// ```
849/// struct PredType { px: Ghost<PX> }
850///
851/// impl UpdatePredicate<AX, AY> for PredType {
852///     open spec fn req(self, x: X)       -> bool { atomic_pre  }
853///     open spec fn ens(self, x: X, y: Y) -> bool { atomic_post }
854///
855///     open spec fn outer_mask(self) -> ISet<int> { Eo }
856///     open spec fn inner_mask(self) -> ISet<int> { Ei }
857/// }
858/// ```
859pub trait UpdatePredicate<X, Y>: Sized {
860    /// The atomic pre-condition.
861    spec fn req(self, x: X) -> bool;
862
863    /// The atomic post-condition.
864    spec fn ens(self, x: X, y: Y) -> bool;
865
866    /// The outer mask of the atomic update.
867    open spec fn outer_mask(self) -> ISet<int> {
868        ISet::empty()
869    }
870
871    /// The inner mask of the atomic update.
872    open spec fn inner_mask(self) -> ISet<int> {
873        ISet::empty()
874    }
875}
876
877/// The control flow corresponding to the atomic update output.
878pub enum UpdateControlFlow {
879    /// The update output value indicates that the atomic update has been committed.
880    ///
881    /// This means [`try_open_atomic_update`] will consume the atomic update (i.e. return `Ok(())`),
882    /// and the atomic function call has to `break`.
883    Commit,
884    /// The update output value indicates that the atomic update has been aborted.
885    ///
886    /// This means [`try_open_atomic_update`] will give back the atomic update (i.e. return `Err(Tracked(au))`),
887    /// and the atomic function call has to `continue`.
888    Abort,
889}
890
891impl UpdateControlFlow {
892    pub open spec fn is_commit(self) -> bool {
893        match self {
894            UpdateControlFlow::Commit => true,
895            UpdateControlFlow::Abort => false,
896        }
897    }
898
899    pub open spec fn is_abort(self) -> bool {
900        !self.is_commit()
901    }
902}
903
904pub trait UpdateTry {
905    spec fn branch(self) -> UpdateControlFlow;
906}
907
908impl<T, E> UpdateTry for Result<T, E> {
909    open spec fn branch(self) -> UpdateControlFlow {
910        match self {
911            Ok(_) => UpdateControlFlow::Commit,
912            Err(_) => UpdateControlFlow::Abort,
913        }
914    }
915}
916
917/// A trivial wrapper type which indicates a commit.
918///
919/// This is useful for logically atomic functions which do not require an abort case.
920#[derive(Debug)]
921pub struct Commit<T>(pub T);
922
923impl<T> Commit<T> {
924    pub proof fn get(tracked self) -> (tracked out: T)
925        ensures
926            self@ == out,
927    {
928        self.0
929    }
930}
931
932impl<T> View for Commit<T> {
933    type V = T;
934
935    #[verifier::inline]
936    open spec fn view(&self) -> T {
937        self.0
938    }
939}
940
941impl<T> UpdateTry for Commit<T> {
942    open spec fn branch(self) -> UpdateControlFlow {
943        UpdateControlFlow::Commit
944    }
945}
946
947impl UpdateTry for () {
948    open spec fn branch(self) -> UpdateControlFlow {
949        UpdateControlFlow::Commit
950    }
951}
952
953#[cfg(verus_keep_ghost)]
954#[rustc_diagnostic_item = "verus::vstd::atomic::branch_bool"]
955#[doc(hidden)]
956pub open spec fn branch_bool<T: UpdateTry>(this: T) -> bool {
957    this.branch().is_commit()
958}
959
960// Definition for atomic function call
961#[cfg(verus_keep_ghost)]
962#[rustc_diagnostic_item = "verus::vstd::atomic::atomically"]
963#[doc(hidden)]
964#[verifier::external]
965pub fn atomically<X, Y: UpdateTry, P: UpdatePredicate<X, Y>>(
966    _body: impl FnOnce(fn (X) -> Y, Ghost<AtomicUpdate<X, Y, P>>),
967) -> AtomicUpdate<X, Y, P> {
968    arbitrary()
969}
970
971// Definitions for `try_open_atomic_update` macro
972#[doc(hidden)]
973pub struct BlockGuard<T> {
974    _inner: core::marker::PhantomData<T>,
975}
976
977#[cfg(verus_keep_ghost)]
978#[doc(hidden)]
979#[verifier::external]  /* vattr */
980pub fn bind_lifetime_internal<'a, X: 'a, Y, P>(
981    _block_guard: &'a BlockGuard<AtomicUpdate<X, Y, P>>,
982) -> X {
983    unimplemented!()
984}
985
986#[cfg(verus_keep_ghost)]
987#[rustc_diagnostic_item = "verus::vstd::atomic::try_open_atomic_update_begin"]
988#[doc(hidden)]
989#[verifier::external]  /* vattr */
990pub fn try_open_atomic_update_begin<X, Y: UpdateTry, P: UpdatePredicate<X, Y>>(
991    _atomic_update: AtomicUpdate<X, Y, P>,
992) -> BlockGuard<AtomicUpdate<X, Y, P>> {
993    unimplemented!()
994}
995
996#[cfg(verus_keep_ghost)]
997#[rustc_diagnostic_item = "verus::vstd::atomic::try_open_atomic_update_end"]
998#[doc(hidden)]
999#[verifier::external]  /* vattr */
1000pub fn try_open_atomic_update_end<X, Y: UpdateTry, P: UpdatePredicate<X, Y>>(
1001    _guard: BlockGuard<AtomicUpdate<X, Y, P>>,
1002    _y: Tracked<Y>,
1003) -> Tracked<Result<(), AtomicUpdate<X, Y, P>>> {
1004    unimplemented!()
1005}
1006
1007// Macro definitions
1008#[macro_export]
1009macro_rules! open_atomic_update {
1010    ($($tail:tt)*) => {
1011        {
1012            let _ = ::verus_builtin_macros::verus_exec_open_au_macro_exprs!(
1013                $crate::atomic::try_open_atomic_update_internal!(
1014                    $($tail)*, @EXEC, au_commit_wrap_exec
1015                )
1016            );
1017        }
1018    };
1019}
1020
1021#[macro_export]
1022macro_rules! open_atomic_update_in_proof {
1023    ($($tail:tt)*) => {
1024        {
1025            let _ = ::verus_builtin_macros::verus_ghost_open_au_macro_exprs!(
1026                $crate::atomic::try_open_atomic_update_internal!(
1027                    $($tail)*, @PROOF, au_commit_wrap_proof
1028                )
1029            );
1030        }
1031    };
1032}
1033
1034#[macro_export]
1035macro_rules! peek_atomic_update {
1036    ($($tail:tt)*) => {
1037        {
1038            #[verifier::exec]
1039            let err_au = ::verus_builtin_macros::verus_exec_open_au_macro_exprs!(
1040                $crate::atomic::try_open_atomic_update_internal!(
1041                    $($tail)*, @EXEC, au_abort_wrap_exec
1042                )
1043            );
1044
1045            match () {
1046                #[cfg(verus_keep_ghost_body)]
1047                _ => $crate::atomic::au_abort_unwrap_exec(err_au),
1048
1049                #[cfg(not(verus_keep_ghost_body))]
1050                _ => ::verus_builtin::Tracked::assume_new_fallback(|| ::core::unreachable!()),
1051            }
1052        }
1053    };
1054}
1055
1056#[macro_export]
1057macro_rules! peek_atomic_update_in_proof {
1058    ($($tail:tt)*) => {
1059        {
1060            #[verifier::proof]
1061            let err_au = ::verus_builtin_macros::verus_ghost_open_au_macro_exprs!(
1062                $crate::atomic::try_open_atomic_update_internal!(
1063                    $($tail)*, @PROOF, au_abort_wrap_proof
1064                )
1065            );
1066
1067            match () {
1068                #[cfg(verus_keep_ghost_body)]
1069                _ => $crate::atomic::au_abort_unwrap_proof(err_au),
1070
1071                #[cfg(not(verus_keep_ghost_body))]
1072                _ => ::verus_builtin::Tracked::assume_new_fallback(|| ::core::unreachable!()),
1073            }
1074        }
1075    };
1076}
1077
1078#[macro_export]
1079macro_rules! try_open_atomic_update {
1080    ($($tail:tt)*) => {
1081        ::verus_builtin_macros::verus_exec_open_au_macro_exprs!(
1082            $crate::atomic::try_open_atomic_update_internal!($($tail)*)
1083        )
1084    };
1085}
1086
1087#[macro_export]
1088macro_rules! try_open_atomic_update_in_proof {
1089    ($($tail:tt)*) => {
1090        ::verus_builtin_macros::verus_ghost_open_au_macro_exprs!(
1091            $crate::atomic::try_open_atomic_update_internal!($($tail)*)
1092        )
1093    };
1094}
1095
1096#[macro_export]
1097macro_rules! try_open_atomic_update_internal {
1098    ($au:expr, $x:pat => $body:block, @EXEC, $wrap_fn:ident) => {
1099        $crate::atomic::try_open_atomic_update_internal!($au, $x => {
1100            #[verifier::exec]
1101            let v = $body;
1102
1103            match () {
1104                #[cfg(verus_keep_ghost_body)]
1105                _ => $crate::atomic::$wrap_fn(v),
1106
1107                #[cfg(not(verus_keep_ghost_body))]
1108                _ => ::verus_builtin::Tracked::assume_new_fallback(|| ::core::unreachable!()),
1109            }
1110        })
1111    };
1112
1113    ($au:expr, $x:pat => $body:block, @PROOF, $wrap_fn:ident) => {
1114        $crate::atomic::try_open_atomic_update_internal!($au, $x => {
1115            #[verifier::proof]
1116            let v = $body;
1117
1118            match () {
1119                #[cfg(verus_keep_ghost_body)]
1120                _ => $crate::atomic::$wrap_fn(v),
1121
1122                #[cfg(not(verus_keep_ghost_body))]
1123                _ => ::verus_builtin::Tracked::assume_new_fallback(|| ::core::unreachable!()),
1124            }
1125        })
1126    };
1127
1128    ($au:expr, $x:pat => $body:block) => {
1129        #[cfg_attr(verus_keep_ghost, verifier::open_au_block)] /* vattr */ {
1130            #[cfg(verus_keep_ghost_body)]
1131            let guard = $crate::atomic::try_open_atomic_update_begin($au);
1132            #[cfg(verus_keep_ghost_body)]
1133            let $x = $crate::atomic::bind_lifetime_internal(&guard);
1134            let res = $body;
1135
1136            match res {
1137                #[cfg(verus_keep_ghost_body)]
1138                res => $crate::atomic::try_open_atomic_update_end(guard, res),
1139
1140                #[cfg(not(verus_keep_ghost_body))]
1141                _ => ::verus_builtin::Tracked::assume_new_fallback(|| ::core::unreachable!()),
1142            }
1143        }
1144    };
1145}
1146
1147#[doc(hidden)]
1148pub use {try_open_atomic_update_internal};
1149pub use {
1150    open_atomic_update,
1151    open_atomic_update_in_proof,
1152    peek_atomic_update,
1153    peek_atomic_update_in_proof,
1154    try_open_atomic_update,
1155    try_open_atomic_update_in_proof,
1156};
1157
1158impl<T> PAtomicPtr<T> {
1159    #[inline(always)]
1160    #[verifier::external_body]  /* vattr */
1161    #[verifier::atomic]  /* vattr */
1162    #[cfg(any(verus_keep_ghost, feature = "strict_provenance_atomic_ptr"))]
1163    pub fn fetch_and(&self, Tracked(perm): Tracked<&mut PermissionPtr<T>>, n: usize) -> (ret:
1164        *mut T)
1165        requires
1166            equal(self.id(), old(perm).view().patomic),
1167        ensures
1168            equal(old(perm).view().value, ret),
1169            final(perm).view().patomic == old(perm).view().patomic,
1170            final(perm).view().value@.addr == (old(perm).view().value@.addr & n),
1171            final(perm).view().value@.provenance == old(perm).view().value@.provenance,
1172            final(perm).view().value@.metadata == old(perm).view().value@.metadata,
1173        opens_invariants none
1174        no_unwind
1175    {
1176        self.ato.fetch_and(n, Ordering::SeqCst)
1177    }
1178
1179    #[inline(always)]
1180    #[verifier::external_body]  /* vattr */
1181    #[verifier::atomic]  /* vattr */
1182    #[cfg(any(verus_keep_ghost, feature = "strict_provenance_atomic_ptr"))]
1183    pub fn fetch_xor(&self, Tracked(perm): Tracked<&mut PermissionPtr<T>>, n: usize) -> (ret:
1184        *mut T)
1185        requires
1186            equal(self.id(), old(perm).view().patomic),
1187        ensures
1188            equal(old(perm).view().value, ret),
1189            final(perm).view().patomic == old(perm).view().patomic,
1190            final(perm).view().value@.addr == (old(perm).view().value@.addr ^ n),
1191            final(perm).view().value@.provenance == old(perm).view().value@.provenance,
1192            final(perm).view().value@.metadata == old(perm).view().value@.metadata,
1193        opens_invariants none
1194        no_unwind
1195    {
1196        self.ato.fetch_xor(n, Ordering::SeqCst)
1197    }
1198
1199    #[inline(always)]
1200    #[verifier::external_body]  /* vattr */
1201    #[verifier::atomic]  /* vattr */
1202    #[cfg(any(verus_keep_ghost, feature = "strict_provenance_atomic_ptr"))]
1203    pub fn fetch_or(&self, Tracked(perm): Tracked<&mut PermissionPtr<T>>, n: usize) -> (ret: *mut T)
1204        requires
1205            equal(self.id(), old(perm).view().patomic),
1206        ensures
1207            equal(old(perm).view().value, ret),
1208            final(perm).view().patomic == old(perm).view().patomic,
1209            final(perm).view().value@.addr == (old(perm).view().value@.addr | n),
1210            final(perm).view().value@.provenance == old(perm).view().value@.provenance,
1211            final(perm).view().value@.metadata == old(perm).view().value@.metadata,
1212        opens_invariants none
1213        no_unwind
1214    {
1215        self.ato.fetch_or(n, Ordering::SeqCst)
1216    }
1217}
1218
1219} // verus!
vstd/atomic.rs

vstd/
atomic.rs
