author | paulson |
Wed, 05 Aug 1998 10:57:25 +0200 | |
changeset 5253 | 82a5ca6290aa |
parent 5240 | bbcd79ef7cf2 |
child 5277 | e4297d03e5d2 |
permissions | -rw-r--r-- |
5111 | 1 |
(* Title: HOL/UNITY/Mutex |
4776 | 2 |
ID: $Id$ |
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
||
6 |
Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra |
|
7 |
*) |
|
8 |
||
5232 | 9 |
(*split_all_tac causes a big blow-up*) |
10 |
claset_ref() := claset() delSWrapper "split_all_tac"; |
|
4776 | 11 |
|
5253 | 12 |
val cmd_defs = [Mprg_def, |
5232 | 13 |
cmd0U_def, cmd1U_def, cmd2U_def, cmd3U_def, cmd4U_def, |
14 |
cmd0V_def, cmd1V_def, cmd2V_def, cmd3V_def, cmd4V_def]; |
|
4776 | 15 |
|
5253 | 16 |
Goalw [Mprg_def] "id : Acts Mprg"; |
4776 | 17 |
by (Simp_tac 1); |
5253 | 18 |
qed "id_in_Acts"; |
19 |
AddIffs [id_in_Acts]; |
|
4776 | 20 |
|
21 |
||
5232 | 22 |
(*Simplification for records*) |
23 |
val select_defs = thms"state.select_defs" |
|
24 |
and update_defs = thms"state.update_defs" |
|
25 |
and dest_defs = thms"state.dest_defs"; |
|
26 |
||
27 |
Addsimps update_defs; |
|
28 |
||
29 |
||
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
30 |
Addsimps [invariantU_def, invariantV_def]; |
4776 | 31 |
|
32 |
||
5253 | 33 |
Goalw [Mprg_def] "invariant Mprg invariantU"; |
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
34 |
by (rtac invariantI 1); |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
35 |
by (constrains_tac cmd_defs 2); |
5232 | 36 |
by Auto_tac; |
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
37 |
qed "invariantU"; |
4776 | 38 |
|
5253 | 39 |
Goalw [Mprg_def] "invariant Mprg invariantV"; |
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
40 |
by (rtac invariantI 1); |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
41 |
by (constrains_tac cmd_defs 2); |
4776 | 42 |
by Auto_tac; |
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
43 |
qed "invariantV"; |
4776 | 44 |
|
5253 | 45 |
val invariantUV = invariant_Int_rule [invariantU, invariantV]; |
4776 | 46 |
|
47 |
||
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
48 |
(*The safety property: mutual exclusion*) |
5253 | 49 |
Goal "(reachable Mprg) Int {s. MM s = 3 & NN s = 3} = {}"; |
50 |
by (cut_facts_tac [invariantUV RS invariant_includes_reachable] 1); |
|
4776 | 51 |
by Auto_tac; |
52 |
qed "mutual_exclusion"; |
|
53 |
||
54 |
||
5232 | 55 |
(*The bad invariant FAILS in cmd1V*) |
5253 | 56 |
Goalw [bad_invariantU_def] "stable (Acts Mprg) bad_invariantU"; |
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
57 |
by (constrains_tac cmd_defs 1); |
5232 | 58 |
by (REPEAT (trans_tac 1)); |
4776 | 59 |
by (safe_tac (claset() addSEs [le_SucE])); |
60 |
by (Asm_full_simp_tac 1); |
|
61 |
(*Resulting state: n=1, p=false, m=4, u=false. |
|
5232 | 62 |
Execution of cmd1V (the command of process v guarded by n=1) sets p:=true, |
4776 | 63 |
violating the invariant!*) |
64 |
(*Check that subgoals remain: proof failed.*) |
|
65 |
getgoal 1; |
|
66 |
||
67 |
||
68 |
(*** Progress for U ***) |
|
69 |
||
5253 | 70 |
Goalw [unless_def] "unless (Acts Mprg) {s. MM s=2} {s. MM s=3}"; |
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
71 |
by (constrains_tac cmd_defs 1); |
4776 | 72 |
qed "U_F0"; |
73 |
||
5253 | 74 |
Goal "LeadsTo Mprg {s. MM s=1} {s. PP s = VV s & MM s = 2}"; |
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
75 |
by (ensures_tac cmd_defs "cmd1U" 1); |
4776 | 76 |
qed "U_F1"; |
77 |
||
5253 | 78 |
Goal "LeadsTo Mprg {s. ~ PP s & MM s = 2} {s. MM s = 3}"; |
79 |
by (cut_facts_tac [invariantUV] 1); |
|
80 |
bw Mprg_def; |
|
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
81 |
by (ensures_tac cmd_defs "cmd2U" 1); |
4776 | 82 |
qed "U_F2"; |
83 |
||
5253 | 84 |
Goal "LeadsTo Mprg {s. MM s = 3} {s. PP s}"; |
4776 | 85 |
by (rtac leadsTo_imp_LeadsTo 1); |
5232 | 86 |
by (res_inst_tac [("B", "{s. MM s = 4}")] leadsTo_Trans 1); |
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
87 |
by (ensures_tac cmd_defs "cmd4U" 2); |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
88 |
by (ensures_tac cmd_defs "cmd3U" 1); |
4776 | 89 |
qed "U_F3"; |
90 |
||
5253 | 91 |
Goal "LeadsTo Mprg {s. MM s = 2} {s. PP s}"; |
4776 | 92 |
by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo] |
93 |
MRS LeadsTo_Diff) 1); |
|
94 |
by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1); |
|
95 |
by (auto_tac (claset() addSEs [less_SucE], simpset())); |
|
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
96 |
val U_lemma2 = result(); |
4776 | 97 |
|
5253 | 98 |
Goal "LeadsTo Mprg {s. MM s = 1} {s. PP s}"; |
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
99 |
by (rtac ([U_F1 RS LeadsTo_weaken_R, U_lemma2] MRS LeadsTo_Trans) 1); |
4776 | 100 |
by (Blast_tac 1); |
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
101 |
val U_lemma1 = result(); |
4776 | 102 |
|
5253 | 103 |
Goal "LeadsTo Mprg {s. 1 <= MM s & MM s <= 3} {s. PP s}"; |
4776 | 104 |
by (simp_tac (simpset() addsimps [le_Suc_eq, conj_disj_distribL] |
105 |
addcongs [rev_conj_cong]) 1); |
|
106 |
by (simp_tac (simpset() addsimps [Collect_disj_eq, LeadsTo_Un_distrib, |
|
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
107 |
U_lemma1, U_lemma2, U_F3] ) 1); |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
108 |
val U_lemma123 = result(); |
4776 | 109 |
|
110 |
(*Misra's F4*) |
|
5253 | 111 |
Goal "LeadsTo Mprg {s. UU s} {s. PP s}"; |
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
112 |
by (rtac ([invariantU, U_lemma123] MRS invariant_LeadsTo_weaken) 1); |
4776 | 113 |
by Auto_tac; |
114 |
qed "u_leadsto_p"; |
|
115 |
||
116 |
||
117 |
(*** Progress for V ***) |
|
118 |
||
119 |
||
5253 | 120 |
Goalw [unless_def] "unless (Acts Mprg) {s. NN s=2} {s. NN s=3}"; |
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
121 |
by (constrains_tac cmd_defs 1); |
4776 | 122 |
qed "V_F0"; |
123 |
||
5253 | 124 |
Goal "LeadsTo Mprg {s. NN s=1} {s. PP s = (~ UU s) & NN s = 2}"; |
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
125 |
by (ensures_tac cmd_defs "cmd1V" 1); |
4776 | 126 |
qed "V_F1"; |
127 |
||
5253 | 128 |
Goal "LeadsTo Mprg {s. PP s & NN s = 2} {s. NN s = 3}"; |
129 |
by (cut_facts_tac [invariantUV] 1); |
|
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
130 |
by (ensures_tac cmd_defs "cmd2V" 1); |
4776 | 131 |
qed "V_F2"; |
132 |
||
5253 | 133 |
Goal "LeadsTo Mprg {s. NN s = 3} {s. ~ PP s}"; |
4776 | 134 |
by (rtac leadsTo_imp_LeadsTo 1); |
5232 | 135 |
by (res_inst_tac [("B", "{s. NN s = 4}")] leadsTo_Trans 1); |
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
136 |
by (ensures_tac cmd_defs "cmd4V" 2); |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
137 |
by (ensures_tac cmd_defs "cmd3V" 1); |
4776 | 138 |
qed "V_F3"; |
139 |
||
5253 | 140 |
Goal "LeadsTo Mprg {s. NN s = 2} {s. ~ PP s}"; |
4776 | 141 |
by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo] |
142 |
MRS LeadsTo_Diff) 1); |
|
143 |
by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1); |
|
144 |
by (auto_tac (claset() addSEs [less_SucE], simpset())); |
|
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
145 |
val V_lemma2 = result(); |
4776 | 146 |
|
5253 | 147 |
Goal "LeadsTo Mprg {s. NN s = 1} {s. ~ PP s}"; |
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
148 |
by (rtac ([V_F1 RS LeadsTo_weaken_R, V_lemma2] MRS LeadsTo_Trans) 1); |
4776 | 149 |
by (Blast_tac 1); |
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
150 |
val V_lemma1 = result(); |
4776 | 151 |
|
5253 | 152 |
Goal "LeadsTo Mprg {s. 1 <= NN s & NN s <= 3} {s. ~ PP s}"; |
4776 | 153 |
by (simp_tac (simpset() addsimps [le_Suc_eq, conj_disj_distribL] |
154 |
addcongs [rev_conj_cong]) 1); |
|
155 |
by (simp_tac (simpset() addsimps [Collect_disj_eq, LeadsTo_Un_distrib, |
|
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
156 |
V_lemma1, V_lemma2, V_F3] ) 1); |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
157 |
val V_lemma123 = result(); |
4776 | 158 |
|
159 |
||
160 |
(*Misra's F4*) |
|
5253 | 161 |
Goal "LeadsTo Mprg {s. VV s} {s. ~ PP s}"; |
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
162 |
by (rtac ([invariantV, V_lemma123] MRS invariant_LeadsTo_weaken) 1); |
4776 | 163 |
by Auto_tac; |
164 |
qed "v_leadsto_not_p"; |
|
165 |
||
166 |
||
167 |
(** Absence of starvation **) |
|
168 |
||
169 |
(*Misra's F6*) |
|
5253 | 170 |
Goal "LeadsTo Mprg {s. MM s = 1} {s. MM s = 3}"; |
4776 | 171 |
by (rtac LeadsTo_Un_duplicate 1); |
172 |
by (rtac LeadsTo_cancel2 1); |
|
173 |
by (rtac U_F2 2); |
|
174 |
by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1); |
|
175 |
by (stac Un_commute 1); |
|
176 |
by (rtac LeadsTo_Un_duplicate 1); |
|
5111 | 177 |
by (rtac ([v_leadsto_not_p, U_F0] MRS R_PSP_unless RSN(2, LeadsTo_cancel2)) 1); |
4776 | 178 |
by (rtac (U_F1 RS LeadsTo_weaken_R) 1); |
179 |
by (auto_tac (claset() addSEs [less_SucE], simpset())); |
|
180 |
qed "m1_leadsto_3"; |
|
181 |
||
182 |
||
183 |
(*The same for V*) |
|
5253 | 184 |
Goal "LeadsTo Mprg {s. NN s = 1} {s. NN s = 3}"; |
4776 | 185 |
by (rtac LeadsTo_Un_duplicate 1); |
186 |
by (rtac LeadsTo_cancel2 1); |
|
187 |
by (rtac V_F2 2); |
|
188 |
by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1); |
|
189 |
by (stac Un_commute 1); |
|
190 |
by (rtac LeadsTo_Un_duplicate 1); |
|
191 |
by (rtac ([u_leadsto_p, V_F0] MRS R_PSP_unless RSN(2, LeadsTo_cancel2)) 1); |
|
192 |
by (rtac (V_F1 RS LeadsTo_weaken_R) 1); |
|
193 |
by (auto_tac (claset() addSEs [less_SucE], simpset())); |
|
194 |
qed "n1_leadsto_3"; |