prio/Paper/Paper.thy
changeset 271 78523b3ae2ad
parent 270 d98435b93063
child 272 ee4611c1e13c
equal deleted inserted replaced
270:d98435b93063 271:78523b3ae2ad
     1 (*<*)
     1 (*<*)
     2 theory Paper
     2 theory Paper
     3 imports CpsG ExtGG LaTeXsugar
     3 imports CpsG ExtGG "~~/src/HOL/Library/LaTeXsugar"
     4 begin
     4 begin
     5 ML {*
     5 ML {*
     6   Printer.show_question_marks_default := false;
     6   Printer.show_question_marks_default := false;
     7   *}
     7   *}
     8 (*>*)
     8 (*>*)
    10 section {* Introduction *}
    10 section {* Introduction *}
    11 
    11 
    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 scheduling
    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
    17   Unfortunately, both features can interact in subtle ways leading to
    18   a 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
    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 were 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 scheduling 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 in time 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 scheduling 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, for example, 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 thorough 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 
    58   However, there are further subtleties: just lowering the priority 
    58   However, there are further subtleties: just lowering the priority 
    59   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 
    60   incorrect.\bigskip
    60   incorrect.\bigskip