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 of the latest load, before any store.
33    ///
34    /// This is used for an update operation.
35    #[logic(opaque)]
36    pub fn timestamp(self) -> Timestamp {
37        dead
38    }
39
40    /// Value read from the atomic operation.
41    #[logic(opaque)]
42    pub fn val_load(self) -> T {
43        dead
44    }
45
46    /// Value written by the atomic operation.
47    #[logic(opaque)]
48    pub fn val_store(self) -> T {
49        dead
50    }
51
52    /// Status of the committer
53    #[logic(opaque)]
54    pub fn shot_store(self) -> bool {
55        dead
56    }
57
58    #[logic(open, inline)]
59    pub fn hist_inv(self, other: Self) -> bool {
60        self.ward() == other.ward()
61            && self.val_load() == other.val_load()
62            && self.val_store() == other.val_store()
63            && self.timestamp() == other.timestamp()
64    }
65}
66
67impl<C, T, Store> Committer<C, T, Relaxed, Store>
68where
69    C: PermTarget<Value = FMap<Timestamp, (T, SyncView)>> + HasTimestamp,
70{
71    /// 'Shoot' the committer
72    ///
73    /// This does the read on the atomic in ghost code.
74    #[requires(!self.shot_store())]
75    #[requires(self.ward() == *(*own).ward())]
76    #[ensures(*sync_view <= ^sync_view)]
77    #[ensures(self.ward().get_timestamp(*sync_view) <= self.timestamp())]
78    #[ensures(self.timestamp() <= self.ward().get_timestamp(^sync_view))]
79    #[ensures(own.val().get(self.timestamp()) == Some((self.val_load(), result@)))]
80    #[check(ghost)]
81    #[trusted]
82    #[allow(unused_variables)]
83    pub fn shoot_load(&self, own: &Perm<C>, sync_view: &mut SyncView) -> AcquireSyncView {
84        panic!("Should not be called outside ghost code")
85    }
86}
87
88impl<C, T, Store> Committer<C, T, Acquire, Store>
89where
90    C: PermTarget<Value = FMap<Timestamp, (T, SyncView)>> + HasTimestamp,
91{
92    /// 'Shoot' the committer
93    ///
94    /// This does the read on the atomic in ghost code.
95    #[requires(!self.shot_store())]
96    #[requires(self.ward() == *(*own).ward())]
97    #[ensures(*sync_view <= ^sync_view)]
98    #[ensures(self.ward().get_timestamp(*sync_view) <= self.timestamp())]
99    #[ensures(self.timestamp() <= self.ward().get_timestamp(^sync_view))]
100    #[ensures(match own.val().get(self.timestamp()) {
101        Some((v, v_view)) => v == self.val_load() && v_view <= ^sync_view,
102        None => false
103    })]
104    #[check(ghost)]
105    #[trusted]
106    #[allow(unused_variables)]
107    pub fn shoot_load(&self, own: &Perm<C>, sync_view: &mut SyncView) {
108        panic!("Should not be called outside ghost code")
109    }
110}
111
112#[cfg(feature = "sc-drf")]
113impl<C, Store> Committer<C, C::Value, SeqCst, Store>
114where
115    C: PermTarget,
116    C::Value: Sized,
117{
118    /// 'Shoot' the committer
119    ///
120    /// This does the read on the atomic in ghost code.
121    #[requires(!self.shot_store())]
122    #[requires(self.ward() == *(*own).ward())]
123    #[ensures(self.val_load() == own.val())]
124    #[check(ghost)]
125    #[trusted]
126    #[allow(unused_variables)]
127    pub fn shoot_load(&self, own: &Perm<C>) {
128        panic!("Should not be called outside ghost code")
129    }
130}
131
132impl<C, T, Load> Committer<C, T, Load, Relaxed>
133where
134    C: PermTarget<Value = FMap<Timestamp, (T, SyncView)>> + HasTimestamp,
135{
136    /// 'Shoot' the committer (Relaxed)
137    ///
138    /// This does the write on the atomic in ghost code, and can only be called once.
139    #[requires(!(*self).shot_store())]
140    #[requires(self.ward() == *(*own).ward())]
141    #[ensures((*self).hist_inv(^self))]
142    #[ensures((^self).shot_store())]
143    #[ensures((*own).ward() == (^own).ward())]
144    #[ensures(*sync_view <= ^sync_view)]
145    #[ensures((*self).ward().get_timestamp(*sync_view) <= self.timestamp())]
146    #[ensures(self.timestamp() < (*self).ward().get_timestamp(^sync_view))]
147    #[ensures((*own).val().get(self.timestamp() + 1) == None)]
148    #[ensures((^own).val() == (*own).val().insert(self.timestamp() + 1, ((*self).val_store(), rel_view@)))]
149    #[check(ghost)]
150    #[trusted]
151    #[allow(unused_variables)]
152    pub fn shoot_store(
153        &mut self,
154        own: &mut Perm<C>,
155        sync_view: &mut SyncView,
156        rel_view: ReleaseSyncView,
157    ) {
158        panic!("Should not be called outside ghost code")
159    }
160}
161
162impl<C, T, Load> Committer<C, T, Load, Release>
163where
164    C: PermTarget<Value = FMap<Timestamp, (T, SyncView)>> + HasTimestamp,
165{
166    /// 'Shoot' the committer
167    ///
168    /// This does the write on the atomic in ghost code, and can only be called once.
169    #[requires(!(*self).shot_store())]
170    #[requires(self.ward() == *(*own).ward())]
171    #[ensures((*self).hist_inv(^self))]
172    #[ensures((^self).shot_store())]
173    #[ensures((*own).ward() == (^own).ward())]
174    #[ensures(*sync_view <= ^sync_view)]
175    #[ensures((*self).ward().get_timestamp(*sync_view) <= self.timestamp())]
176    #[ensures(self.timestamp() < (*self).ward().get_timestamp(^sync_view))]
177    #[ensures((*own).val().get(self.timestamp() + 1) == None)]
178    #[ensures((^own).val() == (*own).val().insert(self.timestamp() + 1, ((*self).val_store(), ^sync_view)))]
179    #[check(ghost)]
180    #[trusted]
181    #[allow(unused_variables)]
182    pub fn shoot_store(&mut self, own: &mut Perm<C>, sync_view: &mut SyncView) {
183        panic!("Should not be called outside ghost code")
184    }
185}
186
187#[cfg(feature = "sc-drf")]
188impl<C, Load> Committer<C, C::Value, Load, SeqCst>
189where
190    C: PermTarget,
191    C::Value: Sized,
192{
193    /// 'Shoot' the committer
194    ///
195    /// This does the write on the atomic in ghost code, and can only be called once.
196    #[requires(!(*self).shot_store())]
197    #[requires(self.ward() == *(*own).ward())]
198    #[ensures((*self).hist_inv(^self))]
199    #[ensures((^self).shot_store())]
200    #[ensures((*own).ward() == (^own).ward())]
201    #[ensures((^own).val() == (*self).val_store())]
202    #[check(ghost)]
203    #[trusted]
204    #[allow(unused_variables)]
205    pub fn shoot_store(&mut self, own: &mut Perm<C>) {
206        panic!("Should not be called outside ghost code")
207    }
208}
creusot_std/std/sync/committer.rs

creusot_std/std/sync/
committer.rs
