creusot_std/std/sync/
atomic_sc.rs

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

creusot_std/std/sync/
atomic_sc.rs
