1009   explain tRAG

  1010   \bigskip

  1011 

  1012 

  1013   Suppose the thread @{term th} is \emph{not} running in state @{term

  1014   "t @ s"}, meaning that it should be blocked by some other thread.

  1015   It is first shown that there is a path in the RAG leading from node

  1016   @{term th} to another thread @{text "th'"}, which is also in the

  1017   @{term readys}-set.  Since @{term readys}-set is non-empty, there

  1018   must be one in it which holds the highest @{term cp}-value, which,

  1019   by definition, is currently the @{term running}-thread.  However, we

  1020   are going to show in the next lemma slightly more: this running

  1021   thread is exactly @{term "th'"}.

  1027 

  1028   \begin{proof}

  1029   %Let me distinguish between cp (current precedence) and assigned precedence (the precedence the

  1030   %thread ``normally'' has).

  1031   %So we want to show what the cp of th' is in state t @ s.

  1032   %We look at all the assingned precedences in the subgraph starting from th'

  1033   %We are looking for the maximum of these assigned precedences.

  1034   %This subgraph must contain the thread th, which actually has the highest precednence

  1035   %so cp of th' in t @ s has this (assigned) precedence of th

  1036   %We know that cp (t @ s) th' 

  1037   %is the Maximum of the threads in the subgraph starting from th'

  1038   %this happens to be the precedence of th

  1039   %th has the highest precedence of all threads

  1040   \end{proof}

  1041 

  1042   \begin{corollary}  

  1043   Using the lemma \ref{runninginversion} we can say more about the thread th'

  1044   \end{corollary}