--- a/Correctness.thy Sat Jan 16 10:59:03 2016 +0800
+++ b/Correctness.thy Sat Jan 16 11:02:17 2016 +0800
@@ -503,29 +503,29 @@
qed
text {*
- The following lemma shows how the counting of
- @{term "P"} and @{term "V"} operations affects
- the running state of threads in @{term t}.
- The lemma shows that if a thread's @{term "P"}-count equals
- its @{term "V"}-count (which means it no longer has any
- resource in its possession), it can not be in running thread.
+ The following lemma shows how the counters for @{term "P"} and
+ @{term "V"} operations relate to the running threads in the states
+ @{term s} and @{term "t @ s"}. The lemma shows that if a thread's
+ @{term "P"}-count equals its @{term "V"}-count (which means it no
+ longer has any resource in its possession), it cannot be a running
+ thread.
- The proof is by contraction with the assumption @{text "th' \<noteq> th"}.
- The key is the use of @{thm count_eq_dependants}
- to derive the emptiness of @{text th'}s @{term dependants}-set
- from the balance of its @{term P} @{term V} counts.
- From this, it can be shown @{text th'}s @{term cp}-value
- equals to its own precedence.
+ The proof is by contraction with the assumption @{text "th' \<noteq> th"}.
+ The key is the use of @{thm count_eq_dependants} to derive the
+ emptiness of @{text th'}s @{term dependants}-set from the balance of
+ its @{term P} and @{term V} counts. From this, it can be shown
+ @{text th'}s @{term cp}-value equals to its own precedence.
- On the other hand, since @{text th'} is running, by
- @{thm runing_preced_inversion}, its @{term cp}-value
- equals to the precedence of @{term th}.
+ On the other hand, since @{text th'} is running, by @{thm
+ runing_preced_inversion}, its @{term cp}-value equals to the
+ precedence of @{term th}.
- Combining the above two we have that @{text th'} and
- @{term th} have the same precedence. By uniqueness of precedence, we
- have @{text "th' = th"}, which is in contradiction with the
- assumption @{text "th' \<noteq> th"}.
+ Combining the above two resukts we have that @{text th'} and @{term
+ th} have the same precedence. By uniqueness of precedences, we have
+ @{text "th' = th"}, which is in contradiction with the assumption
+ @{text "th' \<noteq> th"}.
+
*}
lemma eq_pv_blocked: (* ddd *)
--- a/Correctness.thy~ Sat Jan 16 10:59:03 2016 +0800
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,795 +0,0 @@
-theory Correctness
-imports PIPBasics
-begin
-
-
-text {*
- The following two auxiliary lemmas are used to reason about @{term Max}.
-*}
-lemma image_Max_eqI:
- assumes "finite B"
- and "b \<in> B"
- and "\<forall> x \<in> B. f x \<le> f b"
- shows "Max (f ` B) = f b"
- using assms
- using Max_eqI by blast
-
-lemma image_Max_subset:
- assumes "finite A"
- and "B \<subseteq> A"
- and "a \<in> B"
- and "Max (f ` A) = f a"
- shows "Max (f ` B) = f a"
-proof(rule image_Max_eqI)
- show "finite B"
- using assms(1) assms(2) finite_subset by auto
-next
- show "a \<in> B" using assms by simp
-next
- show "\<forall>x\<in>B. f x \<le> f a"
- by (metis Max_ge assms(1) assms(2) assms(4)
- finite_imageI image_eqI subsetCE)
-qed
-
-text {*
- The following locale @{text "highest_gen"} sets the basic context for our
- investigation: supposing thread @{text th} holds the highest @{term cp}-value
- in state @{text s}, which means the task for @{text th} is the
- most urgent. We want to show that
- @{text th} is treated correctly by PIP, which means
- @{text th} will not be blocked unreasonably by other less urgent
- threads.
-*}
-locale highest_gen =
- fixes s th prio tm
- assumes vt_s: "vt s"
- and threads_s: "th \<in> threads s"
- and highest: "preced th s = Max ((cp s)`threads s)"
- -- {* The internal structure of @{term th}'s precedence is exposed:*}
- and preced_th: "preced th s = Prc prio tm"
-
--- {* @{term s} is a valid trace, so it will inherit all results derived for
- a valid trace: *}
-sublocale highest_gen < vat_s: valid_trace "s"
- by (unfold_locales, insert vt_s, simp)
-
-context highest_gen
-begin
-
-text {*
- @{term tm} is the time when the precedence of @{term th} is set, so
- @{term tm} must be a valid moment index into @{term s}.
-*}
-lemma lt_tm: "tm < length s"
- by (insert preced_tm_lt[OF threads_s preced_th], simp)
-
-text {*
- Since @{term th} holds the highest precedence and @{text "cp"}
- is the highest precedence of all threads in the sub-tree of
- @{text "th"} and @{text th} is among these threads,
- its @{term cp} must equal to its precedence:
-*}
-lemma eq_cp_s_th: "cp s th = preced th s" (is "?L = ?R")
-proof -
- have "?L \<le> ?R"
- by (unfold highest, rule Max_ge,
- auto simp:threads_s finite_threads)
- moreover have "?R \<le> ?L"
- by (unfold vat_s.cp_rec, rule Max_ge,
- auto simp:the_preced_def vat_s.fsbttRAGs.finite_children)
- ultimately show ?thesis by auto
-qed
-
-lemma highest_cp_preced: "cp s th = Max (the_preced s ` threads s)"
- using eq_cp_s_th highest max_cp_eq the_preced_def by presburger
-
-
-lemma highest_preced_thread: "preced th s = Max (the_preced s ` threads s)"
- by (fold eq_cp_s_th, unfold highest_cp_preced, simp)
-
-lemma highest': "cp s th = Max (cp s ` threads s)"
- by (simp add: eq_cp_s_th highest)
-
-end
-
-locale extend_highest_gen = highest_gen +
- fixes t
- assumes vt_t: "vt (t@s)"
- and create_low: "Create th' prio' \<in> set t \<Longrightarrow> prio' \<le> prio"
- and set_diff_low: "Set th' prio' \<in> set t \<Longrightarrow> th' \<noteq> th \<and> prio' \<le> prio"
- and exit_diff: "Exit th' \<in> set t \<Longrightarrow> th' \<noteq> th"
-
-sublocale extend_highest_gen < vat_t: valid_trace "t@s"
- by (unfold_locales, insert vt_t, simp)
-
-lemma step_back_vt_app:
- assumes vt_ts: "vt (t@s)"
- shows "vt s"
-proof -
- from vt_ts show ?thesis
- proof(induct t)
- case Nil
- from Nil show ?case by auto
- next
- case (Cons e t)
- assume ih: " vt (t @ s) \<Longrightarrow> vt s"
- and vt_et: "vt ((e # t) @ s)"
- show ?case
- proof(rule ih)
- show "vt (t @ s)"
- proof(rule step_back_vt)
- from vt_et show "vt (e # t @ s)" by simp
- qed
- qed
- qed
-qed
-
-locale red_extend_highest_gen = extend_highest_gen +
- fixes i::nat
-
-sublocale red_extend_highest_gen < red_moment: extend_highest_gen "s" "th" "prio" "tm" "(moment i t)"
- apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric])
- apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp)
- by (unfold highest_gen_def, auto dest:step_back_vt_app)
-
-context extend_highest_gen
-begin
-
- lemma ind [consumes 0, case_names Nil Cons, induct type]:
- assumes
- h0: "R []"
- and h2: "\<And> e t. \<lbrakk>vt (t@s); step (t@s) e;
- extend_highest_gen s th prio tm t;
- extend_highest_gen s th prio tm (e#t); R t\<rbrakk> \<Longrightarrow> R (e#t)"
- shows "R t"
-proof -
- from vt_t extend_highest_gen_axioms show ?thesis
- proof(induct t)
- from h0 show "R []" .
- next
- case (Cons e t')
- assume ih: "\<lbrakk>vt (t' @ s); extend_highest_gen s th prio tm t'\<rbrakk> \<Longrightarrow> R t'"
- and vt_e: "vt ((e # t') @ s)"
- and et: "extend_highest_gen s th prio tm (e # t')"
- from vt_e and step_back_step have stp: "step (t'@s) e" by auto
- from vt_e and step_back_vt have vt_ts: "vt (t'@s)" by auto
- show ?case
- proof(rule h2 [OF vt_ts stp _ _ _ ])
- show "R t'"
- proof(rule ih)
- from et show ext': "extend_highest_gen s th prio tm t'"
- by (unfold extend_highest_gen_def extend_highest_gen_axioms_def, auto dest:step_back_vt)
- next
- from vt_ts show "vt (t' @ s)" .
- qed
- next
- from et show "extend_highest_gen s th prio tm (e # t')" .
- next
- from et show ext': "extend_highest_gen s th prio tm t'"
- by (unfold extend_highest_gen_def extend_highest_gen_axioms_def, auto dest:step_back_vt)
- qed
- qed
-qed
-
-
-lemma th_kept: "th \<in> threads (t @ s) \<and>
- preced th (t@s) = preced th s" (is "?Q t")
-proof -
- show ?thesis
- proof(induct rule:ind)
- case Nil
- from threads_s
- show ?case
- by auto
- next
- case (Cons e t)
- interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto
- interpret h_t: extend_highest_gen _ _ _ _ t using Cons by auto
- show ?case
- proof(cases e)
- case (Create thread prio)
- show ?thesis
- proof -
- from Cons and Create have "step (t@s) (Create thread prio)" by auto
- hence "th \<noteq> thread"
- proof(cases)
- case thread_create
- with Cons show ?thesis by auto
- qed
- hence "preced th ((e # t) @ s) = preced th (t @ s)"
- by (unfold Create, auto simp:preced_def)
- moreover note Cons
- ultimately show ?thesis
- by (auto simp:Create)
- qed
- next
- case (Exit thread)
- from h_e.exit_diff and Exit
- have neq_th: "thread \<noteq> th" by auto
- with Cons
- show ?thesis
- by (unfold Exit, auto simp:preced_def)
- next
- case (P thread cs)
- with Cons
- show ?thesis
- by (auto simp:P preced_def)
- next
- case (V thread cs)
- with Cons
- show ?thesis
- by (auto simp:V preced_def)
- next
- case (Set thread prio')
- show ?thesis
- proof -
- from h_e.set_diff_low and Set
- have "th \<noteq> thread" by auto
- hence "preced th ((e # t) @ s) = preced th (t @ s)"
- by (unfold Set, auto simp:preced_def)
- moreover note Cons
- ultimately show ?thesis
- by (auto simp:Set)
- qed
- qed
- qed
-qed
-
-text {*
- According to @{thm th_kept}, thread @{text "th"} has its living status
- and precedence kept along the way of @{text "t"}. The following lemma
- shows that this preserved precedence of @{text "th"} remains as the highest
- along the way of @{text "t"}.
-
- The proof goes by induction over @{text "t"} using the specialized
- induction rule @{thm ind}, followed by case analysis of each possible
- operations of PIP. All cases follow the same pattern rendered by the
- generalized introduction rule @{thm "image_Max_eqI"}.
-
- The very essence is to show that precedences, no matter whether they
- are newly introduced or modified, are always lower than the one held
- by @{term "th"}, which by @{thm th_kept} is preserved along the way.
-*}
-lemma max_kept: "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s"
-proof(induct rule:ind)
- case Nil
- from highest_preced_thread
- show ?case by simp
-next
- case (Cons e t)
- interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto
- interpret h_t: extend_highest_gen _ _ _ _ t using Cons by auto
- show ?case
- proof(cases e)
- case (Create thread prio')
- show ?thesis (is "Max (?f ` ?A) = ?t")
- proof -
- -- {* The following is the common pattern of each branch of the case analysis. *}
- -- {* The major part is to show that @{text "th"} holds the highest precedence: *}
- have "Max (?f ` ?A) = ?f th"
- proof(rule image_Max_eqI)
- show "finite ?A" using h_e.finite_threads by auto
- next
- show "th \<in> ?A" using h_e.th_kept by auto
- next
- show "\<forall>x\<in>?A. ?f x \<le> ?f th"
- proof
- fix x
- assume "x \<in> ?A"
- hence "x = thread \<or> x \<in> threads (t@s)" by (auto simp:Create)
- thus "?f x \<le> ?f th"
- proof
- assume "x = thread"
- thus ?thesis
- apply (simp add:Create the_preced_def preced_def, fold preced_def)
- using Create h_e.create_low h_t.th_kept lt_tm preced_leI2
- preced_th by force
- next
- assume h: "x \<in> threads (t @ s)"
- from Cons(2)[unfolded Create]
- have "x \<noteq> thread" using h by (cases, auto)
- hence "?f x = the_preced (t@s) x"
- by (simp add:Create the_preced_def preced_def)
- hence "?f x \<le> Max (the_preced (t@s) ` threads (t@s))"
- by (simp add: h_t.finite_threads h)
- also have "... = ?f th"
- by (metis Cons.hyps(5) h_e.th_kept the_preced_def)
- finally show ?thesis .
- qed
- qed
- qed
- -- {* The minor part is to show that the precedence of @{text "th"}
- equals to preserved one, given by the foregoing lemma @{thm th_kept} *}
- also have "... = ?t" using h_e.th_kept the_preced_def by auto
- -- {* Then it follows trivially that the precedence preserved
- for @{term "th"} remains the maximum of all living threads along the way. *}
- finally show ?thesis .
- qed
- next
- case (Exit thread)
- show ?thesis (is "Max (?f ` ?A) = ?t")
- proof -
- have "Max (?f ` ?A) = ?f th"
- proof(rule image_Max_eqI)
- show "finite ?A" using h_e.finite_threads by auto
- next
- show "th \<in> ?A" using h_e.th_kept by auto
- next
- show "\<forall>x\<in>?A. ?f x \<le> ?f th"
- proof
- fix x
- assume "x \<in> ?A"
- hence "x \<in> threads (t@s)" by (simp add: Exit)
- hence "?f x \<le> Max (?f ` threads (t@s))"
- by (simp add: h_t.finite_threads)
- also have "... \<le> ?f th"
- apply (simp add:Exit the_preced_def preced_def, fold preced_def)
- using Cons.hyps(5) h_t.th_kept the_preced_def by auto
- finally show "?f x \<le> ?f th" .
- qed
- qed
- also have "... = ?t" using h_e.th_kept the_preced_def by auto
- finally show ?thesis .
- qed
- next
- case (P thread cs)
- with Cons
- show ?thesis by (auto simp:preced_def the_preced_def)
- next
- case (V thread cs)
- with Cons
- show ?thesis by (auto simp:preced_def the_preced_def)
- next
- case (Set thread prio')
- show ?thesis (is "Max (?f ` ?A) = ?t")
- proof -
- have "Max (?f ` ?A) = ?f th"
- proof(rule image_Max_eqI)
- show "finite ?A" using h_e.finite_threads by auto
- next
- show "th \<in> ?A" using h_e.th_kept by auto
- next
- show "\<forall>x\<in>?A. ?f x \<le> ?f th"
- proof
- fix x
- assume h: "x \<in> ?A"
- show "?f x \<le> ?f th"
- proof(cases "x = thread")
- case True
- moreover have "the_preced (Set thread prio' # t @ s) thread \<le> the_preced (t @ s) th"
- proof -
- have "the_preced (t @ s) th = Prc prio tm"
- using h_t.th_kept preced_th by (simp add:the_preced_def)
- moreover have "prio' \<le> prio" using Set h_e.set_diff_low by auto
- ultimately show ?thesis by (insert lt_tm, auto simp:the_preced_def preced_def)
- qed
- ultimately show ?thesis
- by (unfold Set, simp add:the_preced_def preced_def)
- next
- case False
- then have "?f x = the_preced (t@s) x"
- by (simp add:the_preced_def preced_def Set)
- also have "... \<le> Max (the_preced (t@s) ` threads (t@s))"
- using Set h h_t.finite_threads by auto
- also have "... = ?f th" by (metis Cons.hyps(5) h_e.th_kept the_preced_def)
- finally show ?thesis .
- qed
- qed
- qed
- also have "... = ?t" using h_e.th_kept the_preced_def by auto
- finally show ?thesis .
- qed
- qed
-qed
-
-lemma max_preced: "preced th (t@s) = Max (the_preced (t@s) ` (threads (t@s)))"
- by (insert th_kept max_kept, auto)
-
-text {*
- The reason behind the following lemma is that:
- Since @{term "cp"} is defined as the maximum precedence
- of those threads contained in the sub-tree of node @{term "Th th"}
- in @{term "RAG (t@s)"}, and all these threads are living threads, and
- @{term "th"} is also among them, the maximum precedence of
- them all must be the one for @{text "th"}.
-*}
-lemma th_cp_max_preced:
- "cp (t@s) th = Max (the_preced (t@s) ` (threads (t@s)))" (is "?L = ?R")
-proof -
- let ?f = "the_preced (t@s)"
- have "?L = ?f th"
- proof(unfold cp_alt_def, rule image_Max_eqI)
- show "finite {th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}"
- proof -
- have "{th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)} =
- the_thread ` {n . n \<in> subtree (RAG (t @ s)) (Th th) \<and>
- (\<exists> th'. n = Th th')}"
- by (smt Collect_cong Setcompr_eq_image mem_Collect_eq the_thread.simps)
- moreover have "finite ..." by (simp add: vat_t.fsbtRAGs.finite_subtree)
- ultimately show ?thesis by simp
- qed
- next
- show "th \<in> {th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}"
- by (auto simp:subtree_def)
- next
- show "\<forall>x\<in>{th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}.
- the_preced (t @ s) x \<le> the_preced (t @ s) th"
- proof
- fix th'
- assume "th' \<in> {th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}"
- hence "Th th' \<in> subtree (RAG (t @ s)) (Th th)" by auto
- moreover have "... \<subseteq> Field (RAG (t @ s)) \<union> {Th th}"
- by (meson subtree_Field)
- ultimately have "Th th' \<in> ..." by auto
- hence "th' \<in> threads (t@s)"
- proof
- assume "Th th' \<in> {Th th}"
- thus ?thesis using th_kept by auto
- next
- assume "Th th' \<in> Field (RAG (t @ s))"
- thus ?thesis using vat_t.not_in_thread_isolated by blast
- qed
- thus "the_preced (t @ s) th' \<le> the_preced (t @ s) th"
- by (metis Max_ge finite_imageI finite_threads image_eqI
- max_kept th_kept the_preced_def)
- qed
- qed
- also have "... = ?R" by (simp add: max_preced the_preced_def)
- finally show ?thesis .
-qed
-
-lemma th_cp_max[simp]: "Max (cp (t@s) ` threads (t@s)) = cp (t@s) th"
- using max_cp_eq th_cp_max_preced the_preced_def vt_t by presburger
-
-lemma [simp]: "Max (cp (t@s) ` threads (t@s)) = Max (the_preced (t@s) ` threads (t@s))"
- by (simp add: th_cp_max_preced)
-
-lemma [simp]: "Max (the_preced (t@s) ` threads (t@s)) = the_preced (t@s) th"
- using max_kept th_kept the_preced_def by auto
-
-lemma [simp]: "the_preced (t@s) th = preced th (t@s)"
- using the_preced_def by auto
-
-lemma [simp]: "preced th (t@s) = preced th s"
- by (simp add: th_kept)
-
-lemma [simp]: "cp s th = preced th s"
- by (simp add: eq_cp_s_th)
-
-lemma th_cp_preced [simp]: "cp (t@s) th = preced th s"
- by (fold max_kept, unfold th_cp_max_preced, simp)
-
-lemma preced_less:
- assumes th'_in: "th' \<in> threads s"
- and neq_th': "th' \<noteq> th"
- shows "preced th' s < preced th s"
- using assms
-by (metis Max.coboundedI finite_imageI highest not_le order.trans
- preced_linorder rev_image_eqI threads_s vat_s.finite_threads
- vat_s.le_cp)
-
-section {* The `blocking thread` *}
-
-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.
-
- In this section, we are going to derive a series of lemmas
- with finally give rise to a picture of the blocking thread.
-
- By `blocking thread`, we mean a thread in running state but
- different from thread @{term th}.
-*}
-
-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
- by (unfold runing_def, auto)
- also have "\<dots> = ?R"
- by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads)
- finally show ?thesis .
-qed
-
-text {*
- The following lemma shows how the counting of
- @{term "P"} and @{term "V"} operations affects
- the running state of threads in @{term t}.
-
- The lemma shows that if a thread's @{term "P"}-count equals
- its @{term "V"}-count (which means it no longer has any
- resource in its possession), it can not be in running thread.
-
- The proof is by contraction with the assumption @{text "th' \<noteq> th"}.
- The key is the use of @{thm count_eq_dependants}
- to derive the emptiness of @{text th'}s @{term dependants}-set
- from the balance of its @{term P} @{term V} counts.
- From this, it can be shown @{text th'}s @{term cp}-value
- equals to its own precedence.
-
- On the other hand, since @{text th'} is running, by
- @{thm runing_preced_inversion}, its @{term cp}-value
- equals to the precedence of @{term th}.
-
- Combining the above two we have that @{text th'} and
- @{term th} have the same precedence. By uniqueness of precedence, we
- have @{text "th' = th"}, which is in contradiction with the
- assumption @{text "th' \<noteq> th"}.
-*}
-
-lemma eq_pv_blocked: (* ddd *)
- assumes neq_th': "th' \<noteq> th"
- and eq_pv: "cntP (t@s) th' = cntV (t@s) th'"
- shows "th' \<notin> runing (t@s)"
-proof
- assume otherwise: "th' \<in> runing (t@s)"
- show False
- proof -
- have th'_in: "th' \<in> threads (t@s)"
- using otherwise readys_threads runing_def by auto
- have "th' = th"
- proof(rule preced_unique)
- -- {* The proof goes like this:
- it is first shown that the @{term preced}-value of @{term th'}
- equals to that of @{term th}, then by uniqueness
- of @{term preced}-values (given by lemma @{thm preced_unique}),
- @{term th'} equals to @{term th}: *}
- show "preced th' (t @ s) = preced th (t @ s)" (is "?L = ?R")
- proof -
- -- {* Since the counts of @{term th'} are balanced, the subtree
- of it contains only itself, so, its @{term cp}-value
- equals its @{term preced}-value: *}
- have "?L = cp (t@s) th'"
- by (unfold cp_eq_cpreced cpreced_def count_eq_dependants[OF eq_pv], simp)
- -- {* Since @{term "th'"} is running, by @{thm runing_preced_inversion},
- its @{term cp}-value equals @{term "preced th s"},
- which equals to @{term "?R"} by simplification: *}
- also have "... = ?R"
- thm runing_preced_inversion
- using runing_preced_inversion[OF otherwise] by simp
- finally show ?thesis .
- qed
- qed (auto simp: th'_in th_kept)
- with `th' \<noteq> th` show ?thesis by simp
- qed
-qed
-
-text {*
- The following lemma is the extrapolation of @{thm eq_pv_blocked}.
- It says if a thread, different from @{term th},
- does not hold any resource at the very beginning,
- it will keep hand-emptied in the future @{term "t@s"}.
-*}
-lemma eq_pv_persist: (* ddd *)
- assumes neq_th': "th' \<noteq> th"
- and eq_pv: "cntP s th' = cntV s th'"
- shows "cntP (t@s) th' = cntV (t@s) th'"
-proof(induction rule:ind) -- {* The proof goes by induction. *}
- -- {* The nontrivial case is for the @{term Cons}: *}
- case (Cons e t)
- -- {* All results derived so far hold for both @{term s} and @{term "t@s"}: *}
- interpret vat_t: extend_highest_gen s th prio tm t using Cons by simp
- interpret vat_e: extend_highest_gen s th prio tm "(e # t)" using Cons by simp
- show ?case
- proof -
- -- {* It can be proved that @{term cntP}-value of @{term th'} does not change
- by the happening of event @{term e}: *}
- have "cntP ((e#t)@s) th' = cntP (t@s) th'"
- proof(rule ccontr) -- {* Proof by contradiction. *}
- -- {* Suppose @{term cntP}-value of @{term th'} is changed by @{term e}: *}
- assume otherwise: "cntP ((e # t) @ s) th' \<noteq> cntP (t @ s) th'"
- -- {* Then the actor of @{term e} must be @{term th'} and @{term e}
- must be a @{term P}-event: *}
- hence "isP e" "actor e = th'" by (auto simp:cntP_diff_inv)
- with vat_t.actor_inv[OF Cons(2)]
- -- {* According to @{thm actor_inv}, @{term th'} must be running at
- the moment @{term "t@s"}: *}
- have "th' \<in> runing (t@s)" by (cases e, auto)
- -- {* However, an application of @{thm eq_pv_blocked} to induction hypothesis
- shows @{term th'} can not be running at moment @{term "t@s"}: *}
- moreover have "th' \<notin> runing (t@s)"
- using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] .
- -- {* Contradiction is finally derived: *}
- ultimately show False by simp
- qed
- -- {* It can also be proved that @{term cntV}-value of @{term th'} does not change
- by the happening of event @{term e}: *}
- -- {* The proof follows exactly the same pattern as the case for @{term cntP}-value: *}
- moreover have "cntV ((e#t)@s) th' = cntV (t@s) th'"
- proof(rule ccontr) -- {* Proof by contradiction. *}
- assume otherwise: "cntV ((e # t) @ s) th' \<noteq> cntV (t @ s) th'"
- hence "isV e" "actor e = th'" by (auto simp:cntV_diff_inv)
- with vat_t.actor_inv[OF Cons(2)]
- have "th' \<in> runing (t@s)" by (cases e, auto)
- moreover have "th' \<notin> runing (t@s)"
- using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] .
- ultimately show False by simp
- qed
- -- {* Finally, it can be shown that the @{term cntP} and @{term cntV}
- value for @{term th'} are still in balance, so @{term th'}
- is still hand-emptied after the execution of event @{term e}: *}
- ultimately show ?thesis using Cons(5) by metis
- qed
-qed (auto simp:eq_pv)
-
-text {*
- By combining @{thm eq_pv_blocked} and @{thm eq_pv_persist},
- it can be derived easily that @{term th'} can not be running in the future:
-*}
-lemma eq_pv_blocked_persist:
- assumes neq_th': "th' \<noteq> th"
- and eq_pv: "cntP s th' = cntV s th'"
- shows "th' \<notin> runing (t@s)"
- using assms
- by (simp add: eq_pv_blocked eq_pv_persist)
-
-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 is_runing: "th' \<in> runing (t@s)"
- and neq_th': "th' \<noteq> th"
- shows "cntP s th' > cntV s th'"
- using assms
-proof -
- -- {* First, it can be shown that the number of @{term P} and
- @{term V} operations can not be equal for thred @{term th'} *}
- have "cntP s th' \<noteq> cntV s th'"
- proof
- -- {* The proof goes by contradiction, suppose otherwise: *}
- assume otherwise: "cntP s th' = cntV s th'"
- -- {* By applying @{thm eq_pv_blocked_persist} to this: *}
- from eq_pv_blocked_persist[OF neq_th' otherwise]
- -- {* we have that @{term th'} can not be running at moment @{term "t@s"}: *}
- have "th' \<notin> runing (t@s)" .
- -- {* This is obvious in contradiction with assumption @{thm is_runing} *}
- thus False using is_runing by simp
- qed
- -- {* However, the number of @{term V} is always less or equal to @{term P}: *}
- moreover have "cntV s th' \<le> cntP s th'" using vat_s.cnp_cnv_cncs by auto
- -- {* Thesis is finally derived by combining the these two results: *}
- ultimately show ?thesis by auto
-qed
-
-
-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}.
-
- The proof is a simple combination of the results above:
-*}
-lemma runing_threads_inv:
- assumes runing': "th' \<in> runing (t@s)"
- and neq_th': "th' \<noteq> th"
- shows "th' \<in> threads s"
-proof(rule ccontr) -- {* Proof by contradiction: *}
- assume otherwise: "th' \<notin> threads s"
- have "th' \<notin> runing (t @ s)"
- proof -
- from vat_s.cnp_cnv_eq[OF otherwise]
- have "cntP s th' = cntV s th'" .
- from eq_pv_blocked_persist[OF neq_th' this]
- show ?thesis .
- qed
- with runing' show False by simp
-qed
-
-text {*
- The following lemma summarizes several foregoing
- lemmas to give an overall picture of the blocking thread @{text "th'"}:
-*}
-lemma runing_inversion: (* ddd, one of the main lemmas to present *)
- 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"
-proof -
- from runing_threads_inv[OF assms]
- show "th' \<in> threads s" .
-next
- from runing_cntP_cntV_inv[OF runing' neq_th]
- 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
-
-section {* The existence of `blocking thread` *}
-
-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}}).
-
- Now, since @{term readys}-set is non-empty, there must be
- one in it which holds the highest @{term cp}-value, which, by definition,
- is the @{term runing}-thread. However, we are going to show more: this running thread
- is exactly @{term "th'"}.
- *}
-lemma th_blockedE: (* ddd, the other main lemma to be presented: *)
- assumes "th \<notin> runing (t@s)"
- obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
- "th' \<in> runing (t@s)"
-proof -
- -- {* According to @{thm vat_t.th_chain_to_ready}, either
- @{term "th"} is in @{term "readys"} or there is path leading from it to
- one thread in @{term "readys"}. *}
- have "th \<in> readys (t @ s) \<or> (\<exists>th'. th' \<in> readys (t @ s) \<and> (Th th, Th th') \<in> (RAG (t @ s))\<^sup>+)"
- using th_kept vat_t.th_chain_to_ready by auto
- -- {* However, @{term th} can not be in @{term readys}, because otherwise, since
- @{term th} holds the highest @{term cp}-value, it must be @{term "runing"}. *}
- moreover have "th \<notin> readys (t@s)"
- using assms runing_def th_cp_max vat_t.max_cp_readys_threads by auto
- -- {* So, there must be a path from @{term th} to another thread @{text "th'"} in
- term @{term readys}: *}
- ultimately obtain th' where th'_in: "th' \<in> readys (t@s)"
- and dp: "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+" by auto
- -- {* We are going to show that this @{term th'} is running. *}
- have "th' \<in> runing (t@s)"
- proof -
- -- {* We only need to show that this @{term th'} holds the highest @{term cp}-value: *}
- have "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" (is "?L = ?R")
- proof -
- have "?L = Max ((the_preced (t @ s) \<circ> the_thread) ` subtree (tRAG (t @ s)) (Th th'))"
- by (unfold cp_alt_def1, simp)
- also have "... = (the_preced (t @ s) \<circ> the_thread) (Th th)"
- proof(rule image_Max_subset)
- show "finite (Th ` (threads (t@s)))" by (simp add: vat_t.finite_threads)
- next
- show "subtree (tRAG (t @ s)) (Th th') \<subseteq> Th ` threads (t @ s)"
- by (metis Range.intros dp trancl_range vat_t.range_in vat_t.subtree_tRAG_thread)
- next
- show "Th th \<in> subtree (tRAG (t @ s)) (Th th')" using dp
- by (unfold tRAG_subtree_eq, auto simp:subtree_def)
- next
- show "Max ((the_preced (t @ s) \<circ> the_thread) ` Th ` threads (t @ s)) =
- (the_preced (t @ s) \<circ> the_thread) (Th th)" (is "Max ?L = _")
- proof -
- have "?L = the_preced (t @ s) ` threads (t @ s)"
- by (unfold image_comp, rule image_cong, auto)
- thus ?thesis using max_preced the_preced_def by auto
- qed
- qed
- also have "... = ?R"
- using th_cp_max th_cp_preced th_kept
- the_preced_def vat_t.max_cp_readys_threads by auto
- finally show ?thesis .
- qed
- -- {* Now, since @{term th'} holds the highest @{term cp}
- and we have already show it is in @{term readys},
- it is @{term runing} by definition. *}
- with `th' \<in> readys (t@s)` show ?thesis by (simp add: runing_def)
- qed
- -- {* It is easy to show @{term th'} is an ancestor of @{term th}: *}
- moreover have "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
- using `(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def)
- ultimately show ?thesis using that by metis
-qed
-
-text {*
- Now it is easy to see there is always a thread to run by case analysis
- on whether thread @{term th} is running: if the answer is Yes, the
- the running thread is obviously @{term th} itself; otherwise, the running
- thread is the @{text th'} given by lemma @{thm th_blockedE}.
-*}
-lemma live: "runing (t@s) \<noteq> {}"
-proof(cases "th \<in> runing (t@s)")
- case True thus ?thesis by auto
-next
- case False
- thus ?thesis using th_blockedE by auto
-qed
-
-
-end
-end
--- a/Journal/Paper.thy Sat Jan 16 10:59:03 2016 +0800
+++ b/Journal/Paper.thy Sat Jan 16 11:02:17 2016 +0800
@@ -5,10 +5,8 @@
"~~/src/HOL/Library/LaTeXsugar"
begin
-
declare [[show_question_marks = false]]
-
notation (latex output)
Cons ("_::_" [78,77] 73) and
If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
@@ -25,40 +23,43 @@
cpreced ("cprec") and
cp ("cprec") and
holdents ("resources") and
- DUMMY ("\<^raw:\mbox{$\_\!\_$}>")
+ DUMMY ("\<^raw:\mbox{$\_\!\_$}>") and
+ cntP ("c\<^bsub>P\<^esub>") and
+ cntV ("c\<^bsub>V\<^esub>")
(*>*)
section {* Introduction *}
text {*
- Many real-time systems need to support threads involving priorities and
- locking of resources. Locking of resources ensures mutual exclusion
- when accessing shared data or devices that cannot be
+
+ Many real-time systems need to support threads involving priorities
+ and locking of resources. Locking of resources ensures mutual
+ exclusion when accessing shared data or devices that cannot be
preempted. Priorities allow scheduling of threads that need to
finish their work within deadlines. Unfortunately, both features
can interact in subtle ways leading to a problem, called
\emph{Priority Inversion}. Suppose three threads having priorities
$H$(igh), $M$(edium) and $L$(ow). We would expect that the thread
- $H$ blocks any other thread with lower priority and the thread itself cannot
- be blocked indefinitely by threads with lower priority. Alas, in a naive
- implementation of resource locking and priorities this property can
- be violated. For this let $L$ be in the
+ $H$ blocks any other thread with lower priority and the thread
+ itself cannot be blocked indefinitely by threads with lower
+ priority. Alas, in a naive implementation of resource locking and
+ priorities this property can be violated. For this let $L$ be in the
possession of a lock for a resource that $H$ also needs. $H$ must
therefore wait for $L$ to exit the critical section and release this
- lock. The problem is that $L$ might in turn be blocked by any
- thread with priority $M$, and so $H$ sits there potentially waiting
- indefinitely. Since $H$ is blocked by threads with lower
- priorities, the problem is called Priority Inversion. It was first
- described in \cite{Lampson80} in the context of the
- Mesa programming language designed for concurrent programming.
+ lock. The problem is that $L$ might in turn be blocked by any thread
+ with priority $M$, and so $H$ sits there potentially waiting
+ indefinitely. Since $H$ is blocked by threads with lower priorities,
+ the problem is called Priority Inversion. It was first described in
+ \cite{Lampson80} in the context of the Mesa programming language
+ designed for concurrent programming.
If the problem of Priority Inversion is ignored, real-time systems
can become unpredictable and resulting bugs can be hard to diagnose.
The classic example where this happened is the software that
- controlled the Mars Pathfinder mission in 1997 \cite{Reeves98}.
- On Earth the software run mostly without any problem, but
- once the spacecraft landed on Mars, it shut down at irregular, but frequent,
+ controlled the Mars Pathfinder mission in 1997 \cite{Reeves98}. On
+ Earth the software run mostly without any problem, but once the
+ spacecraft landed on Mars, it shut down at irregular, but frequent,
intervals leading to loss of project time as normal operation of the
craft could only resume the next day (the mission and data already
collected were fortunately not lost, because of a clever system
@@ -69,11 +70,11 @@
rectified by enabling the \emph{Priority Inheritance Protocol} (PIP)
\cite{Sha90}\footnote{Sha et al.~call it the \emph{Basic Priority
Inheritance Protocol} \cite{Sha90} and others sometimes also call it
- \emph{Priority Boosting}, \emph{Priority Donation} or \emph{Priority Lending}.}
- in the scheduling software.
+ \emph{Priority Boosting}, \emph{Priority Donation} or \emph{Priority
+ Lending}.} in the scheduling software.
- The idea behind PIP is to let the thread $L$ temporarily inherit
- the high priority from $H$ until $L$ leaves the critical section
+ The idea behind PIP is to let the thread $L$ temporarily inherit the
+ high priority from $H$ until $L$ leaves the critical section
unlocking the resource. This solves the problem of $H$ having to
wait indefinitely, because $L$ cannot be blocked by threads having
priority $M$. While a few other solutions exist for the Priority
@@ -81,21 +82,21 @@
implemented. This includes VxWorks (a proprietary real-time OS used
in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, Honda's
ASIMO robot, etc.) and ThreadX (another proprietary real-time OS
- used in nearly all HP inkjet printers \cite{ThreadX}), but also
- the POSIX 1003.1c Standard realised for
- example in libraries for FreeBSD, Solaris and Linux.
+ used in nearly all HP inkjet printers \cite{ThreadX}), but also the
+ POSIX 1003.1c Standard realised for example in libraries for
+ FreeBSD, Solaris and Linux.
- Two advantages of PIP are that it is deterministic and that increasing the priority of a thread
- can be performed dynamically by the scheduler.
- This is in contrast to \emph{Priority Ceiling}
+ Two advantages of PIP are that it is deterministic and that
+ increasing the priority of a thread can be performed dynamically by
+ the scheduler. This is in contrast to \emph{Priority Ceiling}
\cite{Sha90}, another solution to the Priority Inversion problem,
which requires static analysis of the program in order to prevent
- Priority Inversion, and also in contrast to the approach taken in the Windows NT scheduler, which avoids
- this problem by randomly boosting the priority of ready low-priority threads
- (see for instance~\cite{WINDOWSNT}).
- However, there has also been strong criticism against
- PIP. For instance, PIP cannot prevent deadlocks when lock
- dependencies are circular, and also blocking times can be
+ Priority Inversion, and also in contrast to the approach taken in
+ the Windows NT scheduler, which avoids this problem by randomly
+ boosting the priority of ready low-priority threads (see for
+ instance~\cite{WINDOWSNT}). However, there has also been strong
+ criticism against PIP. For instance, PIP cannot prevent deadlocks
+ when lock dependencies are circular, and also blocking times can be
substantial (more than just the duration of a critical section).
Though, most criticism against PIP centres around unreliable
implementations and PIP being too complicated and too inefficient.
@@ -106,18 +107,19 @@
are either incomplete (and unreliable) or surprisingly complex and intrusive.''
\end{quote}
- \noindent
- He suggests avoiding PIP altogether by designing the system so that no
- priority inversion may happen in the first place. However, such ideal designs may
- not always be achievable in practice.
+ \noindent He suggests avoiding PIP altogether by designing the
+ system so that no priority inversion may happen in the first
+ place. However, such ideal designs may not always be achievable in
+ practice.
In our opinion, there is clearly a need for investigating correct
- algorithms for PIP. A few specifications for PIP exist (in English)
- and also a few high-level descriptions of implementations (e.g.~in
- the textbooks \cite[Section 12.3.1]{Liu00} and \cite[Section 5.6.5]{Vahalia96}),
- but they help little with actual implementations. That this is a problem in
- practice is proved by an email by Baker, who wrote on 13 July 2009 on the Linux
- Kernel mailing list:
+ algorithms for PIP. A few specifications for PIP exist (in informal
+ English) and also a few high-level descriptions of implementations
+ (e.g.~in the textbooks \cite[Section 12.3.1]{Liu00} and
+ \cite[Section 5.6.5]{Vahalia96}), but they help little with actual
+ implementations. That this is a problem in practice is proved by an
+ email by Baker, who wrote on 13 July 2009 on the Linux Kernel
+ mailing list:
\begin{quote}
\it{}``I observed in the kernel code (to my disgust), the Linux PIP
@@ -127,70 +129,69 @@
wait operations.''
\end{quote}
- \noindent
- The criticism by Yodaiken, Baker and others suggests another look
- at PIP from a more abstract level (but still concrete enough
- to inform an implementation), and makes PIP a good candidate for a
- formal verification. An additional reason is that the original
+ \noindent The criticism by Yodaiken, Baker and others suggests
+ another look at PIP from a more abstract level (but still concrete
+ enough to inform an implementation), and makes PIP a good candidate
+ for a formal verification. An additional reason is that the original
specification of PIP~\cite{Sha90}, despite being informally
- ``proved'' correct, is actually \emph{flawed}.
+ ``proved'' correct, is actually \emph{flawed}.
-
Yodaiken \cite{Yodaiken02} and also Moylan et
al.~\cite{deinheritance} point to a subtlety that had been
- overlooked in the informal proof by Sha et al. They specify in
- \cite{Sha90} that after the thread (whose priority has been raised)
- completes its critical section and releases the lock, it ``{\it
- returns to its original priority level}''. This leads them to
+ overlooked in the informal proof by Sha et al. They specify PIP in
+ \cite{Sha90} so that after the thread (whose priority has been
+ raised) completes its critical section and releases the lock, it
+ ``{\it returns to its original priority level}''. This leads them to
believe that an implementation of PIP is ``{\it rather
straightforward}''~\cite{Sha90}. Unfortunately, as Yodaiken and
Moylan et al.~point out, this behaviour is too simplistic. Moylan et
- al.~write that there are ``{\it some hidden traps}''~\cite{deinheritance}. Consider the
- case where the low priority thread $L$ locks \emph{two} resources,
- and two high-priority threads $H$ and $H'$ each wait for one of
- them. If $L$ releases one resource so that $H$, say, can proceed,
- then we still have Priority Inversion with $H'$ (which waits for the
- other resource). The correct behaviour for $L$ is to switch to the
- highest remaining priority of the threads that it blocks.
- A similar
- error is made in the textbook \cite[Section 2.3.1]{book} which
- specifies for a process that inherited a higher priority and exits a
- critical section ``{\it it resumes the priority it had at the point
- of entry into the critical section}''. This error can also be
- found in the more recent textbook \cite[Page 119]{Laplante11} where the
- authors state: ``{\it when [the task] exits the critical section that caused
+ al.~write that there are ``{\it some hidden
+ traps}''~\cite{deinheritance}. Consider the case where the low
+ priority thread $L$ locks \emph{two} resources, and two
+ high-priority threads $H$ and $H'$ each wait for one of them. If
+ $L$ releases one resource so that $H$, say, can proceed, then we
+ still have Priority Inversion with $H'$ (which waits for the other
+ resource). The correct behaviour for $L$ is to switch to the highest
+ remaining priority of the threads that it blocks. A similar error
+ is made in the textbook \cite[Section 2.3.1]{book} which specifies
+ for a process that inherited a higher priority and exits a critical
+ section ``{\it it resumes the priority it had at the point of entry
+ into the critical section}''. This error can also be found in the
+ more recent textbook \cite[Page 119]{Laplante11} where the authors
+ state: ``{\it when [the task] exits the critical section that caused
the block, it reverts to the priority it had when it entered that
section}''. The textbook \cite[Page 286]{Liu00} contains a simlar
- flawed specification and even goes on to develop pseudo-code based on this
- flawed specification. Accordingly, the operating system primitives
- for inheritance and restoration of priorities in \cite{Liu00} depend on
- maintaining a data structure called \emph{inheritance log}. This log
- is maintained for every thread and broadly specified as containing ``{\it
- [h]istorical information on how the thread inherited its current
- priority}'' \cite[Page 527]{Liu00}. Unfortunately, the important
- information about actually
- computing the priority to be restored solely from this log is not explained in
- \cite{Liu00} but left as an ``{\it excercise}'' to the reader.
- Of course, a correct version of PIP does not need to maintain
- this (potentially expensive) data structure at all. Surprisingly
- also the widely read and frequently updated textbook \cite{Silberschatz13} gives
- the wrong specification. For example on Page 254 the
- authors write: ``{\it Upon releasing the lock, the [low-priority] thread
- will revert to its original priority.}'' The same error is also repeated
- later in this textbook.
+ flawed specification and even goes on to develop pseudo-code based
+ on this flawed specification. Accordingly, the operating system
+ primitives for inheritance and restoration of priorities in
+ \cite{Liu00} depend on maintaining a data structure called
+ \emph{inheritance log}. This log is maintained for every thread and
+ broadly specified as containing ``{\it [h]istorical information on
+ how the thread inherited its current priority}'' \cite[Page
+ 527]{Liu00}. Unfortunately, the important information about actually
+ computing the priority to be restored solely from this log is not
+ explained in \cite{Liu00} but left as an ``{\it excercise}'' to the
+ reader. Of course, a correct version of PIP does not need to
+ maintain this (potentially expensive) data structure at
+ all. Surprisingly also the widely read and frequently updated
+ textbook \cite{Silberschatz13} gives the wrong specification. For
+ example on Page 254 the authors write: ``{\it Upon releasing the
+ lock, the [low-priority] thread will revert to its original
+ priority.}'' The same error is also repeated later in this textbook.
- While \cite{Laplante11,Liu00,book,Sha90,Silberschatz13} are the only formal publications we have
- found that specify the incorrect behaviour, it seems also many
- informal descriptions of PIP overlook the possibility that another
- high-priority might wait for a low-priority process to finish.
- A notable exception is the texbook \cite{buttazzo}, which gives the correct
- behaviour of resetting the priority of a thread to the highest remaining priority of the
- threads it blocks. This textbook also gives an informal proof for
- the correctness of PIP in the style of Sha et al. Unfortunately, this informal
- proof is too vague to be useful for formalising the correctness of PIP
- and the specification leaves out nearly all details in order
- to implement PIP efficiently.\medskip\smallskip
+ While \cite{Laplante11,Liu00,book,Sha90,Silberschatz13} are the only
+ formal publications we have found that specify the incorrect
+ behaviour, it seems also many informal descriptions of PIP overlook
+ the possibility that another high-priority might wait for a
+ low-priority process to finish. A notable exception is the texbook
+ \cite{buttazzo}, which gives the correct behaviour of resetting the
+ priority of a thread to the highest remaining priority of the
+ threads it blocks. This textbook also gives an informal proof for
+ the correctness of PIP in the style of Sha et al. Unfortunately,
+ this informal proof is too vague to be useful for formalising the
+ correctness of PIP and the specification leaves out nearly all
+ details in order to implement PIP efficiently.\medskip\smallskip
%
%The advantage of formalising the
%correctness of a high-level specification of PIP in a theorem prover
@@ -198,27 +199,29 @@
%informal reasoning (since we have to analyse all possible behaviours
%of threads, i.e.~\emph{traces}, that could possibly happen).
- \noindent
- {\bf Contributions:} There have been earlier formal investigations
- into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model
- checking techniques. This paper presents a formalised and
- mechanically checked proof for the correctness of PIP. For this we
- needed to design a new correctness criterion for PIP. In contrast to model checking, our
- formalisation provides insight into why PIP is correct and allows us
- to prove stronger properties that, as we will show, can help with an
- efficient implementation of PIP in the educational PINTOS operating
- system \cite{PINTOS}. For example, we found by ``playing'' with the
- formalisation that the choice of the next thread to take over a lock
- when a resource is released is irrelevant for PIP being correct---a
- fact that has not been mentioned in the literature and not been used
- in the reference implementation of PIP in PINTOS. This fact, however, is important
- for an efficient implementation of PIP, because we can give the lock
- to the thread with the highest priority so that it terminates more
- quickly. We were also being able to generalise the scheduler of Sha
- et al.~\cite{Sha90} to the practically relevant case where critical
- sections can overlap; see Figure~\ref{overlap} \emph{a)} below for an example of
- this restriction. %In the existing literature there is no
- %proof and also no proving method that cover this generalised case.
+ \noindent {\bf Contributions:} There have been earlier formal
+ investigations into PIP \cite{Faria08,Jahier09,Wellings07}, but they
+ employ model checking techniques. This paper presents a formalised
+ and mechanically checked proof for the correctness of PIP. For this
+ we needed to design a new correctness criterion for PIP. In contrast
+ to model checking, our formalisation provides insight into why PIP
+ is correct and allows us to prove stronger properties that, as we
+ will show, can help with an efficient implementation of PIP. We
+ illustrate this with an implementation of PIP in the educational
+ PINTOS operating system \cite{PINTOS}. For example, we found by
+ ``playing'' with the formalisation that the choice of the next
+ thread to take over a lock when a resource is released is irrelevant
+ for PIP being correct---a fact that has not been mentioned in the
+ literature and not been used in the reference implementation of PIP
+ in PINTOS. This fact, however, is important for an efficient
+ implementation of PIP, because we can give the lock to the thread
+ with the highest priority so that it terminates more quickly. We
+ were also being able to generalise the scheduler of Sha et
+ al.~\cite{Sha90} to the practically relevant case where critical
+ sections can overlap; see Figure~\ref{overlap} \emph{a)} below for
+ an example of this restriction. In the existing literature there is
+ no proof and also no proving method that cover this generalised
+ case.
\begin{figure}
\begin{center}
@@ -384,6 +387,18 @@
tasks involved in the inheritance process and thus minimises the number
of potentially expensive thread-switches.
+ We will also need counters for @{term P} and @{term V} events of a thread @{term th}
+ in a state @{term s}. This can be straightforwardly defined in Isabelle as
+
+ \begin{isabelle}\ \ \ \ \ %%%
+ \mbox{\begin{tabular}{@ {}l}
+ @{thm cntP_def}\\
+ @{thm cntV_def}
+ \end{tabular}}
+ \end{isabelle}
+
+ \noindent using the predefined function @{const count} for lists.
+
Next, we introduce the concept of \emph{waiting queues}. They are
lists of threads associated with every resource. The first thread in
this list (i.e.~the head, or short @{term hd}) is chosen to be the one
@@ -945,8 +960,39 @@
From these two lemmas we can see the correctness of PIP, which is
that: the blockage of th is reasonable and under control.
+ Lemmas we want to describe:
+
+ \begin{lemma}
+ @{thm eq_pv_persist}
+ \end{lemma}
+
+ \begin{lemma}
+ @{thm eq_pv_blocked}
+ \end{lemma}
+
+ \begin{lemma}
+ @{thm runing_cntP_cntV_inv}
+ \end{lemma}
+
+ \noindent
+ Remember we do not have the well-nestedness restriction in our
+ proof, which means the difference between the counters @{const cntV}
+ and @{const cntP} can be larger than @{term 1}.
+
+ \begin{lemma}
+ @{thm runing_inversion}
+ \end{lemma}
+
+
+ \begin{lemma}
+ @{thm th_blockedE}
+ \end{lemma}
+
\subsection*{END OUTLINE}
+
+
+
In what follows we will describe properties of PIP that allow us to prove
Theorem~\ref{mainthm} and, when instructive, briefly describe our argument.
It is relatively easy to see that:
@@ -959,7 +1005,7 @@
\end{isabelle}
\noindent
- The second property is by induction of @{term vt}. The next three
+ The second property is by induction on @{term vt}. The next three
properties are:
\begin{isabelle}\ \ \ \ \ %%%
--- a/Journal/document/root.tex Sat Jan 16 10:59:03 2016 +0800
+++ b/Journal/document/root.tex Sat Jan 16 11:02:17 2016 +0800
@@ -53,7 +53,9 @@
\footnotetext[1]{This paper is a revised, corrected and expanded version of \cite{ZhangUrbanWu12}.
Compared with that paper we give an actual implementation of our formalised scheduling
algorithm in C and the operating system PINTOS. Our implementation follows closely all results
-we proved about optimisations of the Priority Inheritance Protocol.}
+we proved about optimisations of the Priority Inheritance Protocol. We are giving in this paper
+more details about the proof and also surveying
+the existing literature in more depth.}
\renewcommand{\thefootnote}{\arabic{footnote}}
\title{Priority Inheritance Protocol Proved Correct}
@@ -63,28 +65,28 @@
\maketitle
\begin{abstract}
-In real-time systems with threads, resource locking and
-priority sched\-uling, one faces the problem of Priority
-Inversion. This problem can make the behaviour of threads
-unpredictable and the resulting bugs can be hard to find. The
-Priority Inheritance Protocol is one solution implemented in many
-systems for solving this problem, but the correctness of this solution
-has never been formally verified in a theorem prover. As already
-pointed out in the literature, the original informal investigation of
-the Property Inheritance Protocol presents a correctness ``proof'' for
-an \emph{incorrect} algorithm. In this paper we fix the problem of
-this proof by making all notions precise and implementing a variant of
-a solution proposed earlier. We also generalise the original informal proof to the
-practically relevant case where critical sections can
-overlap. Our formalisation in Isabelle/HOL not just
-uncovers facts not mentioned in the literature, but also helps with
-implementing efficiently this protocol. Earlier correct implementations
-were criticised as too inefficient. Our formalisation is based on
-Paulson's inductive approach to verifying protocols; our implementation
-builds on top of the small PINTOS operating system used for teaching.\medskip
+In real-time systems with threads, resource locking and priority
+sched\-uling, one faces the problem of Priority Inversion. This
+problem can make the behaviour of threads unpredictable and the
+resulting bugs can be hard to find. The Priority Inheritance Protocol
+is one solution implemented in many systems for solving this problem,
+but the correctness of this solution has never been formally verified
+in a theorem prover. As already pointed out in the literature, the
+original informal investigation of the Property Inheritance Protocol
+presents a correctness ``proof'' for an \emph{incorrect} algorithm. In
+this paper we fix the problem of this proof by making all notions
+precise and implementing a variant of a solution proposed earlier. We
+also generalise the scheduling problem to the practically relevant case where
+critical sections can overlap. Our formalisation in Isabelle/HOL not
+just uncovers facts not mentioned in the literature, but also helps
+with implementing efficiently this protocol. Earlier correct
+implementations were criticised as too inefficient. Our formalisation
+is based on Paulson's inductive approach to verifying protocols; our
+implementation builds on top of the small PINTOS operating system used
+for teaching.\medskip
-%{\bf Keywords:} Priority Inheritance Protocol, formal correctness proof,
-%real-time systems, Isabelle/HOL
+{\bf Keywords:} Priority Inheritance Protocol, formal correctness proof,
+real-time systems, Isabelle/HOL
\end{abstract}
\input{session}
--- a/Moment.thy Sat Jan 16 10:59:03 2016 +0800
+++ b/Moment.thy Sat Jan 16 11:02:17 2016 +0800
@@ -8,20 +8,6 @@
value "moment 3 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9::int]"
value "moment 2 [5, 4, 3, 2, 1, 0::int]"
-(*
-lemma length_moment_le:
- assumes le_k: "k \<le> length s"
- shows "length (moment k s) = k"
-using le_k unfolding moment_def by auto
-*)
-
-(*
-lemma length_moment_ge:
- assumes le_k: "length s \<le> k"
- shows "length (moment k s) = (length s)"
-using assms unfolding moment_def by simp
-*)
-
lemma moment_app [simp]:
assumes ile: "i \<le> length s"
shows "moment i (s' @ s) = moment i s"
Binary file journal.pdf has changed