equal
deleted
inserted
replaced
1827 in PIP is quite ``heavy weight'' in Linux (see the Introduction). |
1827 in PIP is quite ``heavy weight'' in Linux (see the Introduction). |
1828 In our model of PIP the current precedence of a thread in a state @{text s} |
1828 In our model of PIP the current precedence of a thread in a state @{text s} |
1829 depends on the precedenes of all threads in its subtree---a ``global'' transitive notion, |
1829 depends on the precedenes of all threads in its subtree---a ``global'' transitive notion, |
1830 which is indeed heavy weight (see the equation for @{text cprec} shown in \eqref{overloaded}). |
1830 which is indeed heavy weight (see the equation for @{text cprec} shown in \eqref{overloaded}). |
1831 We can however improve upon this. For this recall the notion |
1831 We can however improve upon this. For this recall the notion |
1832 of @{term children} of @{text th} (defined in \eqref{children}) |
1832 of @{term children} of a thread @{text th} (defined in \eqref{children}) |
1833 where a child is a thread that is only one ``hop'' away from the thread |
1833 where a child is a thread that is only one ``hop'' away from the thread |
1834 @{text th} in the @{term TDG} (and waiting for @{text th} to release |
1834 @{text th} in the @{term TDG} (and waiting for @{text th} to release |
1835 a resource). With this we can prove the following lemma. |
1835 a resource). Using children, we can prove the following lemma for calculating |
|
1836 @{text cprec}. |
1836 |
1837 |
1837 |
1838 |
1838 \begin{lemma}\label{childrenlem} |
1839 \begin{lemma}\label{childrenlem} |
1839 @{text "If"} @{thm (prem 1) valid_trace.cp_rec_tG} @{text "then"} |
1840 @{text "If"} @{thm (prem 1) valid_trace.cp_rec_tG} @{text "then"} |
1840 \begin{center} |
1841 \begin{center} |
1845 \noindent |
1846 \noindent |
1846 That means the current precedence of a thread @{text th} can be |
1847 That means the current precedence of a thread @{text th} can be |
1847 computed locally by considering only the static precedence of @{text th} |
1848 computed locally by considering only the static precedence of @{text th} |
1848 and |
1849 and |
1849 the current precedences of the children of @{text th}. In |
1850 the current precedences of the children of @{text th}. In |
1850 effect, it only needs to be recomputed for @{text th} when one of |
1851 effect, it only needs to be recomputed for @{text th} when its static |
|
1852 precedence is re-set or when one of |
1851 its children changes its current precedence. This is much more efficient |
1853 its children changes its current precedence. This is much more efficient |
1852 because when the @{text cprec}-value is not changed for a child, |
1854 because when the @{text cprec}-value is not changed for a child, |
1853 the recursion does not need to decend into the corresponding subtree. |
1855 the recursion does not need to decend into the corresponding subtree. |
1854 Once the current |
1856 Once the current |
1855 precedence is computed in this more efficient manner, the selection |
1857 precedence is computed in this more efficient manner, the selection |
1867 kind of events.\smallskip |
1869 kind of events.\smallskip |
1868 *} |
1870 *} |
1869 |
1871 |
1870 text {* |
1872 text {* |
1871 \noindent |
1873 \noindent |
1872 \colorbox{mygrey}{@{term "Create th prio"}:} We assume that the current state @{text s'} and |
1874 \colorbox{mygrey}{@{term "Create th prio"}:} We assume that the current state @{text s} and |
1873 the next state @{term "s \<equiv> Create th prio#s'"} are both valid (meaning the event |
1875 the next state @{term "e#s"}, where \mbox{@{term "e = Create th prio"}}, are both valid (meaning the event |
1874 is allowed to occur). In this situation we can show that |
1876 is allowed to occur in @{text s}). In this situation we can show that |
1875 |
1877 |
1876 \begin{isabelle}\ \ \ \ \ %%% |
1878 \begin{isabelle}\ \ \ \ \ %%% |
1877 \begin{tabular}{@ {}l} |
1879 \begin{tabular}{@ {}l} |
1878 HERE ?? %@ {thm eq_dep},\\ |
1880 @{thm (concl) valid_trace_create.RAG_es},\\ |
1879 @{thm valid_trace_create.eq_cp_th}, and\\ |
1881 @{thm (concl) valid_trace_create.eq_cp_th}, and\\ |
1880 @{thm[mode=IfThen] valid_trace_create.eq_cp} |
1882 @{text "If"} @{thm (prem 2) valid_trace_create.eq_cp} @{text "then"} @{thm (concl) valid_trace_create.eq_cp} |
1881 \end{tabular} |
1883 \end{tabular} |
1882 \end{isabelle} |
1884 \end{isabelle} |
1883 |
1885 |
1884 \noindent |
1886 \noindent |
1885 This means in an implementation we do not have to recalculate the @{text RAG} and also none of the |
1887 This means in an implementation we do not have to recalculate the @{text RAG} and also none of the |