pip: comparison Journal/Paper.thy

equal deleted inserted replaced

-:f9e6c4166476
+:cfd17cb339d1
 \end{isabelle}
 \noindent
 Using @{term "holding_raw"} and @{term waiting_raw}, we can introduce \emph{Resource Allocation Graphs}
 (RAG), which represent the dependencies between threads and resources.
-We choose to represent RAGs as relations using pairs of the form
+We choose to represent @{text "RAG"}s as relations using pairs of the form
 \begin{isabelle}\ \ \ \ \ %%%
 @{term "(Th th, Cs cs)"} \hspace{5mm}{\rm and}\hspace{5mm}
 @{term "(Cs cs, Th th)"}\hfill\numbered{pairs}
 \end{isabelle}
 \noindent
 where the first stands for a \emph{waiting edge} and the second for a
 \emph{holding edge} (@{term Cs} and @{term Th} are constructors of a
-datatype for vertices). Given a waiting queue function, a RAG is defined
+datatype for vertices). Given a waiting queue function, a @{text RAG} is defined
 as the union of the sets of waiting and holding edges, namely
 \begin{isabelle}\ \ \ \ \ %%%
 @{thm RAG_raw_def}
 \end{isabelle}
 \end{center}
 \caption{An instance of a Resource Allocation Graph (RAG).\label{RAGgraph}}
 \end{figure}
 \noindent
-If there is no cycle, then every RAG can be pictured as a forrest of trees, as
+If there is no cycle, then every @{text 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
+Because of the @{text RAG}s, 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 justification for this is that we wanted to be able to
+graphs for PIP. The justification for this is that we wanted
-reason about potentially infinite graphs (in the sense of infinitely
+to have a more general theory of graphs which is capable of
-branching and infinite size): the property that our RAGs are
+representing potentially infinite graphs (in the sense of infinitely
+branching and infinite size): the property that our @{text RAG}s are
 actually forrests 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 shown in \eqref{pairs}. The pairs stand for the edges in
 graphs. This relation-based representation is convenient since we
 can use the notions of transitive closure operations @{term "trancl
 DUMMY"} and @{term "rtrancl DUMMY"}, as well as relation
-composition.  A \emph{forrest} is defined as the relation @{text
+composition.  A \emph{forrest} is defined in our representation as the relation @{text
 rel} that is \emph{single valued} and \emph{acyclic}:
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm single_valued_def[where ?r="rel", THEN eq_reflection]}\\
 %\endnote{{\bf Lemma about overlapping paths}}
 The locking mechanism of PIP ensures that for each thread node,
-there can be many incoming holding edges in the RAG, but at most one
+there can be many incoming holding edges in the @{text RAG}, but at most one
 out going waiting edge.  The reason is that when a thread asks for
 resource that is locked already, then the thread is blocked and
 cannot ask for another resource.  Clearly, also every resource can
 only have at most one outgoing holding edge---indicating that the
 resource is locked. So if the @{text "RAG"} is well-founded and
 finite, we can always start at a thread waiting for a resource and
 ``chase'' outgoing arrows leading to a single root of a tree.
-The use of relations for representing @{text RAG}s allows us to conveniently define
+The use of relations for representing @{text RAG}s allows us to
-the \emph{thread dependants graph}
+conveniently define the \emph{Thread Dependants Graph} (TDG):
 \begin{isabelle}\ \ \ \ \ %%%
 @{thm tG_raw_def}\\
 \mbox{}\hfill\numbered{dependants}
 \end{isabelle}
 \noindent This definition represents all threads in a @{text RAG} that wait
-for a thread to release a resource, but the resource is ``hidden''.
+for a thread to release a resource, but the corresponding
-In the
+resource is ``hidden''.
-picture above this means the @{text TDG} connects @{text "th\<^sub>0"} with
+In Figure~\ref{RAGgraph} this means the @{text TDG} connects @{text "th\<^sub>0"} with
 @{text "th\<^sub>1"} and @{text "th\<^sub>2"}, which both wait for
 resource @{text "cs\<^sub>1"}; and @{text "th\<^sub>2"} with @{text "th\<^sub>3"}, which
 cannot make any progress unless @{text "th\<^sub>2"} makes progress.
 Similarly for the other threads.
 If
 While the precedence @{term prec} of any
 thread is determined statically (for example when the thread is
 created), the point of the current precedence is to dynamically
 increase this precedence, if needed according to PIP. Therefore the
 current precedence of @{text th} is given as the maximum of the
-precedence of @{text th} \emph{and} all threads that are dependants
+precedence of @{text th} \emph{and} all threads in its subtree. Since the notion of current precedence is defined as the
-of @{text th} in the state @{text s}. Since the notion of current precedence is defined as the
 transitive closure of the dependent
 threads in the @{text TDG}, we deal correctly with the problem in the informal
 algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is
 lowered prematurely (see Introduction). We again introduce an abbreviation for current
 precedeces of a set of threads, written @{text "cprecs wq s ths"}.
 @{thm (lhs) cp_def}         & @{text "\<equiv>"} & @{thm (rhs) cp_def}\\
 \end{tabular}
 \end{isabelle}
 \noindent
-With these abbreviations in place we can derive for every valid trace @{text s}
+With these abbreviations in place we can derive the following two facts
-the following two facts about  ???????
+about @{text TDG}s and @{term cprec}, which are more convenient to use in
-%@ {term dependants}
+subsequent proofs.
-and @{term cprec} (see \eqref{dependants}
-and \eqref{cpreced}): Given ????? %@ {thm (prem 1) valid_trace.cp_alt_def},
-then
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}rcl}
-@{thm tG_alt_def}\\
+@{thm (lhs) tG_alt_def}  & @{text "\<equiv>"} & @{thm (rhs) tG_alt_def}\\
-@{thm cp_s_def}\\
+@{thm (lhs) cp_s_def}  & @{text "\<equiv>"} & @{thm (rhs) cp_s_def}\\
-\end{tabular}\hfill\numbered{overloaded}
+\end{tabular}\\
-\end{isabelle}
+\mbox{}\hfill\numbered{overloaded}
+\end{isabelle}
-can introduce
+\noindent Next we can introduce
 the notion of a thread being @{term ready} in a state (i.e.~threads
 that do not wait for any resource, which are the roots of the trees
-in the RAG, see Figure~\ref{RAGgraph}). The @{term running} thread
+in the @{text RAG}, see Figure~\ref{RAGgraph}). The @{term running} thread
 is then the thread with the highest current precedence of all ready threads.
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm readys_def}\\

changeset 180	cfd17cb339d1
parent 179	f9e6c4166476
child 181	d37e0d18eddd