author | paulson |
Fri, 17 Sep 1999 10:31:38 +0200 | |
changeset 7538 | 357873391561 |
parent 7537 | 875754b599df |
child 7540 | 8af61a565a4a |
permissions | -rw-r--r-- |
6828 | 1 |
(* Title: HOL/UNITY/Alloc |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
||
6 |
Specification of Chandy and Charpentier's Allocator |
|
7 |
*) |
|
8 |
||
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
9 |
|
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
10 |
Goal "~ f #2 ==> ~ (!t::nat. (#0 <= t & t <= #10) --> f t)"; |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
11 |
|
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
12 |
(*Useful examples: singletonI RS subst_elem, subst_elem RSN (2,IntI) *) |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
13 |
Goal "[| b:A; a=b |] ==> a:A"; |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
14 |
by (etac ssubst 1); |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
15 |
by (assume_tac 1); |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
16 |
qed "subst_elem"; |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
17 |
|
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
18 |
|
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
19 |
|
7538 | 20 |
Goal "(ALL i: lessThan n. f i <= g i) --> sum f n <= sum g n"; |
21 |
by (induct_tac "n" 1); |
|
22 |
by Auto_tac; |
|
23 |
by (dres_inst_tac [("x","n")] bspec 1); |
|
24 |
by Auto_tac; |
|
25 |
by (arith_tac 1); |
|
26 |
qed_spec_mp "sum_mono"; |
|
27 |
||
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
28 |
|
6840 | 29 |
(*Generalized version allowing different clients*) |
30 |
Goal "[| Alloc : alloc_spec; \ |
|
31 |
\ Client : (lessThan Nclients) funcset client_spec; \ |
|
32 |
\ Network : network_spec |] \ |
|
33 |
\ ==> (extend sysOfAlloc Alloc) \ |
|
34 |
\ Join (extend sysOfClient (PLam (lessThan Nclients) Client)) \ |
|
35 |
\ Join Network : system_spec"; |
|
36 |
||
37 |
Goal "System : system_spec"; |
|
38 |
||
39 |
||
6828 | 40 |
Goalw [sysOfAlloc_def] "inj sysOfAlloc"; |
41 |
by (rtac injI 1); |
|
7347 | 42 |
by (auto_tac (claset() addSWrapper record_split_wrapper, simpset())); |
6828 | 43 |
qed "inj_sysOfAlloc"; |
44 |
||
45 |
Goalw [sysOfAlloc_def] "surj sysOfAlloc"; |
|
46 |
by (res_inst_tac [("f", "%s. ((| allocGiv = allocGiv s, \ |
|
47 |
\ allocAsk = allocAsk s, \ |
|
48 |
\ allocRel = allocRel s |), \ |
|
49 |
\ client s)")] surjI 1); |
|
7347 | 50 |
by (auto_tac (claset() addSWrapper record_split_wrapper, simpset())); |
6828 | 51 |
qed "surj_sysOfAlloc"; |
52 |
||
53 |
AddIffs [inj_sysOfAlloc, surj_sysOfAlloc]; |
|
54 |
||
7482 | 55 |
Goalw [good_map_def] "good_map sysOfAlloc"; |
56 |
by Auto_tac; |
|
57 |
qed "good_map_sysOfAlloc"; |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
58 |
|
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
59 |
(*MUST BE AUTOMATED: even the statement of such results*) |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
60 |
Goal "!!s. inv sysOfAlloc s = \ |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
61 |
\ ((| allocGiv = allocGiv s, \ |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
62 |
\ allocAsk = allocAsk s, \ |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
63 |
\ allocRel = allocRel s|), \ |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
64 |
\ client s)"; |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
65 |
by (rtac (inj_sysOfAlloc RS inv_f_eq) 1); |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
66 |
by (auto_tac (claset() addSWrapper record_split_wrapper, |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
67 |
simpset() addsimps [sysOfAlloc_def])); |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
68 |
qed "inv_sysOfAlloc_eq"; |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
69 |
|
7538 | 70 |
Addsimps [inv_sysOfAlloc_eq]; |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
71 |
|
7365 | 72 |
(**SHOULD NOT BE NECESSARY: The various injections into the system |
73 |
state need to be treated symmetrically or done automatically*) |
|
7347 | 74 |
Goalw [sysOfClient_def] "inj sysOfClient"; |
75 |
by (rtac injI 1); |
|
76 |
by (auto_tac (claset() addSDs [inj_sysOfAlloc RS injD] |
|
77 |
addSWrapper record_split_wrapper, simpset())); |
|
78 |
qed "inj_sysOfClient"; |
|
79 |
||
80 |
Goalw [sysOfClient_def] "surj sysOfClient"; |
|
81 |
by (cut_facts_tac [surj_sysOfAlloc] 1); |
|
82 |
by (rewtac surj_def); |
|
83 |
by Auto_tac; |
|
84 |
by (Blast_tac 1); |
|
85 |
qed "surj_sysOfClient"; |
|
86 |
||
87 |
AddIffs [inj_sysOfClient, surj_sysOfClient]; |
|
88 |
||
7482 | 89 |
Goalw [good_map_def] "good_map sysOfClient"; |
90 |
by Auto_tac; |
|
91 |
qed "good_map_sysOfClient"; |
|
6828 | 92 |
|
7347 | 93 |
(*MUST BE AUTOMATED: even the statement of such results*) |
94 |
Goal "!!s. inv sysOfClient s = \ |
|
95 |
\ (client s, \ |
|
96 |
\ (| allocGiv = allocGiv s, \ |
|
97 |
\ allocAsk = allocAsk s, \ |
|
98 |
\ allocRel = allocRel s|) )"; |
|
99 |
by (rtac (inj_sysOfClient RS inv_f_eq) 1); |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
100 |
by (auto_tac (claset() addSWrapper record_split_wrapper, |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
101 |
simpset() addsimps [sysOfAlloc_def, sysOfClient_def])); |
7365 | 102 |
qed "inv_sysOfClient_eq"; |
6837 | 103 |
|
104 |
||
7365 | 105 |
Open_locale "System"; |
106 |
||
107 |
val Alloc = thm "Alloc"; |
|
108 |
val Client = thm "Client"; |
|
109 |
val Network = thm "Network"; |
|
110 |
val System_def = thm "System_def"; |
|
111 |
||
112 |
AddIffs [finite_lessThan]; |
|
113 |
||
114 |
(*Client : <unfolded specification> *) |
|
115 |
val Client_Spec = |
|
116 |
rewrite_rule [client_spec_def, client_increasing_def, |
|
117 |
client_bounded_def, client_progress_def] Client; |
|
118 |
||
119 |
Goal "Client : UNIV guarantees Increasing ask"; |
|
120 |
by (cut_facts_tac [Client_Spec] 1); |
|
121 |
by (asm_full_simp_tac (simpset() addsimps [guarantees_Int_right]) 1); |
|
122 |
qed "Client_Increasing_ask"; |
|
123 |
||
124 |
Goal "Client : UNIV guarantees Increasing rel"; |
|
125 |
by (cut_facts_tac [Client_Spec] 1); |
|
126 |
by (asm_full_simp_tac (simpset() addsimps [guarantees_Int_right]) 1); |
|
127 |
qed "Client_Increasing_rel"; |
|
128 |
||
129 |
AddIffs [Client_Increasing_ask, Client_Increasing_rel]; |
|
130 |
||
131 |
Goal "Client : UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}"; |
|
132 |
by (cut_facts_tac [Client_Spec] 1); |
|
133 |
by Auto_tac; |
|
134 |
qed "Client_Bounded"; |
|
135 |
||
136 |
(*Client_Progress is cumbersome to state*) |
|
137 |
val Client_Progress = Client_Spec RS IntD2; |
|
6828 | 138 |
|
139 |
||
7365 | 140 |
(*Network : <unfolded specification> *) |
141 |
val Network_Spec = |
|
142 |
rewrite_rule [network_spec_def, network_ask_def, |
|
143 |
network_giv_def, network_rel_def] Network; |
|
144 |
||
145 |
(*CANNOT use bind_thm: it puts the theorem into standard form, in effect |
|
146 |
exporting it from the locale*) |
|
147 |
val Network_Ask = Network_Spec RS IntD1 RS IntD1; |
|
148 |
val Network_Giv = Network_Spec RS IntD1 RS IntD2; |
|
149 |
val Network_Rel = Network_Spec RS IntD2 RS INT_D; |
|
150 |
||
151 |
||
152 |
(*Alloc : <unfolded specification> *) |
|
153 |
val Alloc_Spec = |
|
154 |
rewrite_rule [alloc_spec_def, alloc_increasing_def, |
|
155 |
alloc_safety_def, alloc_progress_def] Alloc; |
|
156 |
||
157 |
Goal "i < Nclients ==> Alloc : UNIV guarantees Increasing (sub i o allocAsk)"; |
|
158 |
by (cut_facts_tac [Alloc_Spec] 1); |
|
159 |
by (asm_full_simp_tac (simpset() addsimps [guarantees_INT_right]) 1); |
|
160 |
qed "Alloc_Increasing"; |
|
161 |
||
162 |
val Alloc_Safety = Alloc_Spec RS IntD1 RS IntD2; |
|
163 |
val Alloc_Progress = (Alloc_Spec RS IntD2 |
|
164 |
|> simplify (simpset() addsimps [guarantees_INT_right])) |
|
165 |
RS bspec RS spec; |
|
166 |
||
167 |
||
7347 | 168 |
|
7365 | 169 |
(*Not sure what to say about the other components because they involve |
170 |
extend*) |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
171 |
Goalw [System_def] "Network <= System"; |
7365 | 172 |
by (blast_tac (claset() addIs [componentI]) 1); |
173 |
qed "Network_component_System"; |
|
174 |
||
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
175 |
Goalw [System_def] "(extend sysOfAlloc Alloc) <= System"; |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
176 |
by (blast_tac (claset() addIs [componentI]) 1); |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
177 |
qed "Alloc_component_System"; |
7365 | 178 |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
179 |
AddIffs [Network_component_System, Alloc_component_System]; |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
180 |
|
7365 | 181 |
|
182 |
(* F : UNIV guarantees Increasing func |
|
183 |
==> extend sysOfClient F : UNIV guarantees Increasing (func o client) *) |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
184 |
val extend_Client_guar_Increasing = |
7482 | 185 |
good_map_sysOfClient RS export extend_guar_Increasing |
7365 | 186 |
|> simplify (simpset() addsimps [inv_sysOfClient_eq]); |
187 |
||
188 |
||
189 |
(** Proof of property (1) **) |
|
190 |
||
191 |
(*step 1*) |
|
192 |
Goalw [System_def] |
|
193 |
"i < Nclients ==> System : Increasing (rel o sub i o client)"; |
|
194 |
by (rtac ([guaranteesI RS disjI2 RS guarantees_Join_I, UNIV_I] |
|
195 |
MRS guaranteesD) 1); |
|
196 |
by (asm_simp_tac |
|
197 |
(simpset() addsimps [guarantees_PLam_I, |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
198 |
extend_Client_guar_Increasing RS guaranteesD, |
7365 | 199 |
lift_prog_guar_Increasing]) 1); |
7347 | 200 |
qed "System_Increasing_rel"; |
6828 | 201 |
|
7365 | 202 |
(*Note: the first step above performs simple quantifier reasoning. It could |
203 |
be replaced by a proof mentioning no guarantees primitives*) |
|
6828 | 204 |
|
205 |
||
7365 | 206 |
(*step 2*) |
207 |
Goal "i < Nclients ==> System : Increasing (sub i o allocRel)"; |
|
208 |
by (rtac Follows_Increasing1 1); |
|
209 |
by (blast_tac (claset() addIs [Network_Rel RS component_guaranteesD, |
|
210 |
System_Increasing_rel, Network]) 1); |
|
211 |
qed "System_Increasing_allocRel"; |
|
6828 | 212 |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
213 |
|
7482 | 214 |
fun alloc_export th = good_map_sysOfAlloc RS export th; |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
215 |
|
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
216 |
val extend_Alloc_guar_Increasing = |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
217 |
alloc_export extend_guar_Increasing |
7538 | 218 |
|> simplify (simpset()); |
6828 | 219 |
|
7538 | 220 |
(*step 2*) |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
221 |
Goal "System : Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \ |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
222 |
\ <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}"; |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
223 |
by (res_inst_tac |
7537 | 224 |
[("X", "(INT i : lessThan Nclients. Increasing (sub i o allocRel))")] |
225 |
component_guaranteesD 1); |
|
7482 | 226 |
by (rtac Alloc_component_System 3); |
7537 | 227 |
by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 2); |
7538 | 228 |
by (rtac (Alloc_Safety RS project_guarantees) 1); |
7537 | 229 |
by Auto_tac; |
7538 | 230 |
(*1: Increasing precondition*) |
231 |
by (stac (alloc_export project_Increasing) 1); |
|
232 |
by (force_tac |
|
233 |
(claset(), |
|
234 |
simpset() addsimps [o_def, alloc_export project_Increasing]) 1); |
|
235 |
(*2: Always postcondition*) |
|
236 |
by (dtac (subset_refl RS alloc_export project_Always_D) 1); |
|
237 |
by (asm_full_simp_tac |
|
238 |
(simpset() addsimps [alloc_export Collect_eq_extend_set RS sym]) 1); |
|
239 |
qed "System_sum_bounded"; |
|
7537 | 240 |
|
7538 | 241 |
(*step 3*) |
242 |
Goal "System : Always {s. sum (%i. (tokens o giv o sub i o client) s) Nclients \ |
|
243 |
\ <= NbT + sum (%i. (tokens o rel o sub i o client) s) Nclients}"; |
|
244 |
by (rtac (System_sum_bounded RS Always_weaken) 1); |
|
245 |
by Auto_tac; |
|
246 |
br order_trans 1; |
|
247 |
br sum_mono 1; |
|
248 |
bd order_trans 2; |
|
249 |
br add_le_mono 2; |
|
250 |
br order_refl 2; |
|
251 |
br sum_mono 2; |
|
252 |
ba 3; |
|
7482 | 253 |
by Auto_tac; |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
254 |