creusot_std/std/sync/
committer.rs

1#[cfg(feature = "sc-drf")]
2use crate::std::sync::atomic_sc::ordering::SeqCst;
3use crate::{
4    ghost::{PermTarget, perm::Perm},
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<'static> = FMap<Timestamp, (T, SyncView)>> + HasTimestamp + 'static,
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<'static> = FMap<Timestamp, (T, SyncView)>> + HasTimestamp + 'static,
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<'static>, SeqCst, Store>
114where
115    C: PermTarget,
116{
117    /// 'Shoot' the committer
118    ///
119    /// This does the read on the atomic in ghost code.
120    #[requires(!self.shot_store())]
121    #[requires(self.ward() == *(*own).ward())]
122    #[ensures(self.val_load() == own.val())]
123    #[check(ghost)]
124    #[trusted]
125    #[allow(unused_variables)]
126    pub fn shoot_load(&self, own: &Perm<C>) {
127        panic!("Should not be called outside ghost code")
128    }
129}
130
131impl<C, T, Load> Committer<C, T, Load, Relaxed>
132where
133    C: PermTarget<Value<'static> = FMap<Timestamp, (T, SyncView)>> + HasTimestamp + 'static,
134{
135    /// 'Shoot' the committer (Relaxed)
136    ///
137    /// This does the write on the atomic in ghost code, and can only be called once.
138    #[requires(!(*self).shot_store())]
139    #[requires(self.ward() == *(*own).ward())]
140    #[ensures((*self).hist_inv(^self))]
141    #[ensures((^self).shot_store())]
142    #[ensures((*own).ward() == (^own).ward())]
143    #[ensures(*sync_view <= ^sync_view)]
144    #[ensures((*self).ward().get_timestamp(*sync_view) <= self.timestamp())]
145    #[ensures(self.timestamp() < (*self).ward().get_timestamp(^sync_view))]
146    #[ensures((*own).val().get(self.timestamp() + 1) == None)]
147    #[ensures((^own).val() == (*own).val().insert(self.timestamp() + 1, ((*self).val_store(), rel_view@)))]
148    #[check(ghost)]
149    #[trusted]
150    #[allow(unused_variables)]
151    pub fn shoot_store(
152        &mut self,
153        own: &mut Perm<C>,
154        sync_view: &mut SyncView,
155        rel_view: ReleaseSyncView,
156    ) {
157        panic!("Should not be called outside ghost code")
158    }
159}
160
161impl<C, T, Load> Committer<C, T, Load, Release>
162where
163    C: PermTarget<Value<'static> = FMap<Timestamp, (T, SyncView)>> + HasTimestamp + 'static,
164{
165    /// 'Shoot' the committer
166    ///
167    /// This does the write on the atomic in ghost code, and can only be called once.
168    #[requires(!(*self).shot_store())]
169    #[requires(self.ward() == *(*own).ward())]
170    #[ensures((*self).hist_inv(^self))]
171    #[ensures((^self).shot_store())]
172    #[ensures((*own).ward() == (^own).ward())]
173    #[ensures(*sync_view <= ^sync_view)]
174    #[ensures((*self).ward().get_timestamp(*sync_view) <= self.timestamp())]
175    #[ensures(self.timestamp() < (*self).ward().get_timestamp(^sync_view))]
176    #[ensures((*own).val().get(self.timestamp() + 1) == None)]
177    #[ensures((^own).val() == (*own).val().insert(self.timestamp() + 1, ((*self).val_store(), ^sync_view)))]
178    #[check(ghost)]
179    #[trusted]
180    #[allow(unused_variables)]
181    pub fn shoot_store(&mut self, own: &mut Perm<C>, sync_view: &mut SyncView) {
182        panic!("Should not be called outside ghost code")
183    }
184}
185
186#[cfg(feature = "sc-drf")]
187impl<C, Load> Committer<C, C::Value<'static>, Load, SeqCst>
188where
189    C: PermTarget,
190{
191    /// 'Shoot' the committer
192    ///
193    /// This does the write on the atomic in ghost code, and can only be called once.
194    #[requires(!(*self).shot_store())]
195    #[requires(self.ward() == *(*own).ward())]
196    #[ensures((*self).hist_inv(^self))]
197    #[ensures((^self).shot_store())]
198    #[ensures((*own).ward() == (^own).ward())]
199    #[ensures((^own).val() == (*self).val_store())]
200    #[check(ghost)]
201    #[trusted]
202    #[allow(unused_variables)]
203    pub fn shoot_store(&mut self, own: &mut Perm<C>) {
204        panic!("Should not be called outside ghost code")
205    }
206}
creusot_std/std/sync/committer.rs

creusot_std/std/sync/
committer.rs
