pip: comparison Correctness.thy

equal deleted inserted replaced

-:633b1fc8631b
+:2af87bb52fca
 text {* Changing counting balance to detachedness *}
 lemmas runing_precond_pre_dtc = runing_precond_pre
 [folded vat_t.detached_eq vat_s.detached_eq]
-lemma runing_precond: (* ddd *)
+section {* The blocking thread *}
-fixes th'
+text {*
+The purpose of PIP is to ensure that the most
+urgent thread @{term th} is not blocked unreasonably.
+Therefore, a clear picture of the blocking thread is essential
+to assure people that the purpose is fulfilled.
+The following lemmas will give us such a picture:
+*}
+(* ccc *)
+text {*
+The following lemma shows the blocking thread @{term th'}
+must hold some resource in the very beginning.
+*}
+lemma runing_cntP_cntV_inv: (* ddd *)
 assumes th'_in: "th' \<in> threads s"
 and neq_th': "th' \<noteq> th"
 and is_runing: "th' \<in> runing (t@s)"
 shows "cntP s th' > cntV s th'"
 using assms
 ultimately show ?thesis by auto
 qed
 (* The foregoing two lemmas are preparation for this one, but
 in long run can be combined. Maybe I am wrong.
+This one is useless (* XY *)
 *)
 lemma moment_blocked:
 assumes neq_th': "th' \<noteq> th"
 and th'_in: "th' \<in> threads ((moment i t)@s)"
 and dtc: "detached (moment i t @ s) th'"
 by (metis dtc h_i.detached_elim)
 from moment_blocked_eqpv[OF neq_th' th'_in cnt_i le_ij]
 show ?thesis by (metis h_j.detached_intro)
 qed
+text {*
+The following lemmas shows that the @{term cp}-value
+of the blocking thread @{text th'} equals to the highest
+precedence in the whole system.
+*}
 lemma runing_preced_inversion:
 assumes runing': "th' \<in> runing (t@s)"
 shows "cp (t@s) th' = preced th s" (is "?L = ?R")
 proof -
 have "?L = Max (cp (t @ s) ` readys (t @ s))" using assms
 also have "\<dots> = ?R"
 by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads)
 finally show ?thesis .
 qed
-text {*
-The situation when @{term "th"} is blocked is analyzed by the following lemmas.
+text {*
-*}
+The following lemmas shows the blocking thread @{text th'} must be live
+at the very beginning, i.e. the moment (or state) @{term s}.
-text {*
+*}
-The following lemmas shows the running thread @{text "th'"}, if it is different from
+lemma runing_threads_inv: (* ddd *)
-@{term th}, must be live at the very beginning. By the term {\em the very beginning},
+assumes runing': "th' \<in> runing (t@s)"
-we mean the moment where the formal investigation starts, i.e. the moment (or state)
+and neq_th': "th' \<noteq> th"
-@{term s}.
-*}
-lemma runing_inversion_0:
-assumes neq_th': "th' \<noteq> th"
-and runing': "th' \<in> runing (t@s)"
 shows "th' \<in> threads s"
 proof -
 -- {* The proof is by contradiction: *}
 { assume otherwise: "\<not> ?thesis"
 have "th' \<notin> runing (t @ s)"
 with `th' \<in> runing (t@s)`
 have False by simp
 } thus ?thesis by auto
 qed
 text {*
-The second lemma says, if the running thread @{text th'} is different from
+The following lemma summarizes several foregoing
-@{term th}, then this @{text th'} must in the possession of some resources
+lemmas to give an overall picture of the blocking thread @{text "th'"}:
-at the very beginning.
+*}
+lemma runing_inversion:
-To ease the reasoning of resource possession of one particular thread,
-we used two auxiliary functions @{term cntV} and @{term cntP},
-which are the counters of @{term P}-operations and
-@{term V}-operations respectively.
-If the number of @{term V}-operation is less than the number of
-@{term "P"}-operations, the thread must have some unreleased resource.
-*}
-lemma runing_inversion_1: (* ddd *)
-assumes neq_th': "th' \<noteq> th"
-and runing': "th' \<in> runing (t@s)"
--- {* thread @{term "th'"} is a live on in state @{term "s"} and
-it has some unreleased resource. *}
-shows "th' \<in> threads s \<and> cntV s th' < cntP s th'"
-proof -
--- {* The proof is a simple composition of @{thm runing_inversion_0} and
-@{thm runing_precond}: *}
--- {* By applying @{thm runing_inversion_0} to assumptions,
-it can be shown that @{term th'} is live in state @{term s}: *}
-have "th' \<in> threads s"  using runing_inversion_0[OF assms(1,2)] .
--- {* Then the thesis is derived easily by applying @{thm runing_precond}: *}
-with runing_precond [OF this neq_th' runing'] show ?thesis by simp
-qed
-text {*
-The following lemma is just a rephrasing of @{thm runing_inversion_1}:
-*}
-lemma runing_inversion_2:
-assumes runing': "th' \<in> runing (t@s)"
-shows "th' = th \<or> (th' \<noteq> th \<and> th' \<in> threads s \<and> cntV s th' < cntP s th')"
-proof -
-from runing_inversion_1[OF _ runing']
-show ?thesis by auto
-qed
-lemma runing_inversion_3:
-assumes runing': "th' \<in> runing (t@s)"
-and neq_th: "th' \<noteq> th"
-shows "th' \<in> threads s \<and> (cntV s th' < cntP s th' \<and> cp (t@s) th' = preced th s)"
-by (metis neq_th runing' runing_inversion_2 runing_preced_inversion)
-lemma runing_inversion_4:
 assumes runing': "th' \<in> runing (t@s)"
 and neq_th: "th' \<noteq> th"
 shows "th' \<in> threads s"
 and    "\<not>detached s th'"
 and    "cp (t@s) th' = preced th s"
-apply (metis neq_th runing' runing_inversion_2)
+proof -
-apply (metis neq_th pv_blocked runing' runing_inversion_2 runing_precond_pre_dtc)
+from runing_threads_inv[OF assms]
-by (metis neq_th runing' runing_inversion_3)
+show "th' \<in> threads s" .
+next
+from runing_cntP_cntV_inv[OF runing_threads_inv[OF assms] neq_th runing']
+show "\<not>detached s th'" using vat_s.detached_eq by simp
+next
+from runing_preced_inversion[OF runing']
+show "cp (t@s) th' = preced th s" .
+qed
 text {*
 Suppose @{term th} is not running, it is first shown that
 there is a path in RAG leading from node @{term th} to another thread @{text "th'"}
 in the @{term readys}-set (So @{text "th'"} is an ancestor of @{term th}}).

changeset 66	2af87bb52fca
parent 65	633b1fc8631b
child 67	25fd656667a7