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

creusot_std/std/sync/
atomic.rs
