author | paulson |
Tue, 04 May 1999 10:26:00 +0200 | |
changeset 6570 | a7d7985050a9 |
parent 6565 | de4acf4449fa |
child 6615 | f72f560af0a1 |
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*) |
5706 | 10 |
claset_ref() := claset() delSWrapper record_split_name; |
4776 | 11 |
|
6565 | 12 |
Addsimps [Mutex_def RS def_prg_Init]; |
13 |
program_defs_ref := [Mutex_def]; |
|
4776 | 14 |
|
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
15 |
Addsimps (map simp_of_act |
6565 | 16 |
[U0_def, U1_def, U2_def, U3_def, U4_def, |
17 |
V0_def, V1_def, V2_def, V3_def, V4_def]); |
|
4776 | 18 |
|
6570 | 19 |
Addsimps (map simp_of_set [IU_def, IV_def, bad_IU_def]); |
4776 | 20 |
|
5232 | 21 |
(*Simplification for records*) |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
22 |
Addsimps (thms"state.update_defs"); |
5232 | 23 |
|
6570 | 24 |
Goal "Mutex : Always IU"; |
25 |
by (rtac AlwaysI 1); |
|
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
26 |
by (constrains_tac 2); |
5232 | 27 |
by Auto_tac; |
6570 | 28 |
qed "IU"; |
4776 | 29 |
|
6570 | 30 |
Goal "Mutex : Always IV"; |
31 |
by (rtac AlwaysI 1); |
|
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
32 |
by (constrains_tac 2); |
4776 | 33 |
by Auto_tac; |
6570 | 34 |
qed "IV"; |
4776 | 35 |
|
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
36 |
(*The safety property: mutual exclusion*) |
6570 | 37 |
Goal "Mutex : Always {s. ~ (m s = #3 & n s = #3)}"; |
38 |
by (rtac Always_weaken 1); |
|
39 |
by (rtac ([IU, IV] MRS Always_Int) 1); |
|
4776 | 40 |
by Auto_tac; |
41 |
qed "mutual_exclusion"; |
|
42 |
||
43 |
||
6565 | 44 |
(*The bad invariant FAILS in V1*) |
6570 | 45 |
Goal "Mutex : Always bad_IU"; |
46 |
by (rtac AlwaysI 1); |
|
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
47 |
by (constrains_tac 2); |
5596 | 48 |
by (Force_tac 1); |
49 |
(*Needs a decision procedure to simplify the resulting state*) |
|
50 |
by (auto_tac (claset(), |
|
51 |
simpset_of Int.thy addsimps |
|
52 |
[zadd_int, integ_of_Pls, integ_of_Min, |
|
53 |
integ_of_BIT, le_int_Suc_eq])); |
|
54 |
by (dtac zle_trans 1 THEN assume_tac 1); |
|
55 |
by (full_simp_tac (simpset_of Int.thy) 1); |
|
56 |
by (asm_full_simp_tac (simpset() addsimps int_simps) 1); |
|
4776 | 57 |
(*Resulting state: n=1, p=false, m=4, u=false. |
6565 | 58 |
Execution of V1 (the command of process v guarded by n=1) sets p:=true, |
4776 | 59 |
violating the invariant!*) |
60 |
(*Check that subgoals remain: proof failed.*) |
|
61 |
getgoal 1; |
|
62 |
||
63 |
||
6565 | 64 |
Goal "(#1 <= i & i <= #3) = (i = #1 | i = #2 | i = #3)"; |
5596 | 65 |
by (auto_tac (claset(), |
66 |
simpset_of Int.thy addsimps |
|
67 |
[zle_iff_zadd, zadd_int, integ_of_Pls, integ_of_Min, |
|
68 |
integ_of_BIT])); |
|
69 |
qed "eq_123"; |
|
70 |
||
71 |
||
4776 | 72 |
(*** Progress for U ***) |
73 |
||
6565 | 74 |
Goalw [Unless_def] "Mutex : {s. m s=#2} Unless {s. m s=#3}"; |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
75 |
by (constrains_tac 1); |
4776 | 76 |
qed "U_F0"; |
77 |
||
6565 | 78 |
Goal "Mutex : {s. m s=#1} LeadsTo {s. p s = v s & m s = #2}"; |
79 |
by (ensures_tac "U1" 1); |
|
4776 | 80 |
qed "U_F1"; |
81 |
||
6565 | 82 |
Goal "Mutex : {s. ~ p s & m s = #2} LeadsTo {s. m s = #3}"; |
6570 | 83 |
by (cut_facts_tac [IU] 1); |
6565 | 84 |
by (ensures_tac "U2" 1); |
4776 | 85 |
qed "U_F2"; |
86 |
||
6565 | 87 |
Goal "Mutex : {s. m s = #3} LeadsTo {s. p s}"; |
88 |
by (res_inst_tac [("B", "{s. m s = #4}")] LeadsTo_Trans 1); |
|
89 |
by (ensures_tac "U4" 2); |
|
90 |
by (ensures_tac "U3" 1); |
|
4776 | 91 |
qed "U_F3"; |
92 |
||
6565 | 93 |
Goal "Mutex : {s. m s = #2} LeadsTo {s. p s}"; |
5340 | 94 |
by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] |
4776 | 95 |
MRS LeadsTo_Diff) 1); |
96 |
by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1); |
|
97 |
by (auto_tac (claset() addSEs [less_SucE], simpset())); |
|
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
98 |
val U_lemma2 = result(); |
4776 | 99 |
|
6565 | 100 |
Goal "Mutex : {s. m s = #1} LeadsTo {s. p s}"; |
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
101 |
by (rtac ([U_F1 RS LeadsTo_weaken_R, U_lemma2] MRS LeadsTo_Trans) 1); |
4776 | 102 |
by (Blast_tac 1); |
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
103 |
val U_lemma1 = result(); |
4776 | 104 |
|
6565 | 105 |
Goal "Mutex : {s. #1 <= m s & m s <= #3} LeadsTo {s. p s}"; |
5596 | 106 |
by (simp_tac (simpset() addsimps [eq_123, 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*) |
|
6565 | 111 |
Goal "Mutex : {s. u s} LeadsTo {s. p s}"; |
6570 | 112 |
by (rtac ([IU, U_lemma123] MRS Always_LeadsTo_weaken) 1); |
4776 | 113 |
by Auto_tac; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
114 |
qed "u_Leadsto_p"; |
4776 | 115 |
|
116 |
||
117 |
(*** Progress for V ***) |
|
118 |
||
119 |
||
6565 | 120 |
Goalw [Unless_def] "Mutex : {s. n s=#2} Unless {s. n s=#3}"; |
5426
566f47250bd0
A new approach, using simp_of_act and simp_of_set to activate definitions when
paulson
parents:
5424
diff
changeset
|
121 |
by (constrains_tac 1); |
4776 | 122 |
qed "V_F0"; |
123 |
||
6565 | 124 |
Goal "Mutex : {s. n s=#1} LeadsTo {s. p s = (~ u s) & n s = #2}"; |
125 |
by (ensures_tac "V1" 1); |
|
4776 | 126 |
qed "V_F1"; |
127 |
||
6565 | 128 |
Goal "Mutex : {s. p s & n s = #2} LeadsTo {s. n s = #3}"; |
6570 | 129 |
by (cut_facts_tac [IV] 1); |
6565 | 130 |
by (ensures_tac "V2" 1); |
4776 | 131 |
qed "V_F2"; |
132 |
||
6565 | 133 |
Goal "Mutex : {s. n s = #3} LeadsTo {s. ~ p s}"; |
134 |
by (res_inst_tac [("B", "{s. n s = #4}")] LeadsTo_Trans 1); |
|
135 |
by (ensures_tac "V4" 2); |
|
136 |
by (ensures_tac "V3" 1); |
|
4776 | 137 |
qed "V_F3"; |
138 |
||
6565 | 139 |
Goal "Mutex : {s. n s = #2} LeadsTo {s. ~ p s}"; |
5340 | 140 |
by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] |
4776 | 141 |
MRS LeadsTo_Diff) 1); |
142 |
by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1); |
|
143 |
by (auto_tac (claset() addSEs [less_SucE], simpset())); |
|
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
144 |
val V_lemma2 = result(); |
4776 | 145 |
|
6565 | 146 |
Goal "Mutex : {s. n s = #1} LeadsTo {s. ~ p s}"; |
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
147 |
by (rtac ([V_F1 RS LeadsTo_weaken_R, V_lemma2] MRS LeadsTo_Trans) 1); |
4776 | 148 |
by (Blast_tac 1); |
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
149 |
val V_lemma1 = result(); |
4776 | 150 |
|
6565 | 151 |
Goal "Mutex : {s. #1 <= n s & n s <= #3} LeadsTo {s. ~ p s}"; |
5596 | 152 |
by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib, |
5240
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
153 |
V_lemma1, V_lemma2, V_F3] ) 1); |
bbcd79ef7cf2
Constant "invariant" and new constrains_tac, ensures_tac
paulson
parents:
5232
diff
changeset
|
154 |
val V_lemma123 = result(); |
4776 | 155 |
|
156 |
||
157 |
(*Misra's F4*) |
|
6565 | 158 |
Goal "Mutex : {s. v s} LeadsTo {s. ~ p s}"; |
6570 | 159 |
by (rtac ([IV, V_lemma123] MRS Always_LeadsTo_weaken) 1); |
4776 | 160 |
by Auto_tac; |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
161 |
qed "v_Leadsto_not_p"; |
4776 | 162 |
|
163 |
||
164 |
(** Absence of starvation **) |
|
165 |
||
166 |
(*Misra's F6*) |
|
6565 | 167 |
Goal "Mutex : {s. m s = #1} LeadsTo {s. m s = #3}"; |
4776 | 168 |
by (rtac LeadsTo_Un_duplicate 1); |
169 |
by (rtac LeadsTo_cancel2 1); |
|
170 |
by (rtac U_F2 2); |
|
171 |
by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1); |
|
172 |
by (stac Un_commute 1); |
|
173 |
by (rtac LeadsTo_Un_duplicate 1); |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
174 |
by (rtac ([v_Leadsto_not_p, U_F0] MRS PSP_Unless RSN(2, LeadsTo_cancel2)) 1); |
4776 | 175 |
by (rtac (U_F1 RS LeadsTo_weaken_R) 1); |
176 |
by (auto_tac (claset() addSEs [less_SucE], simpset())); |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
177 |
qed "m1_Leadsto_3"; |
4776 | 178 |
|
179 |
||
180 |
(*The same for V*) |
|
6565 | 181 |
Goal "Mutex : {s. n s = #1} LeadsTo {s. n s = #3}"; |
4776 | 182 |
by (rtac LeadsTo_Un_duplicate 1); |
183 |
by (rtac LeadsTo_cancel2 1); |
|
184 |
by (rtac V_F2 2); |
|
185 |
by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1); |
|
186 |
by (stac Un_commute 1); |
|
187 |
by (rtac LeadsTo_Un_duplicate 1); |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
188 |
by (rtac ([u_Leadsto_p, V_F0] MRS PSP_Unless RSN(2, LeadsTo_cancel2)) 1); |
4776 | 189 |
by (rtac (V_F1 RS LeadsTo_weaken_R) 1); |
190 |
by (auto_tac (claset() addSEs [less_SucE], simpset())); |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5277
diff
changeset
|
191 |
qed "n1_Leadsto_3"; |