creusot_std/std/sync/
committer.rs

1use crate::{
2    ghost::{PermTarget, perm::Perm},
3    logic::FMap,
4    prelude::*,
5    std::sync::{
6        atomic::Ordering,
7        view::{AcquireSyncView, HasTimestamp, ReleaseSyncView, SyncView, Timestamp},
8    },
9};
10use core::marker::PhantomData;
11
12/// Wrapper around a single atomic operation, where multiple ghost steps can be performed.
13///
14/// Note: For load-only accesses, this committer has no observable effect on ghost ressources.
15/// Thus, it is optional to shoot it, and nothing prevent the user from shooting it several times.
16// This trick is correct for SC accesses under SC-DRF, and for Rel/Acq/Rlx and Rlx accesses, but
17// perhaps not for C20's SC accesses.
18#[opaque]
19pub struct Committer<C: PermTarget, T, Load, Store>(PhantomData<(C, T, Load, Store)>);
20
21impl<C: PermTarget, T, Load, Store> Committer<C, T, Load, Store> {
22    /// Identity of the committer
23    ///
24    /// This is used so that we can only use the committer with the right [`AtomicOwn`].
25    #[logic(opaque)]
26    pub fn ward(self) -> C {
27        dead
28    }
29
30    /// Timestamp of the latest load, before any store.
31    ///
32    /// This is used for an update operation.
33    #[logic(opaque)]
34    pub fn timestamp(self) -> Timestamp {
35        dead
36    }
37
38    /// Value read from the atomic operation.
39    #[logic(opaque)]
40    pub fn val_load(self) -> T {
41        dead
42    }
43
44    /// Value written by the atomic operation.
45    #[logic(opaque)]
46    pub fn val_store(self) -> T {
47        dead
48    }
49
50    /// Status of the committer
51    #[logic(opaque)]
52    pub fn shot_store(self) -> bool {
53        dead
54    }
55
56    #[logic(open, inline)]
57    pub fn hist_inv(self, other: Self) -> bool {
58        self.ward() == other.ward()
59            && self.val_load() == other.val_load()
60            && self.val_store() == other.val_store()
61            && self.timestamp() == other.timestamp()
62    }
63}
64
65impl<C, T, Store> Committer<C, T, Ordering::Relaxed, Store>
66where
67    C: PermTarget<Value<'static> = FMap<Timestamp, (T, SyncView)>> + HasTimestamp + 'static,
68{
69    /// 'Shoot' the committer
70    ///
71    /// This does the read on the atomic in ghost code.
72    #[requires(!self.shot_store())]
73    #[requires(self.ward() == *(*own).ward())]
74    #[ensures(*sync_view <= ^sync_view)]
75    #[ensures(self.ward().get_timestamp(*sync_view) <= self.timestamp())]
76    #[ensures(self.timestamp() <= self.ward().get_timestamp(^sync_view))]
77    #[ensures(own.val().get(self.timestamp()) == Some((self.val_load(), result@)))]
78    #[check(ghost)]
79    #[trusted]
80    #[allow(unused_variables)]
81    pub fn shoot_load(&self, own: &Perm<C>, sync_view: &mut SyncView) -> AcquireSyncView {
82        panic!("Should not be called outside ghost code")
83    }
84}
85
86impl<C, T, Store> Committer<C, T, Ordering::Acquire, Store>
87where
88    C: PermTarget<Value<'static> = FMap<Timestamp, (T, SyncView)>> + HasTimestamp + 'static,
89{
90    /// 'Shoot' the committer
91    ///
92    /// This does the read on the atomic in ghost code.
93    #[requires(!self.shot_store())]
94    #[requires(self.ward() == *(*own).ward())]
95    #[ensures(*sync_view <= ^sync_view)]
96    #[ensures(self.ward().get_timestamp(*sync_view) <= self.timestamp())]
97    #[ensures(self.timestamp() <= self.ward().get_timestamp(^sync_view))]
98    #[ensures(match own.val().get(self.timestamp()) {
99        Some((v, v_view)) => v == self.val_load() && v_view <= ^sync_view,
100        None => false
101    })]
102    #[check(ghost)]
103    #[trusted]
104    #[allow(unused_variables)]
105    pub fn shoot_load(&self, own: &Perm<C>, sync_view: &mut SyncView) {
106        panic!("Should not be called outside ghost code")
107    }
108}
109
110impl<C, Store> Committer<C, C::Value<'static>, Ordering::SeqCst, Store>
111where
112    C: PermTarget,
113{
114    /// 'Shoot' the committer
115    ///
116    /// This does the read on the atomic in ghost code.
117    #[requires(!self.shot_store())]
118    #[requires(self.ward() == *(*own).ward())]
119    #[ensures(self.val_load() == own.val())]
120    #[check(ghost)]
121    #[trusted]
122    #[allow(unused_variables)]
123    pub fn shoot_load(&self, own: &Perm<C>) {
124        panic!("Should not be called outside ghost code")
125    }
126}
127
128impl<C, T, Load> Committer<C, T, Load, Ordering::Relaxed>
129where
130    C: PermTarget<Value<'static> = FMap<Timestamp, (T, SyncView)>> + HasTimestamp + 'static,
131{
132    /// 'Shoot' the committer (Relaxed)
133    ///
134    /// This does the write on the atomic in ghost code, and can only be called once.
135    #[requires(!(*self).shot_store())]
136    #[requires(self.ward() == *(*own).ward())]
137    #[ensures((*self).hist_inv(^self))]
138    #[ensures((^self).shot_store())]
139    #[ensures((*own).ward() == (^own).ward())]
140    #[ensures(*sync_view <= ^sync_view)]
141    #[ensures((*self).ward().get_timestamp(*sync_view) <= self.timestamp())]
142    #[ensures(self.timestamp() < (*self).ward().get_timestamp(^sync_view))]
143    #[ensures((*own).val().get(self.timestamp() + 1) == None)]
144    #[ensures((^own).val() == (*own).val().insert(self.timestamp() + 1, ((*self).val_store(), rel_view@)))]
145    #[check(ghost)]
146    #[trusted]
147    #[allow(unused_variables)]
148    pub fn shoot_store(
149        &mut self,
150        own: &mut Perm<C>,
151        sync_view: &mut SyncView,
152        rel_view: ReleaseSyncView,
153    ) {
154        panic!("Should not be called outside ghost code")
155    }
156}
157
158impl<C, T, Load> Committer<C, T, Load, Ordering::Release>
159where
160    C: PermTarget<Value<'static> = FMap<Timestamp, (T, SyncView)>> + HasTimestamp + 'static,
161{
162    /// 'Shoot' the committer
163    ///
164    /// This does the write on the atomic in ghost code, and can only be called once.
165    #[requires(!(*self).shot_store())]
166    #[requires(self.ward() == *(*own).ward())]
167    #[ensures((*self).hist_inv(^self))]
168    #[ensures((^self).shot_store())]
169    #[ensures((*own).ward() == (^own).ward())]
170    #[ensures(*sync_view <= ^sync_view)]
171    #[ensures((*self).ward().get_timestamp(*sync_view) <= self.timestamp())]
172    #[ensures(self.timestamp() < (*self).ward().get_timestamp(^sync_view))]
173    #[ensures((*own).val().get(self.timestamp() + 1) == None)]
174    #[ensures((^own).val() == (*own).val().insert(self.timestamp() + 1, ((*self).val_store(), ^sync_view)))]
175    #[check(ghost)]
176    #[trusted]
177    #[allow(unused_variables)]
178    pub fn shoot_store(&mut self, own: &mut Perm<C>, sync_view: &mut SyncView) {
179        panic!("Should not be called outside ghost code")
180    }
181}
182
183impl<C, Load> Committer<C, C::Value<'static>, Load, Ordering::SeqCst>
184where
185    C: PermTarget,
186{
187    /// 'Shoot' the committer
188    ///
189    /// This does the write on the atomic in ghost code, and can only be called once.
190    #[requires(!(*self).shot_store())]
191    #[requires(self.ward() == *(*own).ward())]
192    #[ensures((*self).hist_inv(^self))]
193    #[ensures((^self).shot_store())]
194    #[ensures((*own).ward() == (^own).ward())]
195    #[ensures((^own).val() == (*self).val_store())]
196    #[check(ghost)]
197    #[trusted]
198    #[allow(unused_variables)]
199    pub fn shoot_store(&mut self, own: &mut Perm<C>) {
200        panic!("Should not be called outside ghost code")
201    }
202}
creusot_std/std/sync/committer.rs

creusot_std/std/sync/
committer.rs
