prio/Paper/Paper.thy
changeset 324 41e4b331ce08
parent 323 eee031cc9634
child 325 163cd8034e5b
equal deleted inserted replaced
323:eee031cc9634 324:41e4b331ce08
   599 (*>*)
   599 (*>*)
   600 text {* 
   600 text {* 
   601   Sha et al.~\cite[Theorem 6]{Sha90} state their correctness criterion
   601   Sha et al.~\cite[Theorem 6]{Sha90} state their correctness criterion
   602   for PIP in terms of the number of critical resources: if there are
   602   for PIP in terms of the number of critical resources: if there are
   603   @{text m} critical resources, then a blocked job with high priority
   603   @{text m} critical resources, then a blocked job with high priority
   604   can only be blocked @{text m} times---that is a \emph{bounded} number of
   604   can only be blocked @{text m} times---that is a \emph{bounded}
   605   times. This result on its own, strictly speaking, does \emph{not} prevent Priority
   605   number of times. This result on its own, strictly speaking, does
   606   Inversion, because if one low-priority thread does not give up its
   606   \emph{not} prevent indefinite, or unbounded, Priority Inversion,
   607   critical resource (the high-priority thread is waiting for), then the
   607   because if one low-priority thread does not give up its critical
       
   608   resource (the one the high-priority thread is waiting for), then the
   608   high-priority thread can never run.  The argument of Sha et al.~is
   609   high-priority thread can never run.  The argument of Sha et al.~is
   609   that \emph{if} threads release locked resources in a finite amount
   610   that \emph{if} threads release locked resources in a finite amount
   610   of time, then Priority Inversion cannot occur---the high-priority
   611   of time, then indefinite Priority Inversion cannot occur---the high-priority
   611   thread is guaranteed to run eventually. The assumption is that
   612   thread is guaranteed to run eventually. The assumption is that
   612   programmers always ensure that this is the case.  However, even
   613   programmers always ensure that this is the case.  However, even
   613   taking this assumption into account, ther correctness property is \emph{not}
   614   taking this assumption into account, ther correctness property is
   614   true for their version of PIP. As Yodaiken
   615   \emph{not} true for their version of PIP. As Yodaiken
   615   \cite{Yodaiken02} pointed out: If a low-priority thread possesses locks to two
   616   \cite{Yodaiken02} pointed out: If a low-priority thread possesses
   616   resources for which two high-priority threads are waiting for, then
   617   locks to two resources for which two high-priority threads are
   617   lowering the priority prematurely after giving up only one lock, can
   618   waiting for, then lowering the priority prematurely after giving up
   618   cause Priority Inversion for one of the high-priority threads, invalidating
   619   only one lock, can cause indefinite Priority Inversion for one of the
   619   their bound.
   620   high-priority threads, invalidating their bound.
   620 
   621 
   621   Even when fixed, their proof idea does not seem to go through for
   622   Even when fixed, their proof idea does not seem to go through for
   622   us, because of the way we have set up our formal model of PIP.  The
   623   us, because of the way we have set up our formal model of PIP.  The
   623   reason is that we allow that critical sections can intersect
   624   reason is that we allow that critical sections can intersect
   624   (something Sha et al.~explicitly exclude).  Therefore we have a 
   625   (something Sha et al.~explicitly exclude).  Therefore we have a 
   686   if @{term "th' \<in> running (s' @ s)"} and @{text "th' \<noteq> th"} then
   687   if @{term "th' \<in> running (s' @ s)"} and @{text "th' \<noteq> th"} then
   687   @{text "th' \<in> threads s"}.
   688   @{text "th' \<in> threads s"}.
   688   \end{theorem}
   689   \end{theorem}
   689 
   690 
   690   \noindent
   691   \noindent
   691   This theorem ensures that the thread @{text th}, which has the highest 
   692   This theorem ensures that the thread @{text th}, which has the
   692   precedence in the state @{text s}, can only be blocked in the state @{text "s' @ s"} 
   693   highest precedence in the state @{text s}, can only be blocked in
   693   by a thread @{text th'} that already existed in @{text s}. As we shall see shortly,
   694   the state @{text "s' @ s"} by a thread @{text th'} that already
   694   that means by only finitely many threads. Consequently, indefinite wait of
   695   existed in @{text s}. As we shall see shortly, that means by only
   695   @{text th}---which would be Priority Inversion---cannot occur.
   696   finitely many threads. Like in the argument by Sha et al.~this
       
   697   finite bound does not guarantee absence of indefinite Priority
       
   698   Inversion. For this we further have to assume that every thread
       
   699   gives up its resources after a finite amount of time. We found that
       
   700   this assumption is awkward to formalise in our model. Therefore we
       
   701   leave it out and let the programmer assume the responsibility to
       
   702   program threads in such a benign manner. In this detail, we do not
       
   703   make any progress in comparison with the work by Sha et al.
   696 
   704 
   697   In what follows we will describe properties of PIP that allow us to prove 
   705   In what follows we will describe properties of PIP that allow us to prove 
   698   Theorem~\ref{mainthm}. It is relatively easily to see that
   706   Theorem~\ref{mainthm}. It is relatively easily to see that
   699 
   707 
   700   \begin{isabelle}\ \ \ \ \ %%%
   708   \begin{isabelle}\ \ \ \ \ %%%