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 = FMap<Timestamp, ($type, SyncView)>;
67            type Objectiveness = ();
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                (exists<c: &mut Committer<Self, $type, _, _>>
146                    !c.shot_store() && c.ward() == *self &&
147                    c.val_load().deep_model() == current.deep_model() &&
148                    c.val_store() == new &&
149                    result == Ok(c.val_load()) &&
150                    f.postcondition_once((Ok(c),), ())) ||
151                (exists<c: &Committer<Self, $type, _, _>>
152                    !c.shot_store() && c.ward() == *self &&
153                    // NOTE: This following line is not present for `weak`
154                    c.val_load().deep_model() != current.deep_model() &&
155                    result == Err(c.val_load()) &&
156                    f.postcondition_once((Err(c),), ())
157                )
158            )]
159            #[inline(always)]
160            #[trusted]
161            #[allow(unused_variables)]
162            pub fn compare_exchange<F, Success: UpdateOrdering, Failure: LoadOrdering>(&self, current: $type, new: $type, f: Ghost<F>) -> Result<$type, $type>
163            where
164                F: FnGhost + FnOnce(Result<
165                    &mut Committer<Self, $type, Success::Load, Success::Store>,
166                    &Committer<Self, $type, Failure, ordering::None>
167                >,
168            )
169            {
170                self.0.compare_exchange(
171                    current,
172                    new,
173                    if cfg!(feature = "sc-drf") { SEQ_CST } else { Success::ORDERING },
174                    if cfg!(feature = "sc-drf") { SEQ_CST } else { Failure::ORDERING }
175                )
176            }
177
178            #[doc = concat!("Wrapper for [`std::sync::atomic::", stringify!($atomic_type), "::compare_exchange_weak`].")]
179            #[doc = ""]
180            #[doc = "The load and the store are always sequentially consistent."]
181            #[requires(forall<c: &mut Committer<Self, $type, _, _>> // TODO: [VL] Wrong permission here (Success == Ordering::RelAcq)
182                !c.shot_store() ==> c.ward() == *self ==>
183                c.val_load().deep_model() == current.deep_model() ==>
184                c.val_store() == new ==>
185                f.precondition((Ok(c),)) && (f.postcondition_once((Ok(c),), ()) ==> (^c).shot_store())
186            )]
187            #[requires(forall<c: &Committer<Self, $type, _, _>>
188                !c.shot_store() ==> c.ward() == *self ==>
189                f.precondition((Err(c),))
190            )]
191            #[ensures(
192                (exists<c: &mut Committer<Self, $type, _, _>>
193                    !c.shot_store() && c.ward() == *self &&
194                    c.val_load().deep_model() == current.deep_model() &&
195                    c.val_store() == new &&
196                    result == Ok(c.val_load()) &&
197                    f.postcondition_once((Ok(c),), ())) ||
198                (exists<c: &Committer<Self, $type, _, _>>
199                    !c.shot_store() && c.ward() == *self &&
200                    result == Err(c.val_load()) &&
201                    f.postcondition_once((Err(c),), ())
202                )
203            )]
204            #[inline(always)]
205            #[trusted]
206            #[allow(unused_variables)]
207            pub fn compare_exchange_weak<F, Success: UpdateOrdering, Failure: LoadOrdering>(&self, current: $type, new: $type, f: Ghost<F>) -> Result<$type, $type>
208            where
209                F: FnGhost + FnOnce(Result<
210                    &mut Committer<Self, $type, Success::Load, Success::Store>,
211                    &Committer<Self, $type, Failure, ordering::None>
212                >,
213            )
214            {
215                self.0.compare_exchange_weak(
216                    current,
217                    new,
218                    if cfg!(feature = "sc-drf") { SEQ_CST } else { Success::ORDERING },
219                    if cfg!(feature = "sc-drf") { SEQ_CST } else { Failure::ORDERING }
220                )
221            }
222
223            #[doc = concat!("Wrapper for [`std::sync::atomic::", stringify!($atomic_type), "::load`].")]
224            #[requires(forall<c: &Committer<Self, $type, Load, ordering::None>>
225                !c.shot_store() ==> c.ward() == *self ==> f.precondition((c,))
226            )]
227            #[ensures(exists<c: &Committer<Self, $type, Load, ordering::None>>
228                !c.shot_store() && c.ward() == *self && c.val_load() == result && f.postcondition_once((c,), ())
229            )]
230            #[inline(always)]
231            #[trusted]
232            #[allow(unused_variables)]
233            pub fn load<F, Load: LoadOrdering>(&self, f: Ghost<F>) -> $type
234            where
235                F: FnGhost + FnOnce(&Committer<Self, $type, Load, ordering::None>),
236            {
237                // TODO: [VL] Do this check inside the macro_rules
238                self.0.load(if cfg!(feature = "sc-drf") { SEQ_CST } else { Load::ORDERING })
239            }
240
241            #[doc = concat!("Wrapper for [`std::sync::atomic::", stringify!($atomic_type), "::store`].")]
242            #[requires(forall<c: &mut Committer<Self, $type, ordering::None, Store>>
243                !c.shot_store() ==> c.ward() == *self ==> c.val_store() == val ==>
244                f.precondition((c,)) && (f.postcondition_once((c,), ()) ==> (^c).shot_store())
245            )]
246            #[ensures(exists<c: &mut Committer<Self, $type, ordering::None, Store>>
247                !c.shot_store() && c.ward() == *self && c.val_store() == val &&
248                f.postcondition_once((c,), ())
249            )]
250            #[inline(always)]
251            #[trusted]
252            #[allow(unused_variables)]
253            pub fn store<F, Store: StoreOrdering>(&self, val: $type, f: Ghost<F>)
254            where
255                F: FnGhost + FnOnce(&mut Committer<Self, $type, ordering::None, Store>),
256            {
257                self.0.store(
258                    val,
259                    if cfg!(feature = "sc-drf") { SEQ_CST } else { Store::ORDERING },
260                )
261            }
262        }
263
264    )* };
265}
266
267macro_rules! impl_atomic_int {
268    ($( ($int_type:ty, $atomic_type:ident) ),+) => { $(
269
270        impl_atomic!(($int_type, $atomic_type));
271
272        impl $atomic_type {
273            #[doc = concat!("Wrapper for [`std::sync::atomic::", stringify!($atomic_type), "::fetch_add`].")]
274            #[requires(forall<c: &mut Committer<Self, $int_type, Ord::Load, Ord::Store>>
275                !c.shot_store() ==> c.ward() == *self ==> c.val_store() == val + c.val_load() ==>
276                f.precondition((c,)) && (f.postcondition_once((c,), ()) ==> (^c).shot_store())
277            )]
278            #[ensures(exists<c: &mut Committer<Self, $int_type, Ord::Load, Ord::Store>>
279                !c.shot_store() && c.ward() == *self && c.val_store() == val + c.val_load() &&
280                c.val_load() == result && f.postcondition_once((c,), ())
281            )]
282            #[inline(always)]
283            #[trusted]
284            #[allow(unused_variables)]
285            pub fn fetch_add<F, Ord: UpdateOrdering>(&self, val: $int_type, f: Ghost<F>) -> $int_type
286            where
287                F: FnGhost + FnOnce(&mut Committer<Self, $int_type, Ord::Load, Ord::Store>),
288            {
289                self.0.fetch_add(
290                    val,
291                    if cfg!(feature = "sc-drf") { SEQ_CST } else { Ord::ORDERING },
292                )
293            }
294        }
295
296    )* };
297}
298
299#[cfg(target_has_atomic = "8")]
300impl_atomic!((bool, AtomicBool));
301#[cfg(target_has_atomic = "ptr")]
302impl_atomic!((*mut T, AtomicPtr<T>));
303
304#[cfg(target_has_atomic = "8")]
305impl_atomic_int!((i8, AtomicI8), (u8, AtomicU8));
306#[cfg(target_has_atomic = "16")]
307impl_atomic_int!((i16, AtomicI16), (u16, AtomicU16));
308#[cfg(target_has_atomic = "32")]
309impl_atomic_int!((i32, AtomicI32), (u32, AtomicU32));
310#[cfg(target_has_atomic = "64")]
311impl_atomic_int!((i64, AtomicI64), (u64, AtomicU64));
312
313// FIXME: somehow, AtomicI128 is feature-gated, but I cannot eanble the feature?
314//#[cfg(target_has_atomic = "128")]
315//impl_atomic_int!((i128, AtomicI128), (u128, AtomicU128));
316
317#[cfg(target_has_atomic = "ptr")]
318impl_atomic_int!((isize, AtomicIsize), (usize, AtomicUsize));
319
320#[ensures(*sync_view == result@)]
321#[trusted]
322#[allow(unused_variables)]
323pub fn fence_release(sync_view: Ghost<SyncView>) -> Ghost<ReleaseSyncView> {
324    fence(OrderingTy::Release);
325    Ghost::conjure()
326}
327
328#[ensures(acq_view@ == *result)]
329#[trusted]
330#[allow(unused_variables)]
331pub fn fence_acquire(acq_view: Ghost<AcquireSyncView>) -> Ghost<SyncView> {
332    fence(OrderingTy::Acquire);
333    Ghost::conjure()
334}
335
336#[ensures(acq_view@ == result@)]
337#[trusted]
338#[allow(unused_variables)]
339pub fn fence_acqrel(acq_view: Ghost<AcquireSyncView>) -> Ghost<ReleaseSyncView> {
340    fence(OrderingTy::AcqRel);
341    Ghost::conjure()
342}
creusot_std/std/sync/atomic.rs

creusot_std/std/sync/
atomic.rs
