creusot_std/std/sync/
atomic_relacq.rs

1#[cfg(creusot)]
2use crate::sync_view::Objective;
3
4use crate::{
5    ghost::{Container, FnGhost, perm::Perm},
6    logic::FMap,
7    prelude::*,
8    sync_view::{HasTimestamp, SyncView, Timestamp},
9};
10use core::marker::PhantomData;
11
12macro_rules! impl_atomic {
13    ($( ($type:ty, $atomic_type:ident $(< $T:ident >)?) ),+) => { $(
14
15        #[doc = concat!("Creusot wrapper around [`std::sync::atomic::", stringify!($atomic_type), "`].")]
16        pub struct $atomic_type $(< $T >)?(::std::sync::atomic::$atomic_type $(< $T >)?);
17
18        unsafe impl $(< $T >)? Send for Perm<$atomic_type $(< $T >)?> {}
19        unsafe impl $(< $T >)? Sync for Perm<$atomic_type $(< $T >)?> {}
20
21        #[cfg(creusot)]
22        #[trusted]
23        impl $(< $T >)? Objective for Perm<$atomic_type $(< $T >)?> {}
24
25        impl $(< $T >)? Container for $atomic_type $(< $T >)? {
26            type Value = FMap<Timestamp, ($type, SyncView)>;
27
28            #[logic(open, inline)]
29            fn is_disjoint(&self, _: &Self::Value, other: &Self, _: &Self::Value) -> bool {
30                self != other
31            }
32        }
33
34        impl $(< $T >)? HasTimestamp for $atomic_type $(< $T >)? {
35            #[logic(opaque)]
36            fn get_timestamp(self, _: SyncView) -> Timestamp {
37                dead
38            }
39
40            #[logic(law)]
41            #[requires(x.le_log(y))]
42            #[ensures(self.get_timestamp(x).le_log(self.get_timestamp(y)))]
43            #[trusted]
44            fn get_timestamp_monotonic(self, x: SyncView, y: SyncView) {}
45        }
46
47        impl $(< $T >)? $atomic_type $(< $T >)? {
48            #[ensures(*result.1.val() == FMap::singleton(result.0.get_timestamp(^view), (val, **view)))]
49            #[ensures(*result.1.ward() == result.0)]
50            #[trusted]
51            #[check(terminates)]
52            #[allow(unused_variables)]
53            pub fn new(val: $type, view: Ghost<&mut SyncView>) -> (Self, Ghost<Box<Perm<$atomic_type $(< $T >)?>>>) {
54                (Self(std::sync::atomic::$atomic_type::new(val)), Ghost::conjure())
55            }
56
57            // TODO: [VL] into_inner
58
59            #[doc = concat!("Wrapper for [`std::sync::atomic::", stringify!($atomic_type), "::load`].")]
60            #[requires(forall<c: &LoadCommitter<$type, Self>> c.ward() == *self ==> f.precondition((c,)))]
61            #[ensures(exists<c: &LoadCommitter<$type, Self>>
62                c.ward() == *self && c.val() == result && f.postcondition_once((c,), ())
63            )]
64            #[trusted]
65            #[allow(unused_variables)]
66            pub fn load<F>(&self, f: Ghost<F>) -> $type
67            where
68                F: FnGhost + FnOnce(&LoadCommitter<$type, Self>),
69            {
70                self.0.load(if cfg!(feature = "sc-drf") {
71                    ::std::sync::atomic::Ordering::SeqCst
72                } else {
73                    ::std::sync::atomic::Ordering::Acquire
74                })
75            }
76
77            #[doc = concat!("Wrapper for [`std::sync::atomic::", stringify!($atomic_type), "::store`].")]
78            #[requires(forall<c: &mut StoreCommitter<$type, Self>> !c.shot() ==> c.ward() == *self ==> c.val() == val ==>
79                f.precondition((c,)) && f.postcondition_once((c,), ()) ==> (^c).shot()
80            )]
81            #[ensures(exists<c: &mut StoreCommitter<$type, Self>>
82                !c.shot() && c.ward() == *self && c.val() == val &&
83                f.postcondition_once((c,), ())
84            )]
85            #[trusted]
86            #[allow(unused_variables)]
87            pub fn store<F>(&self, val: $type, f: Ghost<F>)
88            where
89                F: FnGhost + FnOnce(&mut StoreCommitter<$type, Self>),
90            {
91                self.0.store(
92                    val,
93                    if cfg!(feature = "sc-drf") {
94                        ::std::sync::atomic::Ordering::SeqCst
95                    } else {
96                        ::std::sync::atomic::Ordering::Release
97                    },
98                )
99            }
100        }
101
102    )* };
103}
104
105macro_rules! impl_atomic_int {
106    ($( ($int_type:ty, $atomic_type:ident) ),+) => { $(
107
108        impl_atomic!(($int_type, $atomic_type));
109
110        // Nothing yet.
111
112    )* };
113}
114
115impl_atomic! {
116    (bool, AtomicBool),
117    (*mut T, AtomicPtr<T>)
118}
119
120impl_atomic_int! {
121    (i8, AtomicI8),
122    (u8, AtomicU8),
123    (i16, AtomicI16),
124    (u16, AtomicU16),
125    (i32, AtomicI32),
126    (u32, AtomicU32),
127    (i64, AtomicI64),
128    (u64, AtomicU64),
129    (isize, AtomicIsize),
130    (usize, AtomicUsize)
131}
132
133/// Wrapper around a single atomic load operation, where multiple ghost steps
134/// can be performed.
135///
136/// Note: this committer has no observable effect on ghost ressources. Thus, it is optional to shoot
137/// it, and nothing prevent the user from shooting it several times.
138// This trick is correct for SC accesses under SC-DRF, and for Rel/Acq/Rlx and Rlx accesses, but
139// perhaps not for C20's SC accesses.
140#[opaque]
141pub struct LoadCommitter<T, C: Container<Value = FMap<Timestamp, (T, SyncView)>>>(
142    PhantomData<(T, C)>,
143);
144
145impl<T, C: Container<Value = FMap<Timestamp, (T, SyncView)>> + HasTimestamp> LoadCommitter<T, C> {
146    /// Identity of the committer
147    ///
148    /// This is used so that we can only use the committer with the right [`AtomicOwn`].
149    #[logic(opaque)]
150    pub fn ward(self) -> C {
151        dead
152    }
153
154    /// Value held by the [`AtomicOwn`].
155    #[logic(opaque)]
156    pub fn val(self) -> T {
157        dead
158    }
159
160    /// 'Shoot' the committer
161    ///
162    /// This does the read on the atomic in ghost code.
163    #[requires(self.ward() == *own.ward())]
164    #[ensures((*view).le_log(^view))]
165    #[ensures(self.ward().get_timestamp(*view) <= result)]
166    #[ensures(result <= self.ward().get_timestamp(^view))]
167    #[ensures(match own.val().get(result) {
168        Some((v, v_view)) => v == self.val() && v_view.le_log(^view),
169        None => false
170    })]
171    #[check(ghost)]
172    #[trusted]
173    #[allow(unused_variables)]
174    pub fn shoot(&self, own: &Perm<C>, view: &mut SyncView) -> Timestamp {
175        panic!("Should not be called outside ghost code")
176    }
177}
178
179/// Wrapper around a single atomic operation, where multiple ghost steps can be
180/// performed.
181#[opaque]
182pub struct StoreCommitter<T, C: Container<Value = FMap<Timestamp, (T, SyncView)>>>(
183    PhantomData<(T, C)>,
184);
185
186impl<T, C: Container<Value = FMap<Timestamp, (T, SyncView)>> + HasTimestamp> StoreCommitter<T, C> {
187    /// Status of the committer
188    #[logic(opaque)]
189    pub fn shot(self) -> bool {
190        dead
191    }
192
193    /// Identity of the committer
194    ///
195    /// This is used so that we can only use the committer with the right [`AtomicOwn`].
196    #[logic(opaque)]
197    pub fn ward(self) -> C {
198        dead
199    }
200
201    /// Value held by the [`AtomicOwn`], before the [`shoot`].
202    #[logic(opaque)]
203    pub fn val(self) -> T {
204        dead
205    }
206
207    /// 'Shoot' the committer
208    ///
209    /// This does the write on the atomic in ghost code, and can only be called once.
210    #[requires(!(*self).shot())]
211    #[requires(self.ward() == *(*own).ward())]
212    #[ensures((^self).shot())]
213    #[ensures((*self).ward() == (^self).ward() && (*self).val() == (^self).val())]
214    #[ensures((*own).ward() == (^own).ward())]
215    #[ensures((*view).le_log(^view))]
216    #[ensures((*self).ward().get_timestamp(*view) < result)]
217    #[ensures(result <= (*self).ward().get_timestamp(^view))]
218    #[ensures((*own).val().get(result) == None)]
219    #[ensures(*(^own).val() == (*own).val().insert(result, ((*self).val(), (*view))))]
220    #[check(ghost)]
221    #[trusted]
222    #[allow(unused_variables)]
223    pub fn shoot(&mut self, own: &mut Perm<C>, view: &mut SyncView) -> Timestamp {
224        panic!("Should not be called outside ghost code")
225    }
226}
creusot_std/std/sync/atomic_relacq.rs

creusot_std/std/sync/
atomic_relacq.rs
