regexp: comparison prio/Paper/Paper.thy

equal deleted inserted replaced

-:0a4be67ea7f8
+:f2e0d031a395
 readys ("ready") and
 depend ("RAG") and
 preced ("prec") and
 cpreced ("cprec") and
 dependents ("dependants") and
+cp ("cprec") and
+holdents ("resources") and
 DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")
 (*>*)
 section {* Introduction *}
 The Priority Inheritance Protocol, short PIP, is a scheduling
 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
+given by a list of events that happened so far.  \emph{Events} of PIP fall
 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
 \noindent
 whereby threads, priorities and (critical) resources are represented
 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:
 \begin{isabelle}\ \ \ \ \ %%%
 \mbox{\begin{tabular}{lcl}
 this choice would translate to a quite natural 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 (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
 argument and return a list of threads.  This allows us to define
 when a thread \emph{holds}, respectively \emph{waits} for, a
 \end{tabular}
 \end{isabelle}
 \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,
+At the beginning, that is in the state where no thread is created yet,
-the waiting queue function will be the function that just returns the
+the waiting queue function will be the function that returns the
 empty list for every resource.
 \begin{isabelle}\ \ \ \ \ %%%
 @{abbrev all_unlocked}
 \end{isabelle}
 \begin{isabelle}\ \ \ \ \ %%%
 @{thm cs_depend_def}
 \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}
 \begin{tikzpicture}[scale=1]
 %%\draw[step=2mm] (-3,2) grid (1,-1);
 \node (A) at (0,0) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>0"}};
 \node (B) at (2,0) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>1"}};
 \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.4,sloped,below=-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] (D) to node [pos=0.45,sloped,below=-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.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}
 \noindent
 The use of relations for representing RAGs allows us to conveniently define
 \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 also @{text "th\<^isub>3"},
+wait for a resource being released (in the picture above this means the dependants
-which cannot make any progress unless @{text "th\<^isub>2"} makes progress which
+of @{text "th\<^isub>0"} are @{text "th\<^isub>1"} and @{text "th\<^isub>2"}, but also @{text "th\<^isub>3"},
-in turn needs to wait for @{text "th\<^isub>1"}). If there is a circle in a RAG, then clearly
+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
+Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a
-state @{text s}, which is defined as
+state @{text s}. It is defined as
 \begin{isabelle}\ \ \ \ \ %%%
-@{thm cpreced_def2}
+@{thm cpreced_def2}\numbered{permprops}
 \end{isabelle}
 \noindent
 While the precedence @{term prec} of a thread is determined by the programmer
 (for example when the thread is
 processes 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
 lowered prematurely.
-The next function, called @{term schs}, defines the behaviour of the scheduler. It is defined
+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"} takes a state as argument
+by recursion on the state (a list of events); @{term "schs"} returns a \emph{schedule state}, which
-and returns a \emph{schedule state}, which we define as a record consisting of two
+we represent as a record consisting of two
 functions:
 \begin{isabelle}\ \ \ \ \ %%%
 @{text "\<lparr>wq_fun, cprec_fun\<rparr>"}
 \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}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm (lhs) schs.simps(1)} @{text "\<equiv>"}\\
 \end{isabelle}
 \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\\
 @{thm (lhs) schs.simps(4)} @{text "\<equiv>"}\\
 \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
 \end{tabular}
 \end{isabelle}
 \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}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm (lhs) schs.simps(5)} @{text "\<equiv>"}\\
 \hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (P th cs # s)|)"}
 \end{tabular}
 \end{isabelle}
 \noindent
-The case for @{term V} is similar, except that we need to update the waiting queue function
+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 eliminated. For this we use
+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}
 @{term "release []"} & @{text "\<equiv>"} & @{term "[]"}\\
 @{term "release (DUMMY # qs)"} & @{text "\<equiv>"} & @{term "qs"}\\
 \end{tabular}
 \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
 \begin{isabelle}\ \ \ \ \ %%%
 \end{tabular}
 \end{isabelle}
 \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
+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} and @{term schs} the clause:
+contain the same elements as @{text "qs"}. This gives for @{term V} the clause:
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm (lhs) schs.simps(6)} @{text "\<equiv>"}\\
 \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\
 \hspace{5mm}@{text "let"} @{text "new_wq = release (wq cs)"} @{text "in"}\\
 \hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|)"}
 \end{tabular}
 \end{isabelle}
+Having the scheduler function @{term schs} at our disposal, we can ``lift'' the notions
-TODO
+@{term waiting}, @{term holding} @{term depend} and @{term cp} such that they only depend
+on states.
-\begin{isabelle}\ \ \ \ \ %%%
-\begin{tabular}{@ {}l}
+\begin{isabelle}\ \ \ \ \ %%%
-@{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}
+\noindent
-resources
+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.
-done: threads     not done: 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
-step relation:
+threads. We can also 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. 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}
-@{thm[mode=Rule] thread_set[where thread=th]}\medskip\\
+\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.
+\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=Axiom] vt_nil}\hspace{1cm}
-@{thm[mode=Rule] vt_cons[where cs=step]}
+@{thm[mode=Rule] vt_cons}
 \end{tabular}
 \end{center}
+\noindent
-To define events, the identifiers of {\em threads},
+This completes our formal model of PIP. In the next section we present
-{\em priority} and {\em critical resources } (abbreviated as @{text "cs"})
+properties that show our version of PIP is correct.
-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
 The priority inversion phenomenon was first published in
 \cite{Lampson80}.  The two protocols widely used to eliminate

changeset 298	f2e0d031a395
parent 297	0a4be67ea7f8
child 299	4fcd802eba59