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

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

    27   cntP ("c\<^bsub>P\<^esub>") and

    28   cntV ("c\<^bsub>V\<^esub>")

    35   Many real-time systems need to support threads involving priorities and

    35 

    36   locking of resources. Locking of resources ensures mutual exclusion

    36   Many real-time systems need to support threads involving priorities

    37   when accessing shared data or devices that cannot be

    37   and locking of resources. Locking of resources ensures mutual

    38   exclusion when accessing shared data or devices that cannot be

    43   $H$ blocks any other thread with lower priority and the thread itself cannot

    44   $H$ blocks any other thread with lower priority and the thread

    44   be blocked indefinitely by threads with lower priority. Alas, in a naive

    45   itself cannot be blocked indefinitely by threads with lower

    45   implementation of resource locking and priorities this property can

    46   priority. Alas, in a naive implementation of resource locking and

    46   be violated. For this let $L$ be in the

    47   priorities this property can be violated. For this let $L$ be in the

    49   lock. The problem is that $L$ might in turn be blocked by any

    50   lock. The problem is that $L$ might in turn be blocked by any thread

    50   thread with priority $M$, and so $H$ sits there potentially waiting

    51   with priority $M$, and so $H$ sits there potentially waiting

    51   indefinitely. Since $H$ is blocked by threads with lower

    52   indefinitely. Since $H$ is blocked by threads with lower priorities,

    52   priorities, the problem is called Priority Inversion. It was first

    53   the problem is called Priority Inversion. It was first described in

    53   described in \cite{Lampson80} in the context of the

    54   \cite{Lampson80} in the context of the Mesa programming language

    54   Mesa programming language designed for concurrent programming.

    55   designed for concurrent programming.

    59   controlled the Mars Pathfinder mission in 1997 \cite{Reeves98}.

    60   controlled the Mars Pathfinder mission in 1997 \cite{Reeves98}.  On

    60   On Earth the software run mostly without any problem, but

    61   Earth the software run mostly without any problem, but once the

    61   once the spacecraft landed on Mars, it shut down at irregular, but frequent,

    62   spacecraft landed on Mars, it shut down at irregular, but frequent,

    72   \emph{Priority Boosting}, \emph{Priority Donation} or \emph{Priority Lending}.} 

    73   \emph{Priority Boosting}, \emph{Priority Donation} or \emph{Priority

    73   in the scheduling software.

    74   Lending}.}  in the scheduling software.

    74 

    75 

    75   The idea behind PIP is to let the thread $L$ temporarily inherit

    76   The idea behind PIP is to let the thread $L$ temporarily inherit the

    76   the high priority from $H$ until $L$ leaves the critical section

    77   high priority from $H$ until $L$ leaves the critical section

    84   used in nearly all HP inkjet printers \cite{ThreadX}), but also

    85   used in nearly all HP inkjet printers \cite{ThreadX}), but also the

    85   the POSIX 1003.1c Standard realised for

    86   POSIX 1003.1c Standard realised for example in libraries for

    86   example in libraries for FreeBSD, Solaris and Linux. 

    87   FreeBSD, Solaris and Linux.

    87 

    88 

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

    89   Two advantages of PIP are that it is deterministic and that

    89   can be performed dynamically by the scheduler.

    90   increasing the priority of a thread can be performed dynamically by

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

    91   the scheduler.  This is in contrast to \emph{Priority Ceiling}

    93   Priority Inversion, and also in contrast to the approach taken in the Windows NT scheduler, which avoids

    94   Priority Inversion, and also in contrast to the approach taken in

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

    95   the Windows NT scheduler, which avoids this problem by randomly

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

    96   boosting the priority of ready low-priority threads (see for

    96   However, there has also been strong criticism against

    97   instance~\cite{WINDOWSNT}).  However, there has also been strong

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

    98   criticism against PIP. For instance, PIP cannot prevent deadlocks

    98   dependencies are circular, and also blocking times can be

    99   when lock dependencies are circular, and also blocking times can be

   109   \noindent

   110   \noindent He suggests avoiding PIP altogether by designing the

   110   He suggests avoiding PIP altogether by designing the system so that no 

   111   system so that no priority inversion may happen in the first

   111   priority inversion may happen in the first place. However, such ideal designs may 

   112   place. However, such ideal designs may not always be achievable in

   112   not always be achievable in practice.

   113   practice.

   115   algorithms for PIP. A few specifications for PIP exist (in English)

   116   algorithms for PIP. A few specifications for PIP exist (in informal

   116   and also a few high-level descriptions of implementations (e.g.~in

   117   English) and also a few high-level descriptions of implementations

   117   the textbooks \cite[Section 12.3.1]{Liu00} and \cite[Section 5.6.5]{Vahalia96}), 

   118   (e.g.~in the textbooks \cite[Section 12.3.1]{Liu00} and

   118   but they help little with actual implementations. That this is a problem in 

   119   \cite[Section 5.6.5]{Vahalia96}), but they help little with actual

   119   practice is proved by an email by Baker, who wrote on 13 July 2009 on the Linux

   120   implementations. That this is a problem in practice is proved by an

   120   Kernel mailing list:

   121   email by Baker, who wrote on 13 July 2009 on the Linux Kernel

   122   mailing list:

   130   \noindent

   132   \noindent The criticism by Yodaiken, Baker and others suggests

   131   The criticism by Yodaiken, Baker and others suggests another look

   133   another look at PIP from a more abstract level (but still concrete

   132   at PIP from a more abstract level (but still concrete enough

   134   enough to inform an implementation), and makes PIP a good candidate

   133   to inform an implementation), and makes PIP a good candidate for a

   135   for a formal verification. An additional reason is that the original

   134   formal verification. An additional reason is that the original

   136   ``proved'' correct, is actually \emph{flawed}. 

   137   ``proved'' correct, is actually \emph{flawed}.

   137   

   138   

   138 

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

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

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

   142   \cite{Sha90} so that after the thread (whose priority has been

   143   completes its critical section and releases the lock, it ``{\it

   143   raised) completes its critical section and releases the lock, it

   144   returns to its original priority level}''. This leads them to

   144   ``{\it returns to its original priority level}''. This leads them to

   148   al.~write that there are ``{\it some hidden traps}''~\cite{deinheritance}.  Consider the

   148   al.~write that there are ``{\it some hidden

   149   case where the low priority thread $L$ locks \emph{two} resources,

   149   traps}''~\cite{deinheritance}.  Consider the case where the low

   150   and two high-priority threads $H$ and $H'$ each wait for one of

   150   priority thread $L$ locks \emph{two} resources, and two

   151   them.  If $L$ releases one resource so that $H$, say, can proceed,

   151   high-priority threads $H$ and $H'$ each wait for one of them.  If

   152   then we still have Priority Inversion with $H'$ (which waits for the

   152   $L$ releases one resource so that $H$, say, can proceed, then we

   153   other resource). The correct behaviour for $L$ is to switch to the

   153   still have Priority Inversion with $H'$ (which waits for the other

   154   highest remaining priority of the threads that it blocks. 

   154   resource). The correct behaviour for $L$ is to switch to the highest

   155   A similar

   155   remaining priority of the threads that it blocks.  A similar error

   156   error is made in the textbook \cite[Section 2.3.1]{book} which

   156   is made in the textbook \cite[Section 2.3.1]{book} which specifies

   157   specifies for a process that inherited a higher priority and exits a

   157   for a process that inherited a higher priority and exits a critical

   158   critical section ``{\it it resumes the priority it had at the point

   158   section ``{\it it resumes the priority it had at the point of entry

   159   of entry into the critical section}''.  This error can also be

   159   into the critical section}''.  This error can also be found in the

   160   found in the more recent textbook \cite[Page 119]{Laplante11} where the

   160   more recent textbook \cite[Page 119]{Laplante11} where the authors

   161   authors state: ``{\it when [the task] exits the critical section that caused

   161   state: ``{\it when [the task] exits the critical section that caused

   164   flawed specification and even goes on to develop pseudo-code based on this

   164   flawed specification and even goes on to develop pseudo-code based

   165   flawed specification. Accordingly, the operating system primitives

   165   on this flawed specification. Accordingly, the operating system

   166   for inheritance and restoration of priorities in \cite{Liu00} depend on

   166   primitives for inheritance and restoration of priorities in

   167   maintaining a  data structure called \emph{inheritance log}. This log

   167   \cite{Liu00} depend on maintaining a data structure called

   168   is maintained for every thread and broadly specified as containing ``{\it

   168   \emph{inheritance log}. This log is maintained for every thread and

   169   [h]istorical information on how the thread inherited its current

   169   broadly specified as containing ``{\it [h]istorical information on

   170   priority}'' \cite[Page 527]{Liu00}. Unfortunately, the important

   170   how the thread inherited its current priority}'' \cite[Page

   171   information about actually

   171   527]{Liu00}. Unfortunately, the important information about actually

   172   computing the priority to be restored solely from this log is  not explained in

   172   computing the priority to be restored solely from this log is not

   173   \cite{Liu00} but left as an ``{\it excercise}'' to the reader.

   173   explained in \cite{Liu00} but left as an ``{\it excercise}'' to the

   174   Of course, a correct version of PIP does not need to maintain

   174   reader.  Of course, a correct version of PIP does not need to

   175   this (potentially expensive) data structure at all. Surprisingly

   175   maintain this (potentially expensive) data structure at

   176   also the widely read and frequently updated textbook \cite{Silberschatz13} gives

   176   all. Surprisingly also the widely read and frequently updated

   177   the wrong specification. For example on Page 254 the

   177   textbook \cite{Silberschatz13} gives the wrong specification. For

   178   authors write: ``{\it Upon releasing the lock, the [low-priority] thread

   178   example on Page 254 the authors write: ``{\it Upon releasing the

   179   will revert to its original priority.}'' The same error is also repeated

   179   lock, the [low-priority] thread will revert to its original

   180   later in this textbook.

   180   priority.}'' The same error is also repeated later in this textbook.

   181 

   181 

   182   

   182   

   183   While \cite{Laplante11,Liu00,book,Sha90,Silberschatz13} are the only formal publications we have 

   183   While \cite{Laplante11,Liu00,book,Sha90,Silberschatz13} are the only

   184   found that specify the incorrect behaviour, it seems also many

   184   formal publications we have found that specify the incorrect

   185   informal descriptions of PIP overlook the possibility that another

   185   behaviour, it seems also many informal descriptions of PIP overlook

   186   high-priority might wait for a low-priority process to finish.

   186   the possibility that another high-priority might wait for a

   187   A notable exception is the texbook \cite{buttazzo}, which gives the correct 

   187   low-priority process to finish.  A notable exception is the texbook

   188   behaviour of resetting the priority of a thread to the highest remaining priority of the 

   188   \cite{buttazzo}, which gives the correct behaviour of resetting the

   189   threads it blocks. This textbook also gives an informal proof for 

   189   priority of a thread to the highest remaining priority of the

   190   the correctness of PIP in the style of Sha et al. Unfortunately, this informal 

   190   threads it blocks. This textbook also gives an informal proof for

   191   proof is too vague to be useful for formalising the correctness of PIP

   191   the correctness of PIP in the style of Sha et al. Unfortunately,

   192   and the specification leaves out nearly all details in order 

   192   this informal proof is too vague to be useful for formalising the

   193   to implement PIP efficiently.\medskip\smallskip

   193   correctness of PIP and the specification leaves out nearly all

   194   details in order to implement PIP efficiently.\medskip\smallskip

   201   \noindent

   202   \noindent {\bf Contributions:} There have been earlier formal

   202   {\bf Contributions:} There have been earlier formal investigations

   203   investigations into PIP \cite{Faria08,Jahier09,Wellings07}, but they

   203   into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model

   204   employ model checking techniques. This paper presents a formalised

   204   checking techniques. This paper presents a formalised and

   205   and mechanically checked proof for the correctness of PIP. For this

   205   mechanically checked proof for the correctness of PIP. For this we 

   206   we needed to design a new correctness criterion for PIP. In contrast

   206   needed to design a new correctness criterion for PIP. In contrast to model checking, our

   207   to model checking, our formalisation provides insight into why PIP

   207   formalisation provides insight into why PIP is correct and allows us

   208   is correct and allows us to prove stronger properties that, as we

   208   to prove stronger properties that, as we will show, can help with an

   209   will show, can help with an efficient implementation of PIP. We

   209   efficient implementation of PIP in the educational PINTOS operating

   210   illustrate this with an implementation of PIP in the educational

   210   system \cite{PINTOS}.  For example, we found by ``playing'' with the

   211   PINTOS operating system \cite{PINTOS}.  For example, we found by

   211   formalisation that the choice of the next thread to take over a lock

   212   ``playing'' with the formalisation that the choice of the next

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

   213   thread to take over a lock when a resource is released is irrelevant

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

   214   for PIP being correct---a fact that has not been mentioned in the

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

   215   literature and not been used in the reference implementation of PIP

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

   216   in PINTOS.  This fact, however, is important for an efficient

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

   217   implementation of PIP, because we can give the lock to the thread

   217   quickly.  We were also being able to generalise the scheduler of Sha

   218   with the highest priority so that it terminates more quickly.  We

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

   219   were also being able to generalise the scheduler of Sha et

   219   sections can overlap; see Figure~\ref{overlap} \emph{a)} below for an example of 

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

   220   this restriction. %In the existing literature there is no 

   221   sections can overlap; see Figure~\ref{overlap} \emph{a)} below for

   221   %proof and also no proving method that cover this generalised case.

   222   an example of this restriction. In the existing literature there is

   223   no proof and also no proving method that cover this generalised

   224   case.

   962   The second property is by induction of @{term vt}. The next three

  1008   The second property is by induction on @{term vt}. The next three