src/HOL/UNITY/Comp/AllocImpl.thy
author haftmann
Sun Nov 18 18:07:51 2018 +0000 (8 months ago)
changeset 69313 b021008c5397
parent 65956 639eb3617a86
child 69325 4b6ddc5989fc
permissions -rw-r--r--
removed legacy input syntax
     1 (*  Title:      HOL/UNITY/Comp/AllocImpl.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1998  University of Cambridge
     4 *)
     5 
     6 section\<open>Implementation of a multiple-client allocator from a single-client allocator\<close>
     7 
     8 theory 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*)
    14 record '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 
    19 record ('a,'b) merge_d =
    20   "'b merge" +
    21   dummy :: 'a       (*dummy field for new variables*)
    22 
    23 definition non_dummy :: "('a,'b) merge_d => 'b merge" where
    24     "non_dummy s = (|In = In s, Out = Out s, iOut = iOut s|)"
    25 
    26 record '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 
    31 record ('a,'b) distr_d =
    32   "'b distr" +
    33   dummy :: 'a       (*dummy field for new variables*)
    34 
    35 record 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 
    40 record 'a allocState_d =
    41   allocState +
    42   dummy    :: 'a                (*dummy field for new variables*)
    43 
    44 record '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 
    54 definition
    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 
    60 definition
    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 
    67 definition
    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 
    74 definition
    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 
    85 definition
    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 
    90 definition
    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 
    97 definition
    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 
   104 definition
   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 
   116 definition
   117   distr_allowed_acts :: "('a,'b) distr_d program set"
   118   where "distr_allowed_acts =
   119        {D. AllowedActs D = insert Id (\<Union>(Acts ` (preserves distr.Out)))}"
   120 
   121 definition
   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 
   127 definition
   128   (*spec (18)*)
   129   alloc_increasing :: "'a allocState_d program set"
   130   where "alloc_increasing = UNIV  guarantees  Increasing giv"
   131 
   132 definition
   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 
   139 definition
   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 
   151 definition
   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 
   159 definition
   160   (*environmental constraints*)
   161   alloc_allowed_acts :: "'a allocState_d program set"
   162   where "alloc_allowed_acts =
   163        {F. AllowedActs F = insert Id (\<Union>(Acts ` (preserves giv)))}"
   164 
   165 definition
   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 
   170 locale Merge =
   171   fixes M :: "('a,'b::order) merge_d program"
   172   assumes
   173     Merge_spec:  "M  \<in> merge_spec"
   174 
   175 locale 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 
   235 declare subset_preserves_o [THEN subsetD, intro]
   236 declare funPair_o_distrib [simp]
   237 declare Always_INT_distrib [simp]
   238 declare o_apply [simp del]
   239 
   240 
   241 subsection\<open>Theorems for Merge\<close>
   242 
   243 context Merge
   244 begin
   245 
   246 lemma Merge_Allowed:
   247      "Allowed M = (preserves merge.Out) Int (preserves merge.iOut)"
   248 apply (cut_tac Merge_spec)
   249 apply (auto simp add: merge_spec_def merge_allowed_acts_def Allowed_def
   250                       safety_prop_Acts_iff)
   251 done
   252 
   253 lemma M_ok_iff [iff]:
   254      "M ok G = (G \<in> preserves merge.Out & G \<in> preserves merge.iOut &
   255                      M \<in> Allowed G)"
   256 by (auto simp add: Merge_Allowed ok_iff_Allowed)
   257 
   258 
   259 lemma 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)}"
   262 apply (cut_tac Merge_spec)
   263 apply (force dest: guaranteesD simp add: merge_spec_def merge_eqOut_def)
   264 done
   265 
   266 lemma 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}"
   269 apply (cut_tac Merge_spec)
   270 apply (force dest: guaranteesD simp add: merge_spec_def merge_bounded_def)
   271 done
   272 
   273 lemma 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}"
   279 apply (rule Always_Compl_Un_eq [THEN iffD1])
   280 apply (blast intro: Always_Int_I [OF Merge_Always_Out_eq_iOut Merge_Bounded])
   281 apply (rule UNIV_AlwaysI, clarify)
   282 apply (subst bag_of_nths_UN_disjoint [symmetric])
   283   apply (simp)
   284  apply blast
   285 apply (simp add: set_conv_nth)
   286 apply (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)
   290 apply blast
   291 done
   292 
   293 lemma 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)"
   298 apply (rule Merge_Bag_Follows_lemma [THEN Always_Follows1, THEN guaranteesI], auto)
   299 apply (rule Follows_sum)
   300 apply (cut_tac Merge_spec)
   301 apply (auto simp add: merge_spec_def merge_follows_def o_def)
   302 apply (drule guaranteesD)
   303   prefer 3
   304   apply (best intro: mono_bag_of [THEN mono_Follows_apply, THEN subsetD], auto)
   305 done
   306 
   307 end
   308 
   309 
   310 subsection\<open>Theorems for Distributor\<close>
   311 
   312 context Distrib
   313 begin
   314 
   315 lemma 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))"
   320 apply (cut_tac Distrib_spec)
   321 apply (simp add: distr_spec_def distr_follows_def)
   322 apply clarify
   323 apply (blast intro: guaranteesI Follows_Increasing1 dest: guaranteesD)
   324 done
   325 
   326 lemma 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))))}"
   333 apply (erule Always_Compl_Un_eq [THEN iffD1])
   334 apply (rule UNIV_AlwaysI, clarify)
   335 apply (subst bag_of_nths_UN_disjoint [symmetric])
   336   apply (simp (no_asm))
   337  apply blast
   338 apply (simp add: set_conv_nth)
   339 apply (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))
   343 apply blast
   344 done
   345 
   346 lemma D_ok_iff [iff]:
   347      "D ok G = (G \<in> preserves distr.Out & D \<in> Allowed G)"
   348 apply (cut_tac Distrib_spec)
   349 apply (auto simp add: distr_spec_def distr_allowed_acts_def Allowed_def
   350                       safety_prop_Acts_iff ok_iff_Allowed)
   351 done
   352 
   353 lemma 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))))))"
   361 apply (rule guaranteesI, clarify)
   362 apply (rule Distr_Bag_Follows_lemma [THEN Always_Follows2], auto)
   363 apply (rule Follows_sum)
   364 apply (cut_tac Distrib_spec)
   365 apply (auto simp add: distr_spec_def distr_follows_def o_def)
   366 apply (drule guaranteesD)
   367   prefer 3
   368   apply (best intro: mono_bag_of [THEN mono_Follows_apply, THEN subsetD], auto)
   369 done
   370 
   371 end
   372 
   373 
   374 subsection\<open>Theorems for Allocator\<close>
   375 
   376 lemma 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)}"
   379 apply (induct_tac "n")
   380 apply (auto simp add: lessThan_Suc)
   381 done
   382 
   383 lemma 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)})"
   404 apply (auto simp add: ball_conj_distrib)
   405 apply (rename_tac F hf)
   406 apply (rule LeadsTo_weaken_R [OF Finite_stable_completion alloc_refinement_lemma], blast, blast)
   407 apply (subgoal_tac "F \<in> Increasing (tokens o (sub i o allocRel))")
   408  apply (simp add: Increasing_def o_assoc)
   409 apply (blast intro: mono_tokens [THEN mono_Increasing_o, THEN subsetD])
   410 done
   411 
   412 end