1599 improvement by establishing a finite bound on the duration of |
1599 improvement by establishing a finite bound on the duration of |
1600 Priority Inversion measured by the number of events. The events can |
1600 Priority Inversion measured by the number of events. The events can |
1601 be seen as a \textit{rough(!)} abstraction of the ``runtime |
1601 be seen as a \textit{rough(!)} abstraction of the ``runtime |
1602 behaviour'' of threads and also as an abstract notion of |
1602 behaviour'' of threads and also as an abstract notion of |
1603 ``time''---when a new event happened, some time must have passed. |
1603 ``time''---when a new event happened, some time must have passed. |
1604 In this setting we can prove a more direct bound for the absence of |
1604 |
1605 indefinite Priority Inversion. This is what we shall show below. |
|
1606 |
1605 |
1607 What we will establish in this section is that there can only be a |
1606 What we will establish in this section is that there can only be a |
1608 finite number of states after state @{term s} in which the thread |
1607 finite number of states after state @{term s} in which the thread |
1609 @{term th} is blocked. For this finiteness bound to exist, Sha et |
1608 @{term th} is blocked. For this finiteness bound to exist, Sha et |
1610 al.~informally make two assumtions: first, there is a finite pool of |
1609 al.~informally make two assumtions: first, there is a finite pool of |
1613 have this concept of active or hibernating threads in our model. In |
1612 have this concept of active or hibernating threads in our model. In |
1614 fact we can dispence with the first assumption altogether and allow |
1613 fact we can dispence with the first assumption altogether and allow |
1615 that in our model we can create or exit threads |
1614 that in our model we can create or exit threads |
1616 arbitrarily. Consequently, the avoidance of indefinite priority |
1615 arbitrarily. Consequently, the avoidance of indefinite priority |
1617 inversion we are trying to establish is in our model not true, |
1616 inversion we are trying to establish is in our model not true, |
1618 unless we require that the number of threads created is bounded in |
1617 unless we put up an upper bound on the number of threads that |
1619 every valid future state after @{term s}. So our first assumption |
1618 have been created upto any valid future state after @{term |
1620 states: |
1619 s}. Otherwise our PIP scheduler could be ``swamped'' with @{text |
|
1620 "Create"}-requests. So our first assumption states: |
1621 |
1621 |
1622 \begin{quote} {\bf Assumption on the number of threads created in |
1622 \begin{quote} {\bf Assumption on the number of threads created in |
1623 every valid state after the state {\boldmath@{text s}}:} Given the |
1623 every valid state after the state {\boldmath@{text s}}:} Given the |
1624 state @{text s}, in every ``future'' valid state @{text "t @ s"}, we |
1624 state @{text s}, in every ``future'' valid state @{text "t @ s"}, we |
1625 require that the number of created threads is less than |
1625 require that the number of created threads is less than |
1627 |
1627 |
1628 \[@{text "len (filter isCreate t) < BC"}\;.\] |
1628 \[@{text "len (filter isCreate t) < BC"}\;.\] |
1629 \end{quote} |
1629 \end{quote} |
1630 |
1630 |
1631 \noindent Note that it is not enough to just to state that there are |
1631 \noindent Note that it is not enough to just to state that there are |
1632 only finite number of threads created in a single state @{text "s' @ |
1632 only finite number of threads created up until a single state @{text |
1633 s"} after @{text s}. Instead, we need to put this bound on the |
1633 "s' @ s"} after @{text s}. Instead, we need to put this bound on |
1634 @{text "Create"} events for all valid states after @{text s}. |
1634 the @{text "Create"} events for all valid states after @{text s}. |
|
1635 This ensures that no matter which ``future'' state is reached, the number |
|
1636 of creates is finite. |
1635 |
1637 |
1636 For our second assumption about giving up resources after a finite |
1638 For our second assumption about giving up resources after a finite |
1637 amount of ``time'', let us introduce the following definition about |
1639 amount of ``time'', let us introduce the following definition about |
1638 threads that can potentially block @{text th}: |
1640 threads that can potentially block @{text th}: |
1639 |
1641 |