regexp: comparison prio/Paper/Paper.thy

equal deleted inserted replaced

-:a5dd2c966cbe
+:6a6d0bd16035
 birthtime ("last'_set") and
 If  ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
 Prc ("'(_, _')") and
 holding ("holds") and
 waiting ("waits") and
-Th ("_") and
+Th ("T") and
-Cs ("_") and
+Cs ("C") and
 readys ("ready") and
+depend ("RAG") and
+preced ("prec") and
+cpreced ("cprec") and
 DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")
 (*>*)
 section {* Introduction *}
 algorithm for a single-processor system.\footnote{We shall come back
 later to the case of PIP on multi-processor systems.} Our model of
 PIP is based on Paulson's inductive approach to protocol
 verification \cite{Paulson98}, where the \emph{state} of a system is
 given by a list of events that happened so far.  \emph{Events} in PIP fall
-into five categories defined as the datatype
+into five categories defined as the datatype:
 \begin{isabelle}\ \ \ \ \ %%%
 \mbox{\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{7mm}}l}
 \isacommand{datatype} event
 & @{text "="} & @{term "Create thread priority"}\\
 @{term "threads (DUMMY#s)"} & @{text "\<equiv>"} & @{term "threads s"}\\
 \end{tabular}}
 \end{isabelle}
 \noindent
-Another function calculates the priority for a thread @{text "th"}, defined as
+Another function calculates the priority for a thread @{text "th"}, which is
+defined as
 \begin{isabelle}\ \ \ \ \ %%%
 \mbox{\begin{tabular}{lcl}
 @{thm (lhs) original_priority.simps(1)[where thread="th"]} & @{text "\<equiv>"} &
 @{thm (rhs) original_priority.simps(1)[where thread="th"]}\\
 \noindent
 In this definition we set @{text 0} as the default priority for
 threads that have not (yet) been created. The last function we need
 calculates the ``time'', or index, at which time a process had its
-priority set.
+priority last set.
 \begin{isabelle}\ \ \ \ \ %%%
 \mbox{\begin{tabular}{lcl}
 @{thm (lhs) birthtime.simps(1)[where thread="th"]} & @{text "\<equiv>"} &
 @{thm (rhs) birthtime.simps(1)[where thread="th"]}\\
 \noindent
 In this definition @{term "length s"} stands for the length of the list
 of events @{text s}. Again the default value in this function is @{text 0}
 for threads that have not been created yet. A \emph{precedence} of a thread @{text th} in a
-state @{text s} is a pair of natural numbers defined as
+state @{text s} is the pair of natural numbers defined as
 \begin{isabelle}\ \ \ \ \ %%%
-@{thm (rhs) preced_def[where thread="th"]}
+@{thm preced_def[where thread="th"]}
 \end{isabelle}
 \noindent
 The point of precedences is to schedule threads not according to priorities (because what should
 we do in case two threads have the same priority), but according to precedences.
-Precedences allow us to always discriminate two threads with equal priority by
+Precedences allow us to always discriminate between two threads with equal priority by
 tacking into account the time when the priority was last set. We order precedences so
 that threads with the same priority get a higher precedence if their priority has been
-set earlier, since for such threads it is more urgent to finish. In an impementation
+set earlier, since for such threads it is more urgent to finish their work. In an impementation
 this choice would translate to a quite natural a FIFO-scheduling of processes with
 the same priority.
 Next, we introduce the concept of \emph{waiting queues}. They are
 lists of threads associated with every resource. The first thread in
-this list is chosen to be in the one that is in possession of the
+this list (the head, or short @{term hd}) is chosen to be in the one
+that is in possession of the
 ``lock'' of the corresponding resource. We model waiting queues as
 functions, below abbreviated as @{text wq}, taking a resource as
 argument and returning a list of threads.  This allows us to define
-when a thread \emph{holds}, respectively \emph{waits}, for a
+when a thread \emph{holds}, respectively \emph{waits} for, a
 resource @{text cs} given a waiting queue function.
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
-@{thm s_holding_def[where thread="th"]}\\
+@{thm cs_holding_def[where thread="th"]}\\
-@{thm s_waiting_def[where thread="th"]}
+@{thm cs_waiting_def[where thread="th"]}
 \end{tabular}
 \end{isabelle}
 \noindent
 In this definition we assume @{text "set"} converts a list into a set.
+Using @{term "holding"} and @{term waiting}, we can introduce \emph{Resource Allocation Graphs}
+(RAG), which represent the dependencies between threads and resources.
+We represent RAGs 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)"}
+\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
+as
+\begin{isabelle}\ \ \ \ \ %%%
+@{thm cs_depend_def}
+\end{isabelle}
+\noindent
+An instance of a RAG is as follows:
+\begin{center}
+Picture
+\end{center}
+\noindent
+The use or relations for representing RAGs allows us to conveninetly define
+the notion of the \emph{dependants} of a thread. This is defined as
+\begin{isabelle}\ \ \ \ \ %%%
+@{thm cs_dependents_def}
+\end{isabelle}
+\noindent
+This definition needs to account for all threads that wait for tread to
+release a resource. This means we need to include threads that transitively
+wait for a resource being realeased (in the picture this means also @{text "th\<^isub>3"},
+which cannot make any progress unless @{text "th\<^isub>2"} makes progress which
+in turn waits for @{text "th\<^isub>1"}). If there is a cirle in a RAG, then clearly
+we have a deadlock. Therefore when we state our correctness property for PIP
+we must ensure that RAGs are not circular. This allows us to define the notion
+of the \emph{current precedence} of a thread @{text th} in a state @{text s}.
+\begin{isabelle}\ \ \ \ \ %%%
+@{thm cpreced_def2}\\
+\end{isabelle}
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm s_depend_def}\\
 \end{tabular}

changeset 290	6a6d0bd16035
parent 287	440382eb6427
child 291	5ef9f6ebe827