prio/Paper/Paper.thy
changeset 268 1baf8d0c7093
parent 267 83fb18cadd2b
child 270 d98435b93063
equal deleted inserted replaced
267:83fb18cadd2b 268:1baf8d0c7093
    12 text {*
    12 text {*
    13   Many realtime systems need to support processes with priorities and
    13   Many realtime systems need to support processes with priorities and
    14   locking of resources. Locking of resources ensures mutual exclusion
    14   locking of resources. Locking of resources ensures mutual exclusion
    15   when accessing shared data or devices. Priorities allow schedulling
    15   when accessing shared data or devices. Priorities allow schedulling
    16   of processes that need to finish their work within hard deadlines.
    16   of processes that need to finish their work within hard deadlines.
    17   Unfortunately, both features can interact in subtle ways leading to a
    17   Unfortunately, both features can interact in subtle ways leading to
    18   problem, called \emph{Priority Inversion}. Suppose three processes
    18   a problem, called \emph{Priority Inversion}. Suppose three processes
    19   having priorities $H$(igh), $M$(edium) and $L$(ow). We would expect
    19   having priorities $H$(igh), $M$(edium) and $L$(ow). We would expect
    20   that the process $H$ blocks any other process with lower priority
    20   that the process $H$ blocks any other process with lower priority
    21   and itself cannot be blocked by a process with lower priority. Alas,
    21   and itself cannot be blocked by a process with lower priority. Alas,
    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 that 
    26   must therefore wait for $L$ to release this lock. The problem is
    27   $L$ might be in turn blocked by any process with priority $M$, and so
    27   that $L$ might be in turn blocked by any process with priority $M$,
    28   $H$ sits there potentially waiting indefinitely. Since $H$ is blocked
    28   and so $H$ sits there potentially waiting indefinitely. Since $H$ is
    29   by processes with lower priorities, the problem
    29   blocked by processes with lower priorities, the problem is called
    30   is called Priority Inversion.
    30   Priority Inversion. It was first described in
       
    31   \cite{Lampson:Redell:cacm:1980} in the context of the Mesa
       
    32   programming language designed to support concurrent programming.
    31 
    33 
    32   If the problem of Priority Inversion is ignored, realtime systems
    34   If the problem of Priority Inversion is ignored, realtime systems
    33   can become unpredictable and resulting bugs can be hard to diagnose.
    35   can become unpredictable and resulting bugs can be hard to diagnose.
    34   The classic example where this happened is the software that
    36   The classic example where this happened is the software that
    35   controlled the Mars Pathfinder mission in 1997.  Once the spacecraft
    37   controlled the Mars Pathfinder mission in 1997
    36   landed, the software shut down at irregular intervals leading to
    38   \cite{Reeves-Glenn-1998}.  Once the spacecraft landed, the software
    37   loss of project time, as normal operation of the craft could only
    39   shut down at irregular intervals leading to loss of project time, as
    38   resume the next day (the mission and data already collected was
    40   normal operation of the craft could only resume the next day (the
    39   fortunately not lost, because of a clever system design).  The
    41   mission and data already collected was fortunately not lost, because
    40   problem was that the schedulling software fell victim of Priority
    42   of a clever system design).  The reason for the shutdowns was that
    41   Inversion: a low priority task locking a resource prevented a high
    43   the schedulling software fell victim of Priority Inversion: a low
    42   priority process from running.  Once found, the problem could be
    44   priority task locking a resource prevented a high priority process
    43   rectified by enabling the Priority Inheritance Protocol in the
    45   from running leading to a system reset. Once the problem was found,
    44   schedulling software.
    46   it was rectified by enabling the Priority Inheritance Protocol in
       
    47   the schedulling software.
    45 
    48 
    46   The idea behind the \emph{Priority Inheritance Protocol} (PIP) is to
    49   The idea behind the \emph{Priority Inheritance Protocol} (PIP) is to
    47   temporarily inherit the low priority process the higher priority
    50   let the process $L$ temporarily inherit the high priority from $H$ 
    48   until it released the locked resource.
    51   until $L$ releases the locked resource. This solves the problem of
       
    52   $H$ having to wait indefinitely, because $L$ cannot be blocked by 
       
    53   processes having priority $M$. This solution to the Priority
       
    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
       
    56   proof for an algorithm \cite{journals/tc/ShaRL90}.
    49 
    57 
    50   However, there are further subtleties: just lowering the priority 
    58   However, there are further subtleties: just lowering the priority 
    51   of the process $L$ to its low priority, as proposed in ???, is 
    59   of the process $L$ to its low priority, as proposed in ???, is 
    52   incorrect.\bigskip
    60   incorrect.\bigskip
    53   
    61