creusot_std/std/sync/
committer.rs

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

creusot_std/std/sync/
committer.rs
