595 print_locale extend_highest_gen

   596 thm extend_highest_gen_def

   597 thm extend_highest_gen_axioms_def

   598 thm highest_gen_def

   791 text {* \noindent

   792   Properties about @{term "next_th"}:

   793   \begin{enumerate}

   794   \item The thread taking over is different from the thread which is releasing

   795   (@{text "next_th_neq"}):

   796   @{thm [display] next_th_neq}

   797   \item The thread taking over is unique

   798   (@{text "next_th_unique"}):

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

   800   \end{enumerate}

   801   *}

   838 (*<*)

   839 end

   840 (*>*)

   841 

   843 

   844 (*<*)

   845 context extend_highest_gen

   846 begin

   847 print_locale extend_highest_gen

   848 thm extend_highest_gen_def

   849 thm extend_highest_gen_axioms_def

   850 thm highest_gen_def

   851 (*>*)

   872   So, the key of the proof is to establish the correctness of @{text "moment_blocked"}.

   873   We are going to show how this lemma is proved. At the heart of this proof, is 

   874   lemma @{text "pv_blocked"}:

   875   @{thm [display] pv_blocked}

   876   This lemma says: for any @{text "s"}-extension {text "t"}, if thread @{text "th'"}

   877   does not hold any resource, it can not be running at @{text "t@s"}.

   878 

   879 

   880   \noindent Proof: 

   881   \begin{enumerate}

   882   \item Since thread @{text "th'"} does not hold any resource, no thread may depend on it, 

   883     so its current precedence @{text "cp (t@s) th'"} equals to its own precedence

   884    @{text "preced th' (t@s)"}.  \label{arg_1}

   885   \item Since @{text "th"} has the highest precedence in the system and 

   886     precedences are distinct among threads, we have

   887     @{text "preced th' (t@s) < preced th (t@s)"}. From this and item \ref{arg_1}, 

   888     we have @{text "cp (t@s) th' < preced th (t@s)"}.

   889   \item Since @{text "preced th (t@s)"} is already the highest in the system, 

   890     @{text "cp (t@s) th"} can not be higher than this and can not be lower neither (by 

   891     the definition of @{text "cp"}), we have @{text "preced th (t@s) = cp (t@s) th"}.

   892   \item Finally we have @{text "cp (t@s) th' < cp (t@s) th"}.

   893   \item By defintion of @{text "running"}, @{text "th'"} can not be runing at 

   894     @{text "t@s"}.

   895   \end{enumerate}

   896   Since @{text "th'"} is not able to run at state @{text "t@s"}, it is not able to 

   897   make either {text "P"} or @{text "V"} action, so if @{text "t@s"} is extended

   898   one step further, @{text "th'"} still does not hold any resource. 

   899   The situation will not unchanged in further extensions as long as 

   900   @{text "th"} holds the highest precedence. Since this @{text "t"} is arbitarily chosen 

   901   except being constrained by predicate @{text "extend_highest_gen"} and 

   902   this predicate has the property that if it holds for @{text "t"}, it also holds

   903   for any moment @{text "i"} inside @{text "t"}, as shown by lemma @{text "red_moment"}:

   904 @{thm [display] "extend_highest_gen.red_moment"}

   905   so @{text "pv_blocked"} can be applied to any @{text "moment i t"}. 

   906   From this, lemma @{text "moment_blocked"} follows.

   909 (*<*)

   910 end

   911 (*>*)

   912 

   913 

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

   915 

   916 text {*

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

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

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

   920   with efficiently implementing PIP.

   921 

   922   For example Baker complained that calculating the current precedence

   923   in PIP is quite ``heavy weight'' in Linux (see the Introduction).

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

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

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

   927   We can however improve upon this. For this let us define the notion

   928   of @{term children} of a thread @{text th} in a state @{text s} as

   929 

   930   \begin{isabelle}\ \ \ \ \ %%%

   931   \begin{tabular}{@ {}l}

   932   @{thm children_def2}

   933   \end{tabular}

   934   \end{isabelle}

   935 

   936   \noindent

   937   where a child is a thread that is one ``hop'' away from the tread

   938   @{text th} in the @{term RAG} (and waiting for @{text th} to release

   939   a resource). We can prove that

   940 

   941   \begin{lemma}\label{childrenlem}

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

   943   \begin{center}

   944   @{thm (concl) cp_rec}.

   945   \end{center}

   946   \end{lemma}

   947   

   948   \noindent

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

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

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

   952   its children changes its current precedence.  Once the current 

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

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

   955   a standard scheduling operation implemented in most operating

   956   systems.

   957 

   958   Of course the main implementation work for PIP involves the

   959   scheduler and coding how it should react to events.  Below we

   960   outline how our formalisation guides this implementation for each

   961   kind of event.\smallskip

   962 *}

   963 

   964 (*<*)

   965 context step_create_cps

   966 begin

   967 (*>*)

   968 text {*

   969   \noindent

   970   \colorbox{mygrey}{@{term "Create th prio"}:} We assume that the current state @{text s'} and 

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

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

   973 

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

   975   \begin{tabular}{@ {}l}

   976   @{thm eq_dep},\\

   977   @{thm eq_cp_th}, and\\

   978   @{thm[mode=IfThen] eq_cp}

   979   \end{tabular}

   980   \end{isabelle}

   981 

   982   \noindent

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

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

   985   thread @{text th} is just its precedence, namely the pair @{term "(prio, length (s::event list))"}.

   986   \smallskip

   987   *}

   988 (*<*)

   989 end

   990 context step_exit_cps

   991 begin

   992 (*>*)

   993 text {*

   994   \noindent

   995   \colorbox{mygrey}{@{term "Exit th"}:} We again assume that the current state @{text s'} and 

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

   997 

   998   \begin{isabelle}\ \ \ \ \ %%%

   999   \begin{tabular}{@ {}l}

  1000   @{thm eq_dep}, and\\

  1001   @{thm[mode=IfThen] eq_cp}

  1002   \end{tabular}

  1003   \end{isabelle}

  1004 

  1005   \noindent

  1006   This means again we do not have to recalculate the @{text RAG} and

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

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

  1009   current precedence.

  1010   \smallskip

  1011 *}

  1012 (*<*)

  1013 end

  1014 context step_set_cps

  1015 begin

  1016 (*>*)

  1017 text {*

  1018   \noindent

  1019   \colorbox{mygrey}{@{term "Set th prio"}:} We assume that @{text s'} and 

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

  1021 

  1022   \begin{isabelle}\ \ \ \ \ %%%

  1023   \begin{tabular}{@ {}l}

  1024   @{thm[mode=IfThen] eq_dep}, and\\

  1025   @{thm[mode=IfThen] eq_cp}

  1026   \end{tabular}

  1027   \end{isabelle}

  1028 

  1029   \noindent

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

  1031   however states that only threads that are \emph{not} dependants of @{text th} have their

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

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

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

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

  1036   is loop free, this procedure will always stop. The following two lemmas show, however, 

  1037   that this procedure can actually stop often earlier without having to consider all

  1038   dependants.

  1039 

  1040   \begin{isabelle}\ \ \ \ \ %%%

  1041   \begin{tabular}{@ {}l}

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

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

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

  1045   \end{tabular}

  1046   \end{isabelle}

  1047 

  1048   \noindent

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

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

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

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

  1053   have their current precedence changed.

  1054   \smallskip

  1055   *}

  1056 (*<*)

  1057 end

  1058 context step_v_cps_nt

  1059 begin

  1060 (*>*)

  1061 text {*

  1062   \noindent

  1063   \colorbox{mygrey}{@{term "V th cs"}:} We assume that @{text s'} and 

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

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

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

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

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

  1069 

  1070 

  1071   \begin{isabelle}\ \ \ \ \ %%%

  1072   @{thm depend_s}

  1073   \end{isabelle}

  1074   

  1075   \noindent

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

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

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

  1079   can show

  1080 

  1081   \begin{isabelle}\ \ \ \ \ %%%

  1082   @{thm[mode=IfThen] cp_kept}

  1083   \end{isabelle}

  1084   

  1085   \noindent

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

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

  1088   \noindent

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

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

  1091   to be recalculated.

  1092 

  1093   \begin{isabelle}\ \ \ \ \ %%%

  1094   \begin{tabular}{@ {}l}

  1095   @{thm depend_s}\\

  1096   @{thm eq_cp}

  1097   \end{tabular}

  1098   \end{isabelle}

  1099   *}

  1100 (*<*)

  1101 end

  1102 context step_P_cps_e

  1103 begin

  1104 (*>*)

  1105 

  1106 text {*

  1107   \noindent

  1108   \colorbox{mygrey}{@{term "P th cs"}:} We assume that @{text s'} and 

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

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

  1111   first by showing that

  1112   

  1113   \begin{isabelle}\ \ \ \ \ %%%

  1114   \begin{tabular}{@ {}l}

  1115   @{thm depend_s}\\

  1116   @{thm eq_cp}

  1117   \end{tabular}

  1118   \end{isabelle}

  1119 

  1120   \noindent

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

  1122   current precedence needs to be recalculated.*}(*<*)end context step_P_cps_ne begin(*>*) text {*

  1123   \noindent

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

  1125   

  1126   \begin{isabelle}\ \ \ \ \ %%%

  1127   \begin{tabular}{@ {}l}

  1128   @{thm depend_s}\\

  1129   @{thm[mode=IfThen] eq_cp}

  1130   \end{tabular}

  1131   \end{isabelle}

  1132 

  1133   \noindent

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

  1135   the current precedence for all threads that are not dependants of @{text th}

  1136   are unchanged. For the others we need to follow the edges 

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

  1138   @case of {text Set}, this operation can stop often earlier, namely when intermediate

  1139   values do not change.

  1140   *}

  1141 (*<*)

  1142 end

  1143 (*>*)

  1144 text {*

  1145   \noindent

  1146   A pleasing result of our formalisation is that the properties in

  1147   this section closely inform an implementation of PIP:  Whether the

  1148   @{text RAG} needs to be reconfigured or current precedences need to

  1149   recalculated for an event is given by a lemma we proved.

  1150 *}

  1151 

  1152 section {* Conclusion *}

  1153 

  1154 text {* 

  1155   The Priority Inheritance Protocol (PIP) is a classic textbook

  1156   algorithm used in real-time operating systems in order to avoid the problem of

  1157   Priority Inversion.  Although classic and widely used, PIP does have

  1158   its faults: for example it does not prevent deadlocks in cases where threads

  1159   have circular lock dependencies.

  1160 

  1161   We had two goals in mind with our formalisation of PIP: One is to

  1162   make the notions in the correctness proof by Sha et al.~\cite{Sha90}

  1163   precise so that they can be processed by a theorem prover. The reason is

  1164   that a mechanically checked proof avoids the flaws that crept into their

  1165   informal reasoning. We achieved this goal: The correctness of PIP now

  1166   only hinges on the assumptions behind our formal model. The reasoning, which is

  1167   sometimes quite intricate and tedious, has been checked beyond any

  1168   reasonable doubt by Isabelle/HOL. We can also confirm that Paulson's

  1169   inductive method for protocol verification~\cite{Paulson98} is quite

  1170   suitable for our formal model and proof. The traditional application

  1171   area of this method is security protocols.  The only other

  1172   application of Paulson's method we know of outside this area is

  1173   \cite{Wang09}.

  1174 

  1175   The second goal of our formalisation is to provide a specification for actually

  1176   implementing PIP. Textbooks, for example \cite[Section 5.6.5]{Vahalia96},

  1177   explain how to use various implementations of PIP and abstractly

  1178   discuss their properties, but surprisingly lack most details for a

  1179   programmer who wants to implement PIP.  That this is an issue in practice is illustrated by the

  1180   email from Baker we cited in the Introduction. We achieved also this

  1181   goal: The formalisation gives the first author enough data to enable

  1182   his undergraduate students to implement PIP (as part of their OS course)

  1183   on top of PINTOS, a small operating system for teaching

  1184   purposes. A byproduct of our formalisation effort is that nearly all

  1185   design choices for the PIP scheduler are backed up with a proved

  1186   lemma. We were also able to establish the property that the choice of

  1187   the next thread which takes over a lock is irrelevant for the correctness

  1188   of PIP. Earlier model checking approaches which verified implementations

  1189   of PIP \cite{Faria08,Jahier09,Wellings07} cannot

  1190   provide this kind of ``deep understanding'' about the principles behind 

  1191   PIP and its correctness.

  1192 

  1193   PIP is a scheduling algorithm for single-processor systems. We are

  1194   now living in a multi-processor world. So the question naturally

  1195   arises whether PIP has any relevance in such a world beyond

  1196   teaching. Priority Inversion certainly occurs also in

  1197   multi-processor systems.  However, the surprising answer, according

  1198   to \cite{Steinberg10}, is that except for one unsatisfactory

  1199   proposal nobody has a good idea for how PIP should be modified to

  1200   work correctly on multi-processor systems. The difficulties become

  1201   clear when considering that locking and releasing a resource always

  1202   requires a small amount of time. If processes work independently,

  1203   then a low priority process can ``steal'' in such an unguarded

  1204   moment a lock for a resource that was supposed allow a high-priority

  1205   process to run next. Thus the problem of Priority Inversion is not

  1206   really prevented. It seems difficult to design a PIP-algorithm with

  1207   a meaningful correctness property on a multi-processor systems where

  1208   processes work independently.  We can imagine PIP to be of use in

  1209   situations where processes are \emph{not} independent, but

  1210   coordinated via a master process that distributes work over some

  1211   slave processes. However, a formal investigation of this is beyond

  1212   the scope of this paper.  We are not aware of any proofs in this

  1213   area, not even informal ones.

  1214 

  1215   The most closely related work to ours is the formal verification in

  1216   PVS for Priority Ceiling done by Dutertre \cite{dutertre99b}. His formalisation

  1217   consists of 407 lemmas and 2500 lines of ``specification'' (we do not

  1218   know whether this includes also code for proofs).  Our formalisation

  1219   consists of around 210 lemmas and overall 6950 lines of readable Isabelle/Isar

  1220   code with a few apply-scripts interspersed. The formal model of PIP

  1221   is 385 lines long; the formal correctness proof 3800 lines. Some auxiliary

  1222   definitions and proofs took 770 lines of code. The properties relevant

  1223   for an implementation took 2000 lines.  Our code can be downloaded from

  1224   ...

  1225 

  1226   \bibliographystyle{plain}

  1227   \bibliography{root}

  1228 *}

  1229 

  1232 (*<*)

  1233 context extend_highest_gen

  1234 begin

  1235 (*>*)

  1236 

  1237 text {*

  1238   The essential of {\em Priority Inheritance} is to avoid indefinite priority inversion. For this 

  1239   purpose, we need to investigate what happens after one thread takes the highest precedence. 

  1240   A locale is used to describe such a situation, which assumes:

  1241   \begin{enumerate}

  1242   \item @{term "s"} is a valid state (@{text "vt_s"}):

  1243     @{thm  vt_s}.

  1244   \item @{term "th"} is a living thread in @{term "s"} (@{text "threads_s"}):

  1245     @{thm threads_s}.

  1246   \item @{term "th"} has the highest precedence in @{term "s"} (@{text "highest"}):

  1247     @{thm highest}.

  1248   \item The precedence of @{term "th"} is @{term "Prc prio tm"} (@{text "preced_th"}):

  1249     @{thm preced_th}.

  1250   \end{enumerate}

  1251   *}

  1252 

  1253 text {* \noindent

  1254   Under these assumptions, some basic priority can be derived for @{term "th"}:

  1255   \begin{enumerate}

  1256   \item The current precedence of @{term "th"} equals its own precedence (@{text "eq_cp_s_th"}):

  1257     @{thm [display] eq_cp_s_th}

  1258   \item The current precedence of @{term "th"} is the highest precedence in 

  1259     the system (@{text "highest_cp_preced"}):

  1260     @{thm [display] highest_cp_preced}

  1261   \item The precedence of @{term "th"} is the highest precedence 

  1262     in the system (@{text "highest_preced_thread"}):

  1263     @{thm [display] highest_preced_thread}

  1264   \item The current precedence of @{term "th"} is the highest current precedence 

  1265     in the system (@{text "highest'"}):

  1266     @{thm [display] highest'}

  1267   \end{enumerate}

  1268   *}

  1269 

  1270 text {* \noindent

  1271   To analysis what happens after state @{term "s"} a sub-locale is defined, which 

  1272   assumes:

  1273   \begin{enumerate}

  1274   \item @{term "t"} is a valid extension of @{term "s"} (@{text "vt_t"}): @{thm vt_t}.

  1275   \item Any thread created in @{term "t"} has priority no higher than @{term "prio"}, therefore

  1276     its precedence can not be higher than @{term "th"},  therefore

  1277     @{term "th"} remain to be the one with the highest precedence

  1278     (@{text "create_low"}):

  1279     @{thm [display] create_low}

  1280   \item Any adjustment of priority in 

  1281     @{term "t"} does not happen to @{term "th"} and 

  1282     the priority set is no higher than @{term "prio"}, therefore

  1283     @{term "th"} remain to be the one with the highest precedence (@{text "set_diff_low"}):

  1284     @{thm [display] set_diff_low}

  1285   \item Since we are investigating what happens to @{term "th"}, it is assumed 

  1286     @{term "th"} does not exit during @{term "t"} (@{text "exit_diff"}):

  1287     @{thm [display] exit_diff}

  1288   \end{enumerate}

  1289 *}