creusot_std/std/sync/
atomic.rs

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

creusot_std/std/sync/
atomic.rs
