--- a/prio/Paper/Paper.thy Sat Feb 11 19:39:50 2012 +0000
+++ b/prio/Paper/Paper.thy Sun Feb 12 04:45:20 2012 +0000
@@ -23,6 +23,8 @@
preced ("prec") and
cpreced ("cprec") and
dependents ("dependants") and
+ cp ("cprec") and
+ holdents ("resources") and
DUMMY ("\<^raw:\mbox{$\_\!\_$}>")
(*>*)
@@ -165,7 +167,7 @@
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
+ given by a list of events that happened so far. \emph{Events} of PIP fall
into five categories defined as the datatype:
\begin{isabelle}\ \ \ \ \ %%%
@@ -184,7 +186,7 @@
as natural numbers. The event @{term Set} models the situation that
a thread obtains a new priority given by the programmer or
user (for example via the {\tt nice} utility under UNIX). As in Paulson's work, we
- need to define functions that allow one to make some observations
+ need to define functions that allow us to make some observations
about states. One, called @{term threads}, calculates the set of
``live'' threads that we have seen so far:
@@ -256,7 +258,7 @@
Next, we introduce the concept of \emph{waiting queues}. They are
lists of threads associated with every resource. The first thread in
- this list (the head, or short @{term hd}) is chosen to be the one
+ this list (i.e.~the head, or short @{term hd}) is chosen to be the one
that is in possession of the
``lock'' of the corresponding resource. We model waiting queues as
functions, below abbreviated as @{text wq}. They take a resource as
@@ -273,8 +275,8 @@
\noindent
In this definition we assume @{text "set"} converts a list into a set.
- At the beginning, that is in the state where no process is created yet,
- the waiting queue function will be the function that just returns the
+ At the beginning, that is in the state where no thread is created yet,
+ the waiting queue function will be the function that returns the
empty list for every resource.
\begin{isabelle}\ \ \ \ \ %%%
@@ -302,7 +304,7 @@
\end{isabelle}
\noindent
- An instance of a RAG is as follows:
+ Given three threads and three resources, an instance of a RAG is as follows:
\begin{center}
\newcommand{\fnt}{\fontsize{7}{8}\selectfont}
@@ -314,13 +316,15 @@
\node (C) at (4,0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>1"}};
\node (D) at (4,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>2"}};
\node (E) at (6,-0.7) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>2"}};
+ \node (E1) at (6, 0.2) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>3"}};
\node (F) at (8,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>3"}};
\draw [->,line width=0.6mm] (A) to node [pos=0.45,sloped,above=-0.5mm] {\fnt{}holding} (B);
\draw [->,line width=0.6mm] (C) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waiting} (B);
- \draw [->,line width=0.6mm] (D) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waiting} (B);
- \draw [->,line width=0.6mm] (D) to node [pos=0.45,sloped,above=-0.5mm] {\fnt{}holding} (E);
- \draw [->,line width=0.6mm] (F) to node [pos=0.45,sloped,above=-0.5mm] {\fnt{}waiting} (E);
+ \draw [->,line width=0.6mm] (D) to node [pos=0.4,sloped,below=-0.5mm] {\fnt{}waiting} (B);
+ \draw [->,line width=0.6mm] (D) to node [pos=0.45,sloped,below=-0.5mm] {\fnt{}holding} (E);
+ \draw [->,line width=0.6mm] (D) to node [pos=0.45,sloped,above=-0.5mm] {\fnt{}holding} (E1);
+ \draw [->,line width=0.6mm] (F) to node [pos=0.45,sloped,below=-0.5mm] {\fnt{}waiting} (E);
\end{tikzpicture}
\end{center}
@@ -335,17 +339,18 @@
\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 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"}). If there is a circle in a RAG, then clearly
+ 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"},
+ 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
we have a deadlock. Therefore when a thread requests a resource,
- we must ensure that the resulting RAG is not not circular.
+ we must ensure that the resulting RAG is not circular.
- Next we introduce the notion of the \emph{current precedence} for a thread @{text th} in a
- state @{text s}, which is defined as
+ 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}
+ @{thm cpreced_def2}\numbered{permprops}
\end{isabelle}
\noindent
@@ -359,9 +364,9 @@
problem in the 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 is defined
- by recursion on the state (a list of events); @{term "schs"} takes a state as argument
- and returns a \emph{schedule state}, which we define as a record consisting of two
+ 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
+ we represent as a record consisting of two
functions:
\begin{isabelle}\ \ \ \ \ %%%
@@ -369,13 +374,14 @@
\end{isabelle}
\noindent
- The first is a waiting queue function (that is takes a @{text "cs"} and returns the
+ The first function is a waiting queue function (that is takes a @{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 ???). We have the usual getter and
+ a thread and returns its current precedence (see ???). We assume the usual getter and
setter methods for such records.
In the initial state, the scheduler starts with all resources unlocked and the
- precedence of every thread is initialised with @{term "Prc 0 0"}. Therefore
+ current precedence of every thread is initialised with @{term "Prc 0 0"}; that means
+ @{abbrev initial_cprec}. Therefore
we have
\begin{isabelle}\ \ \ \ \ %%%
@@ -388,15 +394,16 @@
\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;
+ 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
- @{term cpreced}. This gives the following three clauses:
+ @{term cpreced}. This gives the following three clauses for @{term schs}:
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
@{thm (lhs) schs.simps(2)} @{text "\<equiv>"}\\
\hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
- \hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Create th prio # s)|)"}\\
+ \hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Create th prio # s)|)"}\smallskip\\
@{thm (lhs) schs.simps(3)} @{text "\<equiv>"}\\
\hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
\hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Exit th # s)|)"}\smallskip\\
@@ -408,9 +415,9 @@
\noindent
More interesting are the cases when a resource, say @{text cs}, is locked or released. In this case
- we need to calculate a new waiting queue function. In case of @{term P}, we update
+ we need to calculate a new waiting queue function. For the event @{term P}, we have to update
the function so that the new thread list for @{text cs} is old thread list plus the thread @{text th}
- appended to the end (remember the head of this list is in the possession of the
+ appended to the end of that list (remember the head of this list is seen to be in the possession of the
resource).
\begin{isabelle}\ \ \ \ \ %%%
@@ -423,10 +430,10 @@
\end{isabelle}
\noindent
- The case for @{term V} is similar, except that we need to update the waiting queue function
- so that the thread that possessed the lock is eliminated. For this we use
+ The clause for event @{term V} 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 we use
the auxiliary function @{term release}. A simple version of @{term release} would
- just delete this thread and return the rest like so
+ just delete this thread and return the rest, namely
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}lcl}
@@ -436,7 +443,7 @@
\end{isabelle}
\noindent
- However in practice often the thread with the highest precedence will get the
+ In practice, however, often the thread with the highest precedence will get the
lock next. We have implemented this choice, but later found out that the choice
about which thread is chosen next is actually irrelevant for the correctness of PIP.
Therefore we prove the stronger result where @{term release} is defined as
@@ -450,8 +457,8 @@
\noindent
@{text "SOME"} stands for Hilbert's epsilon and implements an arbitrary
- choice for the next waiting list, it just has to be a distinct list and
- contain the same elements as @{text "qs"}. This gives for @{term V} and @{term schs} the clause:
+ 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}
@@ -462,60 +469,107 @@
\end{tabular}
\end{isabelle}
-
- TODO
+ Having the scheduler function @{term schs} at our disposal, we can ``lift'' the notions
+ @{term waiting}, @{term holding} @{term depend} and @{term cp} such that they only depend
+ on states.
\begin{isabelle}\ \ \ \ \ %%%
- \begin{tabular}{@ {}l}
- @{thm s_depend_def}\\
+ \begin{tabular}{@ {}rcl}
+ @{thm (lhs) s_holding_abv} & @{text "\<equiv>"} & @{thm (rhs) s_holding_abv}\\
+ @{thm (lhs) s_waiting_abv} & @{text "\<equiv>"} & @{thm (rhs) s_waiting_abv}\\
+ @{thm (lhs) s_depend_abv} & @{text "\<equiv>"} & @{thm (rhs) s_depend_abv}\\
+ @{thm (lhs) cp_def} & @{text "\<equiv>"} & @{thm (rhs) cp_def}
\end{tabular}
\end{isabelle}
+ \noindent
+ With them we can introduce the notion of threads being @{term readys} (i.e.~threads
+ that do not wait for any resource) and the running thread.
+
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
@{thm readys_def}\\
- \end{tabular}
- \end{isabelle}
-
- \begin{isabelle}\ \ \ \ \ %%%
- \begin{tabular}{@ {}l}
@{thm runing_def}\\
\end{tabular}
\end{isabelle}
-
- resources
+ \noindent
+ 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 can also define the set of resources that are locked by a thread in a
+ given state.
- done: threads not done: running
+ \begin{isabelle}\ \ \ \ \ %%%
+ @{thm holdents_def}
+ \end{isabelle}
- step relation:
+ \noindent
+ These resources are given by the holding edges in the RAG.
+
+ Finally we can define what a \emph{valid state} is. For example we cannot exptect to
+ be able to exit a thread, if it was not created yet. These validity constraints
+ are characterised by the inductive predicate @{term "step"} by the following five
+ inference rules 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]}\medskip\\
+ @{thm[mode=Rule] thread_exit[where thread=th]}
+ \end{tabular}
+ \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. The event @{text Set} can happen
+ if the corresponding thread is running.
- @{thm[mode=Rule] thread_set[where thread=th]}\medskip\\
+ \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 doe not lead to a cycle in the
+ RAG. 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}.
+
+ \begin{center}
+ \begin{tabular}{c}
@{thm[mode=Rule] thread_P[where thread=th]}\medskip\\
@{thm[mode=Rule] thread_V[where thread=th]}\\
\end{tabular}
\end{center}
-
- valid state:
+
+ \noindent
+ A valid state of PIP can then be conveniently be defined as follows:
\begin{center}
\begin{tabular}{c}
- @{thm[mode=Axiom] vt_nil[where cs=step]}\hspace{1cm}
- @{thm[mode=Rule] vt_cons[where cs=step]}
+ @{thm[mode=Axiom] vt_nil}\hspace{1cm}
+ @{thm[mode=Rule] vt_cons}
\end{tabular}
\end{center}
+ \noindent
+ This completes our formal model of PIP. In the next section we present
+ properties that show our version of PIP is correct.
+*}
- To define events, the identifiers of {\em threads},
- {\em priority} and {\em critical resources } (abbreviated as @{text "cs"})
- need to be represented. All three are represetned using standard
- Isabelle/HOL type @{typ "nat"}:
-*}
+section {* Correctness Proof *}
+
+text {* TO DO *}
+
+section {* Properties for an Implementation *}
+
+text {* TO DO *}
+
+section {* Conclusion *}
+
+text {* TO DO *}
text {*
\bigskip