591 \begin{isabelle}\ \ \ \ \ %%% |
591 \begin{isabelle}\ \ \ \ \ %%% |
592 \begin{tabular}{@ {}l} |
592 \begin{tabular}{@ {}l} |
593 @{thm children_def[where ?r="rel" and ?x="node", THEN eq_reflection]}\\ |
593 @{thm children_def[where ?r="rel" and ?x="node", THEN eq_reflection]}\\ |
594 @{thm subtree_def[where ?r="rel" and ?x="node", THEN eq_reflection]}\\ |
594 @{thm subtree_def[where ?r="rel" and ?x="node", THEN eq_reflection]}\\ |
595 @{thm ancestors_def[where ?r="rel" and ?x="node", THEN eq_reflection]}\\ |
595 @{thm ancestors_def[where ?r="rel" and ?x="node", THEN eq_reflection]}\\ |
596 \end{tabular} |
596 \end{tabular}\\ |
|
597 \mbox{}\hfill\numbered{children} |
597 \end{isabelle} |
598 \end{isabelle} |
598 |
599 |
599 \noindent Note that forrests can have trees with infinte depth and |
600 \noindent Note that forrests can have trees with infinte depth and |
600 containing nodes with infinitely many children. A \emph{finite |
601 containing nodes with infinitely many children. A \emph{finite |
601 forrest} is a forrest which is well-founded and every node has |
602 forrest} is a forrest which is well-founded and every node has |
1823 While our formalised proof gives us confidence about the correctness of our model of PIP, |
1824 While our formalised proof gives us confidence about the correctness of our model of PIP, |
1824 we found that the formalisation can even help us with efficiently implementing it. |
1825 we found that the formalisation can even help us with efficiently implementing it. |
1825 For example Baker complained that calculating the current precedence |
1826 For example Baker complained that calculating the current precedence |
1826 in PIP is quite ``heavy weight'' in Linux (see the Introduction). |
1827 in PIP is quite ``heavy weight'' in Linux (see the Introduction). |
1827 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} |
1828 depends on all its dependants---a ``global'' transitive notion, |
1829 depends on the precedenes of all threads in its subtree---a ``global'' transitive notion, |
1829 which is indeed heavy weight (see Definition shown in \eqref{cpreced}). |
1830 which is indeed heavy weight (see the equation for @{text cprec} shown in \eqref{overloaded}). |
1830 We can however improve upon this. For this let us define the notion |
1831 We can however improve upon this. For this recall the notion |
1831 of @{term children} of a thread @{text th} in a state @{text s} as |
1832 of @{term children} of @{text th} (defined in \eqref{children}) |
1832 |
|
1833 \begin{isabelle}\ \ \ \ \ %%% |
|
1834 \begin{tabular}{@ {}l} |
|
1835 ?? @{thm children_def} |
|
1836 \end{tabular} |
|
1837 \end{isabelle} |
|
1838 |
|
1839 \noindent |
|
1840 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 |
1841 @{text th} in the @{term RAG} (and waiting for @{text th} to release |
1834 @{text th} in the @{term TDG} (and waiting for @{text th} to release |
1842 a resource). We can prove the following lemma. |
1835 a resource). With this we can prove the following lemma. |
1843 |
1836 |
|
1837 |
|
1838 \begin{lemma}\label{childrenlem} |
|
1839 @{text "If"} @{thm (prem 1) valid_trace.cp_rec_tG} @{text "then"} |
1844 \begin{center} |
1840 \begin{center} |
1845 @{thm tG_alt_def}\\ |
1841 @{thm (concl) valid_trace.cp_rec_tG}. |
1846 ???? %@ {thm dependants_alt_tG} |
|
1847 \end{center} |
|
1848 |
|
1849 \begin{center} |
|
1850 ???? %@ {thm valid_trace.cp_alt_def3} |
|
1851 \end{center} |
|
1852 |
|
1853 |
|
1854 \begin{lemma}\label{childrenlem} |
|
1855 HERE %@ {text "If"} @ {thm (prem 1) cp_rec} @{text "then"} |
|
1856 \begin{center} |
|
1857 @{thm valid_trace.cp_rec_tG}. |
|
1858 %@ {thm (concl) cp_rec}. |
|
1859 \end{center} |
1842 \end{center} |
1860 \end{lemma} |
1843 \end{lemma} |
1861 |
1844 |
1862 \noindent |
1845 \noindent |
1863 That means the current precedence of a thread @{text th} can be |
1846 That means the current precedence of a thread @{text th} can be |
1864 computed locally by considering only the current precedences of the children of @{text th}. In |
1847 computed locally by considering only the static precedence of @{text th} |
|
1848 and |
|
1849 the current precedences of the children of @{text th}. In |
1865 effect, it only needs to be recomputed for @{text th} when one of |
1850 effect, it only needs to be recomputed for @{text th} when one of |
1866 its children changes its current precedence. Once the current |
1851 its children changes its current precedence. This is much more efficient |
|
1852 because when the @{text cprec}-value is not changed for a child, |
|
1853 the recursion does not need to decend into the corresponding subtree. |
|
1854 Once the current |
1867 precedence is computed in this more efficient manner, the selection |
1855 precedence is computed in this more efficient manner, the selection |
1868 of the thread with highest precedence from a set of ready threads is |
1856 of the thread with highest precedence from a set of ready threads is |
1869 a standard scheduling operation implemented in most operating |
1857 a standard scheduling operation implemented in most operating |
1870 systems. |
1858 systems. |
1871 |
1859 |