712   %@{thm[mode=IfThen] }\\

   712   @{text If}~@{thm (prem 1) acyclic_depend}~@{text "then"}:\\

   713   %@{thm[mode=IfThen] }\\

   713   \hspace{5mm}@{thm (concl) acyclic_depend},

   714   %@{thm[mode=IfThen] }

   714   @{thm (concl) finite_depend} and

   715   @{thm (concl) wf_dep_converse},\\

   716   \hspace{5mm}@{text "if"}~@{thm (prem 2) dm_depend_threads}~@{text "then"}~@{thm (concl) dm_depend_threads}\\

   717   \hspace{5mm}@{text "if"}~@{thm (prem 2) range_in}~@{text "then"}~@{thm (concl) range_in}

   814 section {* Properties for an Implementation \label{implement}*}

   817 section {* Properties for an Implementation\label{implement}*}

   815 

   818 

   816 text {*

   819 text {*

   817   The properties (centered around @{text "runing_inversion_2"} in particular) 

   820   While a formal correctness proof for our model of PIP is certainly

   818   convinced us that the formal model 

   821   attractive (especially in light of the flawed proof by Sha et

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

   822   al.~\cite{Sha90}), we found that the formalisation can even help us

   820   the fundamental requirement of Priority Inheritance protocol. Another purpose of this paper 

   823   with efficiently implementing PIP.

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

   824 

   822 

   825   For example Baker complained that calculating the current precedence

   823   The difficult part of implementation is the calculation of current precedence. 

   826   in PIP is quite ``heavy weight'' in Linux (see our Introduction).

   824   Once current precedence is computed efficiently and correctly, 

   827   In our model of PIP the current precedence of a thread in a state s

   825   the selection of the thread with highest precedence from ready threads is a 

   828   depends on all its dependants---a ``global'' transitive notion,

   826   standard scheduling mechanism implemented in most operating systems. 

   829   which is indeed heavy weight (see Def.~shown in \eqref{cpreced}).

   827 

   830   We can however prove how to improve upon this. For this let us

   828   Our implementation related formalization focuses on how to compute 

   831   define the notion of @{term children} of a thread as

   829   current precedence. First, it can be proved that the computation of current 

   832 

   830   precedence @{term "cp"} of a threads

   833   \begin{isabelle}\ \ \ \ \ %%%

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

   834   \begin{tabular}{@ {}l}

   832   @{thm [display] cp_rec} 

   835   @{thm children_def2}

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

   836   \end{tabular}

   834   RAG: 

   837   \end{isabelle}

   835   \[

   838 

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

   839   \noindent

   837   \]

   840   where a child is a thread that is one ``hop'' away in the @{term RAG} from the 

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

   841   tread @{text th} (and waiting for @{text th} to release a resource). We can prove that

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

   842 

   840   \]

   843   \begin{lemma}\label{childrenlem}

   841   which corresponds a two hop link between threads in the RAG, with a resource in the middle.

   844   @{text "If"} @{thm (prem 1) cp_rec} @{text "then"}

   845   \begin{center}

   846   @{thm (concl) cp_rec}.

   847   \end{center}

   848   \end{lemma}

   843   Lemma @{text "cp_rec"} means, the current precedence of threads can be computed locally, 

   850   \noindent

   844   i.e. the current precedence of one thread only needs to be recomputed when some of its

   851   That means the current precedence of a thread @{text th} can be

   845   children change their current precedence. 

   852   computed locally by considering only the children of @{text th}. In

   846 

   853   effect, it only needs to be recomputed for @{text th} when one of

   847   Each of the following subsections discusses one event type, investigating 

   854   its children change their current precedence.  Once the current 

   848   which parts in the RAG need current precedence re-computation when that type of event

   855   precedence is computed in this more efficient manner, the selection

   849   happens.

   856   of the thread with highest precedence from a set of ready threads is

   850   *}

   857   a standard scheduling operation implemented in most operating

   851  

   858   systems.

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

   859 

   853 

   860   Of course the main implementation work for PIP involves the scheduler

   854 (*<*)

   861   and coding how it should react to the events, for example which 

   855 context step_set_cps

   862   datastructures need to be modified (mainly @{text RAG} and @{text cprec}).

   856 begin

   863   Below we outline how our formalisation guides this implementation for each 

   857 (*>*)

   864   event.\smallskip

   858 

   859 text {*

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

   861   \begin{enumerate}

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

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

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

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

   866   \end{enumerate}

   867   *}

   868 

   869 text {* \noindent

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

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

   872   results:

   873   \begin{enumerate}

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

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

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

   877     @{thm [display] eq_cp}

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

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

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

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

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

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

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

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

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

   887     \begin{enumerate}

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

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

   890         @{thm [display] eq_up_self}

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

   892         gives unchanged result, the procedure can stop:

   893         @{thm [display] eq_up}

   894   \end{enumerate}

   895   \end{enumerate}

   896   *}

   897 

   898 (*<*)

   899 end

   900 (*>*)

   901 

   902 subsection {* Event @{text "V th cs"} *}

   903 

   904 (*<*)

   905 context step_v_cps_nt

   906 begin

   907 (*>*)

   908 

   909 text {*

   910   The context under which event @{text "V th cs"} happens is formalized as follows:

   911   \begin{enumerate}

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

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

   914       event @{text "V th cs"} is eligible to happen under state @{term "s'"} and

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

   916   \end{enumerate}

   917   *}

   918 

   919 text {* \noindent

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

   921   threads change from state @{term "s'"} to @{term "s"}. 

   922 

   923 

   924   Two subcases are considerted, 

   925   where the first is that there exits @{term "th'"} 

   926   such that 

   927   @{thm [display] nt} 

   928   holds, which means there exists a thread @{term "th'"} to take over

   929   the resource release by thread @{term "th"}. 

   930   In this sub-case, the following results are obtained:

   931   \begin{enumerate}

   932   \item The change of RAG is given by lemma @{text "depend_s"}: 

   933   @{thm [display] "depend_s"}

   934   which shows two edges are removed while one is added. These changes imply how

   935   the current precedences should be re-computed.

   936   \item First all threads different from @{term "th"} and @{term "th'"} have their

   937   @{term "cp"}-value kept, therefore do not need a re-computation

   938   (@{text "cp_kept"}): @{thm [display] cp_kept}

   939   This lemma also implies, only the @{term "cp"}-values of @{term "th"} and @{term "th'"}

   940   need to be recomputed.

   941   \end{enumerate}

   942   *}

   943 

   944 (*<*)

   945 end

   946 

   947 context step_v_cps_nnt

   948 begin

   949 (*>*)

   950 

   951 text {*

   952   The other sub-case is when for all @{text "th'"}

   953   @{thm [display] nnt}

   954   holds, no such thread exists. The following results can be obtained for this 

   955   sub-case:

   956   \begin{enumerate}

   957   \item The change of RAG is given by lemma @{text "depend_s"}:

   958   @{thm [display] depend_s}

   959   which means only one edge is removed.

   960   \item In this case, no re-computation is needed (@{text "eq_cp"}):

   961   @{thm [display] eq_cp}

   962   \end{enumerate}

   963   *}

   964 

   965 (*<*)

   966 end

   967 (*>*)

   968 

   969 

   970 subsection {* Event @{text "P th cs"} *}

   971 

   972 (*<*)

   973 context step_P_cps_e

   974 begin

   975 (*>*)

   976 

   977 text {*

   978   The context under which event @{text "P th cs"} happens is formalized as follows:

   979   \begin{enumerate}

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

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

   982       event @{text "P th cs"} is eligible to happen under state @{term "s'"} and

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

   984   \end{enumerate}

   985 

   986   This case is further divided into two sub-cases. The first is when @{thm ee} holds.

   987   The following results can be obtained:

   988   \begin{enumerate}

   989   \item One edge is added to the RAG (@{text "depend_s"}):

   990     @{thm [display] depend_s}

   991   \item No re-computation is needed (@{text "eq_cp"}):

   992     @{thm [display] eq_cp}

   993   \end{enumerate}

  1031 

   871 text {*

  1032 text {*

   872   \noindent

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

   873   @{term "Create th prio"}: We assume that the current state @{text s'} and 

  1034   \begin{enumerate}

   874   the next state @{term "s \<equiv> Create th prio#s'"} are both valid (meaning the event

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

   875   is allowed to occur). In this situation we can show that

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

   876 

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

   877   \begin{isabelle}\ \ \ \ \ %%%

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

   878   \begin{tabular}{@ {}l}

  1039   \end{enumerate}

   879   @{thm eq_dep}\\

  1040   The following results can be obtained under this context:

   880   @{thm eq_cp_th}\\

  1041   \begin{enumerate}

   881   @{thm[mode=IfThen] eq_cp}

  1042   \item The RAG does not change (@{text "eq_dep"}):

   882   \end{tabular}

  1043     @{thm [display] eq_dep}

   883   \end{isabelle}

  1044   \item All threads other than @{term "th"} do not need re-computation (@{text "eq_cp"}):

   884 

  1045     @{thm [display] eq_cp}

   885   \noindent

  1046   \item The @{term "cp"}-value of @{term "th"} equals its precedence 

   886   This means we do not have recalculate the @{text RAG} and also none of the

  1047     (@{text "eq_cp_th"}):

   887   current precedences of the other threads. The current precedence of the created

  1048     @{thm [display] eq_cp_th}

   888   thread is just its precedence, that is the pair @{term "(prio, length (s::event list))"}.

  1049   \end{enumerate}

   889   \smallskip

  1050 

   890   *}

   891 (*<*)

   892 end

   893 context step_exit_cps

   894 begin

   895 (*>*)

   896 text {*

   897   \noindent

   898   @{term "Exit th"}: We again assume that the current state @{text s'} and 

   899   the next state @{term "s \<equiv> Exit th#s'"} are both valid. We can show that

   900 

   901   \begin{isabelle}\ \ \ \ \ %%%

   902   \begin{tabular}{@ {}l}

   903   @{thm eq_dep}\\

   904   @{thm[mode=IfThen] eq_cp}

   905   \end{tabular}

   906   \end{isabelle}

   907 

   908   \noindent

   909   This means also we do not have to recalculate the @{text RAG} and

   910   not the current precedences for the other threads. Since @{term th} is not

   911   alive anymore in state @{term "s"}, there is no need to calculate its

   912   current precedence.

   913   \smallskip

  1052 

   915 (*<*)

  1053 

   916 end

   917 context step_set_cps

   918 begin

   919 (*>*)

   920 text {*

   921   \noindent

   922   @{term "Set th prio"}: We assume that @{text s'} and 

   923   @{term "s \<equiv> Set th prio#s'"} are both valid. We can show that

   924 

   925   \begin{isabelle}\ \ \ \ \ %%%

   926   \begin{tabular}{@ {}l}

   927   @{thm[mode=IfThen] eq_dep}\\

   928   @{thm[mode=IfThen] eq_cp}

   929   \end{tabular}

   930   \end{isabelle}

   931 

   932   \noindent

   933   The first is again telling us we do not need to change the @{text RAG}. The second

   934   however states that only threads that are \emph{not} dependent on @{text th} have their

   935   current precedence unchanged. For the others we have to recalculate the current

   936   precedence. To do this we can start from @{term "th"} 

   937   and follow the @{term "depend"}-chains to recompute the @{term "cp"} of every 

   938   thread encountered on the way using Lemma~\ref{childrenlem}. Since the @{term "depend"}

   939   is loop free, this procedure always stop. The the following two lemmas show this 

   940   procedure can actually stop often earlier.

   941 

   942   \begin{isabelle}\ \ \ \ \ %%%

   943   \begin{tabular}{@ {}l}

   944   @{thm[mode=IfThen] eq_up_self}\\

   945   @{text "If"} @{thm (prem 1) eq_up}, @{thm (prem 2) eq_up} and @{thm (prem 3) eq_up}\\

   946   @{text "then"} @{thm (concl) eq_up}.

   947   \end{tabular}

   948   \end{isabelle}

   949 

   950   \noindent

   951   The first states that if the current precedence of @{text th} is unchanged,

   952   then the procedure can stop immediately (all dependent threads have their @{term cp}-value unchanged).

   953   The second states that if an intermediate @{term cp}-value does not change, then

   954   the procedure can also stop, because none of its dependent threads will

   955   have their current precedence changed.

   956   \smallskip

   957   *}

   958 

   959 (*<*)

   960 end

   961 context step_v_cps_nt

   962 begin

   963 (*>*)

   964 text {*

   965   \noindent

   966   @{term "V th cs"}: We assume that @{text s'} and 

   967   @{term "s \<equiv> V th cs#s'"} are both valid. We have to consider two

   968   subcases: one where there is a thread to ``take over'' the released

   969   resource @{text cs}, and where there is not. Let us consider them

   970   in turn. Suppose in state @{text s}, the thread @{text th'} takes over

   971   resource @{text cs} from thread @{text th}. We can show

   972 

   973 

   974   \begin{isabelle}\ \ \ \ \ %%%

   975   @{thm depend_s}

   976   \end{isabelle}

   977   

   978   \noindent

   979   which shows how the @{text RAG} needs to be changed. This also suggests

   980   how the current precedences need to be recalculated. For threads that are

   981   not @{text "th"} and @{text "th'"} nothing needs to be changed, since we

   982   can show

   983 

   984   \begin{isabelle}\ \ \ \ \ %%%

   985   @{thm[mode=IfThen] cp_kept}

   986   \end{isabelle}

   987   

   988   \noindent

   989   For @{text th} and @{text th'} we need to use Lemma~\ref{childrenlem} to

   990   recalculate their current prcedence since their children have changed. *}(*<*)end context step_v_cps_nnt begin (*>*)text {*

   991   \noindent

   992   In the other case where there is no thread that takes over @{text cs}, we can show how

   993   to recalculate the @{text RAG} and also show that no current precedence needs

   994   to be recalculated, except for @{text th} (like in the case above).

   995 

   996   \begin{isabelle}\ \ \ \ \ %%%

   997   \begin{tabular}{@ {}l}

   998   @{thm depend_s}\\

   999   @{thm eq_cp}

  1000   \end{tabular}

  1001   \end{isabelle}

  1002   *}

  1003 (*<*)

  1004 end

  1005 context step_P_cps_e

  1006 begin

  1007 (*>*)

  1008 

  1009 text {*

  1010   \noindent

  1011   @{term "P th cs"}: We assume that @{text s'} and 

  1012   @{term "s \<equiv> P th cs#s'"} are both valid. We again have to analyse two subcases, namely

  1013   the one where @{text cs} is locked, and where it is not. We treat the second case

  1014   first by showing that

  1015   

  1016   \begin{isabelle}\ \ \ \ \ %%%

  1017   \begin{tabular}{@ {}l}

  1018   @{thm depend_s}\\

  1019   @{thm eq_cp}

  1020   \end{tabular}

  1021   \end{isabelle}

  1022 

  1023   \noindent

  1024   This means we do not need to add a holding edge to the @{text RAG} and no

  1025   current precedence must be recalculated (including that for @{text th}).*}(*<*)end context step_P_cps_ne begin(*>*) text {*

  1026   \noindent

  1027   In the second case we know that resouce @{text cs} is locked. We can show that

  1028   

  1029   \begin{isabelle}\ \ \ \ \ %%%

  1030   \begin{tabular}{@ {}l}

  1031   @{thm depend_s}\\

  1032   @{thm[mode=IfThen] eq_cp}

  1033   \end{tabular}

  1034   \end{isabelle}

  1035 

  1036   \noindent

  1037   That means we have to add a waiting edge to the @{text RAG}. Furthermore

  1038   the current precedence for all threads that are not dependent on @{text th}

  1039   are unchanged. For the others we need to follow the @{term "depend"}-chains 

  1040   in the @{text RAG} and recompute the @{term "cp"}. However, like in the 

  1041   @{text Set}-event, this operation can stop often earlier, namely when intermediate

  1042   values do not change.

  1043   *}

  1058 subsection {* Event @{text "Exit th"} *}

  1048 text {*

  1059 

  1049   \noindent

  1060 (*<*)

  1050   TO DO a few sentences summarising what has been achieved.

  1061 context step_exit_cps

  1062 begin

  1063 (*>*)

  1064 

  1065 text {*

  1066   The context under which event @{text "Exit th"} happens is formalized as follows:

  1067   \begin{enumerate}

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

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

  1070       event @{text "Exit th"} is eligible to happen under state @{term "s'"} and

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

  1072   \end{enumerate}

  1073   The following results can be obtained under this context:

  1074   \begin{enumerate}

  1075   \item The RAG does not change (@{text "eq_dep"}):

  1076     @{thm [display] eq_dep}

  1077   \item All threads other than @{term "th"} do not need re-computation (@{text "eq_cp"}):

  1078     @{thm [display] eq_cp}

  1079   \end{enumerate}

  1080   Since @{term th} does not live in state @{term "s"}, there is no need to compute 

  1081   its @{term cp}-value.