9 

     9 

    10 notation (latex output)

    10 notation (latex output)

    11   Cons ("_::_" [78,77] 73) and

    11   Cons ("_::_" [78,77] 73) and

    12   vt ("valid'_state") and

    12   vt ("valid'_state") and

    13   runing ("running") and

    13   runing ("running") and

    15   If  ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and

    14   If  ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and

    16   Prc ("'(_, _')") and

    15   Prc ("'(_, _')") and

    17   holding ("holds") and

    16   holding ("holds") and

    18   waiting ("waits") and

    17   waiting ("waits") and

    19   Th ("T") and

    18   Th ("T") and

    20   Cs ("C") and

    19   Cs ("C") and

    21   readys ("ready") and

    20   readys ("ready") and

    22   depend ("RAG") and 

    21   depend ("RAG") and 

    23   preced ("prec") and

    22   preced ("prec") and

    24   cpreced ("cprec") and

    23   cpreced ("cprec") and

    26   cp ("cprec") and

    24   cp ("cprec") and

    27   holdents ("resources") and

    25   holdents ("resources") and

    29   DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")

    26   DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")

    30  

    27  

    31   

    28   

    32 (*>*)

    29 (*>*)

    33 

    30 

    81   priority $M$. While a few other solutions exist for the Priority

    78   priority $M$. While a few other solutions exist for the Priority

    82   Inversion problem, PIP is one that is widely deployed and

    79   Inversion problem, PIP is one that is widely deployed and

    83   implemented. This includes VxWorks (a proprietary real-time OS used

    80   implemented. This includes VxWorks (a proprietary real-time OS used

    84   in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, Honda's

    81   in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, Honda's

    85   ASIMO robot, etc.) and ThreadX (another proprietary real-time OS

    82   ASIMO robot, etc.) and ThreadX (another proprietary real-time OS

    87   the POSIX 1003.1c Standard realised for

    84   the POSIX 1003.1c Standard realised for

    88   example in libraries for FreeBSD, Solaris and Linux. 

    85   example in libraries for FreeBSD, Solaris and Linux. 

    89 

    86 

    90   Two advantages of PIP are that it is deterministic and that increasing the priority of a thread

    87   Two advantages of PIP are that it is deterministic and that increasing the priority of a thread

    91   can be performed dynamically by the scheduler.

    88   can be performed dynamically by the scheduler.

    92   This is in contrast to \emph{Priority Ceiling}

    89   This is in contrast to \emph{Priority Ceiling}

    93   \cite{Sha90}, another solution to the Priority Inversion problem,

    90   \cite{Sha90}, another solution to the Priority Inversion problem,

    94   which requires static analysis of the program in order to prevent

    91   which requires static analysis of the program in order to prevent

    96   this problem by randomly boosting the priority of ready low-priority threads

    93   this problem by randomly boosting the priority of ready low-priority threads

    97   (see for instance~\cite{WINDOWSNT}).

    94   (see for instance~\cite{WINDOWSNT}).

    98   However, there has also been strong criticism against

    95   However, there has also been strong criticism against

    99   PIP. For instance, PIP cannot prevent deadlocks when lock

    96   PIP. For instance, PIP cannot prevent deadlocks when lock

   100   dependencies are circular, and also blocking times can be

    97   dependencies are circular, and also blocking times can be

   139 

   136 

   140   Yodaiken \cite{Yodaiken02} and also Moylan et al.~\cite{deinheritance} 

   137   Yodaiken \cite{Yodaiken02} and also Moylan et al.~\cite{deinheritance} 

   141   point to a subtlety that had been

   138   point to a subtlety that had been

   142   overlooked in the informal proof by Sha et al. They specify in

   139   overlooked in the informal proof by Sha et al. They specify in

   143   \cite{Sha90} that after the thread (whose priority has been raised)

   140   \cite{Sha90} that after the thread (whose priority has been raised)

   147   Unfortunately, as Yodaiken and Moylan et al.~point out, this behaviour is too

   144   Unfortunately, as Yodaiken and Moylan et al.~point out, this behaviour is too

   149   locks \emph{two} resources, and two high-priority threads $H$ and

   147   locks \emph{two} resources, and two high-priority threads $H$ and

   150   $H'$ each wait for one of them.  If $L$ releases one resource

   148   $H'$ each wait for one of them.  If $L$ releases one resource

   151   so that $H$, say, can proceed, then we still have Priority Inversion

   149   so that $H$, say, can proceed, then we still have Priority Inversion

   152   with $H'$ (which waits for the other resource). The correct

   150   with $H'$ (which waits for the other resource). The correct

   153   behaviour for $L$ is to switch to the highest remaining priority of

   151   behaviour for $L$ is to switch to the highest remaining priority of

   154   the threads that it blocks. A similar error is made in the textbook

   152   the threads that it blocks. A similar error is made in the textbook

   155   \cite[Section 2.3.1]{book} which specifies for a process that 

   153   \cite[Section 2.3.1]{book} which specifies for a process that 

   158    

   156    

   159   While \cite{book} and

   157   While \cite{book} and

   160   \cite{Sha90} are the only formal publications we have 

   158   \cite{Sha90} are the only formal publications we have 

   161   found that describe the incorrect behaviour, not all, but many

   159   found that describe the incorrect behaviour, not all, but many

   162   informal\footnote{informal as in ``found on the Web''} 

   160   informal\footnote{informal as in ``found on the Web''} 

   182   when a resource is released is irrelevant for PIP being correct---a

   180   when a resource is released is irrelevant for PIP being correct---a

   183   fact that has not been mentioned in the literature and not been used

   181   fact that has not been mentioned in the literature and not been used

   184   in the reference implementation of PIP in PINTOS.  This fact, however, is important

   182   in the reference implementation of PIP in PINTOS.  This fact, however, is important

   185   for an efficient implementation of PIP, because we can give the lock

   183   for an efficient implementation of PIP, because we can give the lock

   186   to the thread with the highest priority so that it terminates more

   184   to the thread with the highest priority so that it terminates more

   188   et al.~\cite{Sha90} to the practically relevant case where critical 

   186   et al.~\cite{Sha90} to the practically relevant case where critical 

   190 *}

   238 *}

   191 

   239 

   192 section {* Formal Model of the Priority Inheritance Protocol\label{model} *}

   240 section {* Formal Model of the Priority Inheritance Protocol\label{model} *}

   193 

   241 

   194 text {*

   242 text {*

   203   into five categories defined as the datatype:

   251   into five categories defined as the datatype:

   204 

   252 

   205   \begin{isabelle}\ \ \ \ \ %%%

   253   \begin{isabelle}\ \ \ \ \ %%%

   206   \mbox{\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{7mm}}l}

   254   \mbox{\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{7mm}}l}

   207   \isacommand{datatype} event 

   255   \isacommand{datatype} event 

   209   & @{text "|"} & @{term "Exit thread"} \\

   257   & @{text "|"} & @{term "Exit thread"} \\

   211   & @{text "|"} & @{term "P thread cs"} & {\rm request of resource} @{text "cs"} {\rm by} @{text "thread"}\\

   259   & @{text "|"} & @{term "P thread cs"} & {\rm request of resource} @{text "cs"} {\rm by} @{text "thread"}\\

   212   & @{text "|"} & @{term "V thread cs"} & {\rm release of resource} @{text "cs"} {\rm by} @{text "thread"}

   260   & @{text "|"} & @{term "V thread cs"} & {\rm release of resource} @{text "cs"} {\rm by} @{text "thread"}

   213   \end{tabular}}

   261   \end{tabular}}

   214   \end{isabelle}

   262   \end{isabelle}

   215 

   263 

   233   @{term "threads (DUMMY#s)"} & @{text "\<equiv>"} & @{term "threads s"}\\

   281   @{term "threads (DUMMY#s)"} & @{text "\<equiv>"} & @{term "threads s"}\\

   234   \end{tabular}}

   282   \end{tabular}}

   235   \end{isabelle}

   283   \end{isabelle}

   236 

   284 

   237   \noindent

   285   \noindent

   239   Another function calculates the priority for a thread @{text "th"}, which is 

   287   Another function calculates the priority for a thread @{text "th"}, which is 

   240   defined as

   288   defined as

   241 

   289 

   242   \begin{isabelle}\ \ \ \ \ %%%

   290   \begin{isabelle}\ \ \ \ \ %%%

   243   \mbox{\begin{tabular}{lcl}

   291   \mbox{\begin{tabular}{lcl}

   251   \end{tabular}}

   299   \end{tabular}}

   252   \end{isabelle}

   300   \end{isabelle}

   253 

   301 

   254   \noindent

   302   \noindent

   255   In this definition we set @{text 0} as the default priority for

   303   In this definition we set @{text 0} as the default priority for

   256   threads that have not (yet) been created. The last function we need 

   304   threads that have not (yet) been created. The last function we need 

   258   priority last set.

   306   priority last set.

   259 

   307 

   260   \begin{isabelle}\ \ \ \ \ %%%

   308   \begin{isabelle}\ \ \ \ \ %%%

   261   \mbox{\begin{tabular}{lcl}

   309   \mbox{\begin{tabular}{lcl}

   269   \end{tabular}}

   317   \end{tabular}}

   270   \end{isabelle}

   318   \end{isabelle}

   271 

   319 

   272   \noindent

   320   \noindent

   273   In this definition @{term "length s"} stands for the length of the list

   321   In this definition @{term "length s"} stands for the length of the list

   284   we do in case two threads have the same priority), but according to precedences. 

   332   we do in case two threads have the same priority), but according to precedences. 

   285   Precedences allow us to always discriminate between two threads with equal priority by 

   333   Precedences allow us to always discriminate between two threads with equal priority by 

   286   taking into account the time when the priority was last set. We order precedences so 

   334   taking into account the time when the priority was last set. We order precedences so 

   287   that threads with the same priority get a higher precedence if their priority has been 

   335   that threads with the same priority get a higher precedence if their priority has been 

   288   set earlier, since for such threads it is more urgent to finish their work. In an implementation

   336   set earlier, since for such threads it is more urgent to finish their work. In an implementation

   291 

   346 

   292   Next, we introduce the concept of \emph{waiting queues}. They are

   347   Next, we introduce the concept of \emph{waiting queues}. They are

   293   lists of threads associated with every resource. The first thread in

   348   lists of threads associated with every resource. The first thread in

   294   this list (i.e.~the head, or short @{term hd}) is chosen to be the one 

   349   this list (i.e.~the head, or short @{term hd}) is chosen to be the one 

   295   that is in possession of the

   350   that is in possession of the

   383 

   438 

   384   We will design our scheduler  

   439   We will design our scheduler  

   385   so that every thread can be in the possession of several resources, that is 

   440   so that every thread can be in the possession of several resources, that is 

   386   it has potentially several incoming holding edges in the RAG, but has at most one outgoing  

   441   it has potentially several incoming holding edges in the RAG, but has at most one outgoing  

   387   waiting edge. The reason is that when a thread asks for resource that is locked

   442   waiting edge. The reason is that when a thread asks for resource that is locked

   389   Clearly, also every resource can only have at most one outgoing holding edge---indicating

   444   Clearly, also every resource can only have at most one outgoing holding edge---indicating

   390   that the resource is locked. In this way we can always start at a thread waiting for a 

   445   that the resource is locked. In this way we can always start at a thread waiting for a 

   391   resource and ``chase'' outgoing arrows leading to a single root of a tree. 

   446   resource and ``chase'' outgoing arrows leading to a single root of a tree. 

   392   

   447   

   393 

   448 

   394 

   449 

   395   The use of relations for representing RAGs allows us to conveniently define

   450   The use of relations for representing RAGs allows us to conveniently define

   396   the notion of the \emph{dependants} of a thread using the transitive closure

   451   the notion of the \emph{dependants} of a thread using the transitive closure

   401   \end{isabelle}

   456   \end{isabelle}

   402 

   457 

   403   \noindent

   458   \noindent

   404   This definition needs to account for all threads that wait for a thread to

   459   This definition needs to account for all threads that wait for a thread to

   405   release a resource. This means we need to include threads that transitively

   460   release a resource. This means we need to include threads that transitively

   407   of @{text "th\<^sub>0"} are @{text "th\<^sub>1"} and @{text "th\<^sub>2"}, which wait for resource @{text "cs\<^sub>1"}, 

   462   of @{text "th\<^sub>0"} are @{text "th\<^sub>1"} and @{text "th\<^sub>2"}, which wait for resource @{text "cs\<^sub>1"}, 

   408   but also @{text "th\<^sub>3"}, 

   463   but also @{text "th\<^sub>3"}, 

   409   which cannot make any progress unless @{text "th\<^sub>2"} makes progress, which

   464   which cannot make any progress unless @{text "th\<^sub>2"} makes progress, which

   410   in turn needs to wait for @{text "th\<^sub>0"} to finish). If there is a circle of dependencies 

   465   in turn needs to wait for @{text "th\<^sub>0"} to finish). If there is a circle of dependencies 

   411   in a RAG, then clearly

   466   in a RAG, then clearly

   646   \noindent

   701   \noindent

   647   Note, however, that apart from the circularity condition, we do not make any 

   702   Note, however, that apart from the circularity condition, we do not make any 

   648   assumption on how different resources can be locked and released relative to each 

   703   assumption on how different resources can be locked and released relative to each 

   649   other. In our model it is possible that critical sections overlap. This is in 

   704   other. In our model it is possible that critical sections overlap. This is in 

   650   contrast to Sha et al \cite{Sha90} who require that critical sections are 

   705   contrast to Sha et al \cite{Sha90} who require that critical sections are 

   652 

   707 

   653   A valid state of PIP can then be conveniently be defined as follows:

   708   A valid state of PIP can then be conveniently be defined as follows:

   654 

   709 

   655   \begin{center}

   710   \begin{center}

   656   \begin{tabular}{c}

   711   \begin{tabular}{c}

   783 

   838 

   784   Like in the argument by Sha et al.~our

   839   Like in the argument by Sha et al.~our

   785   finite bound does not guarantee absence of indefinite Priority

   840   finite bound does not guarantee absence of indefinite Priority

   786   Inversion. For this we further have to assume that every thread

   841   Inversion. For this we further have to assume that every thread

   787   gives up its resources after a finite amount of time. We found that

   842   gives up its resources after a finite amount of time. We found that

   789   leave it out and let the programmer assume the responsibility to

   852   leave it out and let the programmer assume the responsibility to

   790   program threads in such a benign manner (in addition to causing no 

   853   program threads in such a benign manner (in addition to causing no 

   791   circularity in the RAG). In this detail, we do not

   854   circularity in the RAG). In this detail, we do not

   792   make any progress in comparison with the work by Sha et al.

   855   make any progress in comparison with the work by Sha et al.

   793   However, we are able to combine their two separate bounds into a

   856   However, we are able to combine their two separate bounds into a

   939   %\item When a thread is not living, it does not hold any critical resource 

  1002   %\item When a thread is not living, it does not hold any critical resource 

   940   %  (@{text "not_thread_holdents"}):

  1003   %  (@{text "not_thread_holdents"}):

   941   %  @  {thm [display] not_thread_holdents}

  1004   %  @  {thm [display] not_thread_holdents}

   942   %\item When the number of @{text "P"} equals the number of @{text "V"}, the relevant 

  1005   %\item When the number of @{text "P"} equals the number of @{text "V"}, the relevant 

   943   %  thread does not hold any critical resource, therefore no thread can depend on it

  1006   %  thread does not hold any critical resource, therefore no thread can depend on it

   946   %\end{enumerate}

  1009   %\end{enumerate}

   947 

  1010 

   948   %The reason that only threads which already held some resoures

  1011   %The reason that only threads which already held some resoures

   949   %can be runing and block @{text "th"} is that if , otherwise, one thread 

  1012   %can be runing and block @{text "th"} is that if , otherwise, one thread 

   950   %does not hold any resource, it may never have its prioirty raised

  1013   %does not hold any resource, it may never have its prioirty raised

  1255   %%@ {t hm[mode=IfThen] eq_up_self}\\

  1318   %%@ {t hm[mode=IfThen] eq_up_self}\\

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

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

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

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

  1258   \end{tabular}

  1321   \end{tabular}

  1259   \end{isabelle}

  1322   \end{isabelle}

  1261   \noindent

  1324   \noindent

  1262   This lemma states that if an intermediate @{term cp}-value does not change, then

  1325   This lemma states that if an intermediate @{term cp}-value does not change, then

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

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

  1264   have their current precedence changed.

  1327   have their current precedence changed.

  1265   *}(*<*)end(*>*)text {*

  1328   *}(*<*)end(*>*)text {*

  1267   this section closely inform an implementation of PIP, namely whether the

  1330   this section closely inform an implementation of PIP, namely whether the

  1268   RAG needs to be reconfigured or current precedences need to

  1331   RAG needs to be reconfigured or current precedences need to

  1269   be recalculated for an event. This information is provided by the lemmas we proved.

  1332   be recalculated for an event. This information is provided by the lemmas we proved.

  1270   We confirmed that our observations translate into practice by implementing

  1333   We confirmed that our observations translate into practice by implementing

  1271   our version of PIP on top of PINTOS, a small operating system written in C and used for teaching at 

  1334   our version of PIP on top of PINTOS, a small operating system written in C and used for teaching at 

  1273   functions corresponding to the events in our formal model. The events translate to the following 

  1342   functions corresponding to the events in our formal model. The events translate to the following 

  1274   function interface in PINTOS:

  1343   function interface in PINTOS:

  1275 

  1344 

  1276   \begin{center}

  1345   \begin{center}

  1277   \begin{tabular}{|l@ {\hspace{2mm}}|l@ {\hspace{2mm}}|}

  1346   \begin{tabular}{|l@ {\hspace{2mm}}|l@ {\hspace{2mm}}|}

  1448   design choices for the implementation of PIP scheduler are backed up with a proved

  1517   design choices for the implementation of PIP scheduler are backed up with a proved

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

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

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

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

  1451   of PIP. Moreover, we eliminated a crucial restriction present in 

  1520   of PIP. Moreover, we eliminated a crucial restriction present in 

  1452   the proof of Sha et al.: they require that critical sections nest properly, 

  1521   the proof of Sha et al.: they require that critical sections nest properly, 

  1454 

  1531 

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

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

  1456   now living in a multi-processor world. Priority Inversion certainly

  1533   now living in a multi-processor world. Priority Inversion certainly

  1457   occurs also there, see for example \cite{Brandenburg11,Davis11}.  

  1534   occurs also there, see for example \cite{Brandenburg11,Davis11}.  

  1458   However, there is very little ``foundational''

  1535   However, there is very little ``foundational''