# HG changeset patch
# User zhang
# Date 1327672202 0
# Node ID 24199eb2c4230d0622f4d9cbc5641c17c48890ea
# Parent  f1e6071a4613c93bc25c838d98791013525aae02
Newer version.

diff -r f1e6071a4613 -r 24199eb2c423 prio/ExtGG.thy
--- a/prio/ExtGG.thy	Tue Jan 24 00:34:52 2012 +0000
+++ b/prio/ExtGG.thy	Fri Jan 27 13:50:02 2012 +0000
@@ -32,7 +32,6 @@
   assumes vt_s: "vt step s"
   and threads_s: "th \<in> threads s"
   and highest: "preced th s = Max ((cp s)`threads s)"
-  and nh: "preced th s' \<noteq> Max ((cp s)`threads s')"
   and preced_th: "preced th s = Prc prio tm"
 
 context highest_gen
@@ -119,8 +118,6 @@
 context extend_highest_gen
 begin
 
-thm extend_highest_gen.axioms
-
 lemma 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])
@@ -164,7 +161,7 @@
 qed
 
 lemma th_kept: "th \<in> threads (t @ s) \<and> 
-        preced th (t@s) = preced th s" (is "?Q t")
+                 preced th (t@s) = preced th s" (is "?Q t")
 proof -
   show ?thesis
   proof(induct rule:ind)
@@ -521,7 +518,7 @@
 lemma th_cp_preced: "cp (t@s) th = preced th s"
   by (fold max_kept, unfold th_cp_max_preced, simp)
 
-lemma preced_less':
+lemma preced_less:
   fixes th'
   assumes th'_in: "th' \<in> threads s"
   and neq_th': "th' \<noteq> th"
diff -r f1e6071a4613 -r 24199eb2c423 prio/IsaMakefile
--- a/prio/IsaMakefile	Tue Jan 24 00:34:52 2012 +0000
+++ b/prio/IsaMakefile	Fri Jan 27 13:50:02 2012 +0000
@@ -18,7 +18,7 @@
 
 session: ./ROOT.ML ./*.thy
 	@$(USEDIR) -b -D generated -f ROOT.ML HOL Prio
-
+	
 paper: Paper/ROOT.ML \
        Paper/*.thy 
 	@$(USEDIR) -D generated -f ROOT.ML Prio Paper
diff -r f1e6071a4613 -r 24199eb2c423 prio/Paper/Paper.thy
--- a/prio/Paper/Paper.thy	Tue Jan 24 00:34:52 2012 +0000
+++ b/prio/Paper/Paper.thy	Fri Jan 27 13:50:02 2012 +0000
@@ -1,6 +1,6 @@
 (*<*)
 theory Paper
-imports CpsG ExtGG
+imports CpsG ExtGG LaTeXsugar
 begin
 (*>*)
 
@@ -113,11 +113,260 @@
 *}
 
 section {* General properties of Priority Inheritance \label{general} *}
+(*<*)
+ML {*
+  val () = show_question_marks_default := false;
+*}
+(*>*)
+
+text {*
+  The following are several very basic prioprites:
+  \begin{enumerate}
+  \item All runing threads must be ready (@{text "runing_ready"}):
+          @{thm[display] "runing_ready"}  
+  \item All ready threads must be living (@{text "readys_threads"}):
+          @{thm[display] "readys_threads"} 
+  \item There are finite many living threads at any moment (@{text "finite_threads"}):
+          @{thm[display] "finite_threads"} 
+  \item Every waiting queue does not contain duplcated elements (@{text "wq_distinct"}): 
+          @{thm[display] "wq_distinct"} 
+  \item All threads in waiting queues are living threads (@{text "wq_threads"}): 
+          @{thm[display] "wq_threads"} 
+  \item The event which can get a thread into waiting queue must be @{term "P"}-events
+         (@{text "block_pre"}): 
+          @{thm[display] "block_pre"}   
+  \item A thread may never wait for two different critical resources
+         (@{text "waiting_unique"}): 
+          @{thm[display] waiting_unique[of _ _ "cs\<^isub>1" "cs\<^isub>2"]}
+  \item Every resource can only be held by one thread
+         (@{text "held_unique"}): 
+          @{thm[display] held_unique[of _ "th\<^isub>1" _ "th\<^isub>2"]}
+  \item Every living thread has an unique precedence
+         (@{text "preced_unique"}): 
+          @{thm[display] preced_unique[of "th\<^isub>1" _ "th\<^isub>2"]}
+  \end{enumerate}
+*}
+
+text {* \noindent
+  The following lemmas show how RAG is changed with the execution of events:
+  \begin{enumerate}
+  \item Execution of @{term "Set"} does not change RAG (@{text "depend_set_unchanged"}):
+    @{thm[display] depend_set_unchanged}
+  \item Execution of @{term "Create"} does not change RAG (@{text "depend_create_unchanged"}):
+    @{thm[display] depend_create_unchanged}
+  \item Execution of @{term "Exit"} does not change RAG (@{text "depend_exit_unchanged"}):
+    @{thm[display] depend_exit_unchanged}
+  \item Execution of @{term "P"} (@{text "step_depend_p"}):
+    @{thm[display] step_depend_p}
+  \item Execution of @{term "V"} (@{text "step_depend_v"}):
+    @{thm[display] step_depend_v}
+  \end{enumerate}
+  *}
+
+text {* \noindent
+  These properties are used to derive the following important results about RAG:
+  \begin{enumerate}
+  \item RAG is loop free (@{text "acyclic_depend"}):
+  @{thm [display] acyclic_depend}
+  \item RAGs are finite (@{text "finite_depend"}):
+  @{thm [display] finite_depend}
+  \item Reverse paths in RAG are well founded (@{text "wf_dep_converse"}):
+  @{thm [display] wf_dep_converse}
+  \item The dependence relation represented by RAG has a tree structure (@{text "unique_depend"}):
+  @{thm [display] unique_depend[of _ _ "n\<^isub>1" "n\<^isub>2"]}
+  \item All threads in RAG are living threads 
+    (@{text "dm_depend_threads"} and @{text "range_in"}):
+    @{thm [display] dm_depend_threads range_in}
+  \end{enumerate}
+  *}
+
+text {* \noindent
+  The following lemmas show how every node in RAG can be chased to ready threads:
+  \begin{enumerate}
+  \item Every node in RAG can be chased to a ready thread (@{text "chain_building"}):
+    @{thm [display] chain_building[rule_format]}
+  \item The ready thread chased to is unique (@{text "dchain_unique"}):
+    @{thm [display] dchain_unique[of _ _ "th\<^isub>1" "th\<^isub>2"]}
+  \end{enumerate}
+  *}
+
+text {* \noindent
+  Properties about @{term "next_th"}:
+  \begin{enumerate}
+  \item The thread taking over is different from the thread which is releasing
+  (@{text "next_th_neq"}):
+  @{thm [display] next_th_neq}
+  \item The thread taking over is unique
+  (@{text "next_th_unique"}):
+  @{thm [display] next_th_unique[of _ _ _ "th\<^isub>1" "th\<^isub>2"]}  
+  \end{enumerate}
+  *}
+
+text {* \noindent
+  Some deeper results about the system:
+  \begin{enumerate}
+  \item There can only be one running thread (@{text "runing_unique"}):
+  @{thm [display] runing_unique[of _ "th\<^isub>1" "th\<^isub>2"]}
+  \item The maximum of @{term "cp"} and @{term "preced"} are equal (@{text "max_cp_eq"}):
+  @{thm [display] max_cp_eq}
+  \item There must be one ready thread having the max @{term "cp"}-value 
+  (@{text "max_cp_readys_threads"}):
+  @{thm [display] max_cp_readys_threads}
+  \end{enumerate}
+  *}
+
+text {* \noindent
+  The relationship between the count of @{text "P"} and @{text "V"} and the number of 
+  critical resources held by a thread is given as follows:
+  \begin{enumerate}
+  \item The @{term "V"}-operation decreases the number of critical resources 
+    one thread holds (@{text "cntCS_v_dec"})
+     @{thm [display]  cntCS_v_dec}
+  \item The number of @{text "V"} never exceeds the number of @{text "P"} 
+    (@{text "cnp_cnv_cncs"}):
+    @{thm [display]  cnp_cnv_cncs}
+  \item The number of @{text "V"} equals the number of @{text "P"} when 
+    the relevant thread is not living:
+    (@{text "cnp_cnv_eq"}):
+    @{thm [display]  cnp_cnv_eq}
+  \item When a thread is not living, it does not hold any critical resource 
+    (@{text "not_thread_holdents"}):
+    @{thm [display] not_thread_holdents}
+  \item When the number of @{text "P"} equals the number of @{text "V"}, the relevant 
+    thread does not hold any critical resource, therefore no thread can depend on it
+    (@{text "count_eq_dependents"}):
+    @{thm [display] count_eq_dependents}
+  \end{enumerate}
+  *}
 
 section {* Key properties \label{extension} *}
 
+(*<*)
+context extend_highest_gen
+begin
+(*>*)
+
+text {*
+  The essential of {\em Priority Inheritance} is to avoid indefinite priority inversion. For this 
+  purpose, we need to investigate what happens after one thread takes the highest precedence. 
+  A locale is used to describe such a situation, which assumes:
+  \begin{enumerate}
+  \item @{term "s"} is a valid state (@{text "vt_s"}):
+    @{thm  vt_s}.
+  \item @{term "th"} is a living thread in @{term "s"} (@{text "threads_s"}):
+    @{thm threads_s}.
+  \item @{term "th"} has the highest precedence in @{term "s"} (@{text "highest"}):
+    @{thm highest}.
+  \item The precedence of @{term "th"} is @{term "Prc prio tm"} (@{text "preced_th"}):
+    @{thm preced_th}.
+  \end{enumerate}
+  *}
+
+text {* \noindent
+  Under these assumptions, some basic priority can be derived for @{term "th"}:
+  \begin{enumerate}
+  \item The current precedence of @{term "th"} equals its own precedence (@{text "eq_cp_s_th"}):
+    @{thm [display] eq_cp_s_th}
+  \item The current precedence of @{term "th"} is the highest precedence in 
+    the system (@{text "highest_cp_preced"}):
+    @{thm [display] highest_cp_preced}
+  \item The precedence of @{term "th"} is the highest precedence 
+    in the system (@{text "highest_preced_thread"}):
+    @{thm [display] highest_preced_thread}
+  \item The current precedence of @{term "th"} is the highest current precedence 
+    in the system (@{text "highest'"}):
+    @{thm [display] highest'}
+  \end{enumerate}
+  *}
+
+text {* \noindent
+  To analysis what happens after state @{term "s"} a sub-locale is defined, which 
+  assumes:
+  \begin{enumerate}
+  \item @{term "t"} is a valid extension of @{term "s"} (@{text "vt_t"}): @{thm vt_t}.
+  \item Any thread created in @{term "t"} has priority no higher than @{term "prio"}, therefore
+    its precedence can not be higher than @{term "th"},  therefore
+    @{term "th"} remain to be the one with the highest precedence
+    (@{text "create_low"}):
+    @{thm [display] create_low}
+  \item Any adjustment of priority in 
+    @{term "t"} does not happen to @{term "th"} and 
+    the priority set is no higher than @{term "prio"}, therefore
+    @{term "th"} remain to be the one with the highest precedence (@{text "set_diff_low"}):
+    @{thm [display] set_diff_low}
+  \item Since we are investigating what happens to @{term "th"}, it is assumed 
+    @{term "th"} does not exit during @{term "t"} (@{text "exit_diff"}):
+    @{thm [display] exit_diff}
+  \end{enumerate}
+*}
+
+text {* \noindent
+  All these assumptions are put into a predicate @{term "extend_highest_gen"}. 
+  It can be proved that @{term "extend_highest_gen"} holds 
+  for any moment @{text "i"} in it @{term "t"} (@{text "red_moment"}):
+  @{thm [display] red_moment}
+  
+  From this, an induction principle can be derived for @{text "t"}, so that 
+  properties already derived for @{term "t"} can be applied to any prefix 
+  of @{text "t"} in the proof of new properties 
+  about @{term "t"} (@{text "ind"}):
+  \begin{center}
+  @{thm[display] ind}
+  \end{center}
+
+  The following properties can be proved about @{term "th"} in @{term "t"}:
+  \begin{enumerate}
+  \item In @{term "t"}, thread @{term "th"} is kept live and its 
+    precedence is preserved as well
+    (@{text "th_kept"}): 
+    @{thm [display] th_kept}
+  \item In @{term "t"}, thread @{term "th"}'s precedence is always the maximum among 
+    all living threads
+    (@{text "max_preced"}): 
+    @{thm [display] max_preced}
+  \item In @{term "t"}, thread @{term "th"}'s current precedence is always the maximum precedence
+    among all living threads
+    (@{text "th_cp_max_preced"}): 
+    @{thm [display] th_cp_max_preced}
+  \item In @{term "t"}, thread @{term "th"}'s current precedence is always the maximum current 
+    precedence among all living threads
+    (@{text "th_cp_max"}): 
+    @{thm [display] th_cp_max}
+  \item In @{term "t"}, thread @{term "th"}'s current precedence equals its precedence at moment 
+    @{term "s"}
+    (@{text "th_cp_preced"}): 
+    @{thm [display] th_cp_preced}
+  \end{enumerate}
+  *}
+
+text {* \noindent
+  The main theorem is to characterizing the running thread during @{term "t"} 
+  (@{text "runing_inversion_2"}):
+  @{thm [display] runing_inversion_2}
+  According to this, if a thread is running, it is either @{term "th"} or was
+  already live and held some resource 
+  at moment @{text "s"} (expressed by: @{text "cntV s th' < cntP s th'"}).
+
+  Since there are only finite many threads live and holding some resource at any moment,
+  if every such thread can release all its resources in finite duration, then after finite
+  duration, none of them may block @{term "th"} anymore. So, no priority inversion may happen
+  then.
+  *}
+
+(*<*)
+end
+(*>*)
+
 section {* Properties to guide implementation \label{implement} *}
 
+text {*
+  The properties (especially @{text "runing_inversion_2"}) convinced us that model defined 
+  in section \ref{model} does prevent indefinite priority inversion and therefore fulfills 
+  the fundamental requirement of Priority Inheritance protocol. Another purpose of this paper 
+  is to show how this model can be used to guide a concrete implementation.
+  *}
+
+
 section {* Related works \label{related} *}
 
 text {*
diff -r f1e6071a4613 -r 24199eb2c423 prio/PrioG.thy
--- a/prio/PrioG.thy	Tue Jan 24 00:34:52 2012 +0000
+++ b/prio/PrioG.thy	Fri Jan 27 13:50:02 2012 +0000
@@ -1,5 +1,5 @@
 theory PrioG
-imports PrioGDef
+imports PrioGDef 
 begin
 
 lemma runing_ready: "runing s \<subseteq> readys s"
@@ -349,6 +349,7 @@
 qed
 
 lemma waiting_unique:
+  fixes s cs1 cs2
   assumes "vt step s"
   and "waiting s th cs1"
   and "waiting s th cs2"
@@ -359,7 +360,7 @@
     by (auto simp add:s_waiting_def)
 qed
 
-lemma holded_unique:
+lemma held_unique:
   assumes "vt step s"
   and "holding s th1 cs"
   and "holding s th2 cs"