-
Notifications
You must be signed in to change notification settings - Fork 0
/
Transition_Rules.thy
189 lines (178 loc) · 9.33 KB
/
Transition_Rules.thy
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
187
188
189
theory Transition_Rules
imports Rules
begin
context rules
begin
text \<open>
A series of lemmas that demonstrate the logic's rules are preserved across the semantic steps and
ensure any executed behaviours conform to the desired specification.
\<close>
section \<open>Reordering Rules\<close>
text \<open>
Reorder the judgements of a reorderable instruction \<alpha> and program c, given a suitable
interference property.
\<close>
lemma reorder_prog:
assumes "R,G \<turnstile> P {c} M" "R,G \<turnstile>\<^sub>A M {\<alpha>} Q" "inter\<^sub>c w R G c \<alpha>" "\<alpha>' < c <\<^sub>w \<alpha>"
obtains M' where "R,G \<turnstile>\<^sub>A stabilise R P {\<alpha>'} M'" "R,G \<turnstile> M' {c} Q"
using assms
proof (induct c arbitrary: R G P M Q \<alpha> \<alpha>')
case Nil
hence "stabilise R P \<subseteq> M" using stable_preE'[OF Nil(2)] by blast
then show ?case using Nil atomic_rule_def unfolding reorder_com.simps
by (metis atomic_pre nil stable_stabilise)
next
case (Basic \<beta>)
obtain N' where \<beta>: "R,G \<turnstile>\<^sub>A stabilise R P {\<beta>} N'" "N' \<subseteq> M" using Basic by auto
have m': "R,G \<turnstile>\<^sub>A N' {\<alpha>} Q"
using atomic_pre[OF Basic(3)] \<beta>(1,2) Basic(3) by (auto simp: atomic_rule_def)
obtain M' where m'': "R,G \<turnstile>\<^sub>A stabilise R P {\<alpha>'} M'" "R,G \<turnstile>\<^sub>A M' {\<beta>} Q"
using \<beta>(1) m'(1) Basic
unfolding inter\<^sub>\<alpha>_def inter\<^sub>c.simps reorder_com.simps by metis
have "R,G \<turnstile> M' {Basic \<beta>} Q" by (rule rules.basic[OF m''(2)])
then show ?case using Basic(1) \<beta>(1) m''(1) by auto
next
case (Seq c\<^sub>1 w' c\<^sub>2)
obtain M' where m: "R,G \<turnstile> P {c\<^sub>1} M'" "R,G \<turnstile> M' {c\<^sub>2} M" using Seq(4) by fast
obtain \<alpha>'' where r: "\<alpha>'' < c\<^sub>2 <\<^sub>w \<alpha>" "\<alpha>' < c\<^sub>1 <\<^sub>w \<alpha>''" using Seq(7) by auto
hence i: "inter\<^sub>c w R G c\<^sub>1 \<alpha>''" "inter\<^sub>c w R G c\<^sub>2 \<alpha>" using Seq(6) unfolding inter\<^sub>c.simps by blast+
show ?case
proof (rule Seq(2)[OF _ m(2) Seq(5) i(2) r(1)], goal_cases outer)
case (outer N')
hence c1: "R,G \<turnstile> P {c\<^sub>1} stabilise R M'" using m(1) conseq stabilise_supset[of M'] by fast
show ?case
proof (rule Seq(1)[OF _ c1 outer(1) i(1) r(2)], goal_cases inner)
case (inner M'')
then show ?case using Seq(3) outer by auto
qed
qed
qed auto
section \<open>Transition Rules\<close>
text \<open>Judgements are preserved across thread-local execution steps\<close>
lemma lexecute_ruleI [intro]:
assumes "R,G \<turnstile> P {c} Q" "c \<mapsto>[\<alpha>',r] c'" "inter R G r"
shows "\<exists>M. R,G \<turnstile>\<^sub>A stabilise R P {\<alpha>'} M \<and> R,G \<turnstile> M {c'} Q"
using assms(2,1,3)
proof (induct arbitrary: P R G Q)
case (act \<alpha>)
then show ?case by clarsimp (meson atomic_rule_def nil rules.conseq order_refl)
next
case (ino c\<^sub>1 \<alpha>' r c\<^sub>1' w c\<^sub>2)
then obtain M' where m: "R,G \<turnstile> P {c\<^sub>1} M'" "R,G \<turnstile> M' {c\<^sub>2} Q" by auto
then show ?case using ino(2)[OF m(1) ino(4)] m(2) by blast
next
case (ooo c\<^sub>1 \<alpha>' r c\<^sub>1' \<alpha>'' c\<^sub>2 w)
obtain M' where m: "R,G \<turnstile> P {c\<^sub>2} M'" "R,G \<turnstile> M' {c\<^sub>1} Q" using ooo(4) by (rule seqE)
have i: "inter\<^sub>c w R G c\<^sub>2 \<alpha>'" "inter R G r" using ooo(5) by auto
obtain M where m': "R,G \<turnstile>\<^sub>A stabilise R M' {\<alpha>'} M" "R,G \<turnstile> M {c\<^sub>1'} Q"
using ooo(2)[OF m(2) i(2)] by auto
have m'': "R,G \<turnstile> P {c\<^sub>2} stabilise R M'" using m(1) stabilise_supset[of M' R] by auto
show ?case using reorder_prog[OF m'' m'(1)] i(1) m'(2) ooo(3) by (metis rules.seq)
next
case (cap c \<alpha>' r c' s s')
let ?R="uncapRely R" and ?G="uncapGuar G" and ?P="uncapPred s P" and ?Q="pushpredAll Q"
have "?R,?G \<turnstile> ?P {c} ?Q" using cap(3) by (rule captureE)
moreover have "inter ?R ?G r" using cap(4) by simp
ultimately obtain M where m: "?R,?G \<turnstile>\<^sub>A stabilise ?R ?P {\<alpha>'} M" "?R,?G \<turnstile> M {c'} ?Q"
using cap(2) by force
have "R,G \<turnstile>\<^sub>A stabilise R P {popbasic s s' \<alpha>'} poppred' s' M"
using helpa[OF m(1)[simplified stabilise_pushrel]] by simp
moreover have "R,G \<turnstile> (poppred' s' M) {Capture s' c'} Q"
using m(2) push_poppred_subset by blast
ultimately show ?case by blast
qed
lemma test:
assumes "pushpred s (stabilise R P) \<subseteq> pushpredAll Q" "x \<in> stabilise R P"
shows "x \<in> Q"
proof -
have "push x s \<in> pushpred s (stabilise R P)" using assms by auto
hence "push x s \<in> pushpredAll Q" using assms by auto
then obtain x' s' where e: "push x s = push x' s'" "x' \<in> Q" unfolding pushpredAll_def by auto
hence "x' = x" using push_inj by auto
thus ?thesis using e by auto
qed
text \<open>Judgements are preserved across silent steps\<close>
lemma rewrite_ruleI [intro]:
assumes "R,G \<turnstile> P {c} Q"
assumes "c \<leadsto> c'"
shows "R,G \<turnstile> P {c'} Q"
using assms
proof (induct arbitrary: c' rule: rules.induct)
case (seq R G P c\<^sub>1 Q c\<^sub>2 M)
thus ?case by (cases rule: silentE, auto) (blast)+
next
case (capture R G s P c Q)
show ?case using capture
proof (cases "Capture s c" c' rule: silentE)
case 1
then show ?case using capture by auto
next
case (15 k)
hence "uncapRely R,uncapGuar G \<turnstile> uncapPred s P {Nil} pushpredAll Q"
using capture(1) by simp
hence t: "stabilise (uncapRely R) (uncapPred s P) \<subseteq> pushpredAll Q"
using nilE2 by simp
have "R,G \<turnstile> stabilise R P {Nil} stabilise R P"
by (simp add: rules.rules.nil stable_stabilise)
moreover have "P \<subseteq> stabilise R P"
by (simp add: stabilise_supset)
moreover have "stabilise R P \<subseteq> Q"
using t test unfolding stabilise_pushrel by blast
ultimately show ?thesis using 15(2) by blast
next
case (16 c'' c''' k)
then show ?thesis using capture by auto
qed auto
qed (cases rule: silentE, auto)+
text \<open>Judgements are preserved across global execution steps\<close>
lemma gexecute_ruleI [intro]:
assumes "R,G \<turnstile> P {c} Q"
assumes "c \<mapsto>[g] c'" "P \<noteq> {}"
shows "\<exists>M v. P \<subseteq> wp v g M \<and> guar v g G \<and> R,G \<turnstile> M {c'} Q"
using assms
proof (induct arbitrary: g c' rule: rules.induct)
case (par R\<^sub>1 G\<^sub>1 P\<^sub>1 c\<^sub>1 Q\<^sub>1 R\<^sub>2 G\<^sub>2 P\<^sub>2 c\<^sub>2 Q\<^sub>2)
show ?case using par(7)
proof cases
case (par1 c\<^sub>1')
obtain M\<^sub>2 where m2: "P\<^sub>2 \<subseteq> M\<^sub>2" "stable R\<^sub>2 M\<^sub>2" "R\<^sub>2,G\<^sub>2 \<turnstile> M\<^sub>2 {c\<^sub>2} Q\<^sub>2" using par
by (meson stable_preE)
hence "P\<^sub>1 \<noteq> {}" using par by blast
then obtain M\<^sub>1 v where m1: "P\<^sub>1 \<subseteq> wp v g M\<^sub>1" "guar v g G\<^sub>1" "R\<^sub>1,G\<^sub>1 \<turnstile> M\<^sub>1 {c\<^sub>1'} Q\<^sub>1"
using par1 par(2)[OF par1(2)] by blast
hence "R\<^sub>1 \<inter> R\<^sub>2,G\<^sub>1 \<union> G\<^sub>2 \<turnstile> M\<^sub>1 \<inter> M\<^sub>2 {c'} Q\<^sub>1 \<inter> Q\<^sub>2" using par1 m2 par by blast
moreover have "P\<^sub>1 \<inter> P\<^sub>2 \<subseteq> wp v g (M\<^sub>1 \<inter> M\<^sub>2)"
using m1(1,2) m2(1,2) par.hyps(6) unfolding guar_def wp_def stable_def
by auto blast
ultimately show ?thesis using m1(2) unfolding guar_def by blast
next
case (par2 c\<^sub>2')
obtain M\<^sub>1 where m1: "P\<^sub>1 \<subseteq> M\<^sub>1" "stable R\<^sub>1 M\<^sub>1" "R\<^sub>1,G\<^sub>1 \<turnstile> M\<^sub>1 {c\<^sub>1} Q\<^sub>1" using par
by (meson stable_preE)
hence "P\<^sub>2 \<noteq> {}" using par by blast
then obtain M\<^sub>2 v where m2: "P\<^sub>2 \<subseteq> wp v g M\<^sub>2" "guar v g G\<^sub>2" "R\<^sub>2,G\<^sub>2 \<turnstile> M\<^sub>2 {c\<^sub>2'} Q\<^sub>2"
using par2 par(4)[OF par2(2)] by blast
hence "R\<^sub>1 \<inter> R\<^sub>2,G\<^sub>1 \<union> G\<^sub>2 \<turnstile> M\<^sub>1 \<inter> M\<^sub>2 {c'} Q\<^sub>1 \<inter> Q\<^sub>2" using par2 m1 par by blast
moreover have "P\<^sub>1 \<inter> P\<^sub>2 \<subseteq> wp v g (M\<^sub>1 \<inter> M\<^sub>2)"
using m1(1,2) m2(1,2) par.hyps(5) unfolding guar_def wp_def stable_def
by auto blast
ultimately show ?thesis using m2(2) unfolding guar_def by blast
qed
next
case (conseq R G P c Q P' R' G' Q')
hence "P \<noteq> {}" by auto
thus ?case using conseq by (smt Un_iff guar_def rules.conseq subset_iff)
next
case (inv R G P c Q R' M')
then obtain M v where p: "P \<subseteq> wp v g M" "guar v g G" "R,G \<turnstile> M {c'} Q" by blast
hence "P \<inter> M' \<subseteq> wp v g (M \<inter> M')" using inv(3,4) by (auto simp: stable_def guar_def wp_def) blast
thus ?case using rules.inv p(2,3) inv(3,4) by blast
next
case (thread R G P c Q)
then obtain r \<alpha>' c'' where e: "g = beh \<alpha>'" "c \<mapsto>[\<alpha>',r] c''" "c' = Thread c''" by blast
then obtain M where "R,G \<turnstile>\<^sub>A stabilise R P {\<alpha>'} M" "R,G \<turnstile> M {c''} Q" "rif R G c''"
using thread lexecute_ruleI[OF thread(1) e(2)] indep_stepI[OF thread(3) e(2)] by metis
thus ?case using stabilise_supset[of P R] e thread(5) unfolding atomic_rule_def by blast
qed auto
end
end