--- 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}

--- a/prio/Paper/document/root.tex	Fri Feb 10 11:30:47 2012 +0000
+++ b/prio/Paper/document/root.tex	Fri Feb 10 21:01:03 2012 +0000
@@ -4,8 +4,8 @@
 \usepackage{amsmath}
 \usepackage{amssymb}
 \usepackage{mathpartir}
-%\usepackage{tikz}
-%\usepackage{pgf}
+\usepackage{tikz}
+\usepackage{pgf}
 %\usetikzlibrary{arrows,automata,decorations,fit,calc}
 %\usetikzlibrary{shapes,shapes.arrows,snakes,positioning}
 %\usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf
@@ -34,6 +34,7 @@
 
 \newcommand{\isasymcalL}{\ensuremath{\cal{L}}}
 \newcommand{\isasymbigplus}{\ensuremath{\bigplus}}
+\renewcommand{\isasymiota}{}
 
 \newcommand{\bigplus}{\mbox{\Large\bf$+$}}
 \begin{document}

--- a/prio/PrioG.thy	Fri Feb 10 11:30:47 2012 +0000
+++ b/prio/PrioG.thy	Fri Feb 10 21:01:03 2012 +0000
@@ -2072,14 +2072,17 @@
 qed
 
 lemma cp_eq_cpreced: "cp s th = cpreced (wq s) s th"
-proof(unfold cp_def wq_def, induct s)
-  case (Cons e s')
-  show ?case
-    by (auto simp:Let_def)
-next
-  case Nil
-  show ?case by (auto simp:Let_def)
-qed
+unfolding cp_def wq_def
+apply(induct s rule: schs.induct)
+apply(simp add: Let_def cpreced_initial)
+apply(simp add: Let_def)
+apply(simp add: Let_def)
+apply(simp add: Let_def)
+apply(subst (2) schs.simps)
+apply(simp add: Let_def)
+apply(subst (2) schs.simps)
+apply(simp add: Let_def)
+done
 
 
 lemma runing_unique:

--- a/prio/PrioGDef.thy	Fri Feb 10 11:30:47 2012 +0000
+++ b/prio/PrioGDef.thy	Fri Feb 10 21:01:03 2012 +0000
@@ -192,13 +192,27 @@
 definition cpreced :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread \<Rightarrow> precedence"
   where "cpreced wq s = (\<lambda> th. Max ((\<lambda> th. preced th s) ` ({th} \<union> dependents wq th)))"
 
+(*<*)
 lemma 
   cpreced_def2:
-  "cpreced wq s th = Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependents wq th})"
+  "cpreced wq s th \<equiv> Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependents wq th})"
   unfolding cpreced_def image_def
+  apply(rule eq_reflection)
   apply(rule arg_cong)
   back
   by (auto)
+(*>*)
+
+abbreviation
+  "all_unlocked \<equiv> \<lambda>_::cs. ([]::thread list)"
+
+abbreviation 
+  "initial_cprec \<equiv> \<lambda>_::thread. Prc 0 0"
+ 
+abbreviation
+  "release qs \<equiv> case qs of
+             [] => [] 
+          |  (_#qs) => (SOME q. distinct q \<and> set q = set qs)"
 
 text {* \noindent
   The following function @{text "schs"} is used to calculate the schedule state @{text "schs s"}.
@@ -206,14 +220,14 @@
   *}
 fun schs :: "state \<Rightarrow> schedule_state"
   where 
-  "schs [] = (| waiting_queue = \<lambda> cs. [],  cur_preced = cpreced (\<lambda> cs. []) [] |)" |
+  "schs [] = (| waiting_queue = \<lambda> cs. [],  cur_preced = (\<lambda>_. Prc 0 0) |)" |
 
   -- {*
   \begin{minipage}{0.9\textwidth}
   \begin{enumerate}
   \item @{text "ps"} is the schedule state of last moment.
   \item @{text "pwq"} is the waiting queue function of last moment.
-  \item @{text "pcp"} is the precedence function of last moment. 
+  \item @{text "pcp"} is the precedence function of last moment (NOT USED). 
   \item @{text "nwq"} is the new waiting queue function. It is calculated using a @{text "case"} statement:
   \begin{enumerate}
       \item If the happening event is @{text "P thread cs"}, @{text "thread"} is added to 
@@ -233,9 +247,34 @@
   \end{enumerate}
   \end{minipage}
      *}
-   "schs (e#s) = (let ps = schs s in 
+   "schs (Create th prio # s) = 
+       (let wq = waiting_queue (schs s) in
+          (|waiting_queue = wq, cur_preced = cpreced wq (Create th prio # s)|))"
+|  "schs (Exit th # s) = 
+       (let wq = waiting_queue (schs s) in
+          (|waiting_queue = wq, cur_preced = cpreced wq (Exit th # s)|))"
+|  "schs (Set th prio # s) = 
+       (let wq = waiting_queue (schs s) in
+          (|waiting_queue = wq, cur_preced = cpreced wq (Set th prio # s)|))"
+|  "schs (P th cs # s) = 
+       (let wq = waiting_queue (schs s) in
+        let new_wq = wq(cs := (wq cs @ [th])) in
+          (|waiting_queue = new_wq, cur_preced = cpreced new_wq (P th cs # s)|))"
+|  "schs (V th cs # s) = 
+       (let wq = waiting_queue (schs s) in
+        let new_wq = wq(cs := release (wq cs)) in
+          (|waiting_queue = new_wq, cur_preced = cpreced new_wq (V th cs # s)|))"
+
+lemma cpreced_initial: 
+  "cpreced (\<lambda> cs. []) [] = (\<lambda>_. (Prc 0 0))"
+apply(simp add: cpreced_def)
+apply(simp add: cs_dependents_def cs_depend_def cs_waiting_def cs_holding_def)
+apply(simp add: preced_def)
+done
+
+lemma sch_old_def:
+  "schs (e#s) = (let ps = schs s in 
                   let pwq = waiting_queue ps in 
-                  let pcp = cur_preced ps in
                   let nwq = case e of
                              P th cs \<Rightarrow>  pwq(cs:=(pwq cs @ [th])) |
                              V th cs \<Rightarrow> let nq = case (pwq cs) of
@@ -246,6 +285,10 @@
                   in let ncp = cpreced nwq (e#s) in 
                      \<lparr>waiting_queue = nwq, cur_preced = ncp\<rparr>
                  )"
+apply(cases e)
+apply(simp_all)
+done
+
 
 text {* 
   \noindent

Binary file prio/paper.pdf has changed