1548 |
1548 |
1549 Because of these problems, we decided in our earlier paper |
1549 Because of these problems, we decided in our earlier paper |
1550 \cite{ZhangUrbanWu12} to leave out this property and let the |
1550 \cite{ZhangUrbanWu12} to leave out this property and let the |
1551 programmer assume the responsibility to program threads in such a |
1551 programmer assume the responsibility to program threads in such a |
1552 benign manner (in addition to causing no circularity in the |
1552 benign manner (in addition to causing no circularity in the |
1553 RAG). However, in this paper we can make an improvement: we can look |
1553 RAG). This was also the approach taken by Sha et al.~in their paper. |
|
1554 However, in this paper we can make an improvement: we can look |
1554 at the \emph{events} that are happening once a Priority Inversion |
1555 at the \emph{events} that are happening once a Priority Inversion |
1555 occurs. The events can be seen as a rough abstraction of the |
1556 occurs. The events can be seen as a rough abstraction of the |
1556 ``runtime behaviour'' of threads and also as an abstract notion of |
1557 ``runtime behaviour'' of threads and also as an abstract notion of |
1557 ``time''. We can then prove a more direct bound for the absence of |
1558 ``time''. We can then prove a more direct bound for the absence of |
1558 indefinite Priority Inversion. |
1559 indefinite Priority Inversion. |
1563 their work that there is a finite pool of threads (active or |
1564 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). However, we do not have this concept of active or |
1565 hibernating threads in our model, but we can create or exit threads |
1566 hibernating threads in our model, but we can create or exit threads |
1566 arbitrarily. Consequently, in our model the avoidance of indefinite |
1567 arbitrarily. Consequently, in our model the avoidance of indefinite |
1567 priority inversion we are trying to establish is not true, unless we |
1568 priority inversion we are trying to establish is not true, unless we |
1568 require that there number of threads is bounded in every |
1569 require that there number of threads created is bounded in every |
1569 valid future state after @{term s}. So our first assumption |
1570 valid future state after @{term s}. So our first assumption |
1570 states |
1571 states |
1571 |
1572 |
1572 \begin{quote} {\bf Assumption on the number of threads created in |
1573 \begin{quote} {\bf Assumption on the number of threads created in |
1573 every valid state after the state {\boldmath@{text s}}:} Given the |
1574 every valid state after the state {\boldmath@{text s}}:} Given the |
1576 @{text "BC"}, that is @{text "len (filter isCreate (t @ s)) < |
1577 @{text "BC"}, that is @{text "len (filter isCreate (t @ s)) < |
1577 BC"}. \end{quote} |
1578 BC"}. \end{quote} |
1578 |
1579 |
1579 \noindent Note that it is not enough for us to just to state that there |
1580 \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 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 need to put a bound on the @{text "Create"} events for all valid |
1582 states after @{text s}. |
1583 states after @{text s}. |
1583 |
1584 |
1584 For our assumption about giving up resources after a finite amount of ``time'', |
1585 For our second assumption about giving up resources after a finite |
1585 let us introduce the following definition: |
1586 amount of ``time'', let us introduce the following definition: |
1586 |
1587 |
1587 \begin{isabelle}\ \ \ \ \ %%% |
1588 \begin{isabelle}\ \ \ \ \ %%% |
1588 @{thm blockers_def} |
1589 @{thm blockers_def} |
1589 \end{isabelle} |
1590 \end{isabelle} |
1590 |
1591 |
1592 @{text th} after state @{text s}. We need to make the following |
1593 @{text th} after state @{text s}. We need to make the following |
1593 assumption for the threads in this set: |
1594 assumption for the threads in this set: |
1594 |
1595 |
1595 \begin{quote} |
1596 \begin{quote} |
1596 {\bf Assumptions on the threads {\boldmath{@{term "th' \<in> blockers"}}}:} |
1597 {\bf Assumptions on the threads {\boldmath{@{term "th' \<in> blockers"}}}:} |
1597 There exists a finite bound @{text BND} such that for all future |
1598 For each @{text "th'"} there exists a finite bound @{text "BND(th')"} |
|
1599 such that for all future |
1598 valid states @{text "t @ s"}, |
1600 valid states @{text "t @ s"}, |
1599 we have that if @{term "\<not>(detached (t @ s) th')"}, then |
1601 we have that if @{term "\<not>(detached (t @ s) th')"}, then |
1600 @{term "len(actions_of th' (t @ s)) < BND"}. |
1602 @{text "len(actions_of th' (t @ s)) < BND(th')"}. |
1601 \end{quote} |
1603 \end{quote} |
1602 |
1604 |
1603 \noindent |
1605 \noindent By this assumption we enforce that any thread blocking |
1604 By this we mean that any thread that can block @{term th} must become |
1606 @{term th} must become detached (that is hold no resource) after a |
1605 detached (that is hold no resource) after a finite number of events |
1607 finite number of events in @{text "t @ s"}. Again we have to require |
1606 in @{text "t @ s"}. |
1608 this bound to hold in all valid states after @{text s}. The bound |
1607 |
1609 reflects how each thread @{text "th'"} is programmed: Though we cannot |
1608 Now we can prove a lemma which gives a upper bound |
1610 express what instructions a thread is executing, the events correspond |
1609 of the occurrence number when the most urgent thread @{term th} is blocked. |
1611 to the system calls made by thread. Our @{text "BND(th')"} bounds |
|
1612 the number of these calls. |
|
1613 |
|
1614 The main reason for these two assumptions is that we can prove: |
|
1615 |
|
1616 |
|
1617 \begin{isabelle}\ \ \ \ \ %%% |
|
1618 @{thm bound_priority_inversion} |
|
1619 \end{isabelle} |
1610 |
1620 |
1611 It says, the occasions when @{term th} is blocked during period @{term t} |
1621 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 |
1622 is no more than the number of @{term Create}-operations and |
1613 the operations taken by blockers plus one. |
1623 the operations taken by blockers plus one. |
1614 |
1624 |
1615 \begin{isabelle}\ \ \ \ \ %%% |
1625 |
1616 @{thm bound_priority_inversion} |
1626 Now we can prove a lemma which gives a upper bound |
1617 \end{isabelle} |
1627 of the occurrence number when the most urgent thread @{term th} is blocked. |
1618 |
1628 |
1619 |
1629 |
1620 Since the length of @{term t} may extend indefinitely, if @{term t} is full |
1630 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. |
1631 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 |
1632 And, since @{term t} can extend indefinitely, @{term th} my be blocked indefinitely |