creusot_std/std/sync/
atomic_sc.rs

1use crate::{
2    ghost::{FnGhost, Perm, perm::PermTarget},
3    prelude::*,
4    std::sync::committer::Committer,
5};
6use core::sync::atomic::Ordering as OrderingTy;
7
8pub mod ordering {
9    pub struct SeqCst;
10}
11use ordering::SeqCst;
12
13macro_rules! impl_atomic {
14    ($( ($type:ty, $atomic_type:ident $(< $T:ident >)?) ),+) => { $(
15
16        /// Creusot wrapper around [`std::sync::atomic::$atomic_type`]
17        #[doc = concat!("Creusot wrapper around [`std::sync::atomic::", stringify!($atomic_type), "`].")]
18        pub struct $atomic_type $(< $T >)?(::core::sync::atomic::$atomic_type $(< $T >)?);
19
20        impl $(< $T >)? PermTarget for $atomic_type $(< $T >)? {
21            type Value = $type;
22            type Objectiveness = ();
23        }
24
25        impl $(< $T >)? $atomic_type $(< $T >)? {
26            #[ensures(result.1.val() == val)]
27            #[ensures(*result.1.ward() == result.0)]
28            #[inline(always)]
29            #[trusted]
30            #[check(terminates)]
31            pub fn new(val: $type) -> (Self, Ghost<Perm<$atomic_type $(< $T >)?>>) {
32                (Self(::core::sync::atomic::$atomic_type::new(val)), Ghost::conjure())
33            }
34
35            #[doc = concat!("Wrapper for [`std::sync::atomic::", stringify!($atomic_type), "::into_inner`].")]
36            #[requires(self == *own.ward())]
37            #[ensures(result == own.val())]
38            #[inline(always)]
39            #[trusted]
40            #[allow(unused_variables)]
41            pub fn into_inner(self, own: Ghost<Perm<$atomic_type $(< $T >)?>>) -> $type {
42                self.0.into_inner()
43            }
44
45            #[doc = concat!("Wrapper for [`std::sync::atomic::", stringify!($atomic_type), "::compare_exchange`].")]
46            #[doc = ""]
47            #[doc = "The load and the store are always sequentially consistent."]
48            #[requires(forall<c: &mut Committer<Self, $type, SeqCst, SeqCst>>
49                !c.shot_store() ==> c.ward() == *self ==>
50                c.val_load().deep_model() == current.deep_model() ==>
51                c.val_store() == new ==>
52                f.precondition((Ok(c),)) && (f.postcondition_once((Ok(c),), ()) ==> (^c).shot_store())
53            )]
54            #[requires(forall<c: &Committer<Self, $type, SeqCst, ()>>
55                !c.shot_store() ==> c.ward() == *self ==>
56                // NOTE: This following line is not present for `weak`
57                c.val_load().deep_model() != current.deep_model() ==>
58                f.precondition((Err(c),))
59            )]
60            #[ensures(
61                match result {
62                    Ok(result) => {
63                        exists<c: &mut Committer<Self, $type, SeqCst, SeqCst>>
64                            !c.shot_store() && c.ward() == *self &&
65                            c.val_load().deep_model() == current.deep_model() &&
66                            c.val_store() == new &&
67                            result == c.val_load() &&
68                            f.postcondition_once((Ok(c),), ())
69                    },
70                    Err(result) => {
71                       exists<c: &Committer<Self, $type, SeqCst, ()>>
72                            !c.shot_store() && c.ward() == *self &&
73                            // NOTE: This following line is not present for `weak`
74                            c.val_load().deep_model() != current.deep_model() &&
75                            result == c.val_load() &&
76                            f.postcondition_once((Err(c),), ())
77                    }
78                }
79            )]
80            #[inline(always)]
81            #[trusted]
82            #[allow(unused_variables)]
83            pub fn compare_exchange<F>(&self, current: $type, new: $type, f: Ghost<F>) -> Result<$type, $type>
84            where
85                F: FnGhost + FnOnce(Result<
86                    &mut Committer<Self, $type, SeqCst, SeqCst>,
87                    &Committer<Self, $type, SeqCst, ()>
88                >,
89            )
90            {
91                self.0.compare_exchange(current, new, OrderingTy::SeqCst, OrderingTy::SeqCst)
92            }
93
94            #[doc = concat!("Wrapper for [`std::sync::atomic::", stringify!($atomic_type), "::compare_exchange_weak`].")]
95            #[doc = ""]
96            #[doc = "The load and the store are always sequentially consistent."]
97            #[requires(forall<c: &mut Committer<Self, $type, SeqCst, SeqCst>>
98                !c.shot_store() ==> c.ward() == *self ==>
99                c.val_load().deep_model() == current.deep_model() ==>
100                c.val_store() == new ==>
101                f.precondition((Ok(c),)) && (f.postcondition_once((Ok(c),), ()) ==> (^c).shot_store())
102            )]
103            #[requires(forall<c: &Committer<Self, $type, SeqCst, ()>>
104                !c.shot_store() ==> c.ward() == *self ==>
105                f.precondition((Err(c),))
106            )]
107            #[ensures(
108                match result {
109                    Ok(result) => {
110                        exists<c: &mut Committer<Self, $type, SeqCst, SeqCst>>
111                            !c.shot_store() && c.ward() == *self &&
112                            c.val_load().deep_model() == current.deep_model() &&
113                            c.val_store() == new &&
114                            result == c.val_load() &&
115                            f.postcondition_once((Ok(c),), ())
116                    },
117                    Err(result) => {
118                       exists<c: &Committer<Self, $type, SeqCst, ()>>
119                            !c.shot_store() && c.ward() == *self &&
120                            result == c.val_load() &&
121                            f.postcondition_once((Err(c),), ())
122                    }
123                }
124            )]
125            #[inline(always)]
126            #[trusted]
127            #[allow(unused_variables)]
128            pub fn compare_exchange_weak<F>(&self, current: $type, new: $type, f: Ghost<F>) -> Result<$type, $type>
129            where
130                F: FnGhost + FnOnce(Result<
131                    &mut Committer<Self, $type, SeqCst, SeqCst>,
132                    &Committer<Self, $type, SeqCst, ()>
133                >,
134            )
135            {
136                self.0.compare_exchange_weak(current, new, OrderingTy::SeqCst, OrderingTy::SeqCst)
137            }
138
139            #[doc = concat!("Wrapper for [`std::sync::atomic::", stringify!($atomic_type), "::load`].")]
140            #[doc = ""]
141            #[doc = "The load is always sequentially consistent."]
142            #[requires(forall<c: &Committer<Self, $type, SeqCst, ()>>
143                !c.shot_store() ==> c.ward() == *self ==> f.precondition((c,))
144            )]
145            #[ensures(exists<c: &Committer<Self, $type, SeqCst, ()>>
146                !c.shot_store() && c.ward() == *self && c.val_load() == result && f.postcondition_once((c,), ())
147            )]
148            #[inline(always)]
149            #[trusted]
150            #[allow(unused_variables)]
151            pub fn load<F>(&self, f: Ghost<F>) -> $type
152            where
153                F: FnGhost + FnOnce(&Committer<Self, $type, SeqCst, ()>),
154            {
155                self.0.load(OrderingTy::SeqCst)
156            }
157
158            #[doc = concat!("Wrapper for [`std::sync::atomic::", stringify!($atomic_type), "::store`].")]
159            #[doc = ""]
160            #[doc = "The store is always sequentially consistent."]
161            #[requires(forall<c: &mut Committer<Self, $type, (), SeqCst>>
162                !c.shot_store() ==> c.ward() == *self ==> c.val_store() == val ==>
163                f.precondition((c,)) && (f.postcondition_once((c,), ()) ==> (^c).shot_store())
164            )]
165            #[ensures(exists<c: &mut Committer<Self, $type, (), SeqCst>>
166                !c.shot_store() && c.ward() == *self && c.val_store() == val &&
167                f.postcondition_once((c,), ())
168            )]
169            #[inline(always)]
170            #[trusted]
171            #[allow(unused_variables)]
172            pub fn store<F>(&self, val: $type, f: Ghost<F>)
173            where
174                F: FnGhost + FnOnce(&mut Committer<Self, $type, (), SeqCst>),
175            {
176                self.0.store(val, OrderingTy::SeqCst)
177            }
178        }
179
180    )* };
181}
182
183macro_rules! impl_atomic_int {
184    ($( ($int_type:ty, $atomic_type:ident) ),+) => { $(
185
186        impl_atomic!(($int_type, $atomic_type));
187
188        impl $atomic_type {
189            #[doc = concat!("Wrapper for [`std::sync::atomic::", stringify!($atomic_type), "::fetch_add`].")]
190            #[doc = ""]
191            #[doc = "The load and the store are always sequentially consistent."]
192            #[requires(forall<c: &mut Committer<Self, $int_type, SeqCst, SeqCst>>
193                !c.shot_store() ==> c.ward() == *self ==> c.val_store() == val + c.val_load() ==>
194                f.precondition((c,)) && (f.postcondition_once((c,), ()) ==> (^c).shot_store())
195            )]
196            #[ensures(exists<c: &mut Committer<Self, $int_type, SeqCst, SeqCst>>
197                !c.shot_store() && c.ward() == *self && c.val_store() == val + c.val_load() &&
198                c.val_load() == result && f.postcondition_once((c,), ())
199            )]
200            #[inline(always)]
201            #[trusted]
202            #[allow(unused_variables)]
203            pub fn fetch_add<F>(&self, val: $int_type, f: Ghost<F>) -> $int_type
204            where
205                F: FnGhost + FnOnce(&mut Committer<Self, $int_type, SeqCst, SeqCst>),
206            {
207                self.0.fetch_add(val, OrderingTy::SeqCst)
208            }
209        }
210
211    )* };
212}
213
214impl_atomic! {
215    (bool, AtomicBool),
216    (*mut T, AtomicPtr<T>)
217}
218
219impl_atomic_int! {
220    (i8, AtomicI8),
221    (u8, AtomicU8),
222    (i16, AtomicI16),
223    (u16, AtomicU16),
224    (i32, AtomicI32),
225    (u32, AtomicU32),
226    (i64, AtomicI64),
227    (u64, AtomicU64),
228    (isize, AtomicIsize),
229    (usize, AtomicUsize)
230}
creusot_std/std/sync/atomic_sc.rs

creusot_std/std/sync/
atomic_sc.rs
