383   The main theorem is to characterizing the running thread during @{term "t"} 

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

   403   The properties (especially @{text "runing_inversion_2"}) convinced us that model defined 

   406   The properties (especially @{text "runing_inversion_2"}) convinced us that the model defined 

   404   in section \ref{model} does prevent indefinite priority inversion and therefore fulfills 

   407   in Section \ref{model} does prevent indefinite priority inversion and therefore fulfills 

   406   is to show how this model can be used to guide a concrete implementation.

   409   is to show how this model can be used to guide a concrete implementation. As discussed in

   407   *}

   410   Section 5.6.5 of \cite{Vahalia:1996:UI}, the implementation of Priority Inheritance in Solaris 

   408 

   411   uses sophisticated linking data structure. Except discussing two scenarios to show how

   412   the data structure should be manipulated, a lot of details of the implementation are missing. 

   413   In \cite{Faria08,conf/fase/JahierHR09,WellingsBSB07} the protocol is described formally 

   414   using different notations, but little information is given on how this protocol can be 

   415   implemented efficiently, especially there is no information on how these data structure 

   416   should be manipulated. 

   417 

   418   Because the scheduling of threads is based on current precedence, 

   419   the central issue in implementation of Priority Inheritance is how to compute the precedence

   420   correctly and efficiently. As long as the precedence is correct, it is very easy to 

   421   modify the scheduling algorithm to select the correct thread to execute. 

   422 

   423   First, it can be proved that the computation of current precedence @{term "cp"} of a threads

   424   only involves its children (@{text "cp_rec"}):

   425   @{thm [display] cp_rec} 

   426   where @{term "children s th"} represents the set of children of @{term "th"} in the current

   427   RAG: 

   428   \[

   429   @{thm (lhs) children_def} @{text "\<equiv>"} @{thm (rhs) children_def}

   430   \]

   431   where the definition of @{term "child"} is: 

   432   \[ @{thm (lhs) child_def} @{text "\<equiv>"}  @{thm (rhs) child_def}

   433   \]

   434 

   435   The aim of this section is to fill the missing details of how current precedence should

   436   be changed with the happening of events, with each event type treated by one subsection,

   437   where the computation of @{term "cp"} uses lemma @{text "cp_rec"}.

   438   *}

   439  

   440 subsection {* Event @{text "Set th prio"} *}

   441 

   442 (*<*)

   443 context step_set_cps

   444 begin

   445 (*>*)

   446 

   447 text {*

   448   The context under which event @{text "Set th prio"} happens is formalized as follows:

   449   \begin{enumerate}

   450     \item The formation of @{term "s"} (@{text "s_def"}): @{thm s_def}.

   451     \item State @{term "s"} is a valid state (@{text "vt_s"}): @{thm vt_s}. This implies 

   452       event @{text "Set th prio"} is eligible to happen under state @{term "s'"} and

   453       state @{term "s'"} is a valid state.

   454   \end{enumerate}

   455   *}

   456 

   457 text {* \noindent

   458   Under such a context, we investigated how the current precedence @{term "cp"} of 

   459   threads change from state @{term "s'"} to @{term "s"} and obtained the following

   460   conclusions:

   461   \begin{enumerate}

   462   %% \item The RAG does not change (@{text "eq_dep"}): @{thm "eq_dep"}.

   463   \item All threads with no dependence relation with thread @{term "th"} have their

   464     @{term "cp"}-value unchanged (@{text "eq_cp"}):

   465     @{thm [display] eq_cp}

   466     This lemma implies the @{term "cp"}-value of @{term "th"}

   467     and those threads which have a dependence relation with @{term "th"} might need

   468     to be recomputed. The way to do this is to start from @{term "th"} 

   469     and follow the @{term "depend"}-chain to recompute the @{term "cp"}-value of every 

   470     encountered thread using lemma @{text "cp_rec"}. 

   471     Since the @{term "depend"}-relation is loop free, this procedure 

   472     can always stop. The the following lemma shows this procedure actually could stop earlier.

   473   \item The following two lemma shows, if a thread the re-computation of which

   474     gives an unchanged @{term "cp"}-value, the procedure described above can stop. 

   475     \begin{enumerate}

   476       \item Lemma @{text "eq_up_self"} shows if the re-computation of

   477         @{term "th"}'s @{term "cp"} gives the same result, the procedure can stop:

   478         @{thm [display] eq_up_self}

   479       \item Lemma @{text "eq_up"}) shows if the re-computation at intermediate threads

   480         gives unchanged result, the procedure can stop:

   481         @{thm [display] eq_up}

   482   \end{enumerate}

   483   \end{enumerate}

   484   *}

   485 

   486 (*<*)

   487 end

   488 (*>*)