
diff -r 163cd8034e5b -r 8f256104e4f3 prio/Paper/Paper.thy
--- a/prio/Paper/Paper.thy	Tue Feb 14 02:24:09 2012 +0000
+++ b/prio/Paper/Paper.thy	Tue Feb 14 02:53:34 2012 +0000
@@ -788,134 +788,131 @@
   one step further, @{text "th'"} still cannot hold any resource. The situation will 
   not change in further extensions as long as @{text "th"} holds the highest precedence.
 
+  From this lemma we can infer that @{text th} can only be blocked by a thread @{text th'} that
+  held some resource in state @{text s} (that is not @{text "detached"}). And furthermore
+  that the current precedence of @{text th'} in state @{text "(s' @ s)"} must be equal to the 
+  precedence of @{text th} in @{text "s"}.
 
-  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}
-  *}
-
+  \begin{theorem}
+  Given the assumptions about states @{text "s"} and @{text "s' @ s"},
+  the thread @{text th} and the events in @{text "s'"}, if
+  @{term "th' \<in> running (s' @ s)"}, @{text "th' \<noteq> th"}, then
+  @{text "th' \<in> threads s"}, @{text "\<not> detached s th'"} and 
+  @{term "cp (s' @ s) th' = prec th s"}.
+  \end{theorem}
 
-text {* \noindent
-  Some deeper results about the system:
-  \begin{enumerate}
-  \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}
-  *}
+  We show this theorem by induction on @{text "s'"} using Lemma~\ref{mainlem}.
+  This theorem gives a stricter bound on the processes that can block @{text th}:
+  only threads that were alive in state @{text s} and moreover held a resource.
+  Finally, the theorem establishes that the blocking threads have the
+  current precedence raised to the precedence of @{text th}.
+
+  %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
-  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}
+  %Some deeper results about the system:
+  %\begin{enumerate}
+  %\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}
 
-
-  @{thm[display] live}
-*}
-
-subsection {* Proof idea *}
+  %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}
 
-text {*
-The reason that only threads which already held some resoures
-can be runing and block @{text "th"} is that if , otherwise, one thread 
-does not hold any resource, it may never have its prioirty raised
-and will not get a chance to run. This fact is supported by 
-lemma @{text "moment_blocked"}:
-@{thm [display] moment_blocked}
-When instantiating  @{text "i"} to @{text "0"}, the lemma means threads which did not hold any
-resource in state @{text "s"} will not have a change to run latter. Rephrased, it means 
-any thread which is running after @{text "th"} became the highest must have already held
-some resource at state @{text "s"}.
+  %The reason that only threads which already held some resoures
+  %can be runing and block @{text "th"} is that if , otherwise, one thread 
+  %does not hold any resource, it may never have its prioirty raised
+  %and will not get a chance to run. This fact is supported by 
+  %lemma @{text "moment_blocked"}:
+  %@   {thm [display] moment_blocked}
+  %When instantiating  @{text "i"} to @{text "0"}, the lemma means threads which did not hold any
+  %resource in state @{text "s"} will not have a change to run latter. Rephrased, it means 
+  %any thread which is running after @{text "th"} became the highest must have already held
+  %some resource at state @{text "s"}.
 
 
-  When instantiating @{text "i"} to a number larger than @{text "0"}, the lemma means 
-  if a thread releases all its resources at some moment in @{text "t"}, after that, 
-  it may never get a change to run. If every thread releases its resource in finite duration,
-  then after a while, only thread @{text "th"} is left running. This shows how indefinite 
-  priority inversion can be avoided. 
-
-*}
-
-section {* Key properties \label{extension} *}
-
+  %When instantiating @{text "i"} to a number larger than @{text "0"}, the lemma means 
+  %if a thread releases all its resources at some moment in @{text "t"}, after that, 
+  %it may never get a change to run. If every thread releases its resource in finite duration,
+  %then after a while, only thread @{text "th"} is left running. This shows how indefinite 
+  %priority inversion can be avoided. 
 
-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}
+  %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}
+  %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}
+  %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}
+
+  %The main theorem of this part 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.
   *}
-
-text {* \noindent
-  The main theorem of this part 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
 (*>*)




