pip: comparison Journal/Paper.thy

equal deleted inserted replaced

-:fdba35b422a0
+:f933a8ad24e5
 in PIP is quite ``heavy weight'' in Linux (see the Introduction).
 In our model of PIP the current precedence of a thread in a state @{text s}
 depends on the precedenes of all threads in its subtree---a ``global'' transitive notion,
 which is indeed heavy weight (see the equation for @{text cprec} shown in \eqref{overloaded}).
 We can however improve upon this. For this recall the notion
-of @{term children} of a thread @{text th} (defined in \eqref{children})
+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
+There 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 more efficiently calculating
 @{text cprec} of a thread @{text th}.
 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
+If only the static precedence or the children-set changes, then we can
 avoid the recursion and compute the @{text cprec} of @{text th} locally.
-In this cases
+In such 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
 of the thread with highest precedence from a set of ready threads is
-a standard scheduling operation implemented in most operating
+a standard scheduling operation and implemented in most operating
 systems.
 %\begin{proof}[of Lemma~\ref{childrenlem}]
 %Test
 %\end{proof}
 subtree of any other thread. So all current precedences of other
 threads are unchanged.
 %The second
 %however states that only threads that are \emph{not} dependants of @{text th} have their
-%current precedence unchanged. For the others we have to recalculate the current
+%current precedence unchanged. For the ancestors of @{text th}, we
+%have to recalculate the current
 %precedence. To do this we can start from @{term "th"}
 %and follow the @{term "depend"}-edges to recompute  using Lemma~\ref{childrenlem}
 %the @{term "cp"} of every
 %thread encountered on the way. Since the @{term "depend"}
 %is assumed to be loop free, this procedure will always stop. The following two lemmas show, however,
 \end{tabular}
 \end{isabelle}
 \noindent That means we have to add a waiting edge to the @{text
 RAG}. Furthermore the current precedence for all threads that are
-not ancestors of @{text "th"} are unchanged. For the others we need
+not ancestors of @{text "th"} are unchanged. For the ancestors of
+@{text th} we need
 to follow the edges in the @{text TDG} and recompute the @{term
-"cp"}. To do this we can start from @{term "th"} and follow the
+"cprecs"}. Whereas in all other event we might have to make
+modifications to the @{text "RAG"}, no recalculation of @{text
+cprec} depends on the @{text RAG}. This is the only case where
+the recalulation needs to take the connections in the @{text RAG} into
+account.
+To do this we can start from @{term "th"} and follow the
 @{term "children"}-edges to recompute the @{term "cp"} of every
-thread encountered on the way using Lemma~\ref{childrenlem}. Since
+thread encountered on the way using Lemma~\ref{childrenlem}.
+This means the recomputation can be done locally (level-by-level)
+in a bottom-up fashion.
+Since
 the @{text RAG}, and thus @{text "TDG"}, are loop free, this
 procedure will always stop. The following lemma shows, however, that
 this procedure can actually stop often earlier without having to
 consider all ancestors.
 & @{thm (prem 3) valid_trace_p_w.cp_up_tG}\\
 & @{text then} @{thm (concl) valid_trace_p_w.cp_up_tG}\\
 \end{tabular}
 \end{isabelle}
-\noindent This lemma states that if an intermediate @{term cp}-value
+\noindent This property states that if an intermediate @{term cp}-value
 does not change (in this case the @{text cprec}-value of @{text "th'"}), then the procedure can
 also stop, because none of @{text "th'"} ancestor-threads will have their
 current precedence changed.
 *}
 size. Moreover, our result is a good
 witness for one of the major reasons to be interested in machine checked
 reasoning: gaining deeper understanding of the subject matter.
 Our formalisation
-consists of around 210 lemmas and overall 6950 lines of readable Isabelle/Isar
+consists of around 600 lemmas and overall 10800 lines
+of readable and commented Isabelle/Isar
 code with a few apply-scripts interspersed. The formal model of PIP
-is 385 lines long; the formal correctness proof 3800 lines. Some auxiliary
+is 620 lines long; our graph theory implementation using relations is
-definitions and proofs span over 770 lines of code. The properties relevant
+1860 lines; the basic properties of PIP take around 5500 lines of code;
-for an implementation require 2000 lines.
+and the formal correctness proof 1700 lines.
+%Some auxiliary
+%definitions and proofs span over 770 lines of code.
+The properties relevant
+for an implementation require 1000 lines.
 The code of our formalisation
 can be downloaded from the Mercurial repository at
 \url{http://www.dcs.kcl.ac.uk/staff/urbanc/cgi-bin/repos.cgi/pip}.
 %\medskip

changeset 192	f933a8ad24e5
parent 191	fdba35b422a0
child 193	c3a42076b164