Mercurial Mercurial > hg > pip / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Correctness.thy
changeset 92 4763aa246dbd
parent 91 0525670d8e6a
child 93 524bd3caa6b6
equal deleted inserted replaced
91:0525670d8e6a 92:4763aa246dbd 
     1 theory Correctness
 
     1 theory PrioG
 
     2 imports PIPBasics
 
     2 imports CpsG
 
     3 begin
 
     3 begin
 
     4 
       
     5 
     4 
     6 text {* 
     5 text {* 
     7   The following two auxiliary lemmas are used to reason about @{term Max}.
 
     6   The following two auxiliary lemmas are used to reason about @{term Max}.
 
     8 *}
 
     7 *}
 
     9 lemma image_Max_eqI: 
     8 lemma image_Max_eqI: 
   472     vat_s.le_cp)
 
   471     vat_s.le_cp)
 
   473 
   472 
   474 section {* The `blocking thread` *}
 
   473 section {* The `blocking thread` *}
 
   475 
   474 
   476 text {* 
   475 text {* 
   477 
   476   The purpose of PIP is to ensure that the most 
   478   The purpose of PIP is to ensure that the most urgent thread @{term
 
   477   urgent thread @{term th} is not blocked unreasonably. 
   479   th} is not blocked unreasonably. Therefore, below, we will derive
 
   478   Therefore, a clear picture of the blocking thread is essential 
   480   properties of the blocking thread. By blocking thread, we mean a
 
   479   to assure people that the purpose is fulfilled. 
   481   thread in running state t @ s, but is different from thread @{term
 
   480   
   482   th}.
 
   481   In this section, we are going to derive a series of lemmas 
   483 
   482   with finally give rise to a picture of the blocking thread. 
   484   The first lemmas shows that the @{term cp}-value of the blocking
 
   483 
   485   thread @{text th'} equals to the highest precedence in the whole
 
   484   By `blocking thread`, we mean a thread in running state but 
   486   system.
 
   485   different from thread @{term th}.
 
   487 
   486 *}
 
   488 *}
 
   487 
   489 
   488 text {*
 
       
   489   The following lemmas shows that the @{term cp}-value 
       
   490   of the blocking thread @{text th'} equals to the highest
 
       
   491   precedence in the whole system.
 
       
   492 *}
 
   490 lemma runing_preced_inversion:
 
   493 lemma runing_preced_inversion:
 
   491   assumes runing': "th' \<in> runing (t @ s)"
 
   494   assumes runing': "th' \<in> runing (t@s)"
 
   492   shows "cp (t @ s) th' = preced th s" 
   495   shows "cp (t@s) th' = preced th s" (is "?L = ?R")
 
   493 proof -
 
   496 proof -
 
   494   have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" 
   497   have "?L = Max (cp (t @ s) ` readys (t @ s))" using assms
 
   495     using assms by (unfold runing_def, auto)
 
   498       by (unfold runing_def, auto)
 
   496   also have "\<dots> = preced th s"
 
   499   also have "\<dots> = ?R"
 
   497     by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads) 
   500       by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads) 
   498   finally show ?thesis .
 
   501   finally show ?thesis .
 
   499 qed
 
   502 qed
 
   500 
   503 
   501 text {*
 
   504 text {*
 
   502 
   505 
   503   The next lemma shows how the counters for @{term "P"} and @{term
 
   506   The following lemma shows how the counters for @{term "P"} and
 
   504   "V"} operations relate to the running threads in the states @{term
 
   507   @{term "V"} operations relate to the running threads in the states
 
   505   s} and @{term "t @ s"}: if a thread's @{term "P"}-count equals its
 
   508   @{term s} and @{term "t @ s"}.  The lemma shows that if a thread's
 
   506   @{term "V"}-count (which means it no longer has any resource in its
 
   509   @{term "P"}-count equals its @{term "V"}-count (which means it no
 
   507   possession), it cannot be a running thread.
 
   510   longer has any resource in its possession), it cannot be a running
 
       
   511   thread.
 
   508 
   512 
   509   The proof is by contraction with the assumption @{text "th' \<noteq> th"}.
 
   513   The proof is by contraction with the assumption @{text "th' \<noteq> th"}.
 
   510   The key is the use of @{thm count_eq_dependants} to derive the
 
   514   The key is the use of @{thm eq_pv_dependants} to derive the
 
   511   emptiness of @{text th'}s @{term dependants}-set from the balance of
 
   515   emptiness of @{text th'}s @{term dependants}-set from the balance of
 
   512   its @{term P} and @{term V} counts.  From this, it can be shown
 
   516   its @{term P} and @{term V} counts.  From this, it can be shown
 
   513   @{text th'}s @{term cp}-value equals to its own precedence.
 
   517   @{text th'}s @{term cp}-value equals to its own precedence.
 
   514 
   518 
   515   On the other hand, since @{text th'} is running, by @{thm
 
   519   On the other hand, since @{text th'} is running, by @{thm
 
   516   runing_preced_inversion}, its @{term cp}-value equals to the
 
   520   runing_preced_inversion}, its @{term cp}-value equals to the
 
   517   precedence of @{term th}.
 
   521   precedence of @{term th}.
 
   518 
   522 
   519   Combining the above two results we have that @{text th'} and @{term
 
   523   Combining the above two resukts we have that @{text th'} and @{term
 
   520   th} have the same precedence. By uniqueness of precedences, we have
 
   524   th} have the same precedence. By uniqueness of precedences, we have
 
   521   @{text "th' = th"}, which is in contradiction with the assumption
 
   525   @{text "th' = th"}, which is in contradiction with the assumption
 
   522   @{text "th' \<noteq> th"}.
 
   526   @{text "th' \<noteq> th"}.
 
   523 
   527 
   524 *} 
   528 *} 
   525                       
   529                       
   526 lemma eq_pv_blocked: (* ddd *)
 
   530 lemma eq_pv_blocked: (* ddd *)
 
   527   assumes neq_th': "th' \<noteq> th"
 
   531   assumes neq_th': "th' \<noteq> th"
 
   528   and eq_pv: "cntP (t @ s) th' = cntV (t @ s) th'"
 
   532   and eq_pv: "cntP (t@s) th' = cntV (t@s) th'"
 
   529   shows "th' \<notin> runing (t @ s)"
 
   533   shows "th' \<notin> runing (t@s)"
 
   530 proof
 
   534 proof
 
   531   assume otherwise: "th' \<in> runing (t @ s)"
 
   535   assume otherwise: "th' \<in> runing (t@s)"
 
   532   show False
 
   536   show False
 
   533   proof -
 
   537   proof -
 
   534     have th'_in: "th' \<in> threads (t @ s)"
 
   538     have th'_in: "th' \<in> threads (t@s)"
 
   535         using otherwise readys_threads runing_def by auto 
   539         using otherwise readys_threads runing_def by auto 
   536     have "th' = th"
 
   540     have "th' = th"
 
   537     proof(rule preced_unique)
 
   541     proof(rule preced_unique)
 
   538       -- {* The proof goes like this: 
   542       -- {* The proof goes like this: 
   539             it is first shown that the @{term preced}-value of @{term th'} 
   543             it is first shown that the @{term preced}-value of @{term th'} 
   543       show "preced th' (t @ s) = preced th (t @ s)" (is "?L = ?R")
 
   547       show "preced th' (t @ s) = preced th (t @ s)" (is "?L = ?R")
 
   544       proof -
 
   548       proof -
 
   545         -- {* Since the counts of @{term th'} are balanced, the subtree
 
   549         -- {* Since the counts of @{term th'} are balanced, the subtree
 
   546               of it contains only itself, so, its @{term cp}-value
 
   550               of it contains only itself, so, its @{term cp}-value
 
   547               equals its @{term preced}-value: *}
 
   551               equals its @{term preced}-value: *}
 
   548         have "?L = cp (t @ s) th'"
 
   552         have "?L = cp (t@s) th'"
 
   549           by (unfold cp_eq_cpreced cpreced_def count_eq_dependants[OF eq_pv], simp)
 
   553          by (unfold cp_eq_cpreced cpreced_def eq_dependants vat_t.eq_pv_dependants[OF eq_pv], simp)
 
   550         -- {* Since @{term "th'"} is running, by @{thm runing_preced_inversion},
 
   554         -- {* Since @{term "th'"} is running, by @{thm runing_preced_inversion},
 
   551               its @{term cp}-value equals @{term "preced th s"}, 
   555               its @{term cp}-value equals @{term "preced th s"}, 
   552               which equals to @{term "?R"} by simplification: *}
 
   556               which equals to @{term "?R"} by simplification: *}
 
   553         also have "... = ?R" 
   557         also have "... = ?R" 
       
   558         thm runing_preced_inversion
 
   554             using runing_preced_inversion[OF otherwise] by simp
 
   559             using runing_preced_inversion[OF otherwise] by simp
 
   555         finally show ?thesis .
 
   560         finally show ?thesis .
 
   556       qed
 
   561       qed
 
   557     qed (auto simp: th'_in th_kept)
 
   562     qed (auto simp: th'_in th_kept)
 
   558     with `th' \<noteq> th` show ?thesis by simp
 
   563     with `th' \<noteq> th` show ?thesis by simp
 
   566   it will keep hand-emptied in the future @{term "t@s"}.
 
   571   it will keep hand-emptied in the future @{term "t@s"}.
 
   567 *}
 
   572 *}
 
   568 lemma eq_pv_persist: (* ddd *)
 
   573 lemma eq_pv_persist: (* ddd *)
 
   569   assumes neq_th': "th' \<noteq> th"
 
   574   assumes neq_th': "th' \<noteq> th"
 
   570   and eq_pv: "cntP s th' = cntV s th'"
 
   575   and eq_pv: "cntP s th' = cntV s th'"
 
   571   shows "cntP (t @ s) th' = cntV (t @ s) th'"
 
   576   shows "cntP (t@s) th' = cntV (t@s) th'"
 
   572 proof(induction rule: ind) 
   577 proof(induction rule:ind) -- {* The proof goes by induction. *}
 
   573   -- {* The nontrivial case is for the @{term Cons}: *}
 
   578   -- {* The nontrivial case is for the @{term Cons}: *}
 
   574   case (Cons e t)
 
   579   case (Cons e t)
 
   575   -- {* All results derived so far hold for both @{term s} and @{term "t@s"}: *}
 
   580   -- {* All results derived so far hold for both @{term s} and @{term "t@s"}: *}
 
   576   interpret vat_t: extend_highest_gen s th prio tm t using Cons by simp
 
   581   interpret vat_t: extend_highest_gen s th prio tm t using Cons by simp
 
   577   interpret vat_e: extend_highest_gen s th prio tm "(e # t)" using Cons by simp
 
   582   interpret vat_e: extend_highest_gen s th prio tm "(e # t)" using Cons by simp
 
   616     ultimately show ?thesis using Cons(5) by metis
 
   621     ultimately show ?thesis using Cons(5) by metis
 
   617   qed
 
   622   qed
 
   618 qed (auto simp:eq_pv)
 
   623 qed (auto simp:eq_pv)
 
   619 
   624 
   620 text {*
 
   625 text {*
 
   621 
   626   By combining @{thm  eq_pv_blocked} and @{thm eq_pv_persist},
 
   622   By combining @{thm eq_pv_blocked} and @{thm eq_pv_persist}, it can
 
   627   it can be derived easily that @{term th'} can not be running in the future:
 
   623   be derived easily that @{term th'} can not be running in the future:
 
   628 *}
 
   624 
       
   625 *}
 
       
   626 
       
   627 lemma eq_pv_blocked_persist:
 
   629 lemma eq_pv_blocked_persist:
 
   628   assumes neq_th': "th' \<noteq> th"
 
   630   assumes neq_th': "th' \<noteq> th"
 
   629   and eq_pv: "cntP s th' = cntV s th'"
 
   631   and eq_pv: "cntP s th' = cntV s th'"
 
   630   shows "th' \<notin> runing (t @ s)"
 
   632   shows "th' \<notin> runing (t@s)"
 
   631   using assms
 
   633   using assms
 
   632   by (simp add: eq_pv_blocked eq_pv_persist) 
   634   by (simp add: eq_pv_blocked eq_pv_persist) 
   633 
   635 
   634 text {*
 
   636 text {*
 
   635 
   637   The following lemma shows the blocking thread @{term th'}
 
   636   The following lemma shows the blocking thread @{term th'} must hold
 
   638   must hold some resource in the very beginning. 
   637   some resource in the very beginning.
 
   639 *}
 
   638 
       
   639 *}
 
       
   640 
       
   641 lemma runing_cntP_cntV_inv: (* ddd *)
 
   640 lemma runing_cntP_cntV_inv: (* ddd *)
 
   642   assumes is_runing: "th' \<in> runing (t @ s)"
 
   641   assumes is_runing: "th' \<in> runing (t@s)"
 
   643   and neq_th': "th' \<noteq> th"
 
   642   and neq_th': "th' \<noteq> th"
 
   644   shows "cntP s th' > cntV s th'"
 
   643   shows "cntP s th' > cntV s th'"
 
   645   using assms
 
   644   using assms
 
   646 proof -
 
   645 proof -
 
   647   -- {* First, it can be shown that the number of @{term P} and
 
   646   -- {* First, it can be shown that the number of @{term P} and
 
   663   ultimately show ?thesis by auto
 
   662   ultimately show ?thesis by auto
 
   664 qed
 
   663 qed
 
   665 
   664 
   666 
   665 
   667 text {*
 
   666 text {*
 
   668 
   667   The following lemmas shows the blocking thread @{text th'} must be live 
   669   The following lemmas shows the blocking thread @{text th'} must be
 
   668   at the very beginning, i.e. the moment (or state) @{term s}. 
   670   live at the very beginning, i.e. the moment (or state) @{term s}.
 
   669 
   671   The proof is a  simple combination of the results above:
 
   670   The proof is a  simple combination of the results above:
 
   672 
   671 *}
 
   673 *}
 
       
   674 
       
   675 lemma runing_threads_inv: 
   672 lemma runing_threads_inv: 
   676   assumes runing': "th' \<in> runing (t@s)"
 
   673   assumes runing': "th' \<in> runing (t@s)"
 
   677   and neq_th': "th' \<noteq> th"
 
   674   and neq_th': "th' \<noteq> th"
 
   678   shows "th' \<in> threads s"
 
   675   shows "th' \<in> threads s"
 
   679 proof(rule ccontr) -- {* Proof by contradiction: *}
 
   676 proof(rule ccontr) -- {* Proof by contradiction: *}
 
   687   qed
 
   684   qed
 
   688   with runing' show False by simp
 
   685   with runing' show False by simp
 
   689 qed
 
   686 qed
 
   690 
   687 
   691 text {*
 
   688 text {*
 
   692 
   689   The following lemma summarizes several foregoing 
   693   The following lemma summarises the above lemmas to give an overall
 
   690   lemmas to give an overall picture of the blocking thread @{text "th'"}:
 
   694   characterisationof the blocking thread @{text "th'"}:
 
   691 *}
 
   695 
       
   696 *}
 
       
   697                   
       
   698 lemma runing_inversion: (* ddd, one of the main lemmas to present *)
 
   692 lemma runing_inversion: (* ddd, one of the main lemmas to present *)
 
   699   assumes runing': "th' \<in> runing (t@s)"
 
   693   assumes runing': "th' \<in> runing (t@s)"
 
   700   and neq_th: "th' \<noteq> th"
 
   694   and neq_th: "th' \<noteq> th"
 
   701   shows "th' \<in> threads s"
 
   695   shows "th' \<in> threads s"
 
   702   and    "\<not>detached s th'"
 
   696   and    "\<not>detached s th'"
 
   710 next
 
   704 next
 
   711   from runing_preced_inversion[OF runing']
 
   705   from runing_preced_inversion[OF runing']
 
   712   show "cp (t@s) th' = preced th s" .
 
   706   show "cp (t@s) th' = preced th s" .
 
   713 qed
 
   707 qed
 
   714 
   708 
   715 
       
   716 section {* The existence of `blocking thread` *}
 
   709 section {* The existence of `blocking thread` *}
 
   717 
   710 
   718 text {* 
   711 text {* 
   719 
   712   Suppose @{term th} is not running, it is first shown that
 
   720   Suppose @{term th} is not running, it is first shown that there is a
 
   713   there is a path in RAG leading from node @{term th} to another thread @{text "th'"} 
   721   path in RAG leading from node @{term th} to another thread @{text
 
   714   in the @{term readys}-set (So @{text "th'"} is an ancestor of @{term th}}).
 
   722   "th'"} in the @{term readys}-set (So @{text "th'"} is an ancestor of
 
   715 
   723   @{term th}}).
 
   716   Now, since @{term readys}-set is non-empty, there must be
 
   724 
   717   one in it which holds the highest @{term cp}-value, which, by definition, 
   725   Now, since @{term readys}-set is non-empty, there must be one in it
 
   718   is the @{term runing}-thread. However, we are going to show more: this running thread
 
   726   which holds the highest @{term cp}-value, which, by definition, is
 
   719   is exactly @{term "th'"}.
 
   727   the @{term runing}-thread. However, we are going to show more: this
 
   720      *}
 
   728   running thread is exactly @{term "th'"}.
 
       
   729 
       
   730 *}
 
       
   731 
       
   732 lemma th_blockedE: (* ddd, the other main lemma to be presented: *)
 
   721 lemma th_blockedE: (* ddd, the other main lemma to be presented: *)
 
   733   assumes "th \<notin> runing (t@s)"
 
   722   assumes "th \<notin> runing (t@s)"
 
   734   obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
 
   723   obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
 
   735                     "th' \<in> runing (t@s)"
 
   724                     "th' \<in> runing (t@s)"
 
   736 proof -
 
   725 proof -
 
   758       also have "... = (the_preced (t @ s) \<circ> the_thread) (Th th)"
 
   747       also have "... = (the_preced (t @ s) \<circ> the_thread) (Th th)"
 
   759       proof(rule image_Max_subset)
 
   748       proof(rule image_Max_subset)
 
   760         show "finite (Th ` (threads (t@s)))" by (simp add: vat_t.finite_threads)
 
   749         show "finite (Th ` (threads (t@s)))" by (simp add: vat_t.finite_threads)
 
   761       next
 
   750       next
 
   762         show "subtree (tRAG (t @ s)) (Th th') \<subseteq> Th ` threads (t @ s)"
 
   751         show "subtree (tRAG (t @ s)) (Th th') \<subseteq> Th ` threads (t @ s)"
 
   763           by (metis Range.intros dp trancl_range vat_t.range_in vat_t.subtree_tRAG_thread) 
   752           by (metis Range.intros dp trancl_range vat_t.rg_RAG_threads vat_t.subtree_tRAG_thread) 
   764       next
 
   753       next
 
   765         show "Th th \<in> subtree (tRAG (t @ s)) (Th th')" using dp
 
   754         show "Th th \<in> subtree (tRAG (t @ s)) (Th th')" using dp
 
   766                     by (unfold tRAG_subtree_eq, auto simp:subtree_def)
 
   755                     by (unfold tRAG_subtree_eq, auto simp:subtree_def)
 
   767       next
 
   756       next
 
   768         show "Max ((the_preced (t @ s) \<circ> the_thread) ` Th ` threads (t @ s)) =
 
   757         show "Max ((the_preced (t @ s) \<circ> the_thread) ` Th ` threads (t @ s)) =
 
   788     using `(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def)
 
   777     using `(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def)
 
   789   ultimately show ?thesis using that by metis
 
   778   ultimately show ?thesis using that by metis
 
   790 qed
 
   779 qed
 
   791 
   780 
   792 text {*
 
   781 text {*
 
   793 
   782   Now it is easy to see there is always a thread to run by case analysis
 
   794   Now it is easy to see there is always a thread to run by case
 
   783   on whether thread @{term th} is running: if the answer is Yes, the 
   795   analysis on whether thread @{term th} is running: if the answer is
 
   784   the running thread is obviously @{term th} itself; otherwise, the running
 
   796   yes, the the running thread is obviously @{term th} itself;
 
   785   thread is the @{text th'} given by lemma @{thm th_blockedE}.
 
   797   otherwise, the running thread is the @{text th'} given by lemma
 
   786 *}
 
   798   @{thm th_blockedE}.
 
       
   799 
       
   800 *}
 
       
   801 
       
   802 lemma live: "runing (t@s) \<noteq> {}"
 
   787 lemma live: "runing (t@s) \<noteq> {}"
 
   803 proof(cases "th \<in> runing (t@s)") 
   788 proof(cases "th \<in> runing (t@s)") 
   804   case True thus ?thesis by auto
 
   789   case True thus ?thesis by auto
 
   805 next
 
   790 next
 
   806   case False
 
   791   case False
 
   807   thus ?thesis using th_blockedE by auto
 
   792   thus ?thesis using th_blockedE by auto
 
   808 qed
 
   793 qed
 
   809 
   794 
   810 
       
   811 end
 
   795 end
 
   812 end
 
   796 end
pip