creusot_std/std/sync/
atomic.rs

1use crate::{
2    ghost::{
3        FnGhost,
4        perm::{Perm, PermTarget},
5    },
6    logic::FMap,
7    prelude::*,
8    std::sync::{
9        committer::Committer,
10        view::{AcquireSyncView, HasTimestamp, ReleaseSyncView, SyncView, Timestamp},
11    },
12};
13use core::sync::atomic::{Ordering as OrderingTy, fence};
14
15/// Creusot type-level wrappers around [`std::sync::atomic::Ordering`].
16pub mod ordering {
17    use core::sync::atomic::Ordering as OrderingTy;
18
19    pub trait Ordering {
20        const ORDERING: OrderingTy;
21    }
22
23    pub trait LoadOrdering: Ordering {}
24    pub trait StoreOrdering: Ordering {}
25    pub trait UpdateOrdering: Ordering {
26        type Load: LoadOrdering;
27        type Store: StoreOrdering;
28    }
29
30    pub struct None;
31
32    macro_rules! impl_ordering {
33        ( $order:ident, load = $load:ident, store = $store:ident ) => {
34            pub struct $order;
35
36            impl Ordering for $order {
37                const ORDERING: OrderingTy = OrderingTy::$order;
38            }
39
40            impl UpdateOrdering for $order {
41                type Load = $load;
42                type Store = $store;
43            }
44        };
45    }
46
47    impl_ordering!(Relaxed, load = Relaxed, store = Relaxed);
48    impl_ordering!(Acquire, load = Acquire, store = Relaxed);
49    impl_ordering!(Release, load = Relaxed, store = Release);
50    impl_ordering!(AcqRel, load = Acquire, store = Release);
51
52    impl LoadOrdering for Relaxed {}
53    impl StoreOrdering for Relaxed {}
54    impl LoadOrdering for Acquire {}
55    impl StoreOrdering for Release {}
56}
57
58use ordering::{LoadOrdering, StoreOrdering, UpdateOrdering};
59
60const SEQ_CST: OrderingTy = OrderingTy::SeqCst;
61
62macro_rules! impl_atomic {
63    ($( ($type:ty, $atomic_type:ident $(< $T:ident >)?) ),+) => { $(
64
65        #[doc = concat!("Creusot wrapper around [`std::sync::atomic::", stringify!($atomic_type), "`].")]
66        pub struct $atomic_type $(< $T >)?(::core::sync::atomic::$atomic_type $(< $T >)?);
67
68        impl $(< $T >)? PermTarget for $atomic_type $(< $T >)? {
69            type Value<'a> = FMap<Timestamp, ($type, SyncView)> where Self: 'a;
70            type PermPayload = ();
71        }
72
73        impl $(< $T >)? HasTimestamp for $atomic_type $(< $T >)? {
74            #[logic(opaque)]
75            fn get_timestamp(self, _: SyncView) -> Timestamp {
76                dead
77            }
78
79            #[logic(law)]
80            #[requires(x <= y)]
81            #[ensures(self.get_timestamp(x) <= self.get_timestamp(y))]
82            #[trusted]
83            fn get_timestamp_monotonic(self, x: SyncView, y: SyncView) {}
84        }
85
86        impl $(< $T >)? $atomic_type $(< $T >)? {
87            #[ensures(result.1.val() == FMap::singleton(result.0.get_timestamp(^sync_view), (val, **sync_view)))]
88            #[ensures(*result.1.ward() == result.0)]
89            #[inline(always)]
90            #[trusted]
91            #[check(terminates)]
92            #[allow(unused_variables)]
93            pub fn new(val: $type, sync_view: Ghost<&mut SyncView>) -> (Self, Ghost<Perm<$atomic_type $(< $T >)?>>) {
94                (Self(core::sync::atomic::$atomic_type::new(val)), Ghost::conjure())
95            }
96
97            #[doc = concat!("Wrapper for [`std::sync::atomic::", stringify!($atomic_type), "::into_inner`].")]
98            #[requires(self == *own.ward())]
99            #[ensures(match own.val().get(*result.1) { Some((v, _)) => result.0 == v, None => false })]
100            #[ensures(self.get_timestamp(^sync_view) == *result.1)]
101            #[ensures(forall<t> match own.val().get(t) {
102                Some((_, view)) => t <= *result.1 && view <= ^sync_view,
103                None => true
104            })]
105            #[inline(always)]
106            #[trusted]
107            #[allow(unused_variables)]
108            pub fn into_inner(self, own: Ghost<Perm<$atomic_type $(< $T >)?>>, sync_view: Ghost<&mut SyncView>) -> ($type, Ghost<Timestamp>) {
109                (self.0.into_inner(), Ghost::conjure())
110            }
111
112
113            #[doc = "Clear the old unusable history, thanks to the full ownership of the atomic."]
114            #[requires(*self == *own.ward())]
115            #[ensures(match (*own).val().get(*result) {
116                Some((v, _)) => (^own).val() == FMap::singleton(*result, (v, **sync_view)),
117                None => false
118            })]
119            #[ensures(self.get_timestamp(^sync_view) == *result)]
120            #[ensures(forall<t> match own.val().get(t) {
121                Some((_, view)) => t <= *result && view <= ^sync_view ,
122                None => true
123            })]
124            #[ensures(*self == ^self)]
125            #[inline(always)]
126            #[trusted]
127            #[check(terminates)]
128            #[allow(unused_variables)]
129            pub fn refresh(&mut self, own: Ghost<&mut Perm<$atomic_type $(< $T >)?>>, sync_view: Ghost<&mut SyncView>) -> Ghost<Timestamp> {
130                 Ghost::conjure()
131            }
132
133            #[doc = concat!("Wrapper for [`std::sync::atomic::", stringify!($atomic_type), "::compare_exchange`].")]
134            #[doc = ""]
135            #[doc = "The load and the store are always sequentially consistent."]
136            #[requires(forall<c: &mut Committer<Self, $type, _, _>>
137                !c.shot_store() ==> c.ward() == *self ==>
138                c.val_load().deep_model() == current.deep_model() ==>
139                c.val_store() == new ==>
140                f.precondition((Ok(c),)) && (f.postcondition_once((Ok(c),), ()) ==> (^c).shot_store())
141            )]
142            #[requires(forall<c: &Committer<Self, $type, _, _>>
143                !c.shot_store() ==> c.ward() == *self ==>
144                // NOTE: This following line is not present for `weak`
145                c.val_load().deep_model() != current.deep_model() ==>
146                f.precondition((Err(c),))
147            )]
148            #[ensures(
149                match result {
150                    Ok(result) => {
151                        exists<c: &mut Committer<Self, $type, _, _>>
152                            !c.shot_store() && c.ward() == *self &&
153                            c.val_load().deep_model() == current.deep_model() &&
154                            c.val_store() == new &&
155                            result == c.val_load() &&
156                            f.postcondition_once((Ok(c),), ())
157                    },
158                    Err(result) => {
159                       exists<c: &Committer<Self, $type, _, _>>
160                            !c.shot_store() && c.ward() == *self &&
161                            // NOTE: This following line is not present for `weak`
162                            c.val_load().deep_model() != current.deep_model() &&
163                            result == c.val_load() &&
164                            f.postcondition_once((Err(c),), ())
165                    }
166                }
167            )]
168            #[inline(always)]
169            #[trusted]
170            #[allow(unused_variables)]
171            pub fn compare_exchange<F, Success: UpdateOrdering, Failure: LoadOrdering>(&self, current: $type, new: $type, f: Ghost<F>) -> Result<$type, $type>
172            where
173                F: FnGhost + FnOnce(Result<
174                    &mut Committer<Self, $type, Success::Load, Success::Store>,
175                    &Committer<Self, $type, Failure, ordering::None>
176                >,
177            )
178            {
179                self.0.compare_exchange(
180                    current,
181                    new,
182                    if cfg!(feature = "sc-drf") { SEQ_CST } else { Success::ORDERING },
183                    if cfg!(feature = "sc-drf") { SEQ_CST } else { Failure::ORDERING }
184                )
185            }
186
187            #[doc = concat!("Wrapper for [`std::sync::atomic::", stringify!($atomic_type), "::compare_exchange_weak`].")]
188            #[doc = ""]
189            #[doc = "The load and the store are always sequentially consistent."]
190            #[requires(forall<c: &mut Committer<Self, $type, _, _>> // TODO: [VL] Wrong permission here (Success == Ordering::RelAcq)
191                !c.shot_store() ==> c.ward() == *self ==>
192                c.val_load().deep_model() == current.deep_model() ==>
193                c.val_store() == new ==>
194                f.precondition((Ok(c),)) && (f.postcondition_once((Ok(c),), ()) ==> (^c).shot_store())
195            )]
196            #[requires(forall<c: &Committer<Self, $type, _, _>>
197                !c.shot_store() ==> c.ward() == *self ==>
198                f.precondition((Err(c),))
199            )]
200            #[ensures(
201                match result {
202                    Ok(result) => {
203                        exists<c: &mut Committer<Self, $type, _, _>>
204                            !c.shot_store() && c.ward() == *self &&
205                            c.val_load().deep_model() == current.deep_model() &&
206                            c.val_store() == new &&
207                            result == c.val_load() &&
208                            f.postcondition_once((Ok(c),), ())
209                    },
210                    Err(result) => {
211                       exists<c: &Committer<Self, $type, _, _>>
212                            !c.shot_store() && c.ward() == *self &&
213                            result == c.val_load() &&
214                            f.postcondition_once((Err(c),), ())
215                    }
216                }
217            )]
218            #[inline(always)]
219            #[trusted]
220            #[allow(unused_variables)]
221            pub fn compare_exchange_weak<F, Success: UpdateOrdering, Failure: LoadOrdering>(&self, current: $type, new: $type, f: Ghost<F>) -> Result<$type, $type>
222            where
223                F: FnGhost + FnOnce(Result<
224                    &mut Committer<Self, $type, Success::Load, Success::Store>,
225                    &Committer<Self, $type, Failure, ordering::None>
226                >,
227            )
228            {
229                self.0.compare_exchange_weak(
230                    current,
231                    new,
232                    if cfg!(feature = "sc-drf") { SEQ_CST } else { Success::ORDERING },
233                    if cfg!(feature = "sc-drf") { SEQ_CST } else { Failure::ORDERING }
234                )
235            }
236
237            #[doc = concat!("Wrapper for [`std::sync::atomic::", stringify!($atomic_type), "::load`].")]
238            #[requires(forall<c: &Committer<Self, $type, Load, ordering::None>>
239                !c.shot_store() ==> c.ward() == *self ==> f.precondition((c,))
240            )]
241            #[ensures(exists<c: &Committer<Self, $type, Load, ordering::None>>
242                !c.shot_store() && c.ward() == *self && c.val_load() == result && f.postcondition_once((c,), ())
243            )]
244            #[inline(always)]
245            #[trusted]
246            #[allow(unused_variables)]
247            pub fn load<F, Load: LoadOrdering>(&self, f: Ghost<F>) -> $type
248            where
249                F: FnGhost + FnOnce(&Committer<Self, $type, Load, ordering::None>),
250            {
251                // TODO: [VL] Do this check inside the macro_rules
252                self.0.load(if cfg!(feature = "sc-drf") { SEQ_CST } else { Load::ORDERING })
253            }
254
255            #[doc = concat!("Wrapper for [`std::sync::atomic::", stringify!($atomic_type), "::store`].")]
256            #[requires(forall<c: &mut Committer<Self, $type, ordering::None, Store>>
257                !c.shot_store() ==> c.ward() == *self ==> c.val_store() == val ==>
258                f.precondition((c,)) && (f.postcondition_once((c,), ()) ==> (^c).shot_store())
259            )]
260            #[ensures(exists<c: &mut Committer<Self, $type, ordering::None, Store>>
261                !c.shot_store() && c.ward() == *self && c.val_store() == val &&
262                f.postcondition_once((c,), ())
263            )]
264            #[inline(always)]
265            #[trusted]
266            #[allow(unused_variables)]
267            pub fn store<F, Store: StoreOrdering>(&self, val: $type, f: Ghost<F>)
268            where
269                F: FnGhost + FnOnce(&mut Committer<Self, $type, ordering::None, Store>),
270            {
271                self.0.store(
272                    val,
273                    if cfg!(feature = "sc-drf") { SEQ_CST } else { Store::ORDERING },
274                )
275            }
276        }
277
278    )* };
279}
280
281macro_rules! impl_atomic_int {
282    ($( ($int_type:ty, $atomic_type:ident) ),+) => { $(
283
284        impl_atomic!(($int_type, $atomic_type));
285
286        impl $atomic_type {
287            #[doc = concat!("Wrapper for [`std::sync::atomic::", stringify!($atomic_type), "::fetch_add`].")]
288            #[requires(forall<c: &mut Committer<Self, $int_type, Ord::Load, Ord::Store>>
289                !c.shot_store() ==> c.ward() == *self ==> c.val_store() == val + c.val_load() ==>
290                f.precondition((c,)) && (f.postcondition_once((c,), ()) ==> (^c).shot_store())
291            )]
292            #[ensures(exists<c: &mut Committer<Self, $int_type, Ord::Load, Ord::Store>>
293                !c.shot_store() && c.ward() == *self && c.val_store() == val + c.val_load() &&
294                c.val_load() == result && f.postcondition_once((c,), ())
295            )]
296            #[inline(always)]
297            #[trusted]
298            #[allow(unused_variables)]
299            pub fn fetch_add<F, Ord: UpdateOrdering>(&self, val: $int_type, f: Ghost<F>) -> $int_type
300            where
301                F: FnGhost + FnOnce(&mut Committer<Self, $int_type, Ord::Load, Ord::Store>),
302            {
303                self.0.fetch_add(
304                    val,
305                    if cfg!(feature = "sc-drf") { SEQ_CST } else { Ord::ORDERING },
306                )
307            }
308        }
309
310    )* };
311}
312
313#[cfg(target_has_atomic = "8")]
314impl_atomic!((bool, AtomicBool));
315#[cfg(target_has_atomic = "ptr")]
316impl_atomic!((*mut T, AtomicPtr<T>));
317
318#[cfg(target_has_atomic = "8")]
319impl_atomic_int!((i8, AtomicI8), (u8, AtomicU8));
320#[cfg(target_has_atomic = "16")]
321impl_atomic_int!((i16, AtomicI16), (u16, AtomicU16));
322#[cfg(target_has_atomic = "32")]
323impl_atomic_int!((i32, AtomicI32), (u32, AtomicU32));
324#[cfg(target_has_atomic = "64")]
325impl_atomic_int!((i64, AtomicI64), (u64, AtomicU64));
326
327// FIXME: somehow, AtomicI128 is feature-gated, but I cannot eanble the feature?
328//#[cfg(target_has_atomic = "128")]
329//impl_atomic_int!((i128, AtomicI128), (u128, AtomicU128));
330
331#[cfg(target_has_atomic = "ptr")]
332impl_atomic_int!((isize, AtomicIsize), (usize, AtomicUsize));
333
334#[ensures(*sync_view == result@)]
335#[trusted]
336#[allow(unused_variables)]
337pub fn fence_release(sync_view: Ghost<SyncView>) -> Ghost<ReleaseSyncView> {
338    fence(OrderingTy::Release);
339    Ghost::conjure()
340}
341
342#[ensures(acq_view@ == *result)]
343#[trusted]
344#[allow(unused_variables)]
345pub fn fence_acquire(acq_view: Ghost<AcquireSyncView>) -> Ghost<SyncView> {
346    fence(OrderingTy::Acquire);
347    Ghost::conjure()
348}
349
350#[ensures(acq_view@ == result@)]
351#[trusted]
352#[allow(unused_variables)]
353pub fn fence_acqrel(acq_view: Ghost<AcquireSyncView>) -> Ghost<ReleaseSyncView> {
354    fence(OrderingTy::AcqRel);
355    Ghost::conjure()
356}
creusot_std/std/sync/atomic.rs

creusot_std/std/sync/
atomic.rs
