prio/Paper/Paper.thy
changeset 270 d98435b93063
parent 268 1baf8d0c7093
child 271 78523b3ae2ad
equal deleted inserted replaced
269:70395e3fd99f 270:d98435b93063
    22   in a naive implementation of resource looking and priorities this
    22   in a naive implementation of resource looking and priorities this
    23   property can be violated. Even worse, $H$ can be delayed
    23   property can be violated. Even worse, $H$ can be delayed
    24   indefinitely by processes with lower priorities. For this let $L$ be
    24   indefinitely by processes with lower priorities. For this let $L$ be
    25   in the possession of a lock for a resource that also $H$ needs. $H$
    25   in the possession of a lock for a resource that also $H$ needs. $H$
    26   must therefore wait for $L$ to release this lock. The problem is
    26   must therefore wait for $L$ to release this lock. The problem is
    27   that $L$ might be in turn blocked by any process with priority $M$,
    27   that $L$ might in turn be blocked by any process with priority $M$,
    28   and so $H$ sits there potentially waiting indefinitely. Since $H$ is
    28   and so $H$ sits there potentially waiting indefinitely. Since $H$ is
    29   blocked by processes with lower priorities, the problem is called
    29   blocked by processes with lower priorities, the problem is called
    30   Priority Inversion. It was first described in
    30   Priority Inversion. It was first described in
    31   \cite{Lampson:Redell:cacm:1980} in the context of the Mesa
    31   \cite{Lampson:Redell:cacm:1980} in the context of the Mesa
    32   programming language designed to support concurrent programming.
    32   programming language designed for concurrent programming.
    33 
    33 
    34   If the problem of Priority Inversion is ignored, realtime systems
    34   If the problem of Priority Inversion is ignored, realtime systems
    35   can become unpredictable and resulting bugs can be hard to diagnose.
    35   can become unpredictable and resulting bugs can be hard to diagnose.
    36   The classic example where this happened is the software that
    36   The classic example where this happened is the software that
    37   controlled the Mars Pathfinder mission in 1997
    37   controlled the Mars Pathfinder mission in 1997
    38   \cite{Reeves-Glenn-1998}.  Once the spacecraft landed, the software
    38   \cite{Reeves-Glenn-1998}.  Once the spacecraft landed, the software
    39   shut down at irregular intervals leading to loss of project time, as
    39   shut down at irregular intervals leading to loss of project time, as
    40   normal operation of the craft could only resume the next day (the
    40   normal operation of the craft could only resume the next day (the
    41   mission and data already collected was fortunately not lost, because
    41   mission and data already collected were fortunately not lost, because
    42   of a clever system design).  The reason for the shutdowns was that
    42   of a clever system design).  The reason for the shutdowns was that
    43   the schedulling software fell victim of Priority Inversion: a low
    43   the schedulling software fell victim of Priority Inversion: a low
    44   priority task locking a resource prevented a high priority process
    44   priority task locking a resource prevented a high priority process
    45   from running leading to a system reset. Once the problem was found,
    45   from running in time leading to a system reset. Once the problem was found,
    46   it was rectified by enabling the Priority Inheritance Protocol in
    46   it was rectified by enabling the Priority Inheritance Protocol in
    47   the schedulling software.
    47   the schedulling software.
    48 
    48 
    49   The idea behind the \emph{Priority Inheritance Protocol} (PIP) is to
    49   The idea behind the \emph{Priority Inheritance Protocol} (PIP) is to
    50   let the process $L$ temporarily inherit the high priority from $H$ 
    50   let the process $L$ temporarily inherit the high priority from $H$ 
    51   until $L$ releases the locked resource. This solves the problem of
    51   until $L$ releases the locked resource. This solves the problem of
    52   $H$ having to wait indefinitely, because $L$ cannot be blocked by 
    52   $H$ having to wait indefinitely, because $L$ cannot, for example, be blocked by 
    53   processes having priority $M$. This solution to the Priority
    53   processes having priority $M$. This solution to the Priority
    54   Inversion problem has been known since \cite{Lampson:Redell:cacm:1980}
    54   Inversion problem has been known since \cite{Lampson:Redell:cacm:1980}
    55   but Lui et al give the first thourough analysis and present a correctness
    55   but Lui et al give the first thourough analysis and present a correctness
    56   proof for an algorithm \cite{journals/tc/ShaRL90}.
    56   proof for an algorithm \cite{journals/tc/ShaRL90}.
    57 
    57