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' \ running (s' @ s)"}, @{text "th' \ th"}, then + @{text "th' \ threads s"}, @{text "\ 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 (*>*)