--- a/prio/Paper/Paper.thy	Fri Feb 10 11:30:47 2012 +0000
+++ b/prio/Paper/Paper.thy	Fri Feb 10 21:01:03 2012 +0000
@@ -22,6 +22,9 @@
   depend ("RAG") and 
   preced ("prec") and
   cpreced ("cprec") and
+  dependents ("dependants") and
+  waiting_queue ("wq_fun") and
+  cur_preced ("cprec_fun") and
   DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")
 (*>*)
 
@@ -255,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 in the one 
+  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
@@ -272,6 +275,15 @@
 
   \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.
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{abbrev all_unlocked}
+  \end{isabelle}
+
+  \noindent
   Using @{term "holding"} and @{term waiting}, we can introduce \emph{Resource Allocation Graphs} 
   (RAG), which represent the dependencies between threads and resources.
   We represent RAGs as relations using pairs of the form
@@ -295,7 +307,15 @@
   An instance of a RAG is as follows:
 
   \begin{center}
-  Picture
+  \begin{tikzpicture}[scale=1]
+  \draw[step=2mm] (0,0) grid (3,2);
+
+  \draw[rounded corners=1mm, very thick] (0,0) rectangle (0.6,0.6);
+  \draw[rounded corners=1mm, very thick] (3,0) rectangle (3.6,0.6);
+
+  \draw (0.3,0.3) node {\small$th_0$};
+  \draw (3.3,0.3) node {\small$th_1$};
+  \end{tikzpicture}
   \end{center}
 
   \noindent
@@ -312,16 +332,99 @@
   wait for a resource being realeased (in the picture 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
-  we have a deadlock. Therefore when we state our correctness property for PIP
-  we must ensure that RAGs are not circular. This allows us to define the notion
-  of the \emph{current precedence} of a thread @{text th} in a state @{text s}.
+  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 
+  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
+  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 ...
+
+  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}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm (lhs) schs.simps(1)} @{text "\<equiv>"}\\ 
+  \hspace{5mm}@{term "(|waiting_queue = all_unlocked, cur_preced = (\<lambda>_::thread. Prc 0 0)|)"}
+  \end{tabular}
+  \end{isabelle}
+
+  \noindent
+  The cases for @{term Create}, @{term Exit} and @{term Set} are straightforward:
+  we calculuate 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 
+  the next @{term "cprec_fun"} we use @{text wq} and the function @{term cpreced}. 
+  This gives the following clauses:
 
   \begin{isabelle}\ \ \ \ \ %%%
-  @{thm cpreced_def2}\\
+  \begin{tabular}{@ {}l}
+  @{thm (lhs) schs.simps(2)} @{text "\<equiv>"}\\ 
+  \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\
+  \hspace{8mm}@{term "(|waiting_queue = wq\<iota>, cur_preced = cpreced wq\<iota> (Create th prio # s)|)"}\\
+  @{thm (lhs) schs.simps(3)} @{text "\<equiv>"}\\
+  \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\
+  \hspace{8mm}@{term "(|waiting_queue = wq\<iota>, cur_preced = cpreced wq\<iota> (Exit th # s)|)"}\smallskip\\
+  @{thm (lhs) schs.simps(4)} @{text "\<equiv>"}\\ 
+  \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\
+  \hspace{8mm}@{term "(|waiting_queue = wq\<iota>, cur_preced = 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
+  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 
+  thread 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{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\
+  \hspace{5mm}@{text "let"} @{text "new_wq = wq(cs := (wq cs @ [th]))"} @{text "in"}\\
+  \hspace{8mm}@{term "(|waiting_queue = new_wq, cur_preced = 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
+  using the auxiliary definition
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{abbrev release}
+  \end{isabelle}
+
+  \noindent
+  This gives for @{term schs} the clause:
+ 
+  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{tabular}{@ {}l}
+  @{thm (lhs) schs.simps(6)} @{text "\<equiv>"}\\
+  \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\
+  \hspace{5mm}@{text "let"} @{text "new_wq = release (wq cs)"} @{text "in"}\\
+  \hspace{8mm}@{term "(|waiting_queue = new_wq, cur_preced = cpreced new_wq (V th cs # s)|)"}
+  \end{tabular}
   \end{isabelle}
 
 
-
+  TODO
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}