regexp: comparison prio/Paper/Paper.thy

equal deleted inserted replaced

-:8e4a5fff2eda
+:2c8dcf010567
 \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 between two threads with equal priority by
-tacking into account the time when the priority was last set. We order precedences so
+taking 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 their work. In an implementation
 this choice would translate to a quite natural FIFO-scheduling of processes with
 the same priority.
 \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,
-the waiting queue function will be just the function that returns the
+the waiting queue function will be the function that just returns the
 empty list for every resource.
 \begin{isabelle}\ \ \ \ \ %%%
 @{abbrev all_unlocked}
 \end{isabelle}
 \draw (3.3,0.3) node {\small$th_1$};
 \end{tikzpicture}
 \end{center}
 \noindent
-The use or relations for representing RAGs allows us to conveninetly define
+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
 \begin{isabelle}\ \ \ \ \ %%%
 @{thm cs_dependents_def}
 \end{isabelle}
 \noindent
-This definition needs to account for all threads that wait for a tread to
+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 realeased (in the picture above this means also @{text "th\<^isub>3"},
+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 cirle in a RAG, then clearly
+in turn needs to wait for @{text "th\<^isub>1"}). 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.
 Next we introduce the notion of the \emph{current precedence} for a thread @{text th} in a
 state @{text s}, which is defined as
 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
 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 "dependents"} 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
 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
-functions
+functions:
 \begin{isabelle}\ \ \ \ \ %%%
 @{text "\<lparr>wq_fun, cprec_fun\<rparr>"}
 \end{isabelle}
 \noindent
-We have the usual getter and setter methods for such records.
+The first 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
+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"}.
+precedence of every thread is initialised with @{term "Prc 0 0"}. Therefore
+we have
 \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)|)"}
 \end{tabular}
 \end{isabelle}
 \noindent
-The cases for @{term Create}, @{term Exit} and @{term Set} are straightforward:
+The cases for @{term Create}, @{term Exit} and @{term Set} are also straightforward:
-we calculuate the waiting queue function of the (previous) state @{text s};
+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; for calculuating
+this waiting queue function @{text wq} is unchanged in the next schedule state;
-the next @{term "cprec_fun"} we use @{text wq} and the function @{term cpreced}.
+for calculating the next @{term "cprec_fun"}, we use @{text wq} and the function
-This gives the following clauses:
+@{term cpreced}. This gives the following three clauses:
 \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> (Set th prio # s)|)"}
 \end{tabular}
 \end{isabelle}
 \noindent
-More interesting are the cases when a resource, say @{text cs}, is locked or relaesed. In this case
+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. In case of @{term P}, we update
-the function so that the new thread list for @{text cs} is old thread list with the waiting
+the function so that the new thread list for @{text cs} is old thread list plus the thread @{text th}
-thread appended to the end (remember the head of this list is in the possession of the
+appended to the end (remember the head of this list is 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 similarly, except that we update the waiting queue function
+The case for @{term V} is similar, except that we need to update the waiting queue function
-using the auxiliary definition
+so that the thread that possessed the lock is eliminated. For this we use
+the auxiliary function @{term release}. A simple version of @{term release} would
-\begin{isabelle}\ \ \ \ \ %%%
+just delete this thread and return the rest like so
-@{abbrev release}
-\end{isabelle}
+\begin{isabelle}\ \ \ \ \ %%%
+\begin{tabular}{@ {}lcl}
-\noindent
+@{term "release []"} & @{text "\<equiv>"} & @{term "[]"}\\
-This gives for @{term schs} the clause:
+@{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
+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}\ \ \ \ \ %%%
+\begin{tabular}{@ {}lcl}
+@{term "release []"} & @{text "\<equiv>"} & @{term "[]"}\\
+@{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
+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:
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm (lhs) schs.simps(6)} @{text "\<equiv>"}\\
 \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\

changeset 296	2c8dcf010567
parent 294	bc5bf9e9ada2
child 297	0a4be67ea7f8