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 

    78 

   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: *}

   776       thm the_preced_def

   780               thm th_cp_max th_cp_preced th_kept 

   781               the_preced_def vat_t.max_cp_readys_threads

   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 

   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 

  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 

  1462 

  1463 end