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 a thread @{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). Using children, we can prove the following lemma for calculating |
1835 a resource). Using children, we can prove the following lemma for more efficiently calculating |
1836 @{text cprec}. |
1836 @{text cprec} of a thread @{text th}. |
1837 |
1837 |
1838 |
1838 |
1839 \begin{lemma}\label{childrenlem} |
1839 \begin{lemma}\label{childrenlem} |
1840 @{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"} |
1841 \begin{center} |
1841 \begin{center} |
1843 \end{center} |
1843 \end{center} |
1844 \end{lemma} |
1844 \end{lemma} |
1845 |
1845 |
1846 \noindent |
1846 \noindent |
1847 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 |
1848 computed locally by considering only the static precedence of @{text th} |
1848 computed by considering the static precedence of @{text th} |
1849 and |
1849 and |
1850 the current precedences of the children of @{text th}. In |
1850 the current precedences of the children of @{text th}. Their |
1851 effect, it only needs to be recomputed for @{text th} when its static |
1851 @{text "cprec"}s, in general general, need to be computed by recursively decending into |
1852 precedence is re-set or when one of |
1852 deeper ``levels'' of the @{text TDG}. |
1853 its children changes its current precedence. This is much more efficient |
1853 However, the current precedence of a thread @{text th}, say, |
1854 because when the @{text cprec}-value is not changed for a child, |
1854 only needs to be recomputed when @{text "(i)"} its static |
|
1855 precedence is re-set or when @{text "(ii)"} one of |
|
1856 its children changes its current precedence or when @{text "(iii)"} the children set changes |
|
1857 (for example in an @{text "V"}-event). |
|
1858 If only the static precedence or the children-set changes, the we can |
|
1859 avoid the recursion and compute the @{text cprec} of @{text th} locally. |
|
1860 In this cases |
1855 the recursion does not need to decend into the corresponding subtree. |
1861 the recursion does not need to decend into the corresponding subtree. |
1856 Once the current |
1862 Once the current |
1857 precedence is computed in this more efficient manner, the selection |
1863 precedence is computed in this more efficient manner, the selection |
1858 of the thread with highest precedence from a set of ready threads is |
1864 of the thread with highest precedence from a set of ready threads is |
1859 a standard scheduling operation implemented in most operating |
1865 a standard scheduling operation implemented in most operating |