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