--- a/PIPDefs.thy Sat Feb 13 17:18:51 2016 +0800
+++ b/PIPDefs.thy Mon Mar 21 14:07:37 2016 +0000
@@ -163,80 +163,94 @@
all threads in the waiting queue are considered as waiting for the resource.
*}
+(*
consts
holding :: "'b \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> bool"
waiting :: "'b \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> bool"
RAG :: "'b \<Rightarrow> (node \<times> node) set"
dependants :: "'b \<Rightarrow> thread \<Rightarrow> thread set"
+*)
-defs (overloaded)
+definition
-- {*
\begin{minipage}{0.9\textwidth}
- This meaning of @{text "wq"} is reflected in the following definition of @{text "holding wq th cs"},
- where @{text "holding wq th cs"} means thread @{text "th"} is holding the critical
- resource @{text "cs"}. This decision is based on @{text "wq"}.
+ This meaning of @{text "wq"} is reflected in the following definition of
+ @{text "holding wq th cs"}, where @{text "holding wq th cs"} means thread
+ @{text "th"} is holding the critical resource @{text "cs"}. This decision
+ is based on @{text "wq"}.
+ \end{minipage}
+ *}
+
+ cs_holding_raw:
+ "holding_raw wq thread cs \<equiv> (thread \<in> set (wq cs) \<and> thread = hd (wq cs))"
+
+
+definition
+ -- {*
+ \begin{minipage}{0.9\textwidth}
+ In accordance with the definition of @{text "holding wq th cs"}, a thread
+ @{text "th"} is considered waiting for @{text "cs"} if it is in the {\em
+ waiting queue} of critical resource @{text "cs"}, but not at the head.
+ This is reflected in the definition of @{text "waiting wq th cs"} as
+ follows:
\end{minipage}
*}
- cs_holding_def:
- "holding wq thread cs \<equiv> (thread \<in> set (wq cs) \<and> thread = hd (wq cs))"
+ cs_waiting_raw:
+ "waiting_raw wq thread cs \<equiv> (thread \<in> set (wq cs) \<and> thread \<noteq> hd (wq cs))"
+
+definition
-- {*
\begin{minipage}{0.9\textwidth}
- In accordance with the definition of @{text "holding wq th cs"},
- a thread @{text "th"} is considered waiting for @{text "cs"} if
- it is in the {\em waiting queue} of critical resource @{text "cs"}, but not at the head.
- This is reflected in the definition of @{text "waiting wq th cs"} as follows:
- \end{minipage}
+ @{text "RAG wq"} generates RAG (a binary relations on @{text "node"}) out
+ of waiting queues of the system (represented by the @{text "wq"}
+ argument): \end{minipage}
*}
- cs_waiting_def:
- "waiting wq thread cs \<equiv> (thread \<in> set (wq cs) \<and> thread \<noteq> hd (wq cs))"
- -- {*
- \begin{minipage}{0.9\textwidth}
- @{text "RAG wq"} generates RAG (a binary relations on @{text "node"})
- out of waiting queues of the system (represented by the @{text "wq"} argument):
- \end{minipage}
- *}
- cs_RAG_def:
- "RAG (wq::cs \<Rightarrow> thread list) \<equiv>
- {(Th th, Cs cs) | th cs. waiting wq th cs} \<union> {(Cs cs, Th th) | cs th. holding wq th cs}"
+
+ cs_RAG_raw:
+ "RAG_raw (wq::cs \<Rightarrow> thread list) \<equiv>
+ {(Th th, Cs cs) | th cs. waiting_raw wq th cs} \<union> {(Cs cs, Th th) | cs th. holding_raw wq th cs}"
+
+definition
-- {*
\begin{minipage}{0.9\textwidth}
- The following @{text "dependants wq th"} represents the set of threads which are RAGing on
- thread @{text "th"} in Resource Allocation Graph @{text "RAG wq"}.
- Here, "RAGing" means waiting directly or indirectly on the critical resource.
+ The following @{text "dependants wq th"} represents the set of threads
+ which are RAGing on thread @{text "th"} in Resource Allocation Graph
+ @{text "RAG wq"}. Here, "RAGing" means waiting directly or indirectly on
+ the critical resource.
\end{minipage}
*}
+
cs_dependants_def:
- "dependants (wq::cs \<Rightarrow> thread list) th \<equiv> {th' . (Th th', Th th) \<in> (RAG wq)^+}"
-
+ "dependants_raw (wq::cs \<Rightarrow> thread list) th \<equiv> {th' . (Th th', Th th) \<in> (RAG_raw wq)^+}"
-text {* \noindent
- The following
- @{text "cpreced s th"} gives the {\em current precedence} of thread @{text "th"} under
- state @{text "s"}. The definition of @{text "cpreced"} reflects the basic idea of
- Priority Inheritance that the {\em current precedence} of a thread is the precedence
- inherited from the maximum of all its dependants, i.e. the threads which are waiting
- directly or indirectly waiting for some resources from it. If no such thread exits,
- @{text "th"}'s {\em current precedence} equals its original precedence, i.e.
- @{text "preced th s"}.
- *}
+text {*
+ \noindent The following @{text "cpreced s th"} gives the {\em current
+ precedence} of thread @{text "th"} under state @{text "s"}. The definition
+ of @{text "cpreced"} reflects the basic idea of Priority Inheritance that
+ the {\em current precedence} of a thread is the precedence inherited from
+ the maximum of all its dependants, i.e. the threads which are waiting
+ directly or indirectly waiting for some resources from it. If no such
+ thread exits, @{text "th"}'s {\em current precedence} equals its original
+ precedence, i.e. @{text "preced th s"}.
+*}
definition cpreced :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread \<Rightarrow> precedence"
- where "cpreced wq s = (\<lambda>th. Max ((\<lambda>th'. preced th' s) ` ({th} \<union> dependants wq th)))"
+ where "cpreced wq s = (\<lambda>th. Max ((\<lambda>th'. preced th' s) ` ({th} \<union> dependants_raw wq th)))"
text {*
- Notice that the current precedence (@{text "cpreced"}) of one thread @{text "th"} can be boosted
- (becoming larger than its own precedence) by those threads in
- the @{text "dependants wq th"}-set. If one thread get boosted, we say
- it inherits the priority (or, more precisely, the precedence) of
- its dependants. This is how the word "Inheritance" in
+ Notice that the current precedence (@{text "cpreced"}) of one thread
+ @{text "th"} can be boosted (becoming larger than its own precedence) by
+ those threads in the @{text "dependants wq th"}-set. If one thread get
+ boosted, we say it inherits the priority (or, more precisely, the
+ precedence) of its dependants. This is how the word "Inheritance" in
Priority Inheritance Protocol comes.
*}
(*<*)
lemma
cpreced_def2:
- "cpreced wq s th \<equiv> Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependants wq th})"
+ "cpreced wq s th \<equiv> Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependants_raw wq th})"
unfolding cpreced_def image_def
apply(rule eq_reflection)
apply(rule_tac f="Max" in arg_cong)
@@ -244,49 +258,56 @@
(*>*)
-text {* \noindent
- Assuming @{text "qs"} be the waiting queue of a critical resource,
- the following abbreviation "release qs" is the waiting queue after the thread
- holding the resource (which is thread at the head of @{text "qs"}) released
- the resource:
+text {*
+
+ \noindent Assuming @{text "qs"} be the waiting queue of a critical
+ resource, the following abbreviation "release qs" is the waiting queue
+ after the thread holding the resource (which is thread at the head of
+ @{text "qs"}) released the resource:
*}
+
abbreviation
"release qs \<equiv> case qs of
[] => []
| (_#qs') => (SOME q. distinct q \<and> set q = set qs')"
-text {* \noindent
- It can be seen from the definition that the thread at the head of @{text "qs"} is removed
- from the return value, and the value @{term "q"} is an reordering of @{text "qs'"}, the
- tail of @{text "qs"}. Through this reordering, one of the waiting threads (those in @{text "qs'"} }
- is chosen nondeterministically to be the head of the new queue @{text "q"}.
- Therefore, this thread is the one who takes over the resource. This is a little better different
- from common sense that the thread who comes the earliest should take over.
- The intention of this definition is to show that the choice of which thread to take over the
- release resource does not affect the correctness of the PIP protocol.
+
+text {*
+ \noindent It can be seen from the definition that the thread at the head
+ of @{text "qs"} is removed from the return value, and the value @{term
+ "q"} is an reordering of @{text "qs'"}, the tail of @{text "qs"}. Through
+ this reordering, one of the waiting threads (those in @{text "qs'"} } is
+ chosen nondeterministically to be the head of the new queue @{text "q"}.
+ Therefore, this thread is the one who takes over the resource. This is a
+ little better different from common sense that the thread who comes the
+ earliest should take over. The intention of this definition is to show
+ that the choice of which thread to take over the release resource does not
+ affect the correctness of the PIP protocol.
*}
text {*
- The data structure used by the operating system for scheduling is referred to as
- {\em schedule state}. It is represented as a record consisting of
- a function assigning waiting queue to resources
- (to be used as the @{text "wq"} argument in @{text "holding"}, @{text "waiting"}
- and @{text "RAG"}, etc) and a function assigning precedence to threads:
+ The data structure used by the operating system for scheduling is referred
+ to as {\em schedule state}. It is represented as a record consisting of a
+ function assigning waiting queue to resources (to be used as the @{text
+ "wq"} argument in @{text "holding"}, @{text "waiting"} and @{text "RAG"},
+ etc) and a function assigning precedence to threads:
*}
record schedule_state =
wq_fun :: "cs \<Rightarrow> thread list" -- {* The function assigning waiting queue. *}
cprec_fun :: "thread \<Rightarrow> precedence" -- {* The function assigning precedence. *}
-text {* \noindent
- The following two abbreviations (@{text "all_unlocked"} and @{text "initial_cprec"})
- are used to set the initial values of the @{text "wq_fun"} @{text "cprec_fun"} fields
- respectively of the @{text "schedule_state"} record by the following function @{text "sch"},
- which is used to calculate the system's {\em schedule state}.
+text {*
+ \noindent The following two abbreviations (@{text "all_unlocked"} and
+ @{text "initial_cprec"}) are used to set the initial values of the @{text
+ "wq_fun"} @{text "cprec_fun"} fields respectively of the @{text
+ "schedule_state"} record by the following function @{text "sch"}, which is
+ used to calculate the system's {\em schedule state}.
- Since there is no thread at the very beginning to make request, all critical resources
- are free (or unlocked). This status is represented by the abbreviation
- @{text "all_unlocked"}.
- *}
+ Since there is no thread at the very beginning to make request, all
+ critical resources are free (or unlocked). This status is represented by
+ the abbreviation @{text "all_unlocked"}.
+*}
+
abbreviation
"all_unlocked \<equiv> \<lambda>_::cs. ([]::thread list)"
@@ -371,7 +392,7 @@
lemma cpreced_initial:
"cpreced (\<lambda> cs. []) [] = (\<lambda>_. (Prc 0 0))"
apply(simp add: cpreced_def)
-apply(simp add: cs_dependants_def cs_RAG_def cs_waiting_def cs_holding_def)
+apply(simp add: cs_dependants_def cs_RAG_raw cs_waiting_raw cs_holding_raw)
apply(simp add: preced_def)
done
@@ -413,65 +434,79 @@
fictitious {\em waiting queue function}
@{text "wq"}, but on system state @{text "s"}.
*}
-defs (overloaded)
+
+
+definition
s_holding_abv:
- "holding (s::state) \<equiv> holding (wq_fun (schs s))"
+ "holding (s::state) \<equiv> holding_raw (wq_fun (schs s))"
+
+definition
s_waiting_abv:
- "waiting (s::state) \<equiv> waiting (wq_fun (schs s))"
+ "waiting (s::state) \<equiv> waiting_raw (wq_fun (schs s))"
+
+definition
s_RAG_abv:
- "RAG (s::state) \<equiv> RAG (wq_fun (schs s))"
+ "RAG (s::state) \<equiv> RAG_raw (wq_fun (schs s))"
+
+definition
s_dependants_abv:
- "dependants (s::state) \<equiv> dependants (wq_fun (schs s))"
+ "dependants (s::state) \<equiv> dependants_raw (wq_fun (schs s))"
text {*
The following lemma can be proved easily, and the meaning is obvious.
*}
+
lemma
s_holding_def:
"holding (s::state) th cs \<equiv> (th \<in> set (wq_fun (schs s) cs) \<and> th = hd (wq_fun (schs s) cs))"
- by (auto simp:s_holding_abv wq_def cs_holding_def)
+ by (auto simp:s_holding_abv wq_def cs_holding_raw)
lemma s_waiting_def:
"waiting (s::state) th cs \<equiv> (th \<in> set (wq_fun (schs s) cs) \<and> th \<noteq> hd (wq_fun (schs s) cs))"
- by (auto simp:s_waiting_abv wq_def cs_waiting_def)
+ by (auto simp:s_waiting_abv wq_def cs_waiting_raw)
lemma s_RAG_def:
"RAG (s::state) =
- {(Th th, Cs cs) | th cs. waiting (wq s) th cs} \<union> {(Cs cs, Th th) | cs th. holding (wq s) th cs}"
- by (auto simp:s_RAG_abv wq_def cs_RAG_def)
+ {(Th th, Cs cs) | th cs. waiting_raw (wq s) th cs} \<union> {(Cs cs, Th th) | cs th. holding_raw (wq s) th cs}"
+ by (auto simp:s_RAG_abv wq_def cs_RAG_raw)
lemma
s_dependants_def:
- "dependants (s::state) th \<equiv> {th' . (Th th', Th th) \<in> (RAG (wq s))^+}"
+ "dependants (s::state) th \<equiv> {th' . (Th th', Th th) \<in> (RAG_raw (wq s))^+}"
by (auto simp:s_dependants_abv wq_def cs_dependants_def)
text {*
- The following function @{text "readys"} calculates the set of ready threads. A thread is {\em ready}
- for running if it is a live thread and it is not waiting for any critical resource.
+ The following function @{text "readys"} calculates the set of ready
+ threads. A thread is {\em ready} for running if it is a live thread and it
+ is not waiting for any critical resource.
*}
+
definition readys :: "state \<Rightarrow> thread set"
where "readys s \<equiv> {th . th \<in> threads s \<and> (\<forall> cs. \<not> waiting s th cs)}"
-text {* \noindent
- The following function @{text "runing"} calculates the set of running thread, which is the ready
- thread with the highest precedence.
+text {*
+ \noindent The following function @{text "runing"} calculates the set of
+ running thread, which is the ready thread with the highest precedence.
*}
+
definition runing :: "state \<Rightarrow> thread set"
where "runing s \<equiv> {th . th \<in> readys s \<and> cp s th = Max ((cp s) ` (readys s))}"
-text {* \noindent
- Notice that the definition of @{text "running"} reflects the preemptive scheduling strategy,
- because, if the @{text "running"}-thread (the one in @{text "runing"} set)
- lowered its precedence by resetting its own priority to a lower
- one, it will lose its status of being the max in @{text "ready"}-set and be superseded.
+text {*
+ \noindent Notice that the definition of @{text "running"} reflects the
+ preemptive scheduling strategy, because, if the @{text "running"}-thread
+ (the one in @{text "runing"} set) lowered its precedence by resetting its
+ own priority to a lower one, it will lose its status of being the max in
+ @{text "ready"}-set and be superseded.
*}
-text {* \noindent
- The following function @{text "holdents s th"} returns the set of resources held by thread
- @{text "th"} in state @{text "s"}.
- *}
-definition holdents :: "state \<Rightarrow> thread \<Rightarrow> cs set"
+text {*
+ \noindent The following function @{text "holdents s th"} returns the set
+ of resources held by thread @{text "th"} in state @{text "s"}. *}
+
+
+definition holdents :: "state \<Rightarrow> thread \<Rightarrow> cs set"
where "holdents s th \<equiv> {cs . holding s th cs}"
lemma holdents_test:
@@ -659,9 +694,10 @@
definition "tRAG s = wRAG s O hRAG s"
text {* The following lemma splits @{term "RAG"} graph into the above two sub-graphs. *}
+
lemma RAG_split: "RAG s = (wRAG s \<union> hRAG s)"
by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv
- s_holding_abv cs_RAG_def, auto)
+ s_holding_abv cs_RAG_raw, auto)
lemma tRAG_alt_def:
"tRAG s = {(Th th1, Th th2) | th1 th2.