diff -r 463bed130705 -r 5113aa1ae69a prio/Paper/Paper.thy --- 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: