814 section {* Properties for an Implementation *}

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

   815 

   815 

   816 text {* TO DO *}

   816 text {*

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

   818   convinced us that the formal model 

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

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

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

   822 

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

   824   Once current precedence is computed efficiently and correctly, 

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

   826   standard scheduling mechanism implemented in most operating systems. 

   827 

   828   Our implementation related formalization focuses on how to compute 

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

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

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

   832   @{thm [display] cp_rec} 

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

   834   RAG: 

   835   \[

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

   837   \]

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

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

   840   \]

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

   842   

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

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

   845   children change their current precedence. 

   846 

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

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

   849   happens.

   850   *}

   851  

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

   853 

   854 (*<*)

   855 context step_set_cps

   856 begin

   857 (*>*)

   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}

   994 *}

   995 

   996 (*<*)

   997 end

   998 

   999 context step_P_cps_ne

  1000 begin

  1001 (*>*)

  1002 

  1003 text {*

  1004   The second is when @{thm ne} holds.

  1005   The following results can be obtained:

  1006   \begin{enumerate}

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

  1008     @{thm [display] depend_s}

  1009   \item Threads with no dependence relation with @{term "th"} do not need a re-computation

  1010     of their @{term "cp"}-values (@{text "eq_cp"}):

  1011     @{thm [display] eq_cp}

  1012     This lemma implies all threads with a dependence relation with @{term "th"} may need 

  1013     re-computation.

  1014   \item Similar to the case of @{term "Set"}, the computation procedure could stop earlier

  1015     (@{text "eq_up"}):

  1016     @{thm [display] eq_up}

  1017   \end{enumerate}

  1018 

  1019   *}

  1020 

  1021 (*<*)

  1022 end

  1023 (*>*)

  1024 

  1025 subsection {* Event @{text "Create th prio"} *}

  1026 

  1027 (*<*)

  1028 context step_create_cps

  1029 begin

  1030 (*>*)

  1031 

  1032 text {*

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

  1034   \begin{enumerate}

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

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

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

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

  1039   \end{enumerate}

  1040   The following results can be obtained under this context:

  1041   \begin{enumerate}

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

  1043     @{thm [display] eq_dep}

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

  1045     @{thm [display] eq_cp}

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

  1047     (@{text "eq_cp_th"}):

  1048     @{thm [display] eq_cp_th}

  1049   \end{enumerate}

  1050 

  1051 *}

  1052 

  1053 

  1054 (*<*)

  1055 end

  1056 (*>*)

  1057 

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

  1059 

  1060 (*<*)

  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.

  1082 *}

  1083 

  1084 (*<*)

  1085 end

  1086 (*>*)