--- a/Journal/Paper.thy Tue Jul 11 17:01:50 2017 +0100
+++ b/Journal/Paper.thy Fri Jul 14 15:08:39 2017 +0100
@@ -1832,8 +1832,8 @@
of @{term children} of a thread @{text th} (defined in \eqref{children})
where a child is a thread that is only one ``hop'' away from the thread
@{text th} in the @{term TDG} (and waiting for @{text th} to release
- a resource). Using children, we can prove the following lemma for calculating
- @{text cprec}.
+ a resource). Using children, we can prove the following lemma for more efficiently calculating
+ @{text cprec} of a thread @{text th}.
\begin{lemma}\label{childrenlem}
@@ -1845,13 +1845,19 @@
\noindent
That means the current precedence of a thread @{text th} can be
- computed locally by considering only the static precedence of @{text th}
+ computed by considering the static precedence of @{text th}
and
- the current precedences of the children of @{text th}. In
- effect, it only needs to be recomputed for @{text th} when its static
- precedence is re-set or when one of
- its children changes its current precedence. This is much more efficient
- because when the @{text cprec}-value is not changed for a child,
+ the current precedences of the children of @{text th}. Their
+ @{text "cprec"}s, in general general, need to be computed by recursively decending into
+ deeper ``levels'' of the @{text TDG}.
+ However, the current precedence of a thread @{text th}, say,
+ only needs to be recomputed when @{text "(i)"} its static
+ precedence is re-set or when @{text "(ii)"} one of
+ its children changes its current precedence or when @{text "(iii)"} the children set changes
+ (for example in an @{text "V"}-event).
+ If only the static precedence or the children-set changes, the we can
+ avoid the recursion and compute the @{text cprec} of @{text th} locally.
+ In this cases
the recursion does not need to decend into the corresponding subtree.
Once the current
precedence is computed in this more efficient manner, the selection