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

  1535   Like in the work by Sha et al.~our result in Thm 1 does not yet guarantee

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

  1536   absence of indefinite Priority Inversion. For this we further need the property

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

  1537   that every thread gives up its resources after a finite

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

  1538   amount of time. We found that this property is not so

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

  1543   ``good'' programs that contain for every locking request also a

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

  1544   corresponding unlocking request for a resource.  Second, we need to

  1543   it forever. But this seems difficut.

  1547   it forever. 

  1544 

  1548 

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

  1549   Because of these problems, we decided in our earlier paper

  1546   leave out this property and let the programmer assume the

  1550   \cite{ZhangUrbanWu12} to leave out this property and let the

  1547   responsibility to program threads in such a benign manner (in

  1551   programmer assume the responsibility to program threads in such a

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

  1552   benign manner (in addition to causing no circularity in the

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

  1553   RAG). However, in this paper we can make an improvement: we can look

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

  1554   at the \emph{events} that are happening once a Priority Inversion

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

  1555   occurs. The events can be seen as a rough abstraction of the

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

  1556   ``runtime behaviour'' of threads and also as an abstract notion of

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

  1557   ``time''.  We can then prove a more direct bound for the absence of

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

  1558   indefinite Priority Inversion.

  1559 

  1560   What we will establish in this section is that there can only be a

  1561   finite amount of states after state @{term s} in which the thread

  1562   @{term th} is blocked. For this to be true, Sha et al.~assume in

  1563   their work that there is a finite pool of threads (active or

  1564   hibernating). However, we do not have this concept of active or

  1565   hibernating threads in our model, but we can create or exit threads

  1566   arbitrarily. Consequently, in our model the avoidance of indefinite

  1567   priority inversion we are trying to establish is not true, unless we

  1568   require that there number of threads is bounded in every

  1569   valid future state after @{term s}. So our first assumption 

  1570   states

  1571 

  1572   \begin{quote} {\bf Assumption on the number of threads created in

  1573   every valid state after the state {\boldmath@{text s}}:} Given the

  1574   state @{text s}, in every ``future'' valid state @{text "t @ s"}, we

  1575   require that the number of created threads is less than

  1576   @{text "BC"}, that is @{text "len (filter isCreate (t @ s)) <

  1577   BC"}.  \end{quote}

  1578 

  1579   \noindent Note that it is not enough for us to just to state that there

  1580   are only finite number of threads created in the state @{text "s' @ s"}.  Instead, we

  1581   need to put a bound on the @{text "Create"} event for all valid 

  1582   states after @{text s}. 

  1583 

  1584   For our assumption about giving up resources after a finite amount of ``time'',

  1585   let us introduce the following definition:

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

  1592   @{text th} after state @{text s}. We need to make the following

  1593   assumption for the threads in this set:

  1594 

  1595   \begin{quote}

  1596   {\bf Assumptions on the threads {\boldmath{@{term "th' \<in> blockers"}}}:} 

  1597   There exists a finite bound @{text BND} such that for all future 

  1598   valid states @{text "t @ s"},

  1599   we have that if @{term "\<not>(detached (t @ s) th')"}, then 

  1600   @{term "len(actions_of th' (t @ s)) < BND"}. 

  1601   \end{quote}

  1602 

  1603   \noindent

  1604   By this we mean that any thread that can block @{term th} must become

  1605   detached (that is hold no resource) after a finite number of events 

  1606   in @{text "t @ s"}.

  1607   

  1608   Now we can prove a lemma which gives a upper bound

  1609   of the occurrence number when the most urgent thread @{term th} is blocked.

  1610 

  1611   It says, the occasions when @{term th} is blocked during period @{term t} 

  1612   is no more than the number of @{term Create}-operations and 

  1613   the operations taken by blockers plus one. 

  1614 

  1615   \begin{isabelle}\ \ \ \ \ %%%

  1616   @{thm bound_priority_inversion}

  1617   \end{isabelle}

  1618 

  1619 

  1620   Since the length of @{term t} may extend indefinitely, if @{term t} is full

  1621   of the above mentioned blocking operations, @{term th} may have not chance to run. 

  1622   And, since @{term t} can extend indefinitely, @{term th} my be blocked indefinitely 

  1623   with the growth of @{term t}. Therefore, this lemma alone does not ensure 

  1624   the correctness of PIP.