regexp: comparison prio/Paper/Paper.thy

equal deleted inserted replaced

-:463bed130705
+:5113aa1ae69a
 \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
+as the union of the sets of waiting and holding edges, namely
 \begin{isabelle}\ \ \ \ \ %%%
 @{thm cs_depend_def}
 \end{isabelle}
 \noindent
-Given three threads and three resources, an instance of a RAG is as follows:
+Given three threads and three resources, an instance of a RAG can be pictured
+as follows:
 \begin{center}
 \newcommand{\fnt}{\fontsize{7}{8}\selectfont}
 \begin{tikzpicture}[scale=1]
 %%\draw[step=2mm] (-3,2) grid (1,-1);
 \end{tikzpicture}
 \end{center}
 \noindent
 The use of relations for representing RAGs allows us to conveniently define
-the notion of the \emph{dependants} of a thread. This is defined as
+the notion of the \emph{dependants} of a thread using the transitive closure
+operation for relations. This gives
 \begin{isabelle}\ \ \ \ \ %%%
 @{thm cs_dependents_def}
 \end{isabelle}
 \noindent
 This definition needs to account for all threads that wait for a thread to
 release a resource. This means we need to include threads that transitively
 wait for a resource being released (in the picture above this means the dependants
-of @{text "th\<^isub>0"} are @{text "th\<^isub>1"} and @{text "th\<^isub>2"}, but also @{text "th\<^isub>3"},
+of @{text "th\<^isub>0"} are @{text "th\<^isub>1"} and @{text "th\<^isub>2"}, which wait for resource @{text "cs\<^isub>1"},
+but also @{text "th\<^isub>3"},
 which cannot make any progress unless @{text "th\<^isub>2"} makes progress, which
-in turn needs to wait for @{text "th\<^isub>1"} to finish). If there is a circle in a RAG, then clearly
+in turn needs to wait for @{text "th\<^isub>0"} to finish). If there is a circle 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.
 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}\ \ \ \ \ %%%
 @{thm cpreced_def2}\hfill\numbered{cpreced}
 \end{isabelle}
 \noindent
+where the dependants of @{text th} are given by the waiting queue function.
 While the precedence @{term prec} of a thread is determined by the programmer
 (for example when the thread is
-created), the point of the current precedence is to let scheduler increase this
+created), the point of the current precedence is to let the scheduler increase this
-priority, if needed according to PIP. Therefore the current precedence of @{text th} is
+precedence, if needed according to PIP. Therefore the current precedence of @{text th} is
 given as the maximum of the precedence @{text th} has in state @{text s} \emph{and} all
-processes that are dependants of @{text th}. Since the notion @{term "dependants"} is
+threads that are dependants of @{text th}. Since the notion @{term "dependants"} is
 defined as the transitive closure of all dependent threads, we deal correctly with the
-problem in the algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is
+problem in the informal algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is
 lowered prematurely.
 The next function, called @{term schs}, defines the behaviour of the scheduler. It will be defined
-by recursion on the state (a list of events); @{term "schs"} returns a \emph{schedule state}, which
+by recursion on the state (a list of events); this function returns a \emph{schedule state}, which
 we represent as a record consisting of two
 functions:
 \begin{isabelle}\ \ \ \ \ %%%
 @{text "\<lparr>wq_fun, cprec_fun\<rparr>"}
 \end{isabelle}
 \noindent
-The first function is a waiting queue function (that is it takes a resource @{text "cs"} and returns the
+The first function is a waiting queue function (that is, it takes a resource @{text "cs"} and returns the
 corresponding list of threads that wait for it), the second is a function that takes
 a thread and returns its current precedence (see \eqref{cpreced}). We assume the usual getter and
 setter methods for such records.
-In the initial state, the scheduler starts with all resources unlocked (see \eqref{allunlocked}) and the
+In the initial state, the scheduler starts with all resources unlocked (the corresponding
+function is defined in \eqref{allunlocked}) and the
 current precedence of every thread is initialised with @{term "Prc 0 0"}; that means
 \mbox{@{abbrev initial_cprec}}. Therefore
-we have
+we have for the initial state
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm (lhs) schs.simps(1)} @{text "\<equiv>"}\\
 \hspace{5mm}@{term "(|wq_fun = all_unlocked, cprec_fun = (\<lambda>_::thread. Prc 0 0)|)"}
 \noindent
 The cases for @{term Create}, @{term Exit} and @{term Set} are also straightforward:
 we calculate the waiting queue function of the (previous) state @{text s};
 this waiting queue function @{text wq} is unchanged in the next schedule state---because
-none of these events lock or release any resources;
+none of these events lock or release any resource;
-for calculating the next @{term "cprec_fun"}, we use @{text wq} and the function
+for calculating the next @{term "cprec_fun"}, we use @{text wq} and
 @{term cpreced}. This gives the following three clauses for @{term schs}:
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm (lhs) schs.simps(2)} @{text "\<equiv>"}\\
 \hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Set th prio # s)|)"}
 \end{tabular}
 \end{isabelle}
 \noindent
-More interesting are the cases when a resource, say @{text cs}, is locked or released. In these cases
+More interesting are the cases where a resource, say @{text cs}, is locked or released. In these cases
 we need to calculate a new waiting queue function. For the event @{term "P th cs"}, we have to update
-the function so that the new thread list for @{text cs} is old thread list plus the thread @{text th}
+the function so that the new thread list for @{text cs} is the old thread list plus the thread @{text th}
 appended to the end of that list (remember the head of this list is seen to be in the possession of this
-resource).
+resource). This gives the clause
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm (lhs) schs.simps(5)} @{text "\<equiv>"}\\
 \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
 \noindent
 The clause for event @{term "V th cs"} is similar, except that we need to update the waiting queue function
 so that the thread that possessed the lock is deleted from the corresponding thread list. For this
 list transformation, we use
 the auxiliary function @{term release}. A simple version of @{term release} would
-just delete this thread and return the rest, namely
+just delete this thread and return the remaining threads, namely
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}lcl}
 @{term "release []"} & @{text "\<equiv>"} & @{term "[]"}\\
 @{term "release (DUMMY # qs)"} & @{text "\<equiv>"} & @{term "qs"}\\
 @{term "release (DUMMY # qs)"} & @{text "\<equiv>"} & @{term "SOME qs'. distinct qs' \<and> set qs' = set qs"}\\
 \end{tabular}
 \end{isabelle}
 \noindent
-@{text "SOME"} stands for Hilbert's epsilon and implements an arbitrary
+where @{text "SOME"} stands for Hilbert's epsilon and implements an arbitrary
 choice for the next waiting list. It just has to be a list of distinctive threads and
 contain the same elements as @{text "qs"}. This gives for @{term V} the clause:
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm runing_def}\\
 \end{tabular}
 \end{isabelle}
 \noindent
-In this definition @{term "f ` S"} stands for the set @{text S} under the image of the
+In this definition @{term "DUMMY ` DUMMY"} stands for the image of a set under a function.
-function @{text f}.
+Note that in the initial state, that is where the list of events is empty, the set
-Note that in the initial case, that is where the list of events is empty, the set
 @{term threads} is empty and therefore there is no thread ready nor a running.
 If there is one or more threads ready, then there can only be \emph{one} thread
 running, namely the one whose current precedence is equal to the maximum of all ready
 threads. We use the set-comprehension to capture both possibilities.
-We can now also define the set of resources that are locked by a thread in any
+We can now also conveniently define the set of resources that are locked by a thread in a
 given state.
 \begin{isabelle}\ \ \ \ \ %%%
 @{thm holdents_def}
 \end{isabelle}
-\noindent
+Finally we can define what a \emph{valid state} is in our model of PIP. For
-These resources are given by the holding edges in the RAG.
-Finally we can define what a \emph{valid state} is in our PIP. For
 example we cannot expect to be able to exit a thread, if it was not
-created yet. These validity constraints are characterised by the
+created yet. These validity constraints on states are characterised by the
-inductive predicate @{term "step"}. We give five inference rules
+inductive predicate @{term "step"} and @{term vt}. We first give five inference rules
-relating a state and an event that can happen next.
+for @{term step} relating a state and an event that can happen next.
 \begin{center}
 \begin{tabular}{c}
 @{thm[mode=Rule] thread_create[where thread=th]}\hspace{1cm}
 @{thm[mode=Rule] thread_exit[where thread=th]}
 \end{center}
 \noindent
 The first rule states that a thread can only be created, if it does not yet exists.
 Similarly, the second rule states that a thread can only be terminated if it was
-running and does not lock any resources anymore (to simplify ). The event @{text Set} can happen
+running and does not lock any resources anymore (this simplifies slightly our model;
+in practice we would expect the operating system releases all held lock of a
+thread that is about to exit). The event @{text Set} can happen
 if the corresponding thread is running.
 \begin{center}
 @{thm[mode=Rule] thread_set[where thread=th]}
 \end{center}
 \noindent
 If a thread wants to lock a resource, then the thread needs to be
 running and also we have to make sure that the resource lock does
 not lead to a cycle in the RAG. In practice, ensuring the latter is
-of course the responsibility of the programmer.  Here in our formal
+of course the responsibility of the programmer.  In our formal
 model we just exclude such problematic cases in order to make
 some meaningful statements about PIP.\footnote{This situation is
 similar to the infamous occurs check in Prolog: in order to say
-anything meaningful about unification, we need to perform an occurs
+anything meaningful about unification, one needs to perform an occurs
-check; but in practice the occurs check is ommited and the
+check, but in practice the occurs check is ommited and the
-responsibility to avoid problems rests with the programmer.}
+responsibility for avoiding problems rests with the programmer.}
+\begin{center}
+@{thm[mode=Rule] thread_P[where thread=th]}
+\end{center}
+\noindent
 Similarly, if a thread wants to release a lock on a resource, then
 it must be running and in the possession of that lock. This is
-formally given by the last two inference rules of @{term step}.
+formally given by the last inference rule of @{term step}.
 \begin{center}
-\begin{tabular}{c}
+@{thm[mode=Rule] thread_V[where thread=th]}
-@{thm[mode=Rule] thread_P[where thread=th]}\medskip\\
-@{thm[mode=Rule] thread_V[where thread=th]}\\
-\end{tabular}
 \end{center}
 \noindent
 A valid state of PIP can then be conveniently be defined as follows:
 \begin{center}
 \begin{tabular}{c}

changeset 306	5113aa1ae69a
parent 305	463bed130705
child 307	a2d4450b4bf3