1617 unless we put up an upper bound on the number of threads that |
1617 unless we put up an upper bound on the number of threads that |
1618 have been created upto any valid future state after @{term |
1618 have been created upto any valid future state after @{term |
1619 s}. Otherwise our PIP scheduler could be ``swamped'' with @{text |
1619 s}. Otherwise our PIP scheduler could be ``swamped'' with @{text |
1620 "Create"}-requests. So our first assumption states: |
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 |
1623 every valid state after the state {\boldmath@{text s}}:} Given the |
1623 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 |
1626 a bound @{text "BC"}, that is |
1626 a bound @{text "BC"}, that is |
1627 |
1627 |
1628 \[@{text "len (filter isCreate t) < BC"}\;.\] |
1628 \[@{text "len (filter isCreate t) < BC"}\;.\] |
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 up until a single state @{text |
1632 only finite number of threads created up until a single state @{text |
1633 "s' @ s"} after @{text s}. Instead, we need to put this bound on |
1633 "s' @ s"} after @{text s}. Instead, we need to put this bound on |
1634 the @{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 |
1635 This ensures that no matter which ``future'' state is reached, the number |
1636 of creates is finite. |
1636 of @{text "Create"}-events is finite. |
1637 |
1637 |
1638 For our second assumption about giving up resources after a finite |
1638 For our second assumption about giving up resources after a finite |
1639 amount of ``time'', let us introduce the following definition about |
1639 amount of ``time'', let us introduce the following definition about |
1640 threads that can potentially block @{text th}: |
1640 threads that can potentially block @{text th}: |
1641 |
1641 |
1642 \begin{isabelle}\ \ \ \ \ %%% |
1642 \begin{isabelle}\ \ \ \ \ %%% |
1643 @{thm blockers_def[THEN eq_reflection]} |
1643 @{thm blockers_def[THEN eq_reflection]} |
1644 \end{isabelle} |
1644 \end{isabelle} |
1645 |
1645 |
1646 \noindent This set contains all treads that are not detached in |
1646 \noindent This set contains all treads that are not detached in |
1647 state @{text s} (i.e.~they have a lock on a resource) and therefore |
1647 state @{text s}. According to our definiton of @{text "detached"}, |
1648 can potentially block @{text th} after state @{text s}. We need to |
1648 this means a thread in @{text "blockers"} either holds or waits for |
1649 make the following assumption about the threads in this set: |
1649 some resource. Our Theorem~1 implies that they can all potentially |
|
1650 block @{text th} after state @{text s}. We need to make the |
|
1651 following assumption about the threads in this set: |
1650 |
1652 |
1651 \begin{quote} |
1653 \begin{quote} |
1652 {\bf Assumptions on the threads {\boldmath{@{term "th' \<in> blockers"}}}:} |
1654 {\bf Assumptions on the threads {\boldmath{@{term "th' \<in> blockers"}}}:} |
1653 For each such @{text "th'"} there exists a finite bound @{text "BND(th')"} |
1655 For each such @{text "th'"} there exists a finite bound @{text "BND(th')"} |
1654 such that for all future |
1656 such that for all future |
1662 anymore) after a finite number of events in @{text "t @ s"}. Again |
1664 anymore) after a finite number of events in @{text "t @ s"}. Again |
1663 we have to state this bound to hold in all valid states after @{text |
1665 we have to state this bound to hold in all valid states after @{text |
1664 s}. The bound reflects how each thread @{text "th'"} is programmed: |
1666 s}. The bound reflects how each thread @{text "th'"} is programmed: |
1665 Though we cannot express what instructions a thread is executing, |
1667 Though we cannot express what instructions a thread is executing, |
1666 the events in our model correspond to the system calls made by |
1668 the events in our model correspond to the system calls made by |
1667 thread. Our @{text "BND(th')"} binds the number of these calls. |
1669 thread. Our @{text "BND(th')"} binds the number of these ``calls''. |
1668 |
1670 |
1669 The main reason for these two assumptions is that we can prove the |
1671 The main reason for these two assumptions is that we can prove the |
1670 following: The number of states after @{text s} in which the thread |
1672 following: The number of states after @{text s} in which the thread |
1671 @{text th} is not running (that is where Priority Inversion occurs) |
1673 @{text th} is not running (that is where Priority Inversion occurs) |
1672 can be bounded by the number of actions the threads in @{text |
1674 can be bounded by the number of actions the threads in @{text |
1673 blockers} perform and how many threads are newly created. This bound |
1675 blockers} perform and how many threads are newly created. To state |
1674 can be stated for all valid intermediate states @{term "t @ s"} that |
1676 our bound formally, we need to make a definition of what we mean by |
1675 can happen after @{text s}. To state our bound we need to make a |
1677 intermediate states; it will be the list of states starting from |
1676 definition of what we mean by intermediate states; it will be the |
1678 @{text s} upto the state @{text "t @ s"}. For example, suppose |
1677 list of states starting from @{text s} upto the state @{text "t @ |
1679 $\textit{t} = [\textit{e}_n, \textit{e}_{n-1}, \ldots, \textit{e}_2, |
1678 s"}. For example, suppose $\textit{t} = |
1680 \textit{e}_1]$, then the intermediate states from @{text s} upto |
1679 [\textit{e}_n, \textit{e}_{n-1}, \ldots, \textit{e}_2, \textit{e}_1]$, then |
1681 @{text "t @ s"} are |
1680 the intermediate states from @{text s} upto @{text "t @ s"} are |
|
1681 |
1682 |
1682 \begin{center} |
1683 \begin{center} |
1683 \begin{tabular}{l} |
1684 \begin{tabular}{l} |
1684 $\textit{s}$\\ |
1685 $\textit{s}$\\ |
1685 $\textit{e}_1 :: \textit{s}$\\ |
1686 $\textit{e}_1 :: \textit{s}$\\ |
1688 $\textit{e}_{n - 1} :: \ldots :: \textit{e}_2 :: \textit{e}_1 :: \textit{s}$\\ |
1689 $\textit{e}_{n - 1} :: \ldots :: \textit{e}_2 :: \textit{e}_1 :: \textit{s}$\\ |
1689 \end{tabular} |
1690 \end{tabular} |
1690 \end{center} |
1691 \end{center} |
1691 |
1692 |
1692 |
1693 |
1693 \noindent This can be defined by the following recursive function |
1694 \noindent This list of \emph{intermediate states} can be defined by |
|
1695 the following recursive function |
1694 |
1696 |
1695 \begin{center} |
1697 \begin{center} |
1696 \begin{tabular}{lcl} |
1698 \begin{tabular}{lcl} |
1697 @{text "s upto []"} & $\dn$ & $[]$\\ |
1699 @{text "s upto []"} & $\dn$ & $[]$\\ |
1698 @{text "s upto (e::es)"} & $\dn$ & @{text "(es @ s) :: s upto es"} |
1700 @{text "s upto (e::es)"} & $\dn$ & @{text "(es @ s) :: s upto es"} |