120   assumes vt_t: "vt (t @ s)"

   108   assumes vt_t: "vt (t@s)"

   192                 preced th (t @ s) = preced th s" (is "?Q t") 

   190                  preced th (t@s) = preced th s" (is "?Q t") 

   255   According to @{thm th_kept}, thread @{text "th"} has its liveness status

   253   According to @{thm th_kept}, thread @{text "th"} has its living status

   269 lemma max_kept: 

   267 lemma max_kept: "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s"

   270   shows "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s"

   509   assumes running': "th' \<in> running (t @ s)"

   506   assumes running': "th' \<in> running (t@s)"

   510   shows "cp (t @ s) th' = preced th s"

   507   shows "cp (t@s) th' = preced th s" (is "?L = ?R")

   512   have "th' \<in> readys (t @ s)" using assms

   509   have "?L = Max (cp (t @ s) ` readys (t @ s))" using assms

   513     using running_ready subsetCE by blast

   510       by (unfold running_def, auto)

   514     

   511   also have "\<dots> = ?R"

   515   have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" using assms

   512       by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads) 

   516       unfolding running_def by simp

   517   also have "... =  Max (cp (t @ s) ` threads (t @ s))"

   518       using vat_t.max_cp_readys_threads .

   519   also have "... = cp (t @ s) th"

   520       using th_cp_max .

   521   also have "\<dots> = preced th s"

   522       using th_cp_preced .

   733 lemma th_ancestor_has_max_ready:

   723 text {* 

   734   assumes th'_in: "th' \<in> readys (t@s)" 

   724   Suppose @{term th} is not running, it is first shown that

   735   and dp: "th' \<in> nancestors (tG (t @ s)) th"

   725   there is a path in RAG leading from node @{term th} to another thread @{text "th'"} 

   736   shows "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" (is "?L = ?R")

   726   in the @{term readys}-set (So @{text "th'"} is an ancestor of @{term th}}).

   727 

   728   Now, since @{term readys}-set is non-empty, there must be

   729   one in it which holds the highest @{term cp}-value, which, by definition, 

   730   is the @{term running}-thread. However, we are going to show more: this running thread

   731   is exactly @{term "th'"}.

   732      *}

   733 lemma th_blockedE: (* ddd, the other main lemma to be presented: *)

   734   assumes "th \<notin> running (t@s)"

   735   obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"

   736                     "th' \<in> running (t@s)"

   741       have "?L =  Max (the_preced (t @ s) ` (subtree (tG (t @ s)) th'))"

   760       have "?L =  Max ((the_preced (t @ s) \<circ> the_thread) ` subtree (tRAG (t @ s)) (Th th'))"

   742             by (unfold cp_alt_def2, simp)

   761         by (unfold cp_alt_def1, simp)

   762       also have "... = (the_preced (t @ s) \<circ> the_thread) (Th th)"

   763       proof(rule image_Max_subset)

   764         show "finite (Th ` (threads (t@s)))" by (simp add: vat_t.finite_threads)

   765       next

   766         show "subtree (tRAG (t @ s)) (Th th') \<subseteq> Th ` threads (t @ s)"

   767           by (metis Range.intros dp trancl_range vat_t.rg_RAG_threads vat_t.subtree_tRAG_thread) 

   768       next

   769         show "Th th \<in> subtree (tRAG (t @ s)) (Th th')" using dp

   770                     by (unfold tRAG_subtree_eq, auto simp:subtree_def)

   771       next

   772         show "Max ((the_preced (t @ s) \<circ> the_thread) ` Th ` threads (t @ s)) =

   773                       (the_preced (t @ s) \<circ> the_thread) (Th th)" (is "Max ?L = _")

   774         proof -

   775           have "?L = the_preced (t @ s) `  threads (t @ s)" 

   776                      by (unfold image_comp, rule image_cong, auto)

   777           thus ?thesis using max_preced the_preced_def by auto

   778         qed

   779       qed

   780       thm the_preced_def

   781       also have "... = ?R"

   782         using th_cp_max th_cp_preced th_kept 

   783               the_preced_def vat_t.max_cp_readys_threads by auto

   784               thm th_cp_max th_cp_preced th_kept 

   785               the_preced_def vat_t.max_cp_readys_threads

   786       finally show ?thesis .

   787     qed 

   788     -- {* Now, since @{term th'} holds the highest @{term cp} 

   789           and we have already show it is in @{term readys},

   790           it is @{term running} by definition. *}

   791     with `th' \<in> readys (t@s)` show ?thesis by (simp add: running_def) 

   792   qed

   793   -- {* It is easy to show @{term th'} is an ancestor of @{term th}: *}

   794   moreover have "Th th' \<in> ancestors (RAG (t @ s)) (Th th)" 

   795     using `(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def)

   796   ultimately show ?thesis using that by metis

   797 qed

   798 

   799 lemma (* new proof of th_blockedE *)

   800   assumes "th \<notin> running (t @ s)"

   801   obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"

   802                     "th' \<in> running (t @ s)"

   803 proof -

   804   

   805   -- {* According to @{thm vat_t.th_chain_to_ready}, either @{term "th"} is 

   806         in @{term "readys"} or there is path in the @{term RAG} leading from 

   807         it to a thread that is in @{term "readys"}. However, @{term th} cannot 

   808         be in @{term readys}, because otherwise, since @{term th} holds the 

   809         highest @{term cp}-value, it must be @{term "running"}. This would

   810         violate our assumption. *}

   811   have "th \<notin> readys (t @ s)" 

   812     using assms running_def th_cp_max vat_t.max_cp_readys_threads by auto 

   813   then have "\<exists>th'. th' \<in> readys (t @ s) \<and> (Th th, Th th') \<in> (RAG (t @ s))\<^sup>+" 

   814     using th_kept vat_t.th_chain_to_ready by auto

   815   then obtain th' where th'_in: "th' \<in> readys (t@s)"

   816                     and dp: "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+" by auto

   817   

   818   -- {* We are going to first show that this @{term th'} is running. *}

   819   have "th' \<in> running (t @ s)"

   820   proof -

   821     -- {* For this we need to show that @{term th'} holds the highest @{term cp}-value: *}

   822     have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" (is "?L = ?R")

   823     proof -

   824       -- {* First, by the alternative definition of @{term cp} (I mean @{thm cp_alt_def1}),

   825             the  @{term cp}-value of @{term th'} is the maximum of 

   826             all precedences of all thread nodes in its @{term tRAG}-subtree: *}

   827       have "?L =  Max (the_preced (t @ s) ` (the_thread ` subtree (tRAG (t @ s)) (Th th')))"

   828       proof -

   829         have "(the_preced (t @ s) \<circ> the_thread) ` subtree (tRAG (t @ s)) (Th th') =

   830               the_preced (t @ s) ` the_thread ` subtree (tRAG (t @ s)) (Th th')"

   831                 by fastforce

   832         thus ?thesis by (unfold cp_alt_def1, simp)

   833       qed

   747         show "subtree (tG (t @ s)) th' \<subseteq> threads (t @ s)"

   838         show "the_thread ` subtree (tRAG (t @ s)) (Th th') \<subseteq> threads (t @ s)"

   748           using readys_def th'_in vat_t.subtree_tG_thread by auto 

   839           by (smt imageE mem_Collect_eq readys_def subsetCE subsetI th'_in 

   840                 the_thread.simps vat_t.subtree_tRAG_thread)

   750         show "th \<in> subtree (tG (t @ s)) th'" 

   842         show "th \<in> the_thread ` subtree (tRAG (t @ s)) (Th th')"

   751         using dp unfolding subtree_def nancestors_def2 by simp  

   843         proof -

   844           have "Th th \<in> subtree (tRAG (t @ s)) (Th th')" using dp

   845                     by (unfold tRAG_subtree_eq, auto simp:subtree_def)

   846           thus ?thesis by force

   847         qed

   753         show " Max (the_preced (t @ s) ` threads (t @ s)) = the_preced (t @ s) th"

   849         show "Max (the_preced (t @ s) ` threads (t @ s)) = the_preced (t @ s) th"

   760  qed 

   856     qed 

   761 

   857 

   762 

   858     -- {* Now, since @{term th'} holds the highest @{term cp}-value in readys, 

   763 text {* 

   859           it is @{term running} by definition. *}

   764   Suppose @{term th} is not running, it is first shown that

   860     with `th' \<in> readys (t @ s)` show "th' \<in> running (t @ s)" by (simp add: running_def) 

   765   there is a path in RAG leading from node @{term th} to another thread @{text "th'"} 

   861   qed

   766   in the @{term readys}-set (So @{text "th'"} is an ancestor of @{term th}}).

   862 

   767 

   768   Now, since @{term readys}-set is non-empty, there must be

   769   one in it which holds the highest @{term cp}-value, which, by definition, 

   770   is the @{term running}-thread. However, we are going to show more: this 

   771   running thread is exactly @{term "th'"}. *}

   772 

   773 

   774 lemma th_blockedE: (* ddd, the other main lemma to be presented: *)

   775   obtains th' where "th' \<in> nancestors (tG (t @ s)) th"

   776                     "th' \<in> running (t @ s)"

   777 proof -

   778     -- {* According to @{thm vat_t.th_chain_to_ready}, there is a

   779        ready ancestor of @{term th}. *}

   780   have "\<exists>th' \<in> nancestors (tG (t @ s)) th. th' \<in> readys (t @ s)" 

   781     using th_kept vat_t.th_chain_to_ready_tG by auto

   782   then obtain th' where th'_in: "th' \<in> readys (t @ s)"

   783                     and dp: "th' \<in> nancestors (tG (t @ s)) th"

   784     by blast

   785 

   786   -- {* We are going to first show that this @{term th'} is running. *}

   787 

   788   from th'_in dp

   789   have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" 

   790     by (rule th_ancestor_has_max_ready)

   791   with `th' \<in> readys (t @ s)` 

   792   have "th' \<in> running (t @ s)" by (simp add: running_def) 

   793  

   795   moreover have "th' \<in> nancestors (tG (t @ s)) th"

   864   moreover have "Th th' \<in> ancestors (RAG (t @ s)) (Th th)" 

   796     using dp unfolding nancestors_def2 by simp

   865     using `(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def)

   801   shows "\<exists>th' \<in> nancestors (tG (t @ s)) th. th' \<in> running (t @ s)"

   870   assumes "th \<notin> running (t@s)"

   802 using th_blockedE assms 

   871   shows "\<exists>th'. Th th' \<in> ancestors (RAG (t @ s)) (Th th) \<and> th' \<in> running (t@s)"

   803 by blast

   872 using th_blockedE assms by blast

   804 

   808   on whether thread @{term th} is running: if the answer is yes, the 

   876   on whether thread @{term th} is running: if the answer is Yes, the 

   812 lemma live: "running (t @ s) \<noteq> {}"

   880 lemma live: "running (t@s) \<noteq> {}"

   813 using th_blockedE by auto

   881 proof(cases "th \<in> running (t@s)") 

   882   case True thus ?thesis by auto

   883 next

   884   case False

   885   thus ?thesis using th_blockedE by auto

   886 qed

   816   assumes "th \<notin> running (t @ s)"

   889   assumes "th \<notin> running (t@s)"

   817   obtains th' where "th' \<in> nancestors (tG (t @ s)) th"

   890   obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"

   818                     "th' \<in> running (t @ s)"

   891                     "th' \<in> running (t@s)"

   821                     "cp (t @ s) th' = preced th s"

   894                     "cp (t@s) th' = preced th s"

   823 proof -

   896 by (metis assms running_inversion(2) running_preced_inversion running_threads_inv th_blockedE)

   824   obtain th' where a: "th' \<in> nancestors (tG (t @ s)) th" "th' \<in> running (t @ s)"

   825     using th_blockedE by blast

   826   moreover

   827     from a(2) have b: "th' \<in> threads s" 

   828     using running_threads_inv assms by metis

   829   moreover

   830     from a(2) have "\<not>detached s th'" 

   831     using running_inversion(2) assms by metis

   832   moreover

   833     from a(2) have "cp (t @ s) th' = preced th s" 

   834     using running_preced_inversion by blast 

   835   moreover

   836     from a(2) have "th' \<noteq> th" using assms a(2) by blast 

   837   ultimately show ?thesis using that by metis

   838 qed

   839 

   840 

   841 lemma nblockedE:

   842   assumes "th \<notin> running (t @ s)"

   843   obtains th' where "th' \<in> ancestors (tG (t @ s)) th"

   844                     "th' \<in> running (t @ s)"

   845                     "th' \<in> threads s"

   846                     "\<not>detached s th'"

   847                     "cp (t @ s) th' = preced th s"

   848                     "th' \<noteq> th"

   849 using blockedE unfolding nancestors_def

   850 using assms nancestors3 by auto

   851 

   854   assumes "detached (t @ s) th'"

   899   assumes "detached (t@s) th'"

   856   shows "th' \<notin> running (t @ s)"

   901   shows "th' \<notin> running (t@s)"

   882 

   927   In this section, we identify two more conditions in addition to the ones already 

   883   In this section, we identify two more conditions in addition to the ones

   928   specified in the forgoing locales, based on which the correctness of PIP is 

   884   already specified in the current locale, based on which the correctness

   929   formally proved. 

   885   of PIP is formally proved.

   930 

   886 

   931   Note that Priority Inversion refers to the phenomenon where the thread with highest priority 

   887   Note that Priority Inversion refers to the phenomenon where the thread

   932   is blocked by one with lower priority because the resource it is requesting is 

   888   with highest priority is blocked by one with lower priority because the

   933   currently held by the later. The objective of PIP is to avoid {\em Indefinite Priority Inversion}, 

   889   resource it is requesting is currently held by the later. The objective of

   934   i.e. the number of occurrences of {\em Prioirty Inversion} becomes indefinitely large. 

   890   PIP is to avoid {\em Indefinite Priority Inversion}, i.e. the number of

   935 

   891   occurrences of {\em Priority Inversion} becomes indefinitely large.

   936   For PIP to be correct, a finite upper bound needs to be found for the occurrence number, 

   892 

   937   and the existence. This section makes explicit two more conditions so that the existence 

   893   For PIP to be correct, a finite upper bound needs to be found for the

   938   of such a upper bound can be proved to exist. 

   894   occurrence number, and the existence. This section makes explicit two more

   939 *}

   895   conditions so that the existence of such a upper bound can be proved to

   896   exist. *}

   941 text {* The following lemma shows that a blocker does not die as long as the

   984 text {*

   942 highest thread @{term th} is live.

   985   The following lemma shows that a blocker may never die

   943 

   986   as long as the highest thread @{term th} is living. 

   944   The reason for this is that, before a thread can execute an @{term Exit}

   987 

   945   operation, it must give up all its resource. However, the high priority

   988   The reason for this is that, before a thread can execute an @{term Exit} operation,

   946   inherited by a blocker thread also goes with the resources it once held,

   989   it must give up all its resource. However, the high priority inherited by a blocker 

   947   and the consequence is the lost of right to run, the other precondition

   990   thread also goes with the resources it once held, and the consequence is the lost of 

   948   for it to execute its own @{term Exit} operation. For this reason, a

   991   right to run, the other precondition for it to execute its own  @{term Exit} operation.

   949   blocker may never exit before the exit of the highest thread @{term th}.

   992   For this reason, a blocker may never exit before the exit of the highest thread @{term th}.

  1306 

  1328 context extend_highest_gen

  1329 begin

  1330 

  1331 

  1332 (* (* this lemma does not hold *)

  1333 lemma actions_th_occs': "length (actions_of {th} t) = occs' (\<lambda>t'. th \<in> running (t' @ s)) t"

  1334   sorry 

  1335 *)

  1336 

  1337 

  1338 lemma actions_th_occs'_pre:

  1339   assumes "t = e'#t'"

  1340   shows "length (actions_of {th} t) \<le> occs' (\<lambda> t'. th \<in> running (t'@s)) t"

  1341   using assms

  1342 proof(induct arbitrary: e' t' rule:ind)

  1343   case h: (Cons e t e' t')

  1344   interpret vt: valid_trace "(t@s)" using h(1)

  1345     by (unfold_locales, simp)

  1346   interpret ve:  extend_highest_gen s th prio tm t using h by simp

  1347   interpret ve':  extend_highest_gen s th prio tm "e#t" using h by simp

  1348   show ?case (is "?L \<le> ?R")

  1349   proof(cases t)

  1350     case Nil

  1351     show ?thesis

  1352     proof(cases "actor e = th")

  1353       case True

  1354       from ve'.th_no_create[OF _ this]

  1355       have "\<not> isCreate e" by auto

  1356       from PIP_actorE[OF h(2) True this] Nil

  1357       have "th \<in> running s" by simp

  1358       hence "?R = 1" using Nil h by simp

  1359       moreover have "?L = 1" using True Nil by (simp add:actions_of_def)

  1360       ultimately show ?thesis by simp

  1361     next

  1362       case False

  1363       with Nil

  1364       show ?thesis by (auto simp:actions_of_def)

  1365     qed

  1366   next

  1367     case h1: (Cons e1 t1)

  1368     hence eq_t': "t' = e1#t1" using h by simp

  1369     from h(5)[OF h1]

  1370     have le: "length (actions_of {th} t) \<le> occs' (\<lambda>t'. th \<in> running (t' @ s)) t" 

  1371       (is "?F t \<le> ?G t1") .

  1372     show ?thesis 

  1373     proof(cases "actor e = th")

  1374       case True

  1375       from ve'.th_no_create[OF _ this]

  1376       have "\<not> isCreate e" by auto

  1377       from PIP_actorE[OF h(2) True this]

  1378       have "th \<in> running (t@s)" by simp

  1379       hence "?R = 1 + ?G t1" by (unfold h1 eq_t', simp)

  1380       moreover have "?L = 1 + ?F t" using True by (simp add:actions_of_def)

  1381       ultimately show ?thesis using le by simp

  1382     next

  1383       case False

  1384       with le

  1385       show ?thesis by (unfold h1 eq_t', simp add:actions_of_def)

  1386     qed

  1387   qed

  1388 qed auto

  1389 

  1390 text {*

  1391   The following lemma is a simple corollary of @{thm actions_th_occs_pre}. It is the

  1392   lemma really needed in later proofs.

  1393 *}

  1394 

  1395 

  1396 lemma occs'_replacement1: "occs' (\<lambda> t'. th \<in> running (t'@s)) t = length (filter (\<lambda> s'. th \<in> running s') (up_to s t))"

  1397 proof -

  1398   have h: "((\<lambda>s'. th \<in> running s') \<circ> (\<lambda>t'. t' @ s)) = (\<lambda> t'. th \<in> running (t' @ s))" by (rule ext, simp)

  1399   thus ?thesis

  1400     by (unfold occs'_def up_to_def length_filter_map h, simp)

  1401 qed

  1402 

  1403 lemma occs'_replacement2: "occs' (\<lambda> t'. th \<notin> running (t'@s)) t = length (filter (\<lambda> s'. th \<notin> running s') (up_to s t))"

  1404 proof -

  1405   have h: "((\<lambda>s'. th \<notin> running s') \<circ> (\<lambda>t'. t' @ s)) = (\<lambda> t'. th \<notin> running (t' @ s))" by (rule ext, simp)

  1406   thus ?thesis

  1407     by (unfold occs'_def up_to_def length_filter_map h, simp)

  1408 qed

  1409 

  1410 lemma actions_th_occs':

  1411   shows "length (actions_of {th} t) \<le> occs' (\<lambda> t'. th \<in> running (t'@s)) t"

  1412 proof(cases t)

  1413   case (Cons e' t')

  1414   from actions_th_occs'_pre[OF this]

  1415   have "length (actions_of {th} t) \<le> occs' (\<lambda>t'. th \<in> running (t' @ s)) t" .

  1416   thus ?thesis by simp

  1417 qed (auto simp:actions_of_def)

  1418 

  1419 theorem bound_priority_inversion':

  1420   "occs' (\<lambda> t'. th \<notin> running (t'@s)) t \<le> 

  1421           (length (actions_of blockers t) + length (filter (isCreate) t))"

  1422    (is "?L \<le> ?R")

  1423 proof - 

  1424   let ?Q = "(\<lambda> t'. th \<in> running (t'@s))"

  1425   from occs_len'[of ?Q t] 

  1426   have "?L \<le> (length t) - occs' ?Q t" by simp

  1427   also have "... \<le> ?R"

  1428   proof -

  1429     have "length t - (length (actions_of blockers t) + length (filter (isCreate) t))

  1430               \<le> occs' (\<lambda> t'. th \<in> running (t'@s)) t" (is "?L1 \<le> ?R1")

  1431     proof -

  1432       have "?L1 = length (actions_of {th} t)" using actions_split by arith

  1433       also have "... \<le> ?R1" using actions_th_occs' by simp

  1434       finally show ?thesis .

  1435     qed            

  1436     thus ?thesis by simp

  1437   qed

  1438   finally show ?thesis .

  1439 qed

  1440 

  1441 theorem bound_priority_inversion:

  1442   "occs (\<lambda> t'. th \<notin> running (t'@s)) t \<le> 

  1443           1 + (length (actions_of blockers t) + length (filter (isCreate) t))"

  1444    (is "?L \<le> ?R")

  1445 proof - 

  1446   let ?Q = "(\<lambda> t'. th \<in> running (t'@s))"

  1447   from occs_le[of ?Q t] 

  1448   have "?L \<le> 1 + (length t) - occs ?Q t" by simp

  1449   also have "... \<le> ?R"

  1450   proof -

  1451     have "length t - (length (actions_of blockers t) + length (filter (isCreate) t))

  1452               \<le> occs (\<lambda> t'. th \<in> running (t'@s)) t" (is "?L1 \<le> ?R1")

  1453     proof -

  1454       have "?L1 = length (actions_of {th} t)" using actions_split by arith

  1455       also have "... \<le> ?R1" using actions_th_occs by simp

  1456       finally show ?thesis .

  1457     qed            

  1458     thus ?thesis by simp

  1459   qed

  1460   finally show ?thesis .

  1461 qed

  1462 

  1463 end

  1323     blocker regardless of any particular instance of @{term t} in which it operates.

  1480     blocker regardless of any particular instance of @{term t'} in which it operates.

  1331   assumes finite_span:

  1488   (*

  1489   assumes finite_span: 

  1490           "th' \<in> blockers \<Longrightarrow>

  1491                  (\<exists> span. \<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow>

  1492                                 length (actions_of {th'} t') = span \<longrightarrow> detached (t'@s) th')"

  1493    *)

  1494 

  1495   -- {*

  1496     The above definition and explain is problematic because the number of actions taken

  1497     by @{term th'} may be affected by is environment not modeled by the events of our

  1498     PIP model.

  1499   *}

  1500 

  1501   -- {*

  1502     However, we still need to express the idea that every blocker becomes detached in bounded 

  1503     number of steps. Supposing @{term span} is such a bound, the following @{term finite_span}

  1504     assumption says if @{term th'} is not @{term detached} in state (t'@s), then its number 

  1505     of actions must be less than this bound @{term span}:

  1506   *}

  1507 

  1508   assumes finite_span: 

  1362           "\<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow> length (filter isCreate t') \<le> BC"

  1540           "\<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow> length (filter isCreate t') < BC"

  1370   shows "length (filter isCreate t) \<le> BC"

  1548   shows "length (filter isCreate t) < BC"

  1465   moreover have "?B' \<le> ?B" using create_bc .

  1662   moreover have "?B' \<le> ?B" using create_bc by auto