pip: comparison PrioGDef.thy

equal deleted inserted replaced

-:313acffe63b6
+:92f61f6a0fe7
 *}
 consts
 holding :: "'b \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> bool"
 waiting :: "'b \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> bool"
-depend :: "'b \<Rightarrow> (node \<times> node) set"
+RAG :: "'b \<Rightarrow> (node \<times> node) set"
 dependants :: "'b \<Rightarrow> thread \<Rightarrow> thread set"
 text {*
 \noindent
 In the definition of the following several functions, it is supposed that
 *}
 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 "depend wq"} represents the Resource Allocation Graph of the system under the waiting
+@{text "RAG wq"} represents the Resource Allocation Graph of the system under the waiting
 queue function @{text "wq"}.
 \end{minipage}
 *}
-cs_depend_def:
+cs_RAG_def:
-"depend (wq::cs \<Rightarrow> thread list) \<equiv>
+"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}"
 -- {*
 \begin{minipage}{0.9\textwidth}
-The following @{text "dependants wq th"} represents the set of threads which are depending on
+The following @{text "dependants wq th"} represents the set of threads which are RAGing on
-thread @{text "th"} in Resource Allocation Graph @{text "depend wq"}:
+thread @{text "th"} in Resource Allocation Graph @{text "RAG wq"}:
 \end{minipage}
 *}
 cs_dependants_def:
-"dependants (wq::cs \<Rightarrow> thread list) th \<equiv> {th' . (Th th', Th th) \<in> (depend wq)^+}"
+"dependants (wq::cs \<Rightarrow> thread list) th \<equiv> {th' . (Th th', Th th) \<in> (RAG wq)^+}"
 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
 thread in waiting to take over the released resource @{text "cs"}. In our representation,
 this amounts to rearrange elements in waiting queue, so that one of them is put at the head.
 \item For other happening event, the schedule state just does not change.
 \end{enumerate}
 \item @{text "ncp"} is new precedence function, it is calculated from the newly updated waiting queue
-function. The dependency of precedence function on waiting queue function is the reason to
+function. The RAGency of precedence function on waiting queue function is the reason to
 put them in the same record so that they can evolve together.
 \end{enumerate}
 \end{minipage}
 *}
 "schs (Create th prio # s) =
 (|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|))"
 lemma cpreced_initial:
 "cpreced (\<lambda> cs. []) [] = (\<lambda>_. (Prc 0 0))"
 apply(simp add: cpreced_def)
-apply(simp add: cs_dependants_def cs_depend_def cs_waiting_def cs_holding_def)
+apply(simp add: cs_dependants_def cs_RAG_def cs_waiting_def cs_holding_def)
 apply(simp add: preced_def)
 done
 lemma sch_old_def:
 "schs (e#s) = (let ps = schs s in
 *}
 definition cp :: "state \<Rightarrow> thread \<Rightarrow> precedence"
 where "cp s \<equiv> cprec_fun (schs s)"
 text {* \noindent
-Functions @{text "holding"}, @{text "waiting"}, @{text "depend"} and
+Functions @{text "holding"}, @{text "waiting"}, @{text "RAG"} and
 @{text "dependants"} still have the
-same meaning, but redefined so that they no longer depend on the
+same meaning, but redefined so that they no longer RAG on the
 fictitious {\em waiting queue function}
 @{text "wq"}, but on system state @{text "s"}.
 *}
 defs (overloaded)
 s_holding_abv:
 "holding (s::state) \<equiv> holding (wq_fun (schs s))"
 s_waiting_abv:
 "waiting (s::state) \<equiv> waiting (wq_fun (schs s))"
-s_depend_abv:
+s_RAG_abv:
-"depend (s::state) \<equiv> depend (wq_fun (schs s))"
+"RAG (s::state) \<equiv> RAG (wq_fun (schs s))"
 s_dependants_abv:
 "dependants (s::state) \<equiv> dependants (wq_fun (schs s))"
 text {*
 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)
-lemma s_depend_def:
+lemma s_RAG_def:
-"depend (s::state) =
+"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_depend_abv wq_def cs_depend_def)
+by (auto simp:s_RAG_abv wq_def cs_RAG_def)
 lemma
 s_dependants_def:
-"dependants (s::state) th \<equiv> {th' . (Th th', Th th) \<in> (depend (wq s))^+}"
+"dependants (s::state) th \<equiv> {th' . (Th th', Th th) \<in> (RAG (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.
 *}
 definition holdents :: "state \<Rightarrow> thread \<Rightarrow> cs set"
 where "holdents s th \<equiv> {cs . holding s th cs}"
 lemma holdents_test:
-"holdents s th = {cs . (Cs cs, Th th) \<in> depend s}"
+"holdents s th = {cs . (Cs cs, Th th) \<in> RAG s}"
 unfolding holdents_def
-unfolding s_depend_def
+unfolding s_RAG_def
 unfolding s_holding_abv
 unfolding wq_def
 by (simp)
 text {* \noindent
 the request does not form a loop in the current RAG. The latter condition
 is set up to avoid deadlock. The condition also reflects our assumption all threads are
 carefully programmed so that deadlock can not happen:
 \end{minipage}
 *}
-thread_P: "\<lbrakk>thread \<in> runing s;  (Cs cs, Th thread)  \<notin> (depend s)^+\<rbrakk> \<Longrightarrow>
+thread_P: "\<lbrakk>thread \<in> runing s;  (Cs cs, Th thread)  \<notin> (RAG s)^+\<rbrakk> \<Longrightarrow>
 step s (P thread cs)" |
 -- {*
 \begin{minipage}{0.9\textwidth}
 A thread can release a critical resource @{text "cs"}
 if it is running and holding that resource:

changeset 35	92f61f6a0fe7
parent 33	9b9f2117561f
child 48	c0f14399c12f