791 

   791   From this lemma we can infer that @{text th} can only be blocked by a thread @{text th'} that

   792   The following lemmas show how every node in RAG can be chased to ready threads:

   792   held some resource in state @{text s} (that is not @{text "detached"}). And furthermore

   793   \begin{enumerate}

   793   that the current precedence of @{text th'} in state @{text "(s' @ s)"} must be equal to the 

   794   \item Every node in RAG can be chased to a ready thread (@{text "chain_building"}):

   794   precedence of @{text th} in @{text "s"}.

   795     @{thm [display] chain_building[rule_format]}

   795 

   796   \item The ready thread chased to is unique (@{text "dchain_unique"}):

   796   \begin{theorem}

   797     @{thm [display] dchain_unique[of _ _ "th\<^isub>1" "th\<^isub>2"]}

   797   Given the assumptions about states @{text "s"} and @{text "s' @ s"},

   798   \end{enumerate}

   798   the thread @{text th} and the events in @{text "s'"}, if

   799   @{term "th' \<in> running (s' @ s)"}, @{text "th' \<noteq> th"}, then

   800   @{text "th' \<in> threads s"}, @{text "\<not> detached s th'"} and 

   801   @{term "cp (s' @ s) th' = prec th s"}.

   802   \end{theorem}

   803 

   804   We show this theorem by induction on @{text "s'"} using Lemma~\ref{mainlem}.

   805   This theorem gives a stricter bound on the processes that can block @{text th}:

   806   only threads that were alive in state @{text s} and moreover held a resource.

   807   Finally, the theorem establishes that the blocking threads have the

   808   current precedence raised to the precedence of @{text th}.

   809 

   810   %The following lemmas show how every node in RAG can be chased to ready threads:

   811   %\begin{enumerate}

   812   %\item Every node in RAG can be chased to a ready thread (@{text "chain_building"}):

   813   %  @   {thm [display] chain_building[rule_format]}

   814   %\item The ready thread chased to is unique (@{text "dchain_unique"}):

   815   %  @   {thm [display] dchain_unique[of _ _ "th\<^isub>1" "th\<^isub>2"]}

   816   %\end{enumerate}

   817 

   818   %Some deeper results about the system:

   819   %\begin{enumerate}

   820   %\item The maximum of @{term "cp"} and @{term "preced"} are equal (@{text "max_cp_eq"}):

   821   %@  {thm [display] max_cp_eq}

   822   %\item There must be one ready thread having the max @{term "cp"}-value 

   823   %(@{text "max_cp_readys_threads"}):

   824   %@  {thm [display] max_cp_readys_threads}

   825   %\end{enumerate}

   826 

   827   %The relationship between the count of @{text "P"} and @{text "V"} and the number of 

   828   %critical resources held by a thread is given as follows:

   829   %\begin{enumerate}

   830   %\item The @{term "V"}-operation decreases the number of critical resources 

   831   %  one thread holds (@{text "cntCS_v_dec"})

   832   %   @  {thm [display]  cntCS_v_dec}

   833   %\item The number of @{text "V"} never exceeds the number of @{text "P"} 

   834   %  (@  {text "cnp_cnv_cncs"}):

   835   %  @  {thm [display]  cnp_cnv_cncs}

   836   %\item The number of @{text "V"} equals the number of @{text "P"} when 

   837   %  the relevant thread is not living:

   838   %  (@{text "cnp_cnv_eq"}):

   839   %  @  {thm [display]  cnp_cnv_eq}

   840   %\item When a thread is not living, it does not hold any critical resource 

   841   %  (@{text "not_thread_holdents"}):

   842   %  @  {thm [display] not_thread_holdents}

   843   %\item When the number of @{text "P"} equals the number of @{text "V"}, the relevant 

   844   %  thread does not hold any critical resource, therefore no thread can depend on it

   845   %  (@{text "count_eq_dependents"}):

   846   %  @  {thm [display] count_eq_dependents}

   847   %\end{enumerate}

   848 

   849   %The reason that only threads which already held some resoures

   850   %can be runing and block @{text "th"} is that if , otherwise, one thread 

   851   %does not hold any resource, it may never have its prioirty raised

   852   %and will not get a chance to run. This fact is supported by 

   853   %lemma @{text "moment_blocked"}:

   854   %@   {thm [display] moment_blocked}

   855   %When instantiating  @{text "i"} to @{text "0"}, the lemma means threads which did not hold any

   856   %resource in state @{text "s"} will not have a change to run latter. Rephrased, it means 

   857   %any thread which is running after @{text "th"} became the highest must have already held

   858   %some resource at state @{text "s"}.

   859 

   860 

   861   %When instantiating @{text "i"} to a number larger than @{text "0"}, the lemma means 

   862   %if a thread releases all its resources at some moment in @{text "t"}, after that, 

   863   %it may never get a change to run. If every thread releases its resource in finite duration,

   864   %then after a while, only thread @{text "th"} is left running. This shows how indefinite 

   865   %priority inversion can be avoided. 

   866 

   867   %All these assumptions are put into a predicate @{term "extend_highest_gen"}. 

   868   %It can be proved that @{term "extend_highest_gen"} holds 

   869   %for any moment @{text "i"} in it @{term "t"} (@{text "red_moment"}):

   870   %@   {thm [display] red_moment}

   871   

   872   %From this, an induction principle can be derived for @{text "t"}, so that 

   873   %properties already derived for @{term "t"} can be applied to any prefix 

   874   %of @{text "t"} in the proof of new properties 

   875   %about @{term "t"} (@{text "ind"}):

   876   %\begin{center}

   877   %@   {thm[display] ind}

   878   %\end{center}

   879 

   880   %The following properties can be proved about @{term "th"} in @{term "t"}:

   881   %\begin{enumerate}

   882   %\item In @{term "t"}, thread @{term "th"} is kept live and its 

   883   %  precedence is preserved as well

   884   %  (@{text "th_kept"}): 

   885   %  @   {thm [display] th_kept}

   886   %\item In @{term "t"}, thread @{term "th"}'s precedence is always the maximum among 

   887   %  all living threads

   888   %  (@{text "max_preced"}): 

   889   %  @   {thm [display] max_preced}

   890   %\item In @{term "t"}, thread @{term "th"}'s current precedence is always the maximum precedence

   891   %  among all living threads

   892   %  (@{text "th_cp_max_preced"}): 

   893   %  @   {thm [display] th_cp_max_preced}

   894   %\item In @{term "t"}, thread @{term "th"}'s current precedence is always the maximum current 

   895   %  precedence among all living threads

   896   %  (@{text "th_cp_max"}): 

   897   %  @   {thm [display] th_cp_max}

   898   %\item In @{term "t"}, thread @{term "th"}'s current precedence equals its precedence at moment 

   899   %  @{term "s"}

   900   %  (@{text "th_cp_preced"}): 

   901   %  @   {thm [display] th_cp_preced}

   902   %\end{enumerate}

   903 

   904   %The main theorem of this part is to characterizing the running thread during @{term "t"} 

   905   %(@{text "runing_inversion_2"}):

   906   %@   {thm [display] runing_inversion_2}

   907   %According to this, if a thread is running, it is either @{term "th"} or was

   908   %already live and held some resource 

   909   %at moment @{text "s"} (expressed by: @{text "cntV s th' < cntP s th'"}).

   910 

   911   %Since there are only finite many threads live and holding some resource at any moment,

   912   %if every such thread can release all its resources in finite duration, then after finite

   913   %duration, none of them may block @{term "th"} anymore. So, no priority inversion may happen

   914   %then.