wenzelm@32960: (* Title: HOL/UNITY/Comp/AllocImpl.thy paulson@11194: Author: Lawrence C Paulson, Cambridge University Computer Laboratory paulson@11194: Copyright 1998 University of Cambridge paulson@11194: *) paulson@11194: wenzelm@58889: section{*Implementation of a multiple-client allocator from a single-client allocator*} paulson@14089: wenzelm@44871: theory AllocImpl imports AllocBase "../Follows" "../PPROD" begin paulson@11194: paulson@11194: paulson@11194: (** State definitions. OUTPUT variables are locals **) paulson@11194: paulson@11194: (*Type variable 'b is the type of items being merged*) paulson@11194: record 'b merge = paulson@14114: In :: "nat => 'b list" (*merge's INPUT histories: streams to merge*) paulson@14114: Out :: "'b list" (*merge's OUTPUT history: merged items*) paulson@14089: iOut :: "nat list" (*merge's OUTPUT history: origins of merged items*) paulson@11194: paulson@11194: record ('a,'b) merge_d = paulson@14089: "'b merge" + paulson@11194: dummy :: 'a (*dummy field for new variables*) paulson@11194: haftmann@35416: definition non_dummy :: "('a,'b) merge_d => 'b merge" where wenzelm@36866: "non_dummy s = (|In = In s, Out = Out s, iOut = iOut s|)" paulson@11194: paulson@11194: record 'b distr = paulson@14089: In :: "'b list" (*items to distribute*) paulson@14089: iIn :: "nat list" (*destinations of items to distribute*) paulson@14089: Out :: "nat => 'b list" (*distributed items*) paulson@11194: paulson@11194: record ('a,'b) distr_d = paulson@14089: "'b distr" + paulson@11194: dummy :: 'a (*dummy field for new variables*) paulson@11194: paulson@11194: record allocState = paulson@14089: giv :: "nat list" (*OUTPUT history: source of tokens*) paulson@14089: ask :: "nat list" (*INPUT: tokens requested from allocator*) paulson@14089: rel :: "nat list" (*INPUT: tokens released to allocator*) paulson@11194: paulson@11194: record 'a allocState_d = paulson@11194: allocState + paulson@11194: dummy :: 'a (*dummy field for new variables*) paulson@11194: paulson@11194: record 'a systemState = paulson@11194: allocState + paulson@14089: mergeRel :: "nat merge" paulson@14089: mergeAsk :: "nat merge" paulson@14089: distr :: "nat distr" paulson@11194: dummy :: 'a (*dummy field for new variables*) paulson@11194: paulson@11194: paulson@11194: (** Merge specification (the number of inputs is Nclients) ***) paulson@11194: wenzelm@36866: definition paulson@11194: (*spec (10)*) paulson@14089: merge_increasing :: "('a,'b) merge_d program set" wenzelm@36866: where "merge_increasing = paulson@11194: UNIV guarantees (Increasing merge.Out) Int (Increasing merge.iOut)" paulson@11194: wenzelm@36866: definition paulson@11194: (*spec (11)*) paulson@14089: merge_eqOut :: "('a,'b) merge_d program set" wenzelm@36866: where "merge_eqOut = paulson@11194: UNIV guarantees paulson@11194: Always {s. length (merge.Out s) = length (merge.iOut s)}" paulson@11194: wenzelm@36866: definition paulson@11194: (*spec (12)*) paulson@14089: merge_bounded :: "('a,'b) merge_d program set" wenzelm@36866: where "merge_bounded = paulson@11194: UNIV guarantees paulson@14089: Always {s. \elt \ set (merge.iOut s). elt < Nclients}" paulson@11194: wenzelm@36866: definition paulson@11194: (*spec (13)*) paulson@14089: merge_follows :: "('a,'b) merge_d program set" wenzelm@36866: where "merge_follows = wenzelm@32960: (\i \ lessThan Nclients. Increasing (sub i o merge.In)) wenzelm@32960: guarantees wenzelm@32960: (\i \ lessThan Nclients. wenzelm@32960: (%s. sublist (merge.Out s) paulson@11194: {k. k < size(merge.iOut s) & merge.iOut s! k = i}) wenzelm@32960: Fols (sub i o merge.In))" paulson@11194: wenzelm@36866: definition paulson@11194: (*spec: preserves part*) paulson@14089: merge_preserves :: "('a,'b) merge_d program set" wenzelm@36866: where "merge_preserves = preserves merge.In Int preserves merge_d.dummy" paulson@11194: wenzelm@36866: definition paulson@11194: (*environmental constraints*) paulson@14089: merge_allowed_acts :: "('a,'b) merge_d program set" wenzelm@36866: where "merge_allowed_acts = paulson@11194: {F. AllowedActs F = wenzelm@32960: insert Id (UNION (preserves (funPair merge.Out merge.iOut)) Acts)}" paulson@11194: wenzelm@36866: definition paulson@14089: merge_spec :: "('a,'b) merge_d program set" wenzelm@36866: where "merge_spec = merge_increasing Int merge_eqOut Int merge_bounded Int paulson@11194: merge_follows Int merge_allowed_acts Int merge_preserves" paulson@11194: paulson@11194: (** Distributor specification (the number of outputs is Nclients) ***) paulson@11194: wenzelm@36866: definition paulson@11194: (*spec (14)*) paulson@14089: distr_follows :: "('a,'b) distr_d program set" wenzelm@36866: where "distr_follows = wenzelm@32960: Increasing distr.In Int Increasing distr.iIn Int wenzelm@32960: Always {s. \elt \ set (distr.iIn s). elt < Nclients} wenzelm@32960: guarantees wenzelm@32960: (\i \ lessThan Nclients. wenzelm@32960: (sub i o distr.Out) Fols wenzelm@32960: (%s. sublist (distr.In s) paulson@11194: {k. k < size(distr.iIn s) & distr.iIn s ! k = i}))" paulson@11194: wenzelm@36866: definition paulson@14089: distr_allowed_acts :: "('a,'b) distr_d program set" wenzelm@36866: where "distr_allowed_acts = paulson@11194: {D. AllowedActs D = insert Id (UNION (preserves distr.Out) Acts)}" paulson@11194: wenzelm@36866: definition paulson@14089: distr_spec :: "('a,'b) distr_d program set" wenzelm@36866: where "distr_spec = distr_follows Int distr_allowed_acts" paulson@11194: paulson@11194: (** Single-client allocator specification (required) ***) paulson@11194: wenzelm@36866: definition paulson@11194: (*spec (18)*) paulson@14089: alloc_increasing :: "'a allocState_d program set" wenzelm@36866: where "alloc_increasing = UNIV guarantees Increasing giv" paulson@11194: wenzelm@36866: definition paulson@11194: (*spec (19)*) paulson@14089: alloc_safety :: "'a allocState_d program set" wenzelm@36866: where "alloc_safety = wenzelm@32960: Increasing rel paulson@14114: guarantees Always {s. tokens (giv s) \ NbT + tokens (rel s)}" paulson@11194: wenzelm@36866: definition paulson@11194: (*spec (20)*) paulson@14089: alloc_progress :: "'a allocState_d program set" wenzelm@36866: where "alloc_progress = wenzelm@32960: Increasing ask Int Increasing rel Int paulson@14114: Always {s. \elt \ set (ask s). elt \ NbT} paulson@11194: Int paulson@14114: (\h. {s. h \ giv s & h pfixGe (ask s)} wenzelm@32960: LeadsTo wenzelm@32960: {s. tokens h \ tokens (rel s)}) paulson@14114: guarantees (\h. {s. h \ ask s} LeadsTo {s. h pfixLe giv s})" paulson@11194: wenzelm@36866: definition paulson@11194: (*spec: preserves part*) paulson@14089: alloc_preserves :: "'a allocState_d program set" wenzelm@36866: where "alloc_preserves = preserves rel Int paulson@11194: preserves ask Int paulson@11194: preserves allocState_d.dummy" paulson@14114: paulson@11194: wenzelm@36866: definition paulson@11194: (*environmental constraints*) paulson@14089: alloc_allowed_acts :: "'a allocState_d program set" wenzelm@36866: where "alloc_allowed_acts = paulson@11194: {F. AllowedActs F = insert Id (UNION (preserves giv) Acts)}" paulson@11194: wenzelm@36866: definition paulson@14089: alloc_spec :: "'a allocState_d program set" wenzelm@36866: where "alloc_spec = alloc_increasing Int alloc_safety Int alloc_progress Int paulson@11194: alloc_allowed_acts Int alloc_preserves" paulson@11194: paulson@11194: locale Merge = paulson@14089: fixes M :: "('a,'b::order) merge_d program" paulson@11194: assumes paulson@14089: Merge_spec: "M \ merge_spec" paulson@11194: paulson@11194: locale Distrib = paulson@14089: fixes D :: "('a,'b::order) distr_d program" paulson@11194: assumes paulson@14089: Distrib_spec: "D \ distr_spec" paulson@11194: paulson@11194: paulson@11194: (**** paulson@14089: # {** Network specification ***} paulson@11194: paulson@14089: # {*spec (9.1)*} paulson@14089: # network_ask :: "'a systemState program set wenzelm@32960: # "network_ask == \i \ lessThan Nclients. wenzelm@32960: # Increasing (ask o sub i o client) wenzelm@32960: # guarantees[ask] wenzelm@32960: # (ask Fols (ask o sub i o client))" paulson@11194: paulson@14089: # {*spec (9.2)*} paulson@14089: # network_giv :: "'a systemState program set wenzelm@32960: # "network_giv == \i \ lessThan Nclients. wenzelm@32960: # Increasing giv wenzelm@32960: # guarantees[giv o sub i o client] wenzelm@32960: # ((giv o sub i o client) Fols giv)" paulson@11194: paulson@14089: # {*spec (9.3)*} paulson@14089: # network_rel :: "'a systemState program set wenzelm@32960: # "network_rel == \i \ lessThan Nclients. wenzelm@32960: # Increasing (rel o sub i o client) wenzelm@32960: # guarantees[rel] wenzelm@32960: # (rel Fols (rel o sub i o client))" paulson@11194: paulson@14089: # {*spec: preserves part*} wenzelm@32960: # network_preserves :: "'a systemState program set wenzelm@32960: # "network_preserves == preserves giv Int wenzelm@32960: # (\i \ lessThan Nclients. wenzelm@32960: # preserves (funPair rel ask o sub i o client))" paulson@11194: paulson@14089: # network_spec :: "'a systemState program set wenzelm@32960: # "network_spec == network_ask Int network_giv Int wenzelm@32960: # network_rel Int network_preserves" paulson@11194: paulson@11194: paulson@14089: # {** State mappings **} paulson@11194: # sysOfAlloc :: "((nat => merge) * 'a) allocState_d => 'a systemState" wenzelm@32960: # "sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s wenzelm@32960: # in (| giv = giv s, wenzelm@32960: # ask = ask s, wenzelm@32960: # rel = rel s, wenzelm@32960: # client = cl, wenzelm@32960: # dummy = xtr|)" paulson@11194: paulson@11194: paulson@11194: # sysOfClient :: "(nat => merge) * 'a allocState_d => 'a systemState" wenzelm@32960: # "sysOfClient == %(cl,al). (| giv = giv al, wenzelm@32960: # ask = ask al, wenzelm@32960: # rel = rel al, wenzelm@32960: # client = cl, wenzelm@32960: # systemState.dummy = allocState_d.dummy al|)" paulson@11194: ****) paulson@11194: paulson@14089: paulson@14089: declare subset_preserves_o [THEN subsetD, intro] paulson@14089: declare funPair_o_distrib [simp] paulson@14089: declare Always_INT_distrib [simp] paulson@14089: declare o_apply [simp del] paulson@14089: paulson@14089: paulson@14089: subsection{*Theorems for Merge*} paulson@14089: wenzelm@46912: context Merge wenzelm@46912: begin wenzelm@46912: wenzelm@46912: lemma Merge_Allowed: paulson@14089: "Allowed M = (preserves merge.Out) Int (preserves merge.iOut)" paulson@14089: apply (cut_tac Merge_spec) paulson@14114: apply (auto simp add: merge_spec_def merge_allowed_acts_def Allowed_def paulson@14114: safety_prop_Acts_iff) paulson@14089: done paulson@14089: wenzelm@46912: lemma M_ok_iff [iff]: paulson@14114: "M ok G = (G \ preserves merge.Out & G \ preserves merge.iOut & paulson@14089: M \ Allowed G)" paulson@14089: by (auto simp add: Merge_Allowed ok_iff_Allowed) paulson@14089: paulson@14089: wenzelm@46912: lemma Merge_Always_Out_eq_iOut: paulson@14114: "[| G \ preserves merge.Out; G \ preserves merge.iOut; M \ Allowed G |] paulson@14089: ==> M Join G \ Always {s. length (merge.Out s) = length (merge.iOut s)}" paulson@14089: apply (cut_tac Merge_spec) paulson@14089: apply (force dest: guaranteesD simp add: merge_spec_def merge_eqOut_def) paulson@14089: done paulson@14089: wenzelm@46912: lemma Merge_Bounded: paulson@14114: "[| G \ preserves merge.iOut; G \ preserves merge.Out; M \ Allowed G |] paulson@14089: ==> M Join G \ Always {s. \elt \ set (merge.iOut s). elt < Nclients}" paulson@14089: apply (cut_tac Merge_spec) paulson@14089: apply (force dest: guaranteesD simp add: merge_spec_def merge_bounded_def) paulson@14089: done paulson@14089: wenzelm@46912: lemma Merge_Bag_Follows_lemma: paulson@14114: "[| G \ preserves merge.iOut; G \ preserves merge.Out; M \ Allowed G |] paulson@14114: ==> M Join G \ Always paulson@14114: {s. (\i \ lessThan Nclients. bag_of (sublist (merge.Out s) paulson@14114: {k. k < length (iOut s) & iOut s ! k = i})) = paulson@14089: (bag_of o merge.Out) s}" paulson@14114: apply (rule Always_Compl_Un_eq [THEN iffD1]) paulson@14114: apply (blast intro: Always_Int_I [OF Merge_Always_Out_eq_iOut Merge_Bounded]) paulson@14114: apply (rule UNIV_AlwaysI, clarify) paulson@14089: apply (subst bag_of_sublist_UN_disjoint [symmetric]) paulson@14089: apply (simp) paulson@14089: apply blast paulson@14089: apply (simp add: set_conv_nth) paulson@14089: apply (subgoal_tac paulson@14089: "(\i \ lessThan Nclients. {k. k < length (iOut x) & iOut x ! k = i}) = paulson@14089: lessThan (length (iOut x))") paulson@14089: apply (simp (no_asm_simp) add: o_def) paulson@14089: apply blast paulson@14089: done paulson@14089: wenzelm@46912: lemma Merge_Bag_Follows: paulson@14114: "M \ (\i \ lessThan Nclients. Increasing (sub i o merge.In)) paulson@14114: guarantees paulson@14114: (bag_of o merge.Out) Fols paulson@14114: (%s. \i \ lessThan Nclients. (bag_of o sub i o merge.In) s)" paulson@14089: apply (rule Merge_Bag_Follows_lemma [THEN Always_Follows1, THEN guaranteesI], auto) paulson@14089: apply (rule Follows_setsum) paulson@14089: apply (cut_tac Merge_spec) paulson@14089: apply (auto simp add: merge_spec_def merge_follows_def o_def) paulson@14114: apply (drule guaranteesD) paulson@14089: prefer 3 paulson@14089: apply (best intro: mono_bag_of [THEN mono_Follows_apply, THEN subsetD], auto) paulson@14089: done paulson@14089: wenzelm@46912: end wenzelm@46912: paulson@14089: paulson@14089: subsection{*Theorems for Distributor*} paulson@14089: wenzelm@46912: context Distrib wenzelm@46912: begin wenzelm@46912: wenzelm@46912: lemma Distr_Increasing_Out: paulson@14114: "D \ Increasing distr.In Int Increasing distr.iIn Int paulson@14114: Always {s. \elt \ set (distr.iIn s). elt < Nclients} paulson@14114: guarantees paulson@14089: (\i \ lessThan Nclients. Increasing (sub i o distr.Out))" paulson@14089: apply (cut_tac Distrib_spec) paulson@14089: apply (simp add: distr_spec_def distr_follows_def) paulson@14089: apply clarify paulson@14089: apply (blast intro: guaranteesI Follows_Increasing1 dest: guaranteesD) paulson@14089: done paulson@14089: wenzelm@46912: lemma Distr_Bag_Follows_lemma: paulson@14114: "[| G \ preserves distr.Out; paulson@14114: D Join G \ Always {s. \elt \ set (distr.iIn s). elt < Nclients} |] paulson@14114: ==> D Join G \ Always paulson@14114: {s. (\i \ lessThan Nclients. bag_of (sublist (distr.In s) paulson@14114: {k. k < length (iIn s) & iIn s ! k = i})) = paulson@14089: bag_of (sublist (distr.In s) (lessThan (length (iIn s))))}" paulson@14089: apply (erule Always_Compl_Un_eq [THEN iffD1]) paulson@14089: apply (rule UNIV_AlwaysI, clarify) paulson@14089: apply (subst bag_of_sublist_UN_disjoint [symmetric]) paulson@14089: apply (simp (no_asm)) paulson@14089: apply blast paulson@14089: apply (simp add: set_conv_nth) paulson@14089: apply (subgoal_tac paulson@14114: "(\i \ lessThan Nclients. {k. k < length (iIn x) & iIn x ! k = i}) = paulson@14089: lessThan (length (iIn x))") paulson@14089: apply (simp (no_asm_simp)) paulson@14089: apply blast paulson@14089: done paulson@14089: wenzelm@46912: lemma D_ok_iff [iff]: paulson@14089: "D ok G = (G \ preserves distr.Out & D \ Allowed G)" paulson@14089: apply (cut_tac Distrib_spec) paulson@14114: apply (auto simp add: distr_spec_def distr_allowed_acts_def Allowed_def paulson@14089: safety_prop_Acts_iff ok_iff_Allowed) paulson@14089: done paulson@14089: wenzelm@46912: lemma Distr_Bag_Follows: paulson@14114: "D \ Increasing distr.In Int Increasing distr.iIn Int paulson@14114: Always {s. \elt \ set (distr.iIn s). elt < Nclients} paulson@14114: guarantees paulson@14114: (\i \ lessThan Nclients. paulson@14114: (%s. \i \ lessThan Nclients. (bag_of o sub i o distr.Out) s) paulson@14114: Fols paulson@14089: (%s. bag_of (sublist (distr.In s) (lessThan (length(distr.iIn s))))))" paulson@14089: apply (rule guaranteesI, clarify) paulson@14089: apply (rule Distr_Bag_Follows_lemma [THEN Always_Follows2], auto) paulson@14089: apply (rule Follows_setsum) paulson@14089: apply (cut_tac Distrib_spec) paulson@14089: apply (auto simp add: distr_spec_def distr_follows_def o_def) paulson@14089: apply (drule guaranteesD) paulson@14089: prefer 3 paulson@14089: apply (best intro: mono_bag_of [THEN mono_Follows_apply, THEN subsetD], auto) paulson@14089: done paulson@14089: wenzelm@46912: end wenzelm@46912: paulson@14089: paulson@14089: subsection{*Theorems for Allocator*} paulson@14089: paulson@14089: lemma alloc_refinement_lemma: paulson@14114: "!!f::nat=>nat. (\i \ lessThan n. {s. f i \ g i s}) nipkow@15074: \ {s. (SUM x: lessThan n. f x) \ (SUM x: lessThan n. g x s)}" paulson@14089: apply (induct_tac "n") paulson@14089: apply (auto simp add: lessThan_Suc) paulson@14089: done paulson@14089: paulson@14114: lemma alloc_refinement: paulson@14114: "(\i \ lessThan Nclients. Increasing (sub i o allocAsk) Int paulson@14114: Increasing (sub i o allocRel)) paulson@14114: Int paulson@14114: Always {s. \i. i paulson@14114: (\elt \ set ((sub i o allocAsk) s). elt \ NbT)} paulson@14114: Int paulson@14114: (\i \ lessThan Nclients. paulson@14114: \h. {s. h \ (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s} paulson@14114: LeadsTo {s. tokens h \ (tokens o sub i o allocRel)s}) paulson@14114: \ paulson@14114: (\i \ lessThan Nclients. Increasing (sub i o allocAsk) Int paulson@14114: Increasing (sub i o allocRel)) paulson@14114: Int paulson@14114: Always {s. \i. i paulson@14114: (\elt \ set ((sub i o allocAsk) s). elt \ NbT)} paulson@14114: Int paulson@14114: (\hf. (\i \ lessThan Nclients. paulson@14114: {s. hf i \ (sub i o allocGiv)s & hf i pfixGe (sub i o allocAsk)s}) paulson@14114: LeadsTo {s. (\i \ lessThan Nclients. tokens (hf i)) \ paulson@14114: (\i \ lessThan Nclients. (tokens o sub i o allocRel)s)})" paulson@14089: apply (auto simp add: ball_conj_distrib) paulson@14089: apply (rename_tac F hf) paulson@14089: apply (rule LeadsTo_weaken_R [OF Finite_stable_completion alloc_refinement_lemma], blast, blast) paulson@14089: apply (subgoal_tac "F \ Increasing (tokens o (sub i o allocRel))") paulson@14089: apply (simp add: Increasing_def o_assoc) paulson@14089: apply (blast intro: mono_tokens [THEN mono_Increasing_o, THEN subsetD]) paulson@14089: done paulson@14089: paulson@11194: end