1527   Like in the argument by Sha et al.~our result does not

  1531   Like in the argument by Sha et al.~our result does not yet guarantee

  1528   yet guarantee absence of indefinite Priority Inversion. For this we

  1532   absence of indefinite Priority Inversion. For this we further have

  1529   further have to assume that every thread gives up its resources

  1533   to assume that every thread gives up its resources after a finite

  1530   after a finite amount of time. We found that this assumption is not

  1534   amount of time. We found that this assumption is not so

  1531   so straightforward to formalise in our model. There are mainly two

  1535   straightforward to formalise in our model. There are mainly two

  1536   corresponding unlocking request for a resource. Second, we would

  1540   corresponding unlocking request for a resource.  Second, we can

  1537   need to specify a kind of global clock that tracks the time how long

  1541   distinghish between a thread that ``just'' locks a resource for a

  1538   a thread locks a resource. But this seems difficult, because how do

  1542   finite amount of time (even if it is very long) and one that locks

  1539   we conveniently distinguish between a thread that ``just'' locks a

  1543   it forever. But this seems difficut.

  1540   resource for a very long time and one that locks it forever.

  1546   paper we can make an improvement: 

  1549   paper we can make an improvement: we can look at the \emph{events}

  1547 

  1550   that are happening once a Priority Inversion occurs. The events can

  1548 In this detail, we

  1551   be seen as a rough abstraction of the ``runtime behaviour'' of

  1549   do not make any progress in comparison with the work by Sha et al.

  1552   threads and also as an abstract notion for ``time''.  We can then

  1550   However, we are able to combine their two separate bounds into a

  1553   prove a more direct result for the absence of indefinite Priority

  1551   single theorem improving their bound. We can characterise a 

  1554   Inversion. For this let us introduce the following definition:

  1552   program

  1555 

  1556   \begin{isabelle}\ \ \ \ \ %%%

  1557   @{thm blockers_def}

  1558   \end{isabelle}

  1559 

  1560   \noindent This set contains all treads that can potentially block

  1561   @{text th} after state @{text s}.

  1562 

  1555 

  1565 (*<*)

  1566 end

  1567 (*>*)