forked from PrincetonUniversity/VST
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathacq_rel_SW.v
186 lines (156 loc) · 7.29 KB
/
acq_rel_SW.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
Require Import VST.veric.rmaps.
Require Import VST.veric.compcert_rmaps.
Require Import VST.concurrency.conclib.
Require Import VST.concurrency.ghosts.
Require Import VST.floyd.library.
Require Import VST.zlist.sublist.
Require Import VST.atomics.general_atomics.
Require Import VST.atomics.acq_rel_atomics.
Set Bullet Behavior "Strict Subproofs".
Section atomics.
Context {CS : compspecs}.
Section protocols.
Context {state : Type}.
Parameter protocol_piece : share -> val -> state -> (state -> state -> Prop) ->
((state -> Z -> mpred) * (state -> Z -> mpred)) -> mpred.
Definition protocol_R := protocol_piece Share.bot.
Definition protocol_W := protocol_piece gsh2.
Context (ord : state -> state -> Prop) `{RelationClasses.PreOrder _ ord}
(Tread Tfull : state -> Z -> mpred).
Axiom protocol_piece_nonexpansive : forall sh l s ord Tread1 Tfull1 Tread2 Tfull2,
(ALL s : state, ALL v : Z, (Tread1 s v <=> Tread2 s v) && (Tfull1 s v <=> Tfull2 s v)) |--
protocol_piece sh l s ord (Tread1, Tfull1) <=> protocol_piece sh l s ord (Tread2, Tfull2).
Lemma protocol_piece_super_non_expansive : forall n sh l s ord Tread Tfull,
approx n (protocol_piece sh l s ord (Tread, Tfull)) =
approx n (protocol_piece sh l s ord (fun s v => approx n (Tread s v), fun s v => approx n (Tfull s v))).
Proof.
intros.
apply approx_eq_i'.
intros m ?.
apply protocol_piece_nonexpansive.
intros ??; split; apply fash_equiv_approx; auto.
Qed.
Notation T := (Tread, Tfull).
Axiom make_protocol_R : forall sh l s,
protocol_piece sh l s ord T |-- |==> protocol_piece sh l s ord T * protocol_R l s ord T.
Corollary protocol_R_duplicable : forall l s, duplicable (protocol_R l s ord T).
Proof.
intros; apply make_protocol_R.
Qed.
Corollary protocol_W_R : forall l s,
protocol_W l s ord T |-- |==> protocol_W l s ord T * protocol_R l s ord T.
Proof.
intros; apply make_protocol_R.
Qed.
Axiom protocol_R_absorb : forall sh l s s', sh <> Share.bot ->
protocol_piece sh l s ord T * protocol_R l s' ord T |-- |==> !!(ord s' s) && protocol_piece sh l s ord T.
Corollary protocol_R_W : forall l s s',
protocol_W l s ord T * protocol_R l s' ord T |-- |==> !!(ord s' s) && protocol_W l s ord T.
Proof.
intros; apply protocol_R_absorb; auto.
Qed.
Axiom protocol_R_join' : forall l s1 s2,
protocol_R l s1 ord T * protocol_R l s2 ord T |--
EX s : _, !!(ord s1 s /\ ord s2 s) && protocol_R l s ord T.
Axiom make_protocol : forall {P : protocol Tread Tfull} l v s, repable_signed v ->
data_at Tsh tint (vint v) l * |> Tfull s v |-- |==> protocol_W l s ord T.
Axiom protocol_piece_share_join : forall sh1 sh2 sh l s1 s2 (Hsh : sepalg.join sh1 sh2 sh)
(Hsh1 : sh1 <> Share.bot) (Hsh2 : sh2 <> Share.bot),
protocol_piece sh1 l s1 ord T * protocol_piece sh2 l s2 ord T =
!!(s1 = s2) && protocol_piece sh l s1 ord T.
Axiom protocol_later : forall sh l s,
protocol_piece sh l s ord (|>Tread, |>Tfull) |-- |>protocol_piece sh l s ord T.
Axiom protocol_delay : forall sh l s,
protocol_piece sh l s ord T |-- protocol_piece sh l s ord (|>Tread, |>Tfull).
End protocols.
Definition OrdType s := ArrowType s (ArrowType s (ConstType Prop)).
Definition PredType s := ArrowType s (ArrowType (ConstType Z) Mpred).
Program Definition load_acq_spec := TYPE LA_type
WITH l : val, s : _, st_ord : _ -> _ -> Prop, T : ((_ -> Z -> mpred) * (_ -> Z -> mpred)),
P : mpred, E : _, Q : _ -> Z -> mpred
PRE [ 1%positive OF tptr tint ]
PROP ()
LOCAL (temp 1%positive l)
SEP (ALL s' : _, !!(st_ord s s') --> ALL v : _,
weak_fview_shift E E (fst T s' v * P * protocol_R l s' st_ord T) (Q s' v) && emp;
P; protocol_R l s st_ord T)
POST [ tint ]
EX v : Z, EX s' : _,
PROP (repable_signed v; st_ord s s')
LOCAL (temp ret_temp (vint v))
SEP (Q s' v).
Next Obligation.
Proof.
repeat intro.
destruct x as ((((((?, s), ?), (?, ?)), P), ?), Q); simpl.
unfold PROPx, LOCALx, SEPx; simpl; rewrite !approx_andp; f_equal;
f_equal; rewrite !sepcon_emp, ?approx_sepcon, ?approx_idem.
unfold protocol_R; rewrite protocol_piece_super_non_expansive; f_equal.
rewrite !approx_allp by auto; f_equal; extensionality.
setoid_rewrite approx_imp; f_equal; f_equal.
rewrite !(approx_allp _ _ _ 0); f_equal; extensionality.
rewrite !approx_andp; f_equal.
rewrite fview_shift_nonexpansive.
setoid_rewrite fview_shift_nonexpansive at 2.
rewrite !approx_sepcon, !approx_idem, protocol_piece_super_non_expansive; auto.
Qed.
Next Obligation.
Proof.
repeat intro.
destruct x as ((((((?, ?), ?), ?), ?), ?), ?); simpl.
rewrite !approx_exp; apply f_equal; extensionality.
rewrite !approx_exp; apply f_equal; extensionality.
unfold PROPx, LOCALx, SEPx; simpl; rewrite !approx_andp; do 2 apply f_equal;
rewrite !sepcon_emp, ?approx_sepcon, ?approx_idem; auto.
Qed.
Program Definition store_rel_spec := TYPE SR_type
WITH l : val, v : Z, s : _, s'' : _, st_ord : _ -> _ -> Prop, T : ((_ -> Z -> mpred) * (_ -> Z -> mpred)),
P : mpred, E : _, Q : mpred
PRE [ 1%positive OF tptr tint, 2%positive OF tint ]
PROP (repable_signed v; st_ord s s'')
LOCAL (temp 1%positive l; temp 2%positive (vint v))
SEP (ALL v0 : Z, weak_fview_shift E E
(P * snd T s v0 * protocol_W l s'' st_ord T) (Q * |> snd T s'' v) && emp;
P; protocol_W l s st_ord T)
POST [ tvoid ]
PROP ()
LOCAL ()
SEP (protocol_W l s'' st_ord T; Q).
Next Obligation.
Proof.
repeat intro.
destruct x as ((((((((?, ?), ?), ?), ?), (?, ?)), ?), ?), ?); simpl.
unfold PROPx; simpl; rewrite !approx_andp; f_equal.
unfold LOCALx; simpl; rewrite !approx_andp; apply f_equal.
unfold SEPx; simpl; rewrite !sepcon_emp, !approx_sepcon, !approx_idem.
unfold protocol_W; rewrite protocol_piece_super_non_expansive; f_equal.
rewrite !approx_allp by auto; f_equal; extensionality.
rewrite !approx_andp; f_equal.
rewrite fview_shift_nonexpansive.
setoid_rewrite fview_shift_nonexpansive at 2.
rewrite !approx_sepcon, !approx_idem, protocol_piece_super_non_expansive; f_equal; f_equal; f_equal.
destruct n; [rewrite !approx_0; auto|].
setoid_rewrite approx_later.
etransitivity; [rewrite <- approx_oo_approx' with (n' := S n)|]; auto.
Qed.
Next Obligation.
Proof.
repeat intro.
destruct x as ((((((((?, ?), ?), ?), ?), (?, ?)), ?), ?), ?); simpl.
unfold PROPx, LOCALx, SEPx; simpl; rewrite !approx_andp; do 2 apply f_equal;
rewrite !sepcon_emp, ?approx_sepcon, ?approx_idem.
unfold protocol_W; rewrite protocol_piece_super_non_expansive; auto.
Qed.
(* There's no need for a CAS because anyone with write permission knows the current value already. *)
End atomics.
(*(* Witnesses for common use cases *)
(* simple load_acq with read assertion *)
Definition load_acq_witness {state} l (s : state) st_ord T P Q := (l, s, st_ord, T, protocol_R l s st_ord T * P,
fun _ : Z => FF, @nil Z, P, fun s' (v' : Z) => protocol_R l s' st_ord T * Q s' v').
(* simple load_acq with write assertion *)
Definition load_acq_W_witness {state} l (s : state) st_ord T P Q := (l, s, st_ord, T, protocol_W l s st_ord T * P,
fun _ : Z => FF, @nil Z, protocol_W l s st_ord T * P,
fun s' (v' : Z) => !!(s' = s) && protocol_W l s st_ord T * Q s' v').
(* simple store_rel recovering write assertion *)
Definition store_rel_witness {state} l (v : Z) (s s'' : state) st_ord T P Q := (l, v, s, s'', st_ord, T,
protocol_W l s st_ord T * P, fun _ : Z => FF, @nil Z, P, protocol_W l s'' st_ord T * Q).*)