395   for threads that have not been created yet. A \emph{precedence} of a thread @{text th} in a 

   395   for threads that have not been created yet. An actor of an event is

   396   defined as

   397 

   398   \begin{isabelle}\ \ \ \ \ %%%

   399   \mbox{\begin{tabular}{lcl}

   400   @{thm (lhs) actor.simps(5)} & @{text "\<equiv>"} & 

   401     @{thm (rhs) actor.simps(5)}\\

   402   @{thm (lhs) actor.simps(1)} & @{text "\<equiv>"} & 

   403     @{thm (rhs) actor.simps(1)}\\

   404   @{thm (lhs) actor.simps(2)} & @{text "\<equiv>"} & 

   405     @{thm (rhs) actor.simps(2)}\\

   406   @{thm (lhs) actor.simps(3)} & @{text "\<equiv>"} & 

   407     @{thm (rhs) actor.simps(3)}\\

   408   \end{tabular}}

   409   \end{isabelle}

   410 

   411 

   412 

   413 

   414 

   415   A \emph{precedence} of a thread @{text th} in a 

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

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

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

  1556   guarantee the absence of indefinite Priority Inversion. For this we

  1537   that every thread gives up its resources after a finite

  1557   further need the property that every thread gives up its resources

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

  1558   after a finite amount of time. We found that this property is not so

  1547   it forever. 

  1567   it forever (there might be a lookp in between the locking and

  1568   unlocking requests).

  1553   RAG). This was also the approach taken by Sha et al.~in their paper.

  1574   RAG). This leave-it-to-the-programmer was also the approach taken by

  1554   However, in this paper we can make an improvement: we can look at

  1575   Sha et al.~in their paper.  However, in this paper we can make an

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

  1576   improvement: we can look at the \emph{events} that are happening

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

  1577   after a Priority Inversion occurs. The events can be seen as a

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

  1578   \textbf{rough} abstraction of the ``runtime behaviour'' of threads

  1558   ``time''---when an event occured, some time must have passed.  We

  1579   and also as an abstract notion of ``time''---when a new event

  1559   can then prove a more direct bound for the absence of indefinite

  1580   happened, some time must have passed.  In this setting we can prove

  1560   Priority Inversion. This is what we shall show below.

  1581   a more direct bound for the absence of indefinite Priority

  1582   Inversion. This is what we shall show below.

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

  1586   @{term th} is blocked.  For this finiteness bound to exist, Sha et

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

  1587   al.~assume in their work that there is a finite pool of threads

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

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

  1567   hibernating threads in our model. Rather, in our model we can create

  1589   active or hibernating threads in our model. Rather, in our model we

  1568   or exit threads arbitrarily. Consequently, the avoidance of

  1590   can create or exit threads arbitrarily. Consequently, the avoidance

  1569   indefinite priority inversion we are trying to establish is in our

  1591   of indefinite priority inversion we are trying to establish is in

  1570   model not true, unless we require that the number of threads

  1592   our model not true, unless we require that the number of threads

  1580   \[@{text "len (filter isCreate (t @ s)) < BC"}\;.\]  

  1602   \[@{text "len (filter isCreate t) < BC"}\;.\]  

  1584   only finite number of threads created in the state @{text "s' @ s"}.

  1606   only finite number of threads created in a single state @{text "s' @

  1585   Instead, we need to put a bound on the @{text "Create"} events for

  1607   s"} after @{text s}.  Instead, we need to put this bound on the

  1586   all valid states after @{text s}.

  1608   @{text "Create"} events for all valid states after @{text s}.

  1597   state @{text s} (i.e.~have a lock on a resource) and therefore can

  1619   state @{text s} (i.e.~they have a lock on a resource) and therefore

  1598   potentially block @{text th} after state @{text s}. We need to make

  1620   can potentially block @{text th} after state @{text s}. We need to

  1599   the following assumption about the threads in this set:

  1621   make the following assumption about the threads in this set:

  1603   For each @{text "th'"} there exists a finite bound @{text "BND(th')"} 

  1625   For each such @{text "th'"} there exists a finite bound @{text "BND(th')"} 

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

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

  1607   \[@{text "len(actions_of th' (t @ s)) < BND(th')"}\] 

  1629   \[@{text "len (actions_of {th'} t) < BND(th')"}\] 

  1611   blocking @{term th} must become detached (that is lock no resource)

  1633   blocking @{term th} must become detached (that is lock no resource

  1612   after a finite number of events in @{text "t @ s"}. Again we have to

  1634   anymore) after a finite number of events in @{text "t @ s"}. Again

  1613   require this bound to hold in all valid states after @{text s}. The

  1635   we have to state this bound to hold in all valid states after @{text

  1614   bound reflects how each thread @{text "th'"} is programmed: Though

  1636   s}. The bound reflects how each thread @{text "th'"} is programmed:

  1615   we cannot express what instructions a thread is executing, the

  1637   Though we cannot express what instructions a thread is executing,

  1616   events in our model correspond to the system calls made by thread. Our @{text

  1638   the events in our model correspond to the system calls made by

  1617   "BND(th')"} binds the number of these calls.

  1639   thread. Our @{text "BND(th')"} binds the number of these calls.

  1621   is not running (that is where PI occurs) can be bounded by the

  1643   is not running (that is where Priority Inversion occurs) can be

  1622   number of actions the threads in @{text blockers} perform and how

  1644   bounded by the number of actions the threads in @{text blockers}

  1623   many threads are newly created. This bound can be stated for all

  1645   perform and how many threads are newly created. This bound can be

  1624   valid states @{term "t @ s"} that can happen after @{text s}. To

  1646   stated for all valid states @{term "t @ s"} that can happen after

  1625   state our bound we use the definition @{term "Postfixes t \<equiv> {p. \<exists> s'. t = s' @ p}"}.

  1647   @{text s}. To state our bound we need to make a definition of what we

  1626 

  1648   mean by intermediate states: it will be the list of traces/states starting 

  1627 

  1649   from @{text s} ending in @{text "t @ s"}

  1628 To state this we use the 

  1650 

  1629   

  1651   \begin{center}

  1630 

  1652   @{text "t @ s"},\; \ldots,\; @{text "e2 :: e1 :: s"},\;@{text "e1 :: s"},\;@{text "s"}

  1631   \begin{isabelle}\ \ \ \ \ %%%

  1653   \end{center}

  1632   @{thm bound_priority_inversion}

  1654 

  1633   \end{isabelle}

  1655   \noindent This can be defined by the following recursive functions

  1634 

  1656 

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

  1657   \begin{center}

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

  1658   \begin{tabular}{rcl}

  1637   the operations taken by blockers plus one. 

  1659   @{text "s upto t"} & $\equiv$ & @{text "if (t = []) then [s]"} \\

  1638    

  1660   & & @{text "else (t @ s) :: s upto (tail t)"}

  1639 

  1661   \end{tabular}

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

  1662   \end{center}

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

  1663   

  1642 

  1664 

  1643 

  1665   \noindent Assume you have an extension @{text t}, this essentially 

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

  1666   defines in out list representation of states all the postfixes of 

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

  1667   @{text t}.

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

  1668 

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

  1669   Theorem: 

  1648   the correctness of PIP. 

  1670 

  1671   \begin{isabelle}\ \ \ \ \ %%%

  1672   @{text "len (filter (\<lambda>t'. th \<notin> running t') (s upto t)) \<le>

  1673   1 + len (actions_of blockers t) + len (filter isCreate t)"}

  1674   \end{isabelle}

  1675 

  1676   Proof:

  1677   

  1678   Consider the states @{text "s upto t"}. It holds that all the states where

  1679   @{text "th"} runs and all the states where @{text "th"} does not run is 

  1680   equalt to @{text "1 + len t"}. That means

  1681 

  1682   \begin{center}

  1683   @{text "states where th does not run = 1 + len t - states where th runs"} (*)

  1684   \end{center}

  1685 

  1686   It also holds that all the actions of @{text "th"} are less or equal to 

  1687   the states where @{text th} runs. That is

  1688 

  1689   \begin{center}

  1690   @{text "len (actions_of {th} t) \<le> states where th runs"}

  1691   \end{center}

  1692   

  1693   That means in $(*)$ we have 

  1694 

  1695   \begin{center}

  1696   @{text "states where th does not run \<le> 1 + len t - len (actions_of {th} t)"}

  1697   \end{center}

  1698 

  1699   If we look at all the events that can occur in @{text "s upto t"}, we have that

  1700 

  1701   \begin{center}

  1702   @{text "len t = len (action_of {th}) + len (action_of blockers t) + 

  1703   len (filter isCreate t)"}

  1704   \end{center}

  1705 

  1706   This gives us finally our theorem. \hfill\qed\medskip

  1707 

  1708   \noindent In order to now show the absence of indefinite Priority

  1709   Inversion, we need to show that the number of actions of the @{text

  1710   "blockers"} is bounded---the number of @{text "Creates"} is clearly

  1711   bounded by our first assumption. The number of actions of each

  1712   individual thread in @{text "blockers"} is bound by our second

  1713   assumption.  Since there can only be a finite number of @{text

  1714   blockers} in state @{text s} their overall sum is also bounded.

  1715   This is actually the main conclusion we obtain for the Priority

  1716   Inheritance Protocol: this above theorem shows is that set of @{text

  1717   blockers} is fixed at state @{text s} when the Priority Inversion

  1718   occured and no additional blocker of @{text th} can appear after the

  1719   state @{text s}. And in this way we can bound the number of states

  1720   where the thread @{text th} with the highest priority is prevented

  1721   fropm running.