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