# HG changeset patch # User Christian Urban # Date 1498744795 -3600 # Node ID cfd17cb339d14fe51dc76dfead7f8e063f74e42a # Parent f9e6c41664760631c86dfeb1f9541fc1c0daaa44 updated diff -r f9e6c4166476 -r cfd17cb339d1 Journal/Paper.thy --- a/Journal/Paper.thy Tue Jun 27 14:49:42 2017 +0100 +++ b/Journal/Paper.thy Thu Jun 29 14:59:55 2017 +0100 @@ -498,7 +498,7 @@ \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} @@ -508,7 +508,7 @@ \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}\ \ \ \ \ %%% @@ -555,15 +555,16 @@ \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 - reason about potentially infinite graphs (in the sense of infinitely - branching and infinite size): the property that our RAGs are + graphs for PIP. The justification for this is that we wanted + to have a more general theory of graphs which is capable of + 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 @@ -573,7 +574,7 @@ 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}\ \ \ \ \ %%% @@ -614,7 +615,7 @@ %\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 @@ -623,8 +624,8 @@ 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 \emph{thread dependants graph} + The use of relations for representing @{text RAG}s allows us to + conveniently define the \emph{Thread Dependants Graph} (TDG): \begin{isabelle}\ \ \ \ \ %%% @{thm tG_raw_def}\\ @@ -632,9 +633,9 @@ \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''. - In the - picture above this means the @{text TDG} connects @{text "th\<^sub>0"} with + for a thread to release a resource, but the corresponding + resource is ``hidden''. + 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. @@ -660,8 +661,7 @@ 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 - of @{text th} in the state @{text s}. Since the notion of current precedence is defined as the + precedence of @{text th} \emph{and} all threads in its subtree. 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 @@ -798,25 +798,22 @@ \end{isabelle} \noindent - With these abbreviations in place we can derive for every valid trace @{text s} - the following two facts about ??????? - %@ {term dependants} - and @{term cprec} (see \eqref{dependants} - and \eqref{cpreced}): Given ????? %@ {thm (prem 1) valid_trace.cp_alt_def}, - then + With these abbreviations in place we can derive the following two facts + about @{text TDG}s and @{term cprec}, which are more convenient to use in + subsequent proofs. \begin{isabelle}\ \ \ \ \ %%% \begin{tabular}{@ {}rcl} - @{thm tG_alt_def}\\ - @{thm cp_s_def}\\ - \end{tabular}\hfill\numbered{overloaded} + @{thm (lhs) tG_alt_def} & @{text "\"} & @{thm (rhs) tG_alt_def}\\ + @{thm (lhs) cp_s_def} & @{text "\"} & @{thm (rhs) cp_s_def}\\ + \end{tabular}\\ + \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}\ \ \ \ \ %%% diff -r f9e6c4166476 -r cfd17cb339d1 PIPDefs.thy --- a/PIPDefs.thy Tue Jun 27 14:49:42 2017 +0100 +++ b/PIPDefs.thy Thu Jun 29 14:59:55 2017 +0100 @@ -679,8 +679,8 @@ "tG (s::state) \ tG_raw (wq s)" lemma tG_alt_def: - "tG s = {(th1, th2) | th1 th2. - \ cs. (Th th1, Cs cs) \ RAG s \ (Cs cs, Th th2) \ RAG s}" (is "?L = ?R") + "tG s = {(th\<^sub>1, th\<^sub>2) | th\<^sub>1 th\<^sub>2. + \ cs. (Th th\<^sub>1, Cs cs) \ RAG s \ (Cs cs, Th th\<^sub>2) \ RAG s}" (is "?L = ?R") by (unfold s_tG_abv s_RAG_abv tG_raw_def, simp) lemma tRAG_def_tG: "tRAG s = (map_prod Th Th) ` (tG s)" diff -r f9e6c4166476 -r cfd17cb339d1 journal.pdf Binary file journal.pdf has changed