vstd/std_specs/
atomic.rs

1#![allow(unused_imports)]
2use super::super::prelude::*;
3use core::sync::atomic::*;
4
5// Supports the core::sync::atomic functions
6// This provides NO support for reasoning about the values inside the atomics.
7// If you need to do that, see `vstd::atomic` or `vstd::atomic_ghost` instead.
8#[verifier::external_type_specification]
9#[verifier::external_body]
10#[verifier::reject_recursive_types(T)]
11pub struct ExAtomic<T: AtomicPrimitive>(Atomic<T>);
12
13#[verifier::external_trait_specification]
14pub trait ExAtomicPrimitive: Sized + Copy {
15    type ExternalTraitSpecificationFor: AtomicPrimitive;
16}
17
18#[verifier::external_type_specification]
19pub struct ExOrdering(Ordering);
20
21macro_rules! atomic_specs_common {
22    ($at:ty, $ty:ty) => {
23        verus!{
24
25        // Panic preconditions per the std docs: load rejects Release/AcqRel, store rejects
26        // Acquire/AcqRel, and compare_exchange(_weak) rejects Release/AcqRel as `failure`.
27        pub assume_specification [ <$at>::new ](v: $ty) -> $at
28            no_unwind;
29
30        pub assume_specification [ <$at>::compare_exchange ](
31            atomic: &$at,
32            current: $ty,
33            new: $ty,
34            success: Ordering,
35            failure: Ordering,
36        ) -> Result<$ty, $ty>
37            requires
38                failure != Ordering::Release,
39                failure != Ordering::AcqRel,
40            no_unwind;
41
42        pub assume_specification [ <$at>::compare_exchange_weak ](
43            atomic: &$at,
44            current: $ty,
45            new: $ty,
46            success: Ordering,
47            failure: Ordering,
48        ) -> Result<$ty, $ty>
49            requires
50                failure != Ordering::Release,
51                failure != Ordering::AcqRel,
52            no_unwind;
53
54        pub assume_specification [ <$at>::fetch_and ](atomic: &$at, val: $ty, order: Ordering) -> $ty
55            no_unwind;
56
57        pub assume_specification [ <$at>::fetch_nand ](atomic: &$at, val: $ty, order: Ordering) -> $ty
58            no_unwind;
59
60        pub assume_specification [ <$at>::fetch_or ](atomic: &$at, val: $ty, order: Ordering) -> $ty
61            no_unwind;
62
63        pub assume_specification [ <$at>::fetch_xor ](atomic: &$at, val: $ty, order: Ordering) -> $ty
64            no_unwind;
65
66        pub assume_specification [ <$at>::load ](atomic: &$at, order: Ordering) -> $ty
67            requires
68                order != Ordering::Release,
69                order != Ordering::AcqRel,
70            no_unwind;
71
72        pub assume_specification [ <$at>::store ](atomic: &$at, val: $ty, order: Ordering)
73            requires
74                order != Ordering::Acquire,
75                order != Ordering::AcqRel,
76            no_unwind;
77
78        pub assume_specification [ <$at>::swap ](atomic: &$at, val: $ty, order: Ordering) -> $ty
79            no_unwind;
80
81        }
82    };
83}
84
85macro_rules! atomic_specs_int_specific {
86    ($at:ty, $ty:ty) => {
87        verus!{
88
89        pub assume_specification [ <$at>::fetch_add ](atomic: &$at, val: $ty, order: Ordering) -> $ty
90            no_unwind;
91
92        pub assume_specification [ <$at>::fetch_sub ](atomic: &$at, val: $ty, order: Ordering) -> $ty
93            no_unwind;
94
95        pub assume_specification [ <$at>::fetch_min ](atomic: &$at, val: $ty, order: Ordering) -> $ty
96            no_unwind;
97
98        pub assume_specification [ <$at>::fetch_max ](atomic: &$at, val: $ty, order: Ordering) -> $ty
99            no_unwind;
100
101        }
102    };
103}
104
105macro_rules! atomic_specs_int {
106    ($at:ty, $ty:ty) => {
107        atomic_specs_common!($at, $ty);
108        atomic_specs_int_specific!($at, $ty);
109    };
110}
111
112macro_rules! atomic_specs_bool {
113    ($at:ty, $ty:ty) => {
114        atomic_specs_common!($at, $ty);
115    };
116}
117
118atomic_specs_int!(AtomicU8, u8);
119atomic_specs_int!(AtomicU16, u16);
120atomic_specs_int!(AtomicU32, u32);
121#[cfg(target_has_atomic = "64")]
122atomic_specs_int!(AtomicU64, u64);
123atomic_specs_int!(AtomicUsize, usize);
124
125atomic_specs_int!(AtomicI8, i8);
126atomic_specs_int!(AtomicI16, i16);
127atomic_specs_int!(AtomicI32, i32);
128#[cfg(target_has_atomic = "64")]
129atomic_specs_int!(AtomicI64, i64);
130atomic_specs_int!(AtomicIsize, isize);
131
132atomic_specs_bool!(AtomicBool, bool);
vstd/std_specs/atomic.rs

vstd/std_specs/
atomic.rs
