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) => {
513        verus!{
514    impl $at_ty {
515        /// Store a value via a raw pointer using atomic store.
516        ///
517        /// This is useful if a user wants to implement lockless algorithm for a
518        /// struct where elements are linked through pointers. In that
519        /// case, PointsTo<$value_ty> might be stored in AtomicInvariant.
520        ///
521        /// The specification is similar to raw_ptr::ptr_mut_ref,
522        /// but the implementation is atomic and so we can mark it as verifier::atomic,
523        /// and so it can be used in open_atomic_invariant!.
524        #[inline(always)]
525        #[verifier::atomic]
526        #[verifier::external_body]
527        pub fn from_ptr_store(ptr: *mut $value_ty, value: $value_ty, Tracked(perm): Tracked<&mut PointsTo<$value_ty>>)
528            requires
529                old(perm).ptr() == ptr,
530            ensures
531                value == final(perm).value(),
532                old(perm).ptr() == final(perm).ptr(),
533                final(perm).is_init(),
534            opens_invariants none
535            no_unwind
536        {
537            unsafe { $rust_ty::from_ptr(ptr).store(value, Ordering::SeqCst) }
538        }
539
540        /// Create a copy of the value via atomic load.
541        #[inline(always)]
542        #[verifier::atomic]
543        #[verifier::external_body]
544        pub fn from_ptr_load(ptr: *mut $value_ty, perm: Tracked<&PointsTo<$value_ty>>) -> (ret: $value_ty)
545            requires
546                perm.ptr() == ptr,
547                perm.is_init(),
548            ensures
549                ret == perm.value(),
550            opens_invariants none
551            no_unwind
552        {
553            unsafe { $rust_ty::from_ptr(ptr).load(Ordering::SeqCst) }
554        }
555
556        /// Swap the value via atomic swap.
557        ///
558        /// The swap reads the old value, so the memory must already be
559        /// initialized; it writes `v`, so it is initialized on return.
560        #[inline(always)]
561        #[verifier::external_body] /* vattr */
562        #[verifier::atomic] /* vattr */
563        pub fn from_ptr_swap(ptr: *mut $value_ty, Tracked(perm): Tracked<&mut PointsTo<$value_ty>>, v: $value_ty) -> (ret: $value_ty)
564            requires
565                ptr == old(perm).ptr(),
566                old(perm).is_init(),
567            ensures
568                final(perm).value() == v,
569                final(perm).is_init(),
570                old(perm).value() == ret,
571                ptr == final(perm).ptr(),
572            opens_invariants none
573            no_unwind
574        {
575            unsafe {
576                $rust_ty::from_ptr(ptr).swap(v, Ordering::SeqCst)}
577        }
578    }
579}
580    };
581}
582
583#[cfg(target_has_atomic = "64")]
584ptr_atomic_methods!(PAtomicU64, AtomicU64, u64);
585
586ptr_atomic_methods!(PAtomicU32, AtomicU32, u32);
587ptr_atomic_methods!(PAtomicU16, AtomicU16, u16);
588ptr_atomic_methods!(PAtomicU8, AtomicU8, u8);
589ptr_atomic_methods!(PAtomicUsize, AtomicUsize, usize);
590
591#[cfg(target_has_atomic = "64")]
592ptr_atomic_methods!(PAtomicI64, AtomicI64, i64);
593
594ptr_atomic_methods!(PAtomicI32, AtomicI32, i32);
595ptr_atomic_methods!(PAtomicI16, AtomicI16, i16);
596ptr_atomic_methods!(PAtomicI8, AtomicI8, i8);
597ptr_atomic_methods!(PAtomicIsize, AtomicIsize, isize);
598
599make_bool_atomic!(PAtomicBool, PermissionBool, PermissionDataBool, AtomicBool, bool);
600
601make_unsigned_integer_atomic!(PAtomicU8, PermissionU8, PermissionDataU8, AtomicU8, u8, u8_specs);
602make_unsigned_integer_atomic!(
603    PAtomicU16,
604    PermissionU16,
605    PermissionDataU16,
606    AtomicU16,
607    u16,
608    u16_specs
609);
610make_unsigned_integer_atomic!(
611    PAtomicU32,
612    PermissionU32,
613    PermissionDataU32,
614    AtomicU32,
615    u32,
616    u32_specs
617);
618
619#[cfg(target_has_atomic = "64")]
620make_unsigned_integer_atomic!(
621    PAtomicU64,
622    PermissionU64,
623    PermissionDataU64,
624    AtomicU64,
625    u64,
626    u64_specs
627);
628make_unsigned_integer_atomic!(
629    PAtomicUsize,
630    PermissionUsize,
631    PermissionDataUsize,
632    AtomicUsize,
633    usize,
634    usize_specs
635);
636
637make_signed_integer_atomic!(PAtomicI8, PermissionI8, PermissionDataI8, AtomicI8, i8, i8_specs);
638make_signed_integer_atomic!(
639    PAtomicI16,
640    PermissionI16,
641    PermissionDataI16,
642    AtomicI16,
643    i16,
644    i16_specs
645);
646make_signed_integer_atomic!(
647    PAtomicI32,
648    PermissionI32,
649    PermissionDataI32,
650    AtomicI32,
651    i32,
652    i32_specs
653);
654
655#[cfg(target_has_atomic = "64")]
656make_signed_integer_atomic!(
657    PAtomicI64,
658    PermissionI64,
659    PermissionDataI64,
660    AtomicI64,
661    i64,
662    i64_specs
663);
664make_signed_integer_atomic!(
665    PAtomicIsize,
666    PermissionIsize,
667    PermissionDataIsize,
668    AtomicIsize,
669    isize,
670    isize_specs
671);
672
673atomic_types_generic!(PAtomicPtr, PermissionPtr, PermissionDataPtr, AtomicPtr<T>, *mut T);
674
675#[cfg_attr(verus_keep_ghost, verifier::verus_macro)]
676impl<T> PAtomicPtr<T> {
677    atomic_common_methods!(
678        PAtomicPtr::<T>,
679        PermissionPtr::<T>,
680        PermissionDataPtr::<T>,
681        AtomicPtr::<T>,
682        *mut T,
683        [ .view().addr ]
684    );
685}
686
687impl<X, Y, Pred> core::fmt::Debug for AtomicUpdate<X, Y, Pred> {
688    fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
689        f.debug_struct("AtomicUpdate").finish_non_exhaustive()
690    }
691}
692
693/// Mark the `AtomicUpdate` as `Send` if both `X` and `Y` are also `Send`.
694///
695/// # SAFETY
696/// While the `AtomicUpdate` is only a stand-in for a stack of nested callback functions,
697/// when the AU is moved to another thread, e.g. by moving it in and out of an atomic invariant,
698/// it allows resources to cross thread boundaries with it,
699/// so we must ensure the AU is only `Send` when `X: Send` and `Y: Send`.
700///
701/// The predicate type we generate as part of the atomic specification only contains
702/// a ghost copy of function arguments, and ghost-mode data is always fine to move between threads.
703/// There is no need to restrict it, as it is safe by construction.
704unsafe impl<X: Send, Y: Send, Pred> Send for AtomicUpdate<X, Y, Pred> {}
705
706/// Unconditionally mark the `AtomicUpdate` as `Sync`.
707///
708/// # SAFETY
709/// A shared reference to an `AtomicUpdate` is pretty much useless.
710/// The only thing the user can do with an AU is open it, which requires full ownership.
711/// All methods provided by this type are spec-mode,
712/// meaning they can already be used with a much weaker ghost copy of the AU.
713unsafe impl<X, Y, Pred> Sync for AtomicUpdate<X, Y, Pred> {}
714
715verus! {
716
717/// The **atomic update (AU)** is a ghost object which encapsulates the linearization point of a logically atomic function.
718///
719/// 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.
720/// 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.
721/// We specify the behavior of such a function by describing the state of the program at four distinct points in time, specifically:
722/// - **(private pre)** at the start of the function,
723/// - **(atomic pre)** just before the linearization point,
724/// - **(atomic post)** just after the linearization point,
725/// - **(private post)** at the end of the function.
726/// ```
727///                        linearization point
728///                                 🠗
729/// ├──────────────────────────────┤●├─────────────────────────┤
730///  private                 atomic   atomic            private
731///  pre                        pre   post                 post
732/// ```
733/// 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.
734/// 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").
735#[verifier::reject_recursive_types(X)]
736#[verifier::reject_recursive_types(Y)]
737#[verifier::reject_recursive_types(Pred)]
738#[verifier::external_body]
739pub struct AtomicUpdate<X, Y, Pred> {
740    pred: Pred,
741    _dummy: core::marker::PhantomData<fn (fn (X) -> Y)>,
742    _not_send_sync: core::marker::PhantomData<*const ()>,
743}
744
745impl<X, Y, Pred> AtomicUpdate<X, Y, Pred> {
746    /// The predicate of the atomic update.
747    ///
748    /// See [`UpdatePredicate`] for more information.
749    #[rustc_diagnostic_item = "verus::vstd::atomic::AtomicUpdate::pred"]
750    pub uninterp spec fn pred(self) -> Pred;
751
752    /// A prophesy variable which indicates that an atomic update has been resolved.
753    ///
754    /// Initially, the value of this function is unknown, i.e. we can neither prove that it is `true` or `false`.
755    /// Once the atomic update has been committed using the [`try_open_atomic_update`] macro, we learn that `au.resolves()` is `true`.
756    ///
757    /// We must be able to prove that `au.resolves()` when the logically atomic function exits.
758    #[rustc_diagnostic_item = "verus::vstd::atomic::AtomicUpdate::resolves"]
759    pub uninterp spec fn resolves(self) -> bool;
760
761    /// A prophesy variable for the input value of the atomic update.
762    ///
763    /// When the atomic update is committed, this variable is resolved to the input value of the atomic update.
764    /// This variable is used internally in the (private) postcondition of the logically atomic function.
765    #[rustc_diagnostic_item = "verus::vstd::atomic::AtomicUpdate::input"]
766    pub uninterp spec fn input(self) -> X;
767
768    /// A prophesy variable for the output value of the atomic update.
769    ///
770    /// When the atomic update is committed, this variable is resolved to the output value of the atomic update.
771    /// This variable is used internally in the (private) postcondition of the logically atomic function.
772    #[rustc_diagnostic_item = "verus::vstd::atomic::AtomicUpdate::output"]
773    pub uninterp spec fn output(self) -> Y;
774}
775
776impl<X, Y, Pred: UpdatePredicate<X, Y>> AtomicUpdate<X, Y, Pred> {
777    #[rustc_diagnostic_item = "verus::vstd::atomic::AtomicUpdate::req"]
778    pub open spec fn req(self, x: X) -> bool {
779        self.pred().req(x)
780    }
781
782    #[rustc_diagnostic_item = "verus::vstd::atomic::AtomicUpdate::ens"]
783    pub open spec fn ens(self, x: X, y: Y) -> bool {
784        self.pred().ens(x, y)
785    }
786
787    #[rustc_diagnostic_item = "verus::vstd::atomic::AtomicUpdate::outer_mask"]
788    pub open spec fn outer_mask(self) -> ISet<int> {
789        self.pred().outer_mask()
790    }
791
792    #[rustc_diagnostic_item = "verus::vstd::atomic::AtomicUpdate::inner_mask"]
793    pub open spec fn inner_mask(self) -> ISet<int> {
794        self.pred().inner_mask()
795    }
796}
797
798#[cfg(verus_keep_ghost)]
799#[rustc_diagnostic_item = "verus::vstd::atomic::pred_args"]
800#[doc(hidden)]
801pub uninterp spec fn pred_args<Pred, Args>(pred: Pred) -> Args;
802
803/// Trait used to specify the update predicate for the [`AtomicUpdate`].
804///
805/// This trait is implemented automatically by Verus when a logically atomic function is defined.
806/// ```
807/// exec fn function(px: PX) -> (py: PY)
808///     atomically (atomic_update) {
809///         type PredType,
810///
811///         (ax: AX) -> (ay: AY),
812///
813///         requires atomic_pre(px, ax),
814///         ensures atomic_post(px, ax, ay),
815///
816///         outer_mask Eo,
817///         inner_mask Ei,
818///     },
819///     requires private_pre(px),
820///     ensures private_post(px, ax, ay, py),
821/// ```
822/// The above code snipped generates (roughly) the type and trait implementation below.
823/// ```
824/// struct PredType { px: Ghost<PX> }
825///
826/// impl UpdatePredicate<AX, AY> for PredType {
827///     open spec fn req(self, x: X)       -> bool { atomic_pre  }
828///     open spec fn ens(self, x: X, y: Y) -> bool { atomic_post }
829///
830///     open spec fn outer_mask(self) -> ISet<int> { Eo }
831///     open spec fn inner_mask(self) -> ISet<int> { Ei }
832/// }
833/// ```
834pub trait UpdatePredicate<X, Y>: Sized {
835    /// The atomic pre-condition.
836    spec fn req(self, x: X) -> bool;
837
838    /// The atomic post-condition.
839    spec fn ens(self, x: X, y: Y) -> bool;
840
841    /// The outer mask of the atomic update.
842    open spec fn outer_mask(self) -> ISet<int> {
843        ISet::empty()
844    }
845
846    /// The inner mask of the atomic update.
847    open spec fn inner_mask(self) -> ISet<int> {
848        ISet::empty()
849    }
850}
851
852/// The control flow corresponding to the atomic update output.
853pub enum UpdateControlFlow {
854    /// The update output value indicates that the atomic update has been committed.
855    ///
856    /// This means [`try_open_atomic_update`] will consume the atomic update (i.e. return `Ok(())`),
857    /// and the atomic function call has to `break`.
858    Commit,
859    /// The update output value indicates that the atomic update has been aborted.
860    ///
861    /// This means [`try_open_atomic_update`] will give back the atomic update (i.e. return `Err(Tracked(au))`),
862    /// and the atomic function call has to `continue`.
863    Abort,
864}
865
866impl UpdateControlFlow {
867    pub open spec fn is_commit(self) -> bool {
868        match self {
869            UpdateControlFlow::Commit => true,
870            UpdateControlFlow::Abort => false,
871        }
872    }
873
874    pub open spec fn is_abort(self) -> bool {
875        !self.is_commit()
876    }
877}
878
879pub trait UpdateTry {
880    spec fn branch(self) -> UpdateControlFlow;
881}
882
883impl<T, E> UpdateTry for Result<T, E> {
884    open spec fn branch(self) -> UpdateControlFlow {
885        match self {
886            Ok(_) => UpdateControlFlow::Commit,
887            Err(_) => UpdateControlFlow::Abort,
888        }
889    }
890}
891
892/// A trivial wrapper type which indicates a commit.
893///
894/// This is useful for logically atomic functions which do not require an abort case.
895#[derive(Debug)]
896pub struct Commit<T>(pub T);
897
898impl<T> Commit<T> {
899    pub proof fn get(tracked self) -> (tracked out: T)
900        ensures
901            self@ == out,
902    {
903        self.0
904    }
905}
906
907impl<T> View for Commit<T> {
908    type V = T;
909
910    #[verifier::inline]
911    open spec fn view(&self) -> T {
912        self.0
913    }
914}
915
916impl<T> UpdateTry for Commit<T> {
917    open spec fn branch(self) -> UpdateControlFlow {
918        UpdateControlFlow::Commit
919    }
920}
921
922impl UpdateTry for () {
923    open spec fn branch(self) -> UpdateControlFlow {
924        UpdateControlFlow::Commit
925    }
926}
927
928#[cfg(verus_keep_ghost)]
929#[rustc_diagnostic_item = "verus::vstd::atomic::branch_bool"]
930#[doc(hidden)]
931pub open spec fn branch_bool<T: UpdateTry>(this: T) -> bool {
932    this.branch().is_commit()
933}
934
935// Definition for atomic function call
936#[cfg(verus_keep_ghost)]
937#[rustc_diagnostic_item = "verus::vstd::atomic::atomically"]
938#[doc(hidden)]
939#[verifier::external]
940pub fn atomically<X, Y: UpdateTry, P: UpdatePredicate<X, Y>>(
941    _body: impl FnOnce(fn (X) -> Y, Ghost<AtomicUpdate<X, Y, P>>),
942) -> AtomicUpdate<X, Y, P> {
943    arbitrary()
944}
945
946// Definitions for `try_open_atomic_update` macro
947#[doc(hidden)]
948pub struct BlockGuard<T> {
949    _inner: core::marker::PhantomData<T>,
950}
951
952#[cfg(verus_keep_ghost)]
953#[doc(hidden)]
954#[verifier::external]  /* vattr */
955pub fn bind_lifetime_internal<'a, X: 'a, Y, P>(
956    _block_guard: &'a BlockGuard<AtomicUpdate<X, Y, P>>,
957) -> X {
958    unimplemented!()
959}
960
961#[cfg(verus_keep_ghost)]
962#[rustc_diagnostic_item = "verus::vstd::atomic::try_open_atomic_update_begin"]
963#[doc(hidden)]
964#[verifier::external]  /* vattr */
965pub fn try_open_atomic_update_begin<X, Y: UpdateTry, P: UpdatePredicate<X, Y>>(
966    _atomic_update: AtomicUpdate<X, Y, P>,
967) -> BlockGuard<AtomicUpdate<X, Y, P>> {
968    unimplemented!()
969}
970
971#[cfg(verus_keep_ghost)]
972#[rustc_diagnostic_item = "verus::vstd::atomic::try_open_atomic_update_end"]
973#[doc(hidden)]
974#[verifier::external]  /* vattr */
975pub fn try_open_atomic_update_end<X, Y: UpdateTry, P: UpdatePredicate<X, Y>>(
976    _guard: BlockGuard<AtomicUpdate<X, Y, P>>,
977    _y: Tracked<Y>,
978) -> Tracked<Result<(), AtomicUpdate<X, Y, P>>> {
979    unimplemented!()
980}
981
982// Macro definitions
983#[macro_export]
984macro_rules! open_atomic_update {
985    ($($tail:tt)*) => {
986        {
987            let _ = ::verus_builtin_macros::verus_exec_open_au_macro_exprs!(
988                $crate::atomic::try_open_atomic_update_internal!(
989                    $($tail)*, @EXEC, au_commit_wrap_exec
990                )
991            );
992        }
993    };
994}
995
996#[macro_export]
997macro_rules! open_atomic_update_in_proof {
998    ($($tail:tt)*) => {
999        {
1000            let _ = ::verus_builtin_macros::verus_ghost_open_au_macro_exprs!(
1001                $crate::atomic::try_open_atomic_update_internal!(
1002                    $($tail)*, @PROOF, au_commit_wrap_proof
1003                )
1004            );
1005        }
1006    };
1007}
1008
1009#[macro_export]
1010macro_rules! peek_atomic_update {
1011    ($($tail:tt)*) => {
1012        {
1013            #[verifier::exec]
1014            let err_au = ::verus_builtin_macros::verus_exec_open_au_macro_exprs!(
1015                $crate::atomic::try_open_atomic_update_internal!(
1016                    $($tail)*, @EXEC, au_abort_wrap_exec
1017                )
1018            );
1019
1020            match () {
1021                #[cfg(verus_keep_ghost_body)]
1022                _ => $crate::atomic::au_abort_unwrap_exec(err_au),
1023
1024                #[cfg(not(verus_keep_ghost_body))]
1025                _ => ::verus_builtin::Tracked::assume_new_fallback(|| ::core::unreachable!()),
1026            }
1027        }
1028    };
1029}
1030
1031#[macro_export]
1032macro_rules! peek_atomic_update_in_proof {
1033    ($($tail:tt)*) => {
1034        {
1035            #[verifier::proof]
1036            let err_au = ::verus_builtin_macros::verus_ghost_open_au_macro_exprs!(
1037                $crate::atomic::try_open_atomic_update_internal!(
1038                    $($tail)*, @PROOF, au_abort_wrap_proof
1039                )
1040            );
1041
1042            match () {
1043                #[cfg(verus_keep_ghost_body)]
1044                _ => $crate::atomic::au_abort_unwrap_proof(err_au),
1045
1046                #[cfg(not(verus_keep_ghost_body))]
1047                _ => ::verus_builtin::Tracked::assume_new_fallback(|| ::core::unreachable!()),
1048            }
1049        }
1050    };
1051}
1052
1053#[macro_export]
1054macro_rules! try_open_atomic_update {
1055    ($($tail:tt)*) => {
1056        ::verus_builtin_macros::verus_exec_open_au_macro_exprs!(
1057            $crate::atomic::try_open_atomic_update_internal!($($tail)*)
1058        )
1059    };
1060}
1061
1062#[macro_export]
1063macro_rules! try_open_atomic_update_in_proof {
1064    ($($tail:tt)*) => {
1065        ::verus_builtin_macros::verus_ghost_open_au_macro_exprs!(
1066            $crate::atomic::try_open_atomic_update_internal!($($tail)*)
1067        )
1068    };
1069}
1070
1071#[macro_export]
1072macro_rules! try_open_atomic_update_internal {
1073    ($au:expr, $x:pat => $body:block, @EXEC, $wrap_fn:ident) => {
1074        $crate::atomic::try_open_atomic_update_internal!($au, $x => {
1075            #[verifier::exec]
1076            let v = $body;
1077
1078            match () {
1079                #[cfg(verus_keep_ghost_body)]
1080                _ => $crate::atomic::$wrap_fn(v),
1081
1082                #[cfg(not(verus_keep_ghost_body))]
1083                _ => ::verus_builtin::Tracked::assume_new_fallback(|| ::core::unreachable!()),
1084            }
1085        })
1086    };
1087
1088    ($au:expr, $x:pat => $body:block, @PROOF, $wrap_fn:ident) => {
1089        $crate::atomic::try_open_atomic_update_internal!($au, $x => {
1090            #[verifier::proof]
1091            let v = $body;
1092
1093            match () {
1094                #[cfg(verus_keep_ghost_body)]
1095                _ => $crate::atomic::$wrap_fn(v),
1096
1097                #[cfg(not(verus_keep_ghost_body))]
1098                _ => ::verus_builtin::Tracked::assume_new_fallback(|| ::core::unreachable!()),
1099            }
1100        })
1101    };
1102
1103    ($au:expr, $x:pat => $body:block) => {
1104        #[cfg_attr(verus_keep_ghost, verifier::open_au_block)] /* vattr */ {
1105            #[cfg(verus_keep_ghost_body)]
1106            let guard = $crate::atomic::try_open_atomic_update_begin($au);
1107            #[cfg(verus_keep_ghost_body)]
1108            let $x = $crate::atomic::bind_lifetime_internal(&guard);
1109            let res = $body;
1110
1111            match res {
1112                #[cfg(verus_keep_ghost_body)]
1113                res => $crate::atomic::try_open_atomic_update_end(guard, res),
1114
1115                #[cfg(not(verus_keep_ghost_body))]
1116                _ => ::verus_builtin::Tracked::assume_new_fallback(|| ::core::unreachable!()),
1117            }
1118        }
1119    };
1120}
1121
1122#[doc(hidden)]
1123pub use {try_open_atomic_update_internal};
1124pub use {
1125    open_atomic_update,
1126    open_atomic_update_in_proof,
1127    peek_atomic_update,
1128    peek_atomic_update_in_proof,
1129    try_open_atomic_update,
1130    try_open_atomic_update_in_proof,
1131};
1132
1133impl<T> PAtomicPtr<T> {
1134    #[inline(always)]
1135    #[verifier::external_body]  /* vattr */
1136    #[verifier::atomic]  /* vattr */
1137    #[cfg(any(verus_keep_ghost, feature = "strict_provenance_atomic_ptr"))]
1138    pub fn fetch_and(&self, Tracked(perm): Tracked<&mut PermissionPtr<T>>, n: usize) -> (ret:
1139        *mut T)
1140        requires
1141            equal(self.id(), old(perm).view().patomic),
1142        ensures
1143            equal(old(perm).view().value, ret),
1144            final(perm).view().patomic == old(perm).view().patomic,
1145            final(perm).view().value@.addr == (old(perm).view().value@.addr & n),
1146            final(perm).view().value@.provenance == old(perm).view().value@.provenance,
1147            final(perm).view().value@.metadata == old(perm).view().value@.metadata,
1148        opens_invariants none
1149        no_unwind
1150    {
1151        self.ato.fetch_and(n, Ordering::SeqCst)
1152    }
1153
1154    #[inline(always)]
1155    #[verifier::external_body]  /* vattr */
1156    #[verifier::atomic]  /* vattr */
1157    #[cfg(any(verus_keep_ghost, feature = "strict_provenance_atomic_ptr"))]
1158    pub fn fetch_xor(&self, Tracked(perm): Tracked<&mut PermissionPtr<T>>, n: usize) -> (ret:
1159        *mut T)
1160        requires
1161            equal(self.id(), old(perm).view().patomic),
1162        ensures
1163            equal(old(perm).view().value, ret),
1164            final(perm).view().patomic == old(perm).view().patomic,
1165            final(perm).view().value@.addr == (old(perm).view().value@.addr ^ n),
1166            final(perm).view().value@.provenance == old(perm).view().value@.provenance,
1167            final(perm).view().value@.metadata == old(perm).view().value@.metadata,
1168        opens_invariants none
1169        no_unwind
1170    {
1171        self.ato.fetch_xor(n, Ordering::SeqCst)
1172    }
1173
1174    #[inline(always)]
1175    #[verifier::external_body]  /* vattr */
1176    #[verifier::atomic]  /* vattr */
1177    #[cfg(any(verus_keep_ghost, feature = "strict_provenance_atomic_ptr"))]
1178    pub fn fetch_or(&self, Tracked(perm): Tracked<&mut PermissionPtr<T>>, n: usize) -> (ret: *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_or(n, Ordering::SeqCst)
1191    }
1192}
1193
1194} // verus!
vstd/atomic.rs

vstd/
atomic.rs
