--- a/prio/CpsG.thy	Thu Feb 09 16:34:18 2012 +0000
+++ b/prio/CpsG.thy	Fri Feb 10 11:30:47 2012 +0000
@@ -276,13 +276,13 @@
 qed
 
 
-lemma cp_eq_cpreced_f: "cp s = cpreced s (wq s)"
+lemma cp_eq_cpreced_f: "cp s = cpreced (wq s) s"
 proof -
   from fun_eq_iff 
   have h:"\<And>f g. (\<forall> x. f x = g x) \<Longrightarrow> f = g" by auto
   show ?thesis
   proof(rule h)
-    from cp_eq_cpreced show "\<forall>x. cp s x = cpreced s (wq s) x" by auto
+    from cp_eq_cpreced show "\<forall>x. cp s x = cpreced (wq s) s x" by auto
   qed
 qed
 

--- a/prio/ExtGG.thy	Thu Feb 09 16:34:18 2012 +0000
+++ b/prio/ExtGG.thy	Fri Feb 10 11:30:47 2012 +0000
@@ -461,7 +461,7 @@
 lemma th_cp_max_preced: "cp (t@s) th = Max ((\<lambda> th'. preced th' (t @ s)) ` (threads (t@s)))" 
   (is "?L = ?R")
 proof -
-  have "?L = cpreced (t@s) (wq (t@s)) th" 
+  have "?L = cpreced (wq (t@s)) (t@s) th" 
     by (unfold cp_eq_cpreced, simp)
   also have "\<dots> = ?R"
   proof(unfold cpreced_def)

--- a/prio/Paper/Paper.thy	Thu Feb 09 16:34:18 2012 +0000
+++ b/prio/Paper/Paper.thy	Fri Feb 10 11:30:47 2012 +0000
@@ -16,9 +16,12 @@
   Prc ("'(_, _')") and
   holding ("holds") and
   waiting ("waits") and
-  Th ("_") and
-  Cs ("_") and
+  Th ("T") and
+  Cs ("C") and
   readys ("ready") and
+  depend ("RAG") and 
+  preced ("prec") and
+  cpreced ("cprec") and
   DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")
 (*>*)
 
@@ -162,7 +165,7 @@
   PIP is based on Paulson's inductive approach to protocol
   verification \cite{Paulson98}, where the \emph{state} of a system is
   given by a list of events that happened so far.  \emph{Events} in PIP fall
-  into five categories defined as the datatype
+  into five categories defined as the datatype:
 
   \begin{isabelle}\ \ \ \ \ %%%
   \mbox{\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{7mm}}l}
@@ -197,7 +200,8 @@
   \end{isabelle}
 
   \noindent
-  Another function calculates the priority for a thread @{text "th"}, defined as
+  Another function calculates the priority for a thread @{text "th"}, which is 
+  defined as
 
   \begin{isabelle}\ \ \ \ \ %%%
   \mbox{\begin{tabular}{lcl}
@@ -215,7 +219,7 @@
   In this definition we set @{text 0} as the default priority for
   threads that have not (yet) been created. The last function we need 
   calculates the ``time'', or index, at which time a process had its 
-  priority set.
+  priority last set.
 
   \begin{isabelle}\ \ \ \ \ %%%
   \mbox{\begin{tabular}{lcl}
@@ -233,40 +237,91 @@
   In this definition @{term "length s"} stands for the length of the list
   of events @{text s}. Again the default value in this function is @{text 0}
   for threads that have not been created yet. A \emph{precedence} of a thread @{text th} in a 
-  state @{text s} is a pair of natural numbers defined as
+  state @{text s} is the pair of natural numbers defined as
   
   \begin{isabelle}\ \ \ \ \ %%%
-  @{thm (rhs) preced_def[where thread="th"]}
+  @{thm preced_def[where thread="th"]}
   \end{isabelle}
 
   \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 two threads with equal priority by 
+  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. In an impementation
+  set earlier, since for such threads it is more urgent to finish their work. In an impementation
   this choice would translate to a quite natural a 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 is chosen to be in the one that is in possession of the
+  this list (the head, or short @{term hd}) is chosen to be in 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
   argument and returning a list of threads.  This allows us to define
-  when a thread \emph{holds}, respectively \emph{waits}, for a
+  when a thread \emph{holds}, respectively \emph{waits} for, a
   resource @{text cs} given a waiting queue function.
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
-  @{thm s_holding_def[where thread="th"]}\\
-  @{thm s_waiting_def[where thread="th"]}
+  @{thm cs_holding_def[where thread="th"]}\\
+  @{thm cs_waiting_def[where thread="th"]}
   \end{tabular}
   \end{isabelle}
 
   \noindent
   In this definition we assume @{text "set"} converts a list into a set.
+  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
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{term "(Th th, Cs cs)"} \hspace{5mm}{\rm and}\hspace{5mm}
+  @{term "(Cs cs, Th th)"}
+  \end{isabelle}
+
+  \noindent
+  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
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm cs_depend_def}
+  \end{isabelle}
+
+  \noindent
+  An instance of a RAG is as follows:
+
+  \begin{center}
+  Picture
+  \end{center}
+
+  \noindent
+  The use or relations for representing RAGs allows us to conveninetly 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 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"}, 
+  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}.
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  @{thm cpreced_def2}\\
+  \end{isabelle}
+
+
+
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}

--- a/prio/PrioG.thy	Thu Feb 09 16:34:18 2012 +0000
+++ b/prio/PrioG.thy	Fri Feb 10 11:30:47 2012 +0000
@@ -2071,7 +2071,7 @@
   from wq_threads [OF vt this] show ?thesis .
 qed
 
-lemma cp_eq_cpreced: "cp s th = cpreced s (wq s) th"
+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

--- a/prio/PrioGDef.thy	Thu Feb 09 16:34:18 2012 +0000
+++ b/prio/PrioGDef.thy	Fri Feb 10 11:30:47 2012 +0000
@@ -110,7 +110,7 @@
   This explains the following definition:
   *}
 definition preced :: "thread \<Rightarrow> state \<Rightarrow> precedence"
-  where "preced thread s = Prc (original_priority thread s) (birthtime thread s)"
+  where "preced thread s \<equiv> Prc (original_priority thread s) (birthtime thread s)"
 
 
 text {*
@@ -189,15 +189,25 @@
   @{text "th"}'s {\em current precedence} equals its original precedence, i.e. 
   @{text "preced th s"}.
   *}
-definition cpreced :: "state \<Rightarrow> (cs \<Rightarrow> thread list) \<Rightarrow> thread \<Rightarrow> precedence"
-  where "cpreced s wq = (\<lambda> th. Max ((\<lambda> th. preced th s) ` ({th} \<union> dependents wq th)))"
+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})"
+  unfolding cpreced_def image_def
+  apply(rule arg_cong)
+  back
+  by (auto)
 
 text {* \noindent
   The following function @{text "schs"} is used to calculate the schedule state @{text "schs s"}.
   It is the key function to model Priority Inheritance:
   *}
 fun schs :: "state \<Rightarrow> schedule_state"
-  where "schs [] = \<lparr>waiting_queue = \<lambda> cs. [],  cur_preced = cpreced [] (\<lambda> cs. [])\<rparr>" |
+  where 
+  "schs [] = (| waiting_queue = \<lambda> cs. [],  cur_preced = cpreced (\<lambda> cs. []) [] |)" |
+
   -- {*
   \begin{minipage}{0.9\textwidth}
   \begin{enumerate}
@@ -227,13 +237,13 @@
                   let pwq = waiting_queue ps in 
                   let pcp = cur_preced ps in
                   let nwq = case e of
-                             P thread cs \<Rightarrow>  pwq(cs:=(pwq cs @ [thread])) |
-                             V thread cs \<Rightarrow> let nq = case (pwq cs) of
+                             P th cs \<Rightarrow>  pwq(cs:=(pwq cs @ [th])) |
+                             V th cs \<Rightarrow> let nq = case (pwq cs) of
                                                       [] \<Rightarrow> [] | 
-                                                      (th'#qs) \<Rightarrow> (SOME q. distinct q \<and> set q = set qs)
+                                                      (_#qs) \<Rightarrow> (SOME q. distinct q \<and> set q = set qs)
                                             in pwq(cs:=nq)                 |
                               _ \<Rightarrow> pwq
-                  in let ncp = cpreced (e#s) nwq in 
+                  in let ncp = cpreced nwq (e#s) in 
                      \<lparr>waiting_queue = nwq, cur_preced = ncp\<rparr>
                  )"
 

Binary file prio/paper.pdf has changed