--- 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
(*>*)