1(*  Title:      HOL/UNITY/Comp/AllocImpl.thy
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Copyright   1998  University of Cambridge
4*)
5
6section\<open>Implementation of a multiple-client allocator from a single-client allocator\<close>
7
8theory AllocImpl imports AllocBase "../Follows" "../PPROD" begin
9
10
11(** State definitions.  OUTPUT variables are locals **)
12
13(*Type variable 'b is the type of items being merged*)
14record 'b merge =
15  In   :: "nat => 'b list"  (*merge's INPUT histories: streams to merge*)
16  Out  :: "'b list"         (*merge's OUTPUT history: merged items*)
17  iOut :: "nat list"        (*merge's OUTPUT history: origins of merged items*)
18
19record ('a,'b) merge_d =
20  "'b merge" +
21  dummy :: 'a       (*dummy field for new variables*)
22
23definition non_dummy :: "('a,'b) merge_d => 'b merge" where
24    "non_dummy s = (|In = In s, Out = Out s, iOut = iOut s|)"
25
26record 'b distr =
27  In  :: "'b list"          (*items to distribute*)
28  iIn :: "nat list"         (*destinations of items to distribute*)
29  Out :: "nat => 'b list"   (*distributed items*)
30
31record ('a,'b) distr_d =
32  "'b distr" +
33  dummy :: 'a       (*dummy field for new variables*)
34
35record allocState =
36  giv :: "nat list"   (*OUTPUT history: source of tokens*)
37  ask :: "nat list"   (*INPUT: tokens requested from allocator*)
38  rel :: "nat list"   (*INPUT: tokens released to allocator*)
39
40record 'a allocState_d =
41  allocState +
42  dummy    :: 'a                (*dummy field for new variables*)
43
44record 'a systemState =
45  allocState +
46  mergeRel :: "nat merge"
47  mergeAsk :: "nat merge"
48  distr    :: "nat distr"
49  dummy    :: 'a                  (*dummy field for new variables*)
50
51
52(** Merge specification (the number of inputs is Nclients) ***)
53
54definition
55  (*spec (10)*)
56  merge_increasing :: "('a,'b) merge_d program set"
57  where "merge_increasing =
58         UNIV guarantees (Increasing merge.Out) Int (Increasing merge.iOut)"
59
60definition
61  (*spec (11)*)
62  merge_eqOut :: "('a,'b) merge_d program set"
63  where "merge_eqOut =
64         UNIV guarantees
65         Always {s. length (merge.Out s) = length (merge.iOut s)}"
66
67definition
68  (*spec (12)*)
69  merge_bounded :: "('a,'b) merge_d program set"
70  where "merge_bounded =
71         UNIV guarantees
72         Always {s. \<forall>elt \<in> set (merge.iOut s). elt < Nclients}"
73
74definition
75  (*spec (13)*)
76  merge_follows :: "('a,'b) merge_d program set"
77  where "merge_follows =
78         (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o merge.In))
79         guarantees
80         (\<Inter>i \<in> lessThan Nclients.
81          (%s. nths (merge.Out s)
82                       {k. k < size(merge.iOut s) & merge.iOut s! k = i})
83          Fols (sub i o merge.In))"
84
85definition
86  (*spec: preserves part*)
87  merge_preserves :: "('a,'b) merge_d program set"
88  where "merge_preserves = preserves merge.In Int preserves merge_d.dummy"
89
90definition
91  (*environmental constraints*)
92  merge_allowed_acts :: "('a,'b) merge_d program set"
93  where "merge_allowed_acts =
94       {F. AllowedActs F =
95            insert Id (UNION (preserves (funPair merge.Out merge.iOut)) Acts)}"
96
97definition
98  merge_spec :: "('a,'b) merge_d program set"
99  where "merge_spec = merge_increasing Int merge_eqOut Int merge_bounded Int
100                   merge_follows Int merge_allowed_acts Int merge_preserves"
101
102(** Distributor specification (the number of outputs is Nclients) ***)
103
104definition
105  (*spec (14)*)
106  distr_follows :: "('a,'b) distr_d program set"
107  where "distr_follows =
108         Increasing distr.In Int Increasing distr.iIn Int
109         Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients}
110         guarantees
111         (\<Inter>i \<in> lessThan Nclients.
112          (sub i o distr.Out) Fols
113          (%s. nths (distr.In s)
114                       {k. k < size(distr.iIn s) & distr.iIn s ! k = i}))"
115
116definition
117  distr_allowed_acts :: "('a,'b) distr_d program set"
118  where "distr_allowed_acts =
119       {D. AllowedActs D = insert Id (UNION (preserves distr.Out) Acts)}"
120
121definition
122  distr_spec :: "('a,'b) distr_d program set"
123  where "distr_spec = distr_follows Int distr_allowed_acts"
124
125(** Single-client allocator specification (required) ***)
126
127definition
128  (*spec (18)*)
129  alloc_increasing :: "'a allocState_d program set"
130  where "alloc_increasing = UNIV  guarantees  Increasing giv"
131
132definition
133  (*spec (19)*)
134  alloc_safety :: "'a allocState_d program set"
135  where "alloc_safety =
136         Increasing rel
137         guarantees  Always {s. tokens (giv s) \<le> NbT + tokens (rel s)}"
138
139definition
140  (*spec (20)*)
141  alloc_progress :: "'a allocState_d program set"
142  where "alloc_progress =
143         Increasing ask Int Increasing rel Int
144         Always {s. \<forall>elt \<in> set (ask s). elt \<le> NbT}
145         Int
146         (\<Inter>h. {s. h \<le> giv s & h pfixGe (ask s)}
147                 LeadsTo
148                 {s. tokens h \<le> tokens (rel s)})
149         guarantees  (\<Inter>h. {s. h \<le> ask s} LeadsTo {s. h pfixLe giv s})"
150
151definition
152  (*spec: preserves part*)
153  alloc_preserves :: "'a allocState_d program set"
154  where "alloc_preserves = preserves rel Int
155                        preserves ask Int
156                        preserves allocState_d.dummy"
157
158
159definition
160  (*environmental constraints*)
161  alloc_allowed_acts :: "'a allocState_d program set"
162  where "alloc_allowed_acts =
163       {F. AllowedActs F = insert Id (UNION (preserves giv) Acts)}"
164
165definition
166  alloc_spec :: "'a allocState_d program set"
167  where "alloc_spec = alloc_increasing Int alloc_safety Int alloc_progress Int
168                   alloc_allowed_acts Int alloc_preserves"
169
170locale Merge =
171  fixes M :: "('a,'b::order) merge_d program"
172  assumes
173    Merge_spec:  "M  \<in> merge_spec"
174
175locale Distrib =
176  fixes D :: "('a,'b::order) distr_d program"
177  assumes
178    Distrib_spec:  "D \<in> distr_spec"
179
180
181(****
182#  {** Network specification ***}
183
184#    {*spec (9.1)*}
185#    network_ask :: "'a systemState program set
186#       "network_ask == \<Inter>i \<in> lessThan Nclients.
187#                           Increasing (ask o sub i o client)
188#                           guarantees[ask]
189#                           (ask  Fols (ask o sub i o client))"
190
191#    {*spec (9.2)*}
192#    network_giv :: "'a systemState program set
193#       "network_giv == \<Inter>i \<in> lessThan Nclients.
194#                           Increasing giv
195#                           guarantees[giv o sub i o client]
196#                           ((giv o sub i o client) Fols giv)"
197
198#    {*spec (9.3)*}
199#    network_rel :: "'a systemState program set
200#       "network_rel == \<Inter>i \<in> lessThan Nclients.
201#                           Increasing (rel o sub i o client)
202#                           guarantees[rel]
203#                           (rel  Fols (rel o sub i o client))"
204
205#    {*spec: preserves part*}
206#       network_preserves :: "'a systemState program set
207#       "network_preserves == preserves giv  Int
208#                             (\<Inter>i \<in> lessThan Nclients.
209#                              preserves (funPair rel ask o sub i o client))"
210
211#    network_spec :: "'a systemState program set
212#       "network_spec == network_ask Int network_giv Int
213#                        network_rel Int network_preserves"
214
215
216#  {** State mappings **}
217#    sysOfAlloc :: "((nat => merge) * 'a) allocState_d => 'a systemState"
218#       "sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s
219#                          in (| giv = giv s,
220#                                ask = ask s,
221#                                rel = rel s,
222#                                client   = cl,
223#                                dummy    = xtr|)"
224
225
226#    sysOfClient :: "(nat => merge) * 'a allocState_d => 'a systemState"
227#       "sysOfClient == %(cl,al). (| giv = giv al,
228#                                    ask = ask al,
229#                                    rel = rel al,
230#                                    client   = cl,
231#                                    systemState.dummy = allocState_d.dummy al|)"
232****)
233
234
235declare subset_preserves_o [THEN subsetD, intro]
236declare funPair_o_distrib [simp]
237declare Always_INT_distrib [simp]
238declare o_apply [simp del]
239
240
241subsection\<open>Theorems for Merge\<close>
242
243context Merge
244begin
245
246lemma Merge_Allowed:
247     "Allowed M = (preserves merge.Out) Int (preserves merge.iOut)"
248apply (cut_tac Merge_spec)
249apply (auto simp add: merge_spec_def merge_allowed_acts_def Allowed_def
250                      safety_prop_Acts_iff)
251done
252
253lemma M_ok_iff [iff]:
254     "M ok G = (G \<in> preserves merge.Out & G \<in> preserves merge.iOut &
255                     M \<in> Allowed G)"
256by (auto simp add: Merge_Allowed ok_iff_Allowed)
257
258
259lemma Merge_Always_Out_eq_iOut:
260     "[| G \<in> preserves merge.Out; G \<in> preserves merge.iOut; M \<in> Allowed G |]
261      ==> M \<squnion> G \<in> Always {s. length (merge.Out s) = length (merge.iOut s)}"
262apply (cut_tac Merge_spec)
263apply (force dest: guaranteesD simp add: merge_spec_def merge_eqOut_def)
264done
265
266lemma Merge_Bounded:
267     "[| G \<in> preserves merge.iOut; G \<in> preserves merge.Out; M \<in> Allowed G |]
268      ==> M \<squnion> G \<in> Always {s. \<forall>elt \<in> set (merge.iOut s). elt < Nclients}"
269apply (cut_tac Merge_spec)
270apply (force dest: guaranteesD simp add: merge_spec_def merge_bounded_def)
271done
272
273lemma Merge_Bag_Follows_lemma:
274     "[| G \<in> preserves merge.iOut; G \<in> preserves merge.Out; M \<in> Allowed G |]
275  ==> M \<squnion> G \<in> Always
276          {s. (\<Sum>i \<in> lessThan Nclients. bag_of (nths (merge.Out s)
277                                  {k. k < length (iOut s) & iOut s ! k = i})) =
278              (bag_of o merge.Out) s}"
279apply (rule Always_Compl_Un_eq [THEN iffD1])
280apply (blast intro: Always_Int_I [OF Merge_Always_Out_eq_iOut Merge_Bounded])
281apply (rule UNIV_AlwaysI, clarify)
282apply (subst bag_of_nths_UN_disjoint [symmetric])
283  apply (simp)
284 apply blast
285apply (simp add: set_conv_nth)
286apply (subgoal_tac
287       "(\<Union>i \<in> lessThan Nclients. {k. k < length (iOut x) & iOut x ! k = i}) =
288       lessThan (length (iOut x))")
289 apply (simp (no_asm_simp) add: o_def)
290apply blast
291done
292
293lemma Merge_Bag_Follows:
294     "M \<in> (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o merge.In))
295          guarantees
296             (bag_of o merge.Out) Fols
297             (%s. \<Sum>i \<in> lessThan Nclients. (bag_of o sub i o merge.In) s)"
298apply (rule Merge_Bag_Follows_lemma [THEN Always_Follows1, THEN guaranteesI], auto)
299apply (rule Follows_sum)
300apply (cut_tac Merge_spec)
301apply (auto simp add: merge_spec_def merge_follows_def o_def)
302apply (drule guaranteesD)
303  prefer 3
304  apply (best intro: mono_bag_of [THEN mono_Follows_apply, THEN subsetD], auto)
305done
306
307end
308
309
310subsection\<open>Theorems for Distributor\<close>
311
312context Distrib
313begin
314
315lemma Distr_Increasing_Out:
316     "D \<in> Increasing distr.In Int Increasing distr.iIn Int
317          Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients}
318          guarantees
319          (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o distr.Out))"
320apply (cut_tac Distrib_spec)
321apply (simp add: distr_spec_def distr_follows_def)
322apply clarify
323apply (blast intro: guaranteesI Follows_Increasing1 dest: guaranteesD)
324done
325
326lemma Distr_Bag_Follows_lemma:
327     "[| G \<in> preserves distr.Out;
328         D \<squnion> G \<in> Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients} |]
329  ==> D \<squnion> G \<in> Always
330          {s. (\<Sum>i \<in> lessThan Nclients. bag_of (nths (distr.In s)
331                                  {k. k < length (iIn s) & iIn s ! k = i})) =
332              bag_of (nths (distr.In s) (lessThan (length (iIn s))))}"
333apply (erule Always_Compl_Un_eq [THEN iffD1])
334apply (rule UNIV_AlwaysI, clarify)
335apply (subst bag_of_nths_UN_disjoint [symmetric])
336  apply (simp (no_asm))
337 apply blast
338apply (simp add: set_conv_nth)
339apply (subgoal_tac
340       "(\<Union>i \<in> lessThan Nclients. {k. k < length (iIn x) & iIn x ! k = i}) =
341        lessThan (length (iIn x))")
342 apply (simp (no_asm_simp))
343apply blast
344done
345
346lemma D_ok_iff [iff]:
347     "D ok G = (G \<in> preserves distr.Out & D \<in> Allowed G)"
348apply (cut_tac Distrib_spec)
349apply (auto simp add: distr_spec_def distr_allowed_acts_def Allowed_def
350                      safety_prop_Acts_iff ok_iff_Allowed)
351done
352
353lemma Distr_Bag_Follows:
354 "D \<in> Increasing distr.In Int Increasing distr.iIn Int
355      Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients}
356      guarantees
357       (\<Inter>i \<in> lessThan Nclients.
358        (%s. \<Sum>i \<in> lessThan Nclients. (bag_of o sub i o distr.Out) s)
359        Fols
360        (%s. bag_of (nths (distr.In s) (lessThan (length(distr.iIn s))))))"
361apply (rule guaranteesI, clarify)
362apply (rule Distr_Bag_Follows_lemma [THEN Always_Follows2], auto)
363apply (rule Follows_sum)
364apply (cut_tac Distrib_spec)
365apply (auto simp add: distr_spec_def distr_follows_def o_def)
366apply (drule guaranteesD)
367  prefer 3
368  apply (best intro: mono_bag_of [THEN mono_Follows_apply, THEN subsetD], auto)
369done
370
371end
372
373
374subsection\<open>Theorems for Allocator\<close>
375
376lemma alloc_refinement_lemma:
377     "!!f::nat=>nat. (\<Inter>i \<in> lessThan n. {s. f i \<le> g i s})
378      \<subseteq> {s. (\<Sum>x \<in> lessThan n. f x) \<le> (\<Sum>x \<in> lessThan n. g x s)}"
379apply (induct_tac "n")
380apply (auto simp add: lessThan_Suc)
381done
382
383lemma alloc_refinement:
384"(\<Inter>i \<in> lessThan Nclients. Increasing (sub i o allocAsk) Int
385                           Increasing (sub i o allocRel))
386  Int
387  Always {s. \<forall>i. i<Nclients -->
388              (\<forall>elt \<in> set ((sub i o allocAsk) s). elt \<le> NbT)}
389  Int
390  (\<Inter>i \<in> lessThan Nclients.
391   \<Inter>h. {s. h \<le> (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}
392        LeadsTo {s. tokens h \<le> (tokens o sub i o allocRel)s})
393  \<subseteq>
394 (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o allocAsk) Int
395                           Increasing (sub i o allocRel))
396  Int
397  Always {s. \<forall>i. i<Nclients -->
398              (\<forall>elt \<in> set ((sub i o allocAsk) s). elt \<le> NbT)}
399  Int
400  (\<Inter>hf. (\<Inter>i \<in> lessThan Nclients.
401         {s. hf i \<le> (sub i o allocGiv)s & hf i pfixGe (sub i o allocAsk)s})
402  LeadsTo {s. (\<Sum>i \<in> lessThan Nclients. tokens (hf i)) \<le>
403              (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocRel)s)})"
404apply (auto simp add: ball_conj_distrib)
405apply (rename_tac F hf)
406apply (rule LeadsTo_weaken_R [OF Finite_stable_completion alloc_refinement_lemma], blast, blast)
407apply (subgoal_tac "F \<in> Increasing (tokens o (sub i o allocRel))")
408 apply (simp add: Increasing_def o_assoc)
409apply (blast intro: mono_tokens [THEN mono_Increasing_o, THEN subsetD])
410done
411
412end
413