regexp: comparison prio/Paper/Paper.thy

equal deleted inserted replaced

-:1f16ff7fea94
+:cab43c4a96d2
 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
-about states.  One, called @{term threads}, calculates the set of
+about states.  One, called @{term threads}, calculates, given a state @{text s}, the set of
-``live'' threads that we have seen so far in a state:
+``live'' threads that we have seen so far:
 \begin{isabelle}\ \ \ \ \ %%%
 \mbox{\begin{tabular}{lcl}
 @{thm (lhs) threads.simps(1)} & @{text "\<equiv>"} &
 @{thm (rhs) threads.simps(1)}\\
 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
 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 impementation
+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 a FIFO-scheduling of processes with
+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
 that is in possession of the
 ``lock'' of the corresponding resource. We model waiting queues as
-functions, below abbreviated as @{text wq}, taking a resource as
+functions, below abbreviated as @{text wq}. They take a resource as
-argument and returning a list of threads.  This allows us to define
+argument and return a list of threads.  This allows us to define
 when a thread \emph{holds}, respectively \emph{waits} for, a
-resource @{text cs} given a waiting queue function.
+resource @{text cs} given a waiting queue function @{text wq}.
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm cs_holding_def[where thread="th"]}\\
 @{thm cs_waiting_def[where thread="th"]}
 \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
-empty list.
+empty list for every resource.
 \begin{isabelle}\ \ \ \ \ %%%
 @{abbrev all_unlocked}
 \end{isabelle}
 \begin{isabelle}\ \ \ \ \ %%%
 @{thm cs_dependents_def}
 \end{isabelle}
 \noindent
-This definition needs to account for all threads that wait for tread to
+This definition needs to account for all threads that wait for a tread to
 release a resource. This means we need to include threads that transitively
-wait for a resource being realeased (in the picture this means also @{text "th\<^isub>3"},
+wait for a resource being realeased (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 waits 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 cirle 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 \emph{current precedence} for a thread @{text th} in a
+Next we introduce the notion of the \emph{current precedence} for a thread @{text th} in a
 state @{text s}, which is defined as
 \begin{isabelle}\ \ \ \ \ %%%
 @{thm cpreced_def2}
 \end{isabelle}
 \noindent
-While the precedence of a thread is determined by the programmer (for example when the thread is
+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
 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 defined as a record consisting of ...
+and returns a \emph{schedule state}, which we define as a record consisting of two
+functions
+\begin{isabelle}\ \ \ \ \ %%%
+@{text "\<lparr>wq_fun, cprec_fun\<rparr>"}
+\end{isabelle}
 In the initial state, the scheduler starts with all resources unlocked and the
 precedence of every thread is initialised with @{term "Prc 0 0"}.
 \begin{isabelle}\ \ \ \ \ %%%

changeset 293	cab43c4a96d2
parent 292	1f16ff7fea94
child 294	bc5bf9e9ada2