Correctness.thy
changeset 125 95e7933968f8
parent 122 420e03a2d9cc
child 126 a88af0e4731f
equal deleted inserted replaced
124:71a3300d497b 125:95e7933968f8
    50 -- {* @{term s} is a valid trace, so it will inherit all results derived for
    50 -- {* @{term s} is a valid trace, so it will inherit all results derived for
    51       a valid trace: *}
    51       a valid trace: *}
    52 sublocale highest_gen < vat_s?: valid_trace "s"
    52 sublocale highest_gen < vat_s?: valid_trace "s"
    53   by (unfold_locales, insert vt_s, simp)
    53   by (unfold_locales, insert vt_s, simp)
    54 
    54 
       
    55 fun occs where
       
    56   "occs Q [] = (if Q [] then 1 else 0::nat)" |
       
    57   "occs Q (x#xs) = (if Q (x#xs) then (1 + occs Q xs) else occs Q xs)"
       
    58 
       
    59 lemma occs_le: "occs Q t + occs (\<lambda> e. \<not> Q e) t \<le> (1 + length t)"
       
    60   by  (induct t, auto)
       
    61 
    55 context highest_gen
    62 context highest_gen
    56 begin
    63 begin
    57 
    64 
    58 text {*
    65 text {*
    59   @{term tm} is the time when the precedence of @{term th} is set, so 
    66   @{term tm} is the time when the precedence of @{term th} is set, so 
    66   Since @{term th} holds the highest precedence and @{text "cp"}
    73   Since @{term th} holds the highest precedence and @{text "cp"}
    67   is the highest precedence of all threads in the sub-tree of 
    74   is the highest precedence of all threads in the sub-tree of 
    68   @{text "th"} and @{text th} is among these threads, 
    75   @{text "th"} and @{text th} is among these threads, 
    69   its @{term cp} must equal to its precedence:
    76   its @{term cp} must equal to its precedence:
    70 *}
    77 *}
       
    78 
    71 lemma eq_cp_s_th: "cp s th = preced th s" (is "?L = ?R")
    79 lemma eq_cp_s_th: "cp s th = preced th s" (is "?L = ?R")
    72 proof -
    80 proof -
    73   have "?L \<le> ?R"
    81   have "?L \<le> ?R"
    74   by (unfold highest, rule Max_ge, 
    82   by (unfold highest, rule Max_ge, 
    75         auto simp:threads_s finite_threads)
    83         auto simp:threads_s finite_threads)
   740   have "th' \<in> runing (t@s)"
   748   have "th' \<in> runing (t@s)"
   741   proof -
   749   proof -
   742     -- {* We only need to show that this @{term th'} holds the highest @{term cp}-value: *}
   750     -- {* We only need to show that this @{term th'} holds the highest @{term cp}-value: *}
   743     have "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" (is "?L = ?R")
   751     have "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" (is "?L = ?R")
   744     proof -
   752     proof -
       
   753       -- {* First, by the alternative definition of @{term cp} (I mean @{thm cp_alt_def1}),
       
   754             the  @{term cp}-value of @{term th'} is the maximum of 
       
   755             all precedences of all thread nodes in its @{term tRAG}-subtree: *}
   745       have "?L =  Max ((the_preced (t @ s) \<circ> the_thread) ` subtree (tRAG (t @ s)) (Th th'))"
   756       have "?L =  Max ((the_preced (t @ s) \<circ> the_thread) ` subtree (tRAG (t @ s)) (Th th'))"
   746         by (unfold cp_alt_def1, simp)
   757         by (unfold cp_alt_def1, simp)
   747       also have "... = (the_preced (t @ s) \<circ> the_thread) (Th th)"
   758       also have "... = (the_preced (t @ s) \<circ> the_thread) (Th th)"
   748       proof(rule image_Max_subset)
   759       proof(rule image_Max_subset)
   749         show "finite (Th ` (threads (t@s)))" by (simp add: vat_t.finite_threads)
   760         show "finite (Th ` (threads (t@s)))" by (simp add: vat_t.finite_threads)
   760           have "?L = the_preced (t @ s) `  threads (t @ s)" 
   771           have "?L = the_preced (t @ s) `  threads (t @ s)" 
   761                      by (unfold image_comp, rule image_cong, auto)
   772                      by (unfold image_comp, rule image_cong, auto)
   762           thus ?thesis using max_preced the_preced_def by auto
   773           thus ?thesis using max_preced the_preced_def by auto
   763         qed
   774         qed
   764       qed
   775       qed
       
   776       thm the_preced_def
   765       also have "... = ?R"
   777       also have "... = ?R"
   766         using th_cp_max th_cp_preced th_kept 
   778         using th_cp_max th_cp_preced th_kept 
   767               the_preced_def vat_t.max_cp_readys_threads by auto
   779               the_preced_def vat_t.max_cp_readys_threads by auto
       
   780               thm th_cp_max th_cp_preced th_kept 
       
   781               the_preced_def vat_t.max_cp_readys_threads
   768       finally show ?thesis .
   782       finally show ?thesis .
   769     qed 
   783     qed 
   770     -- {* Now, since @{term th'} holds the highest @{term cp} 
   784     -- {* Now, since @{term th'} holds the highest @{term cp} 
   771           and we have already show it is in @{term readys},
   785           and we have already show it is in @{term readys},
   772           it is @{term runing} by definition. *}
   786           it is @{term runing} by definition. *}
   776   moreover have "Th th' \<in> ancestors (RAG (t @ s)) (Th th)" 
   790   moreover have "Th th' \<in> ancestors (RAG (t @ s)) (Th th)" 
   777     using `(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def)
   791     using `(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def)
   778   ultimately show ?thesis using that by metis
   792   ultimately show ?thesis using that by metis
   779 qed
   793 qed
   780 
   794 
       
   795 lemma (* new proof of th_blockedE *)
       
   796   assumes "th \<notin> runing (t@s)"
       
   797   obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
       
   798                     "th' \<in> runing (t@s)"
       
   799 proof -
       
   800   -- {* According to @{thm vat_t.th_chain_to_ready}, either 
       
   801         @{term "th"} is in @{term "readys"} or there is path leading from it to 
       
   802         one thread in @{term "readys"}. *}
       
   803   have "th \<in> readys (t @ s) \<or> (\<exists>th'. th' \<in> readys (t @ s) \<and> (Th th, Th th') \<in> (RAG (t @ s))\<^sup>+)" 
       
   804     using th_kept vat_t.th_chain_to_ready by auto
       
   805   -- {* However, @{term th} can not be in @{term readys}, because otherwise, since 
       
   806        @{term th} holds the highest @{term cp}-value, it must be @{term "runing"}. *}
       
   807   moreover have "th \<notin> readys (t@s)" 
       
   808     using assms runing_def th_cp_max vat_t.max_cp_readys_threads by auto 
       
   809   -- {* So, there must be a path from @{term th} to another thread @{text "th'"} in 
       
   810         term @{term readys}: *}
       
   811   ultimately obtain th' where th'_in: "th' \<in> readys (t@s)"
       
   812                           and dp: "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+" by auto
       
   813   -- {* We are going to show that this @{term th'} is running. *}
       
   814   have "th' \<in> runing (t@s)"
       
   815   proof -
       
   816     -- {* We only need to show that this @{term th'} holds the highest @{term cp}-value: *}
       
   817     have "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" (is "?L = ?R")
       
   818     proof -
       
   819       -- {* First, by the alternative definition of @{term cp} (I mean @{thm cp_alt_def1}),
       
   820             the  @{term cp}-value of @{term th'} is the maximum of 
       
   821             all precedences of all thread nodes in its @{term tRAG}-subtree: *}
       
   822       have "?L =  Max (the_preced (t @ s) ` (the_thread ` subtree (tRAG (t @ s)) (Th th')))"
       
   823       proof -
       
   824         have "(the_preced (t @ s) \<circ> the_thread) ` subtree (tRAG (t @ s)) (Th th') =
       
   825               the_preced (t @ s) ` the_thread ` subtree (tRAG (t @ s)) (Th th')"
       
   826                 by fastforce
       
   827         thus ?thesis by (unfold cp_alt_def1, simp)
       
   828       qed
       
   829       also have "... = (the_preced (t @ s) th)"
       
   830       proof(rule image_Max_subset)
       
   831         show "finite (threads (t@s))" by (simp add: vat_t.finite_threads)
       
   832       next
       
   833         show "the_thread ` subtree (tRAG (t @ s)) (Th th') \<subseteq> threads (t @ s)"
       
   834           by (smt imageE mem_Collect_eq readys_def subsetCE subsetI th'_in 
       
   835                 the_thread.simps vat_t.subtree_tRAG_thread)
       
   836       next
       
   837         show "th \<in> the_thread ` subtree (tRAG (t @ s)) (Th th')"
       
   838         proof -
       
   839           have "Th th \<in> subtree (tRAG (t @ s)) (Th th')" using dp
       
   840                     by (unfold tRAG_subtree_eq, auto simp:subtree_def)
       
   841           thus ?thesis by force
       
   842         qed
       
   843       next
       
   844         show "Max (the_preced (t @ s) ` threads (t @ s)) = the_preced (t @ s) th"
       
   845           by simp
       
   846       qed
       
   847       also have "... = ?R"
       
   848         using th_cp_max th_cp_preced th_kept 
       
   849               the_preced_def vat_t.max_cp_readys_threads by auto
       
   850               thm th_cp_max th_cp_preced th_kept 
       
   851               the_preced_def vat_t.max_cp_readys_threads
       
   852       finally show ?thesis .
       
   853     qed 
       
   854     -- {* Now, since @{term th'} holds the highest @{term cp} 
       
   855           and we have already show it is in @{term readys},
       
   856           it is @{term runing} by definition. *}
       
   857     with `th' \<in> readys (t@s)` show ?thesis by (simp add: runing_def) 
       
   858   qed
       
   859   -- {* It is easy to show @{term th'} is an ancestor of @{term th}: *}
       
   860   moreover have "Th th' \<in> ancestors (RAG (t @ s)) (Th th)" 
       
   861     using `(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def)
       
   862   ultimately show ?thesis using that by metis
       
   863 qed
       
   864 
   781 text {*
   865 text {*
   782   Now it is easy to see there is always a thread to run by case analysis
   866   Now it is easy to see there is always a thread to run by case analysis
   783   on whether thread @{term th} is running: if the answer is Yes, the 
   867   on whether thread @{term th} is running: if the answer is Yes, the 
   784   the running thread is obviously @{term th} itself; otherwise, the running
   868   the running thread is obviously @{term th} itself; otherwise, the running
   785   thread is the @{text th'} given by lemma @{thm th_blockedE}.
   869   thread is the @{text th'} given by lemma @{thm th_blockedE}.
   790 next
   874 next
   791   case False
   875   case False
   792   thus ?thesis using th_blockedE by auto
   876   thus ?thesis using th_blockedE by auto
   793 qed
   877 qed
   794 
   878 
       
   879 lemma blockedE:
       
   880   assumes "th \<notin> runing (t@s)"
       
   881   obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
       
   882                     "th' \<in> runing (t@s)"
       
   883                     "th' \<in> threads s"
       
   884                     "\<not>detached s th'"
       
   885                     "cp (t@s) th' = preced th s"
       
   886                     "th' \<noteq> th"
       
   887 by (metis assms runing_inversion(2) runing_preced_inversion runing_threads_inv th_blockedE)
       
   888 
       
   889 lemma detached_not_runing:
       
   890   assumes "detached (t@s) th'"
       
   891   and "th' \<noteq> th"
       
   892   shows "th' \<notin> runing (t@s)"
       
   893 proof
       
   894     assume otherwise: "th' \<in> runing (t @ s)"
       
   895     have "cp (t@s) th' = cp (t@s) th"
       
   896     proof -
       
   897       have "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" using otherwise
       
   898           by (simp add:runing_def)
       
   899       moreover have "cp (t@s) th = ..." by (simp add: vat_t.max_cp_readys_threads)
       
   900       ultimately show ?thesis by simp
       
   901     qed
       
   902     moreover have "cp (t@s) th' = preced th' (t@s)" using assms(1)
       
   903       by (simp add: detached_cp_preced)
       
   904     moreover have "cp (t@s) th = preced th (t@s)" by simp
       
   905     ultimately have "preced th' (t@s) = preced th (t@s)" by simp
       
   906     from preced_unique[OF this] 
       
   907     have "th' \<in> threads (t @ s) \<Longrightarrow> th \<in> threads (t @ s) \<Longrightarrow> th' = th" .
       
   908     moreover have "th' \<in> threads (t@s)" 
       
   909       using otherwise by (unfold runing_def readys_def, auto)
       
   910     moreover have "th \<in> threads (t@s)" by (simp add: th_kept) 
       
   911     ultimately have "th' = th" by metis
       
   912     with assms(2) show False by simp
       
   913 qed
       
   914 
       
   915 section {* The correctness theorem of PIP *}
       
   916 
       
   917 text {*
       
   918   In this section, we identify two more conditions in addition to the ones already 
       
   919   specified in the forgoing locales, based on which the correctness of PIP is 
       
   920   formally proved. 
       
   921 
       
   922   Note that Priority Inversion refers to the phenomenon where the thread with highest priority 
       
   923   is blocked by one with lower priority because the resource it is requesting is 
       
   924   currently held by the later. The objective of PIP is to avoid {\em Indefinite Priority Inversion}, 
       
   925   i.e. the number of occurrences of {\em Prioirty Inversion} becomes indefinitely large. 
       
   926 
       
   927   For PIP to be correct, a finite upper bound needs to be found for the occurrence number, 
       
   928   and the existence. This section makes explicit two more conditions so that the existence 
       
   929   of such a upper bound can be proved to exist. 
       
   930 *}
       
   931 
       
   932 text {*
       
   933   The following set @{text "blockers"} characterizes the set of threads which 
       
   934   might block @{term th} in @{term t}:
       
   935 *}
       
   936 
       
   937 definition "blockers = {th'. \<not>detached s th' \<and> th' \<noteq> th}"
       
   938 
       
   939 text {*
       
   940   The following lemma shows that the definition of @{term "blockers"} is correct, 
       
   941   i.e. blockers do block @{term "th"}. It is a very simple corollary of @{thm blockedE}.
       
   942 *}
       
   943 lemma runingE:
       
   944   assumes "th' \<in> runing (t@s)"
       
   945   obtains (is_th) "th' = th"
       
   946         | (is_other) "th' \<in> blockers"
       
   947   using assms blockers_def runing_inversion(2) by auto
       
   948 
       
   949 text {*
       
   950   The following lemma shows that the number of blockers are finite.
       
   951   The reason is simple, because blockers are subset of thread set, which
       
   952   has been shown finite.
       
   953 *}
       
   954 
       
   955 lemma finite_blockers: "finite blockers"
       
   956 proof -
       
   957   have "finite {th'. \<not>detached s th'}"
       
   958   proof -
       
   959     have "finite {th'. Th th' \<in> Field (RAG s)}"
       
   960     proof -
       
   961       have "{th'. Th th' \<in> Field (RAG s)} \<subseteq> threads s"
       
   962       proof
       
   963         fix x
       
   964         assume "x \<in> {th'. Th th' \<in> Field (RAG s)}"
       
   965         thus "x \<in> threads s" using vat_s.RAG_threads by auto
       
   966       qed
       
   967       moreover have "finite ..." by (simp add: vat_s.finite_threads) 
       
   968       ultimately show ?thesis using rev_finite_subset by auto 
       
   969     qed
       
   970     thus ?thesis by (unfold detached_test, auto)
       
   971   qed
       
   972   thus ?thesis unfolding blockers_def by simp
       
   973 qed
       
   974 
       
   975 text {*
       
   976   The following lemma shows that a blocker may never die
       
   977   as long as the highest thread @{term th} is living. 
       
   978 
       
   979   The reason for this is that, before a thread can execute an @{term Exit} operation,
       
   980   it must give up all its resource. However, the high priority inherited by a blocker 
       
   981   thread also goes with the resources it once held, and the consequence is the lost of 
       
   982   right to run, the other precondition for it to execute its own  @{term Exit} operation.
       
   983   For this reason, a blocker may never exit before the exit of the highest thread @{term th}.
       
   984 *}
       
   985 
       
   986 lemma blockers_kept:
       
   987   assumes "th' \<in> blockers"
       
   988   shows "th' \<in> threads (t@s)"
       
   989 proof(induct rule:ind)
       
   990   case Nil
       
   991   from assms[unfolded blockers_def detached_test]
       
   992   have "Th th' \<in> Field (RAG s)" by simp
       
   993   from vat_s.RAG_threads[OF this]
       
   994   show ?case by simp
       
   995 next
       
   996   case h: (Cons e t)
       
   997   interpret et: extend_highest_gen s th prio tm t
       
   998     using h by simp
       
   999   show ?case
       
  1000   proof -
       
  1001     { assume otherwise: "th' \<notin> threads ((e # t) @ s)"
       
  1002       from threads_Exit[OF h(5)] this have eq_e: "e = Exit th'" by auto
       
  1003       from h(2)[unfolded this]
       
  1004       have False
       
  1005       proof(cases)
       
  1006         case h: (thread_exit)
       
  1007         hence "th' \<in> readys (t@s)" by (auto simp:runing_def)
       
  1008         from readys_holdents_detached[OF this h(2)]
       
  1009         have "detached (t @ s) th'" .
       
  1010         from et.detached_not_runing[OF this] assms[unfolded blockers_def]
       
  1011         have "th' \<notin> runing (t @ s)" by auto
       
  1012         with h(1) show ?thesis by simp
       
  1013       qed
       
  1014     } thus ?thesis by auto
       
  1015   qed
       
  1016 qed
       
  1017 
       
  1018 text {*
       
  1019   The following lemma shows that a blocker may never execute its @{term Create}-operation
       
  1020   during the period of @{term t}. The reason is that for a thread to be created 
       
  1021   (or executing its @{term Create} operation), it must be non-existing (or dead). 
       
  1022   However, since lemma @{thm blockers_kept} shows that blockers are always living, 
       
  1023   it can not be created. 
       
  1024 
       
  1025   A thread is created only when there is some external reason, there is need for it to run. 
       
  1026   The precondition for this is that it has already died (or get out of existence).
       
  1027 *}
       
  1028 
       
  1029 lemma blockers_no_create:
       
  1030   assumes "th' \<in> blockers"
       
  1031   and "e \<in> set t"
       
  1032   and "actor e = th'"
       
  1033   shows "\<not> isCreate e"
       
  1034   using assms(2,3)
       
  1035 proof(induct rule:ind)
       
  1036   case h: (Cons e' t)
       
  1037   interpret et: extend_highest_gen s th prio tm t
       
  1038     using h by simp
       
  1039   { assume eq_e: "e = e'"
       
  1040     from et.blockers_kept assms
       
  1041     have "th' \<in> threads (t @ s)" by auto
       
  1042     with h(2,7)
       
  1043     have ?case 
       
  1044       by (unfold eq_e, cases, auto simp:blockers_def)
       
  1045   } with h
       
  1046   show ?case by auto
       
  1047 qed auto
       
  1048 
       
  1049 text {*
       
  1050   The following lemma shows that, same as blockers, 
       
  1051   the highest thread @{term th} also can not execute its @{term Create}-operation.
       
  1052   And the reason is similar: since @{thm th_kept} says that thread @{term th} is kept live
       
  1053   during @{term t}, it can not (or need not) be created another time.
       
  1054 *}
       
  1055 lemma th_no_create:
       
  1056   assumes "e \<in> set t"
       
  1057   and "actor e = th"
       
  1058   shows "\<not> isCreate e"
       
  1059   using assms
       
  1060 proof(induct rule:ind)
       
  1061   case h:(Cons e' t)
       
  1062   interpret et: extend_highest_gen s th prio tm t
       
  1063     using h by simp
       
  1064   { assume eq_e: "e = e'"
       
  1065     from et.th_kept have "th \<in> threads (t @ s)" by simp
       
  1066     with h(2,7)
       
  1067     have ?case by (unfold eq_e, cases, auto)
       
  1068   } with h
       
  1069   show ?case by auto
       
  1070 qed auto
       
  1071 
       
  1072 text {*
       
  1073   The following is a preliminary lemma in order to show that the number of 
       
  1074   actions (or operations) taken by the highest thread @{term th} is 
       
  1075   less or equal to the number of occurrences when @{term th} is in running
       
  1076   state. What is proved in this lemma is essentially a strengthening, which 
       
  1077   says the inequality holds even if the occurrence at the very beginning is
       
  1078   ignored.
       
  1079 
       
  1080   The reason for this lemma is that for every operation to be executed, its actor must
       
  1081   be in running state. Therefore, there is one occurrence of running state
       
  1082   behind every action. 
       
  1083 
       
  1084   However, this property does not hold in general, because, for 
       
  1085   the execution of @{term Create}-operation, the actor does not have to be in running state. 
       
  1086   Actually, the actor must be in dead state, in order to be created. For @{term th}, this 
       
  1087   property holds because, according to lemma @{thm th_no_create}, @{term th} can not execute
       
  1088   any @{term Create}-operation during the period of @{term t}.
       
  1089 *}
       
  1090 lemma actions_th_occs_pre:
       
  1091   assumes "t = e'#t'"
       
  1092   shows "length (actions_of {th} t) \<le> occs (\<lambda> t'. th \<in> runing (t'@s)) t'"
       
  1093   using assms
       
  1094 proof(induct arbitrary: e' t' rule:ind)
       
  1095   case h: (Cons e t e' t')
       
  1096   interpret vt: valid_trace "(t@s)" using h(1)
       
  1097     by (unfold_locales, simp)
       
  1098   interpret ve:  extend_highest_gen s th prio tm t using h by simp
       
  1099   interpret ve':  extend_highest_gen s th prio tm "e#t" using h by simp
       
  1100   show ?case (is "?L \<le> ?R")
       
  1101   proof(cases t)
       
  1102     case Nil
       
  1103     show ?thesis
       
  1104     proof(cases "actor e = th")
       
  1105       case True
       
  1106       from ve'.th_no_create[OF _ this]
       
  1107       have "\<not> isCreate e" by auto
       
  1108       from PIP_actorE[OF h(2) True this] Nil
       
  1109       have "th \<in> runing s" by simp
       
  1110       hence "?R = 1" using Nil h by simp
       
  1111       moreover have "?L = 1" using True Nil by (simp add:actions_of_def)
       
  1112       ultimately show ?thesis by simp
       
  1113     next
       
  1114       case False
       
  1115       with Nil
       
  1116       show ?thesis by (auto simp:actions_of_def)
       
  1117     qed
       
  1118   next
       
  1119     case h1: (Cons e1 t1)
       
  1120     hence eq_t': "t' = e1#t1" using h by simp
       
  1121     from h(5)[OF h1]
       
  1122     have le: "length (actions_of {th} t) \<le> occs (\<lambda>t'. th \<in> runing (t' @ s)) t1" 
       
  1123       (is "?F t \<le> ?G t1") .
       
  1124     show ?thesis 
       
  1125     proof(cases "actor e = th")
       
  1126       case True
       
  1127       from ve'.th_no_create[OF _ this]
       
  1128       have "\<not> isCreate e" by auto
       
  1129       from PIP_actorE[OF h(2) True this]
       
  1130       have "th \<in> runing (t@s)" by simp
       
  1131       hence "?R = 1 + ?G t1" by (unfold h1 eq_t', simp)
       
  1132       moreover have "?L = 1 + ?F t" using True by (simp add:actions_of_def)
       
  1133       ultimately show ?thesis using le by simp
       
  1134     next
       
  1135       case False
       
  1136       with le
       
  1137       show ?thesis by (unfold h1 eq_t', simp add:actions_of_def)
       
  1138     qed
       
  1139   qed
       
  1140 qed auto
       
  1141 
       
  1142 text {*
       
  1143   The following lemma is a simple corollary of @{thm actions_th_occs_pre}. It is the
       
  1144   lemma really needed in later proofs.
       
  1145 *}
       
  1146 lemma actions_th_occs:
       
  1147   shows "length (actions_of {th} t) \<le> occs (\<lambda> t'. th \<in> runing (t'@s)) t"
       
  1148 proof(cases t)
       
  1149   case (Cons e' t')
       
  1150   from actions_th_occs_pre[OF this]
       
  1151   have "length (actions_of {th} t) \<le> occs (\<lambda>t'. th \<in> runing (t' @ s)) t'" .
       
  1152   moreover have "... \<le> occs (\<lambda>t'. th \<in> runing (t' @ s)) t" 
       
  1153     by (unfold Cons, auto)
       
  1154   ultimately show ?thesis by simp
       
  1155 qed (auto simp:actions_of_def)
       
  1156 
       
  1157 text {*
       
  1158   The following lemma splits all the operations in @{term t} into three
       
  1159   disjoint sets, namely the operations of @{term th}, the operations of 
       
  1160   blockers and @{term Create}-operations. These sets are mutually disjoint
       
  1161   because: @{term "{th}"} and @{term blockers} are disjoint by definition, 
       
  1162   and neither @{term th} nor any blocker can execute @{term Create}-operation
       
  1163   (according to lemma @{thm th_no_create} and @{thm blockers_no_create}).
       
  1164 
       
  1165   One important caveat noted by this lemma is that: 
       
  1166   Although according to assumption @{thm create_low}, each thread created in 
       
  1167   @{term t} has precedence lower than @{term th}, therefore, will get no
       
  1168   change to run after creation, therefore, can not acquire any resource 
       
  1169   to become a blocker, the @{term Create}-operations of such 
       
  1170   lower threads may still consume overall execution time of duration @{term t}, therefore,
       
  1171   may compete for execution time with the most urgent thread @{term th}.
       
  1172   For PIP to be correct, the number of such competing operations needs to be 
       
  1173   bounded somehow.
       
  1174 *}
       
  1175 
       
  1176 lemma actions_split:
       
  1177   "length t = length (actions_of {th} t) + 
       
  1178               length (actions_of blockers t) + 
       
  1179               length (filter (isCreate) t)"
       
  1180 proof(induct rule:ind)
       
  1181   case h: (Cons e t)
       
  1182   interpret ve :  extend_highest_gen s th prio tm t using h by simp
       
  1183   interpret ve':  extend_highest_gen s th prio tm "e#t" using h by simp
       
  1184   show ?case (is "?L (e#t) = ?T (e#t) + ?O (e#t) + ?C (e#t)")
       
  1185   proof(cases "actor e \<in> runing (t@s)")
       
  1186     case True
       
  1187     thus ?thesis
       
  1188     proof(rule ve.runingE)
       
  1189       assume 1: "actor e = th"
       
  1190       have "?T (e#t) = 1 + ?T (t)" using 1 by (simp add:actions_of_def)
       
  1191       moreover have "?O (e#t) = ?O t" 
       
  1192       proof -
       
  1193         have "actor e \<notin> blockers" using 1
       
  1194           by (simp add:actions_of_def blockers_def)
       
  1195         thus ?thesis by (simp add:actions_of_def)
       
  1196       qed
       
  1197       moreover have "?C (e#t) = ?C t"
       
  1198       proof -
       
  1199         from ve'.th_no_create[OF _ 1]
       
  1200         have "\<not> isCreate e" by auto
       
  1201         thus ?thesis by (simp add:actions_of_def)
       
  1202       qed
       
  1203       ultimately show ?thesis using h by simp
       
  1204     next
       
  1205       assume 2: "actor e \<in> ve'.blockers"
       
  1206       have "?T (e#t) = ?T (t)"
       
  1207       proof -
       
  1208         from 2 have "actor e \<noteq> th" by (auto simp:blockers_def)
       
  1209         thus ?thesis by (auto simp:actions_of_def)
       
  1210       qed
       
  1211       moreover have "?O (e#t) = 1 + ?O(t)" using 2
       
  1212         by (auto simp:actions_of_def)
       
  1213       moreover have "?C (e#t) = ?C(t)"
       
  1214       proof -
       
  1215         from ve'.blockers_no_create[OF 2, of e]
       
  1216         have "\<not> isCreate e" by auto
       
  1217         thus ?thesis by (simp add:actions_of_def)
       
  1218       qed
       
  1219       ultimately show ?thesis using h by simp
       
  1220     qed
       
  1221   next
       
  1222     case False
       
  1223     from h(2)
       
  1224     have is_create: "isCreate e"
       
  1225       by (cases; insert False, auto)
       
  1226     have "?T (e#t) = ?T t"
       
  1227     proof -
       
  1228       have "actor e \<noteq> th"
       
  1229       proof
       
  1230         assume "actor e = th"
       
  1231         from ve'.th_no_create[OF _ this]
       
  1232         have "\<not> isCreate e" by auto
       
  1233         with is_create show False by simp
       
  1234       qed
       
  1235       thus ?thesis by (auto simp:actions_of_def)
       
  1236     qed
       
  1237     moreover have "?O (e#t) = ?O t"
       
  1238     proof -
       
  1239       have "actor e \<notin> blockers"
       
  1240       proof
       
  1241         assume "actor e \<in> blockers"
       
  1242         from ve'.blockers_no_create[OF this, of e]
       
  1243         have "\<not> isCreate e" by simp
       
  1244         with is_create show False by simp
       
  1245       qed
       
  1246       thus ?thesis by (simp add:actions_of_def)
       
  1247     qed
       
  1248     moreover have "?C (e#t) = 1 + ?C t" using is_create
       
  1249         by (auto simp:actions_of_def)
       
  1250     ultimately show ?thesis using h by simp
       
  1251   qed
       
  1252 qed (auto simp:actions_of_def)
       
  1253 
       
  1254 text {*
       
  1255   By combining several of forging lemmas, this lemma gives a upper bound
       
  1256   of the occurrence number when the most urgent thread @{term th} is blocked.
       
  1257 
       
  1258   It says, the occasions when @{term th} is blocked during period @{term t} 
       
  1259   is no more than the number of @{term Create}-operations and 
       
  1260   the operations taken by blockers plus one. 
       
  1261 
       
  1262   Since the length of @{term t} may extend indefinitely, if @{term t} is full
       
  1263   of the above mentioned blocking operations, @{term th} may have not chance to run. 
       
  1264   And, since @{term t} can extend indefinitely, @{term th} my be blocked indefinitely 
       
  1265   with the growth of @{term t}. Therefore, this lemma alone does not ensure 
       
  1266   the correctness of PIP. 
       
  1267 
       
  1268 *}
       
  1269 
       
  1270 theorem bound_priority_inversion:
       
  1271   "occs (\<lambda> t'. th \<notin> runing (t'@s)) t \<le> 
       
  1272           1 + (length (actions_of blockers t) + length (filter (isCreate) t))"
       
  1273    (is "?L \<le> ?R")
       
  1274 proof - 
       
  1275   let ?Q = "(\<lambda> t'. th \<in> runing (t'@s))"
       
  1276   from occs_le[of ?Q t] 
       
  1277   have "?L \<le> (1 + length t) - occs ?Q t" by simp
       
  1278   also have "... \<le> ?R"
       
  1279   proof -
       
  1280     have "length t - (length (actions_of blockers t) + length (filter (isCreate) t))
       
  1281               \<le> occs (\<lambda> t'. th \<in> runing (t'@s)) t" (is "?L1 \<le> ?R1")
       
  1282     proof -
       
  1283       have "?L1 = length (actions_of {th} t)" using actions_split by arith
       
  1284       also have "... \<le> ?R1" using actions_th_occs by simp
       
  1285       finally show ?thesis .
       
  1286     qed            
       
  1287     thus ?thesis by simp
       
  1288   qed
       
  1289   finally show ?thesis .
       
  1290 qed
       
  1291 
   795 end
  1292 end
       
  1293 
       
  1294 text {*
       
  1295   As explained before, lemma @{text bound_priority_inversion} alone does not
       
  1296   ensure the correctness of PIP. For PIP to be correct, the number of blocking operations 
       
  1297   (by {\em blocking operation}, we mean the @{term Create}-operations and 
       
  1298            operations taken by blockers) has to be bounded somehow.
       
  1299 
       
  1300   And the following lemma is for this purpose.
       
  1301 *}
       
  1302 
       
  1303 locale bounded_extend_highest = extend_highest_gen + 
       
  1304   -- {*
       
  1305     To bound operations of blockers, the locale specifies that each blocker 
       
  1306     releases all resources and becomes detached after a certain number 
       
  1307     of operations. In the assumption, this number is given by the 
       
  1308     existential variable @{text span}. Notice that this number is fixed for each 
       
  1309     blocker regardless of any particular instance of @{term t} in which it operates.
       
  1310     
       
  1311     This assumption is reasonable, because it is a common sense that 
       
  1312     the total number of operations take by any standalone thread (or process) 
       
  1313     is only determined by its own input, and should not be affected by 
       
  1314     the particular environment in which it operates. In this particular case,
       
  1315     we regard the @{term t} as the environment of thread @{term th}.
       
  1316   *}
       
  1317   assumes finite_span: 
       
  1318           "th' \<in> blockers \<Longrightarrow>
       
  1319                  (\<exists> span. \<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow>
       
  1320                                 length (actions_of {th'} t') = span \<longrightarrow> detached (t'@s) th')"
       
  1321   -- {* The following @{text BC} is bound of @{term Create}-operations *}
       
  1322   fixes BC
       
  1323   -- {* 
       
  1324   The following assumption requires the number of @{term Create}-operations is 
       
  1325   less or equal to @{term BC} regardless of any particular extension of @{term t}.
       
  1326 
       
  1327    Although this assumption might seem doubtful at first sight, it is necessary 
       
  1328    to ensure the occasions when @{term th} is blocked to be finite. Just consider
       
  1329    the extreme case when @{term Create}-operations consume all the time in duration 
       
  1330    @{term "t"} and leave no space for neither @{term "th"} nor blockers to operate.
       
  1331    An investigate of the precondition for @{term Create}-operation in the definition 
       
  1332    of @{term PIP} may reveal that such extreme cases are well possible, because it 
       
  1333    is only required the thread to be created be a fresh (or dead one), and there 
       
  1334    are infinitely many such threads. 
       
  1335 
       
  1336    However, if we relax the correctness criterion of PIP, allowing @{term th} to be 
       
  1337    blocked indefinitely while still attaining a certain portion of @{term t} to complete 
       
  1338    its task, then this bound @{term BC} can be lifted to function depending on @{term t}
       
  1339    where @{text "BC t"} is of a certain proportion of @{term "length t"}.
       
  1340   *}
       
  1341   assumes finite_create: 
       
  1342           "\<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow> length (filter isCreate t') \<le> BC"
       
  1343 begin 
       
  1344 
       
  1345 text {*
       
  1346   The following lemmas show that the number of @{term Create}-operations is bound by @{term BC}:
       
  1347 *}
       
  1348 
       
  1349 lemma create_bc: 
       
  1350   shows "length (filter isCreate t) \<le> BC"
       
  1351     by (meson extend_highest_gen_axioms finite_create)
       
  1352 
       
  1353 text {*
       
  1354   The following @{term span}-function gives the upper bound of 
       
  1355   operations take by each particular blocker.
       
  1356 *}
       
  1357 definition "span th' = (SOME span.
       
  1358          \<forall>t'. extend_highest_gen s th prio tm t' \<longrightarrow>
       
  1359               length (actions_of {th'} t') = span \<longrightarrow> detached (t' @ s) th')"
       
  1360 
       
  1361 text {*
       
  1362   The following lemmas shows the correctness of @{term span}, i.e. 
       
  1363   the number of operations of taken by @{term th'} is given by 
       
  1364   @{term "span th"}.
       
  1365 
       
  1366   The reason for this lemma is that since @{term th'} gives up all resources 
       
  1367   after @{term "span th'"} operations and becomes detached,
       
  1368   its inherited high priority is lost, with which the right to run goes as well.
       
  1369 *}
       
  1370 lemma le_span:
       
  1371   assumes "th' \<in> blockers"
       
  1372   shows "length (actions_of {th'} t) \<le> span th'"
       
  1373 proof -
       
  1374   from finite_span[OF assms(1)] obtain span' 
       
  1375   where span': "\<forall>t'. extend_highest_gen s th prio tm t' \<longrightarrow>
       
  1376                      length (actions_of {th'} t') = span' \<longrightarrow> detached (t' @ s) th'" (is "?P span'")
       
  1377                      by auto
       
  1378   have "length (actions_of {th'} t) \<le> (SOME span. ?P span)"
       
  1379   proof(rule someI2[where a = span'])
       
  1380     fix span
       
  1381     assume fs: "?P span" 
       
  1382     show "length (actions_of {th'} t) \<le> span"
       
  1383     proof(induct rule:ind)
       
  1384       case h: (Cons e t)
       
  1385         interpret ve':  extend_highest_gen s th prio tm "e#t" using h by simp
       
  1386       show ?case
       
  1387       proof(cases "length (actions_of {th'} t) < span")
       
  1388         case True
       
  1389         thus ?thesis by (simp add:actions_of_def)
       
  1390       next
       
  1391         case False
       
  1392         have "actor e \<noteq> th'"
       
  1393         proof
       
  1394           assume otherwise: "actor e = th'"
       
  1395           from ve'.blockers_no_create [OF assms _ this]
       
  1396           have "\<not> isCreate e" by auto
       
  1397           from PIP_actorE[OF h(2) otherwise this]
       
  1398           have "th' \<in> runing (t @ s)" .
       
  1399           moreover have "th' \<notin> runing (t @ s)"
       
  1400           proof -
       
  1401             from False h(4) h(5) have "length (actions_of {th'} t) = span" by simp
       
  1402             from fs[rule_format, OF h(3) this] have "detached (t @ s) th'" .
       
  1403             from extend_highest_gen.detached_not_runing[OF h(3) this] assms
       
  1404             show ?thesis by (auto simp:blockers_def)
       
  1405           qed
       
  1406           ultimately show False by simp
       
  1407         qed
       
  1408         with h show ?thesis by (auto simp:actions_of_def)
       
  1409       qed
       
  1410     qed (simp add: actions_of_def)
       
  1411   next
       
  1412     from span'
       
  1413     show "?P span'" .
       
  1414   qed
       
  1415   thus ?thesis by (unfold span_def, auto)
       
  1416 qed
       
  1417 
       
  1418 text {*
       
  1419   The following lemma is a corollary of @{thm le_span}, which says 
       
  1420   the total operations of blockers is bounded by the 
       
  1421   sum of @{term span}-values of all blockers.
       
  1422 *}
       
  1423 lemma len_action_blockers: 
       
  1424   "length (actions_of blockers t) \<le> (\<Sum> th' \<in> blockers . span th')"
       
  1425     (is "?L \<le> ?R")
       
  1426 proof -
       
  1427   from len_actions_of_sigma[OF finite_blockers]
       
  1428   have "?L  = (\<Sum>th'\<in>blockers. length (actions_of {th'} t))" by simp
       
  1429   also have "... \<le> ?R"
       
  1430     by (rule Groups_Big.setsum_mono, insert le_span, auto)
       
  1431   finally show ?thesis .
       
  1432 qed
       
  1433 
       
  1434 text {*
       
  1435   By combining forgoing lemmas, it is proved that the number of 
       
  1436   blocked occurrences of the most urgent thread @{term th} is finitely bounded:
       
  1437 *}
       
  1438 theorem priority_inversion_is_finite:
       
  1439   "occs (\<lambda> t'. th \<notin> runing (t'@s)) t \<le> 
       
  1440           1 + ((\<Sum> th' \<in> blockers . span th') + BC)" (is "?L \<le> ?R" is "_ \<le> 1 + (?A + ?B)" )
       
  1441 proof -
       
  1442   from bound_priority_inversion
       
  1443   have "?L \<le> 1 + (length (actions_of blockers t) + length (filter isCreate t))" 
       
  1444       (is "_ \<le> 1 + (?A' + ?B')") .
       
  1445   moreover have "?A' \<le> ?A" using len_action_blockers .
       
  1446   moreover have "?B' \<le> ?B" using create_bc .
       
  1447   ultimately show ?thesis by simp
       
  1448 qed
       
  1449 
       
  1450 text {*
       
  1451   The following lemma says the most urgent thread @{term th} will get as many 
       
  1452   as operations it wishes, provided @{term t} is long enough. 
       
  1453   Similar result can also be obtained under the slightly weaker assumption where
       
  1454   @{term BC} is lifted to a function and @{text "BC t"} is a portion of 
       
  1455   @{term "length t"}.
       
  1456 *}
       
  1457 theorem enough_actions_for_the_highest:
       
  1458   "length t - ((\<Sum> th' \<in> blockers . span th') + BC) \<le> length (actions_of {th} t)"
       
  1459   using actions_split create_bc len_action_blockers by linarith
       
  1460 
   796 end
  1461 end
       
  1462 
       
  1463 end