pip: comparison Journal/Paper.thy

equal deleted inserted replaced

-:10c16b85a839
+:c5a65d98191a
 text {*
 The Priority Inheritance Protocol, short PIP, is a scheduling
 algorithm for a single-processor system.\footnote{We shall come back
 later to the case of PIP on multi-processor systems.}
 Following good experience in earlier work \cite{Wang09},
-our model of PIP is based on Paulson's inductive approach to protocol
+our model of PIP is based on Paulson's inductive approach for protocol
 verification \cite{Paulson98}. In this approach a \emph{state} of a system is
 given by a list of events that happened so far (with new events prepended to the list).
 \emph{Events} of PIP fall
 into five categories defined as the datatype:
 \noindent
 If there is no cycle, then every RAG can be pictured as a forrest of trees, as
 for example in Figure~\ref{RAGgraph}.
+Because of the RAGs, we will need to formalise some results about graphs.
 While there are few formalisations for graphs already implemented in
 Isabelle, we choose to introduce our own library of graphs for
 PIP. The reason for this is that we wanted to be able to reason with
 potentially infinite graphs (in the sense of infinitely branching
 and infinite size): the property that our RAGs are actually forrests
-of finitely branching trees having only an finite depth should be a
+of finitely branching trees having only an finite depth should be
 something we can \emph{prove} for our model of PIP---it should not
 be an assumption we build already into our model. It seemed for our
 purposes the most convenient represeantation of graphs are binary
 relations given by sets of pairs from \eqref{pairs}. The pairs stand for the edges in
 graphs. This relation-based representation is convenient since we
 @{thm subtree_def[where ?r="rel" and ?x="node", THEN eq_reflection]}\\
 @{thm ancestors_def[where ?r="rel" and ?x="node", THEN eq_reflection]}\\
 \end{tabular}
 \end{isabelle}
-\noindent Note that forests can have trees with infinte depth and
+\noindent Note that forrests can have trees with infinte depth and
 containing nodes with infinitely many children.  A \emph{finite
-forrest} is a forest which is well-founded and every node has
+forrest} is a forrest which is well-founded and every node has
 finitely many children (is only finitely branching).
 \endnote{
 \begin{isabelle}\ \ \ \ \ %%%
 @{thm rtrancl_path.intros}
 \end{isabelle}}
 \endnote{{\bf Lemma about overlapping paths}}
+The locking mechanism of PIP ensures that for each thread node,
-We will design our PIP-scheduler
+there can be many incoming holding edges in the RAG, but at most one
-so that every thread can be in the possession of several resources, that is
+out going waiting edge.  The reason is that when a thread asks for
-it has potentially several incoming holding edges in the RAG, but has at most one outgoing
+resource that is locked already, then the thread is blocked and
-waiting edge. The reason is that when a thread asks for resource that is locked
+cannot ask for another resource.  Clearly, also every resource can
-already, then the thread is blocked and cannot ask for another resource.
+only have at most one outgoing holding edge---indicating that the
-Clearly, also every resource can only have at most one outgoing holding edge---indicating
+resource is locked. So if the @{text "RAG"} is well-founded and
-that the resource is locked. In this way we can always start at a thread waiting for a
+finite, we can always start at a thread waiting for a resource and
-resource and ``chase'' outgoing arrows leading to a single root of a tree.
+``chase'' outgoing arrows leading to a single root of a tree.
 The use of relations for representing RAGs allows us to conveniently define
 the notion of the \emph{dependants} of a thread using the transitive closure
 operation for relations, written ~@{term "trancl DUMMY"}. This gives
 which in turn needs to wait for @{text "th\<^sub>0"} to finish). If
 there is a circle of dependencies in a RAG, then clearly we have a
 deadlock. Therefore when a thread requests a resource, we must
 ensure that the resulting RAG is not circular. In practice, the
 programmer has to ensure this. Our model will assume that critical
-reseources can only be requested provided no circularity can arise.
+resources can only be requested provided no circularity can arise.
 Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a
 state @{text s}. It is defined as
 \begin{isabelle}\ \ \ \ \ %%%

changeset 143	c5a65d98191a
parent 142	10c16b85a839
child 144	e4d151d761c4