--- a/prio/Paper/Paper.thy Sun Feb 12 23:25:49 2012 +0000
+++ b/prio/Paper/Paper.thy Mon Feb 13 00:06:59 2012 +0000
@@ -303,14 +303,15 @@
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}
@@ -336,7 +337,8 @@
\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}
@@ -346,9 +348,10 @@
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.
@@ -360,18 +363,19 @@
\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
- priority, if needed according to PIP. Therefore the current precedence of @{text th} is
+ created), the point of the current precedence is to let the scheduler increase this
+ 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:
@@ -380,15 +384,16 @@
\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}
@@ -401,8 +406,8 @@
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;
- for calculating the next @{term "cprec_fun"}, we use @{text wq} and the function
+ none of these events lock or release any resource;
+ 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}\ \ \ \ \ %%%
@@ -420,11 +425,11 @@
\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}
@@ -440,7 +445,7 @@
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}
@@ -463,7 +468,7 @@
\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:
@@ -502,28 +507,24 @@
\end{isabelle}
\noindent
- In this definition @{term "f ` S"} stands for the set @{text S} under the image of the
- function @{text f}.
- Note that in the initial case, that is where the list of events is empty, the set
+ In this definition @{term "DUMMY ` DUMMY"} stands for the image of a set under a function.
+ Note that in the initial state, 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
- 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
+ Finally we can define what a \emph{valid state} is in our model of 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
- inductive predicate @{term "step"}. We give five inference rules
- relating a state and an event that can happen next.
+ created yet. These validity constraints on states are characterised by the
+ inductive predicate @{term "step"} and @{term vt}. We first give five inference rules
+ for @{term step} relating a state and an event that can happen next.
\begin{center}
\begin{tabular}{c}
@@ -535,7 +536,9 @@
\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}
@@ -546,24 +549,27 @@
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
- check; but in practice the occurs check is ommited and the
- responsibility to avoid problems rests with the programmer.}
+ anything meaningful about unification, one needs to perform an occurs
+ check, but in practice the occurs check is ommited and the
+ 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_P[where thread=th]}\medskip\\
- @{thm[mode=Rule] thread_V[where thread=th]}\\
- \end{tabular}
+ @{thm[mode=Rule] thread_V[where thread=th]}
\end{center}
-
+
\noindent
A valid state of PIP can then be conveniently be defined as follows: