1523 section {* Avoiding Indefinite Priority Inversion *}

  1523 section {* A Finite Bound on Priority Inversion *}

  1526      Like in the argument by Sha et al.~our finite bound does not

  1526 

  1527   guarantee absence of indefinite Priority Inversion. For this we

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

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

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

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

  1530   awkward to formalise in our model. There are mainly two reasons for

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

  1531   this: First, we do not specify what ``running'' the code of a thread

  1532   reasons for this: First, we do not specify what ``running'' the code

  1532   means, for example by giving an operational semantics for machine

  1533   of a thread means, for example by giving an operational semantics

  1533   instructions. Therefore we cannot characterise what are ``good''

  1534   for machine instructions. Therefore we cannot characterise what are

  1534   programs that contain for every looking request also a corresponding

  1535   ``good'' programs that contain for every looking request also a

  1535   unlocking request for a resource. Second, we would need to specify a

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

  1536   kind of global clock that tracks the time how long a thread locks a

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

  1537   resource. But this seems difficult, because how do we conveniently

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

  1538   distinguish between a thread that ``just'' locks a resource for a

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

  1539   very long time and one that locks it forever.  Therefore we decided

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

  1540   to leave out this property and let the programmer assume the

  1541 

  1542   Therefore we decided in our earlier paper \cite{ZhangUrbanWu12} to

  1543   leave out this property and let the programmer assume the

  1542   addition to causing no circularity in the RAG). In this detail, we

  1545   addition to causing no circularity in the RAG). However, in this

  1546   paper we can make an improvement: 

  1547 

  1548 In this detail, we

  1545   single theorem improving their bound.

  1551   single theorem improving their bound. We can characterise a 

  1552   program