
diff -r 8f026b608378 -r e861aff29655 Journal/Paper.thy
--- a/Journal/Paper.thy	Wed Mar 12 10:08:20 2014 +0000
+++ b/Journal/Paper.thy	Tue May 06 14:36:40 2014 +0100
@@ -11,7 +11,6 @@
   Cons ("_::_" [78,77] 73) and
   vt ("valid'_state") and
   runing ("running") and
-  birthtime ("last'_set") and
   If  ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
   Prc ("'(_, _')") and
   holding ("holds") and
@@ -22,10 +21,8 @@
   depend ("RAG") and 
   preced ("prec") and
   cpreced ("cprec") and
-  dependents ("dependants") and
   cp ("cprec") and
   holdents ("resources") and
-  original_priority ("priority") and
   DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")
  
   
@@ -83,7 +80,7 @@
   implemented. This includes VxWorks (a proprietary real-time OS used
   in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, Honda's
   ASIMO robot, etc.) and ThreadX (another proprietary real-time OS
-  used in HP inkjet printers \cite{ThreadX}), but also
+  used in nearly all HP inkjet printers \cite{ThreadX}), but also
   the POSIX 1003.1c Standard realised for
   example in libraries for FreeBSD, Solaris and Linux. 
 
@@ -92,7 +89,7 @@
   This is in contrast to \emph{Priority Ceiling}
   \cite{Sha90}, another solution to the Priority Inversion problem,
   which requires static analysis of the program in order to prevent
-  Priority Inversion, and also in contrast to the Windows NT scheduler, which avoids
+  Priority Inversion, and also in contrast to the approach taken in the Windows NT scheduler, which avoids
   this problem by randomly boosting the priority of ready low-priority threads
   (see for instance~\cite{WINDOWSNT}).
   However, there has also been strong criticism against
@@ -141,11 +138,12 @@
   point to a subtlety that had been
   overlooked in the informal proof by Sha et al. They specify in
   \cite{Sha90} that after the thread (whose priority has been raised)
-  completes its critical section and releases the lock, it ``returns
-  to its original priority level.'' This leads them to believe that an
-  implementation of PIP is ``rather straightforward''~\cite{Sha90}.
+  completes its critical section and releases the lock, it ``{\it returns
+  to its original priority level}''. This leads them to believe that an
+  implementation of PIP is ``{\it rather straightforward}''~\cite{Sha90}.
   Unfortunately, as Yodaiken and Moylan et al.~point out, this behaviour is too
-  simplistic.  Consider the case where the low priority thread $L$
+  simplistic. Moylan et al.~write that there are ``{\it some hidden traps}''. 
+  Consider the case where the low priority thread $L$
   locks \emph{two} resources, and two high-priority threads $H$ and
   $H'$ each wait for one of them.  If $L$ releases one resource
   so that $H$, say, can proceed, then we still have Priority Inversion
@@ -153,8 +151,8 @@
   behaviour for $L$ is to switch to the highest remaining priority of
   the threads that it blocks. A similar error is made in the textbook
   \cite[Section 2.3.1]{book} which specifies for a process that 
-  inherited a higher priority and exits a critical section ``it resumes 
-  the priority it had at the point of entry into the critical section''.
+  inherited a higher priority and exits a critical section ``{\it it resumes 
+  the priority it had at the point of entry into the critical section}''.
    
   While \cite{book} and
   \cite{Sha90} are the only formal publications we have 
@@ -184,9 +182,59 @@
   in the reference implementation of PIP in PINTOS.  This fact, however, is important
   for an efficient implementation of PIP, because we can give the lock
   to the thread with the highest priority so that it terminates more
-  quickly.  We were also able to generalise the scheduler of Sha
+  quickly.  We were also being able to generalise the scheduler of Sha
   et al.~\cite{Sha90} to the practically relevant case where critical 
-  sections can overlap.
+  sections can overlap; see Figure~\ref{overlap} below for an example of 
+  this restriction. In the existing literature there is no 
+  proof and also no prove method that cover this generalised case.
+
+  \begin{figure}
+  \begin{center}
+  \begin{tikzpicture}[scale=1]
+  %%\draw[step=2mm] (0,0) grid (10,2);
+  \draw [->,line width=0.6mm] (0,0) -- (10,0);
+  \draw [->,line width=0.6mm] (0,1.5) -- (10,1.5);
+  \draw [line width=0.6mm, pattern=horizontal lines] (0.8,0) rectangle (4,0.5);
+  \draw [line width=0.6mm, pattern=north east lines] (3.0,0) rectangle (6,0.5);
+  \draw [line width=0.6mm, pattern=vertical lines] (5.0,0) rectangle (9,0.5);
+
+  \draw [line width=0.6mm, pattern=horizontal lines] (0.6,1.5) rectangle (4.0,2); 
+  \draw [line width=0.6mm, pattern=north east lines] (1.0,1.5) rectangle (3.4,2); 
+  \draw [line width=0.6mm, pattern=vertical lines] (5.0,1.5) rectangle (8.8,2); 
+ 
+  \node at (0.8,-0.3) {@{term "P\<^sub>1"}};
+  \node at (3.0,-0.3) {@{term "P\<^sub>2"}};
+  \node at (4.0,-0.3) {@{term "V\<^sub>1"}}; 
+  \node at (5.0,-0.3) {@{term "P\<^sub>3"}};
+  \node at (6.0,-0.3) {@{term "V\<^sub>2"}};
+  \node at (9.0,-0.3) {@{term "V\<^sub>3"}};
+  
+  \node at (0.6,1.2) {@{term "P\<^sub>1"}};
+  \node at (1.0,1.2) {@{term "P\<^sub>2"}};
+  \node at (3.4,1.2) {@{term "V\<^sub>2"}};
+  \node at (4.0,1.2) {@{term "V\<^sub>1"}};
+  \node at (5.0,1.2) {@{term "P\<^sub>3"}};
+  \node at (8.8,1.2) {@{term "V\<^sub>3"}};
+  \node at (10.3,0) {$t$};
+  \node at (10.3,1.5) {$t$};
+
+  \node at (-0.3,0.2) {$b)$};
+  \node at (-0.3,1.7) {$a)$};
+  \end{tikzpicture}\mbox{}\\[-10mm]\mbox{}
+  \end{center}
+  \caption{Assume a process is over time locking and unlocking, say, three resources.
+  The locking requests are labelled @{term "P\<^sub>1"}, @{term "P\<^sub>2"}, and @{term "P\<^sub>3"} 
+  respectively, and the corresponding unlocking operations are labelled
+  @{term "V\<^sub>1"}, @{term "V\<^sub>2"}, and @{term "V\<^sub>3"}. 
+  Then graph $a)$ shows \emph{properly nested} critical sections as required 
+  by Sha et al.~\cite{Sha90} in their proof---the sections must either be contained within 
+  each other
+  (the section @{term "P\<^sub>2"}--@{term "V\<^sub>2"} is contained in @{term "P\<^sub>1"}--@{term "V\<^sub>1"}) or
+  be independent (@{term "P\<^sub>3"}--@{term "V\<^sub>3"} is independent from the other 
+  two). Graph $b)$ shows the general case where 
+  the locking and unlocking of different critical sections can 
+  overlap.\label{overlap}}
+  \end{figure}
 *}
 
 section {* Formal Model of the Priority Inheritance Protocol\label{model} *}
@@ -205,9 +253,9 @@
   \begin{isabelle}\ \ \ \ \ %%%
   \mbox{\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{7mm}}l}
   \isacommand{datatype} event 
-  & @{text "="} & @{term "Create thread priority"}\\
+  & @{text "="} & @{term "Create thread priority\<iota>"}\\
   & @{text "|"} & @{term "Exit thread"} \\
-  & @{text "|"} & @{term "Set thread priority"} & {\rm reset of the priority for} @{text thread}\\
+  & @{text "|"} & @{term "Set thread priority\<iota>"} & {\rm reset of the priority for} @{text thread}\\
   & @{text "|"} & @{term "P thread cs"} & {\rm request of resource} @{text "cs"} {\rm by} @{text "thread"}\\
   & @{text "|"} & @{term "V thread cs"} & {\rm release of resource} @{text "cs"} {\rm by} @{text "thread"}
   \end{tabular}}
@@ -235,37 +283,37 @@
   \end{isabelle}
 
   \noindent
-  In this definition @{term "DUMMY # DUMMY"} stands for list-cons.
+  In this definition @{term "DUMMY # DUMMY"} stands for list-cons and @{term "[]"} for the empty list.
   Another function calculates the priority for a thread @{text "th"}, which is 
   defined as
 
   \begin{isabelle}\ \ \ \ \ %%%
   \mbox{\begin{tabular}{lcl}
-  @{thm (lhs) original_priority.simps(1)[where thread="th"]} & @{text "\<equiv>"} & 
-    @{thm (rhs) original_priority.simps(1)[where thread="th"]}\\
-  @{thm (lhs) original_priority.simps(2)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} & 
-    @{thm (rhs) original_priority.simps(2)[where thread="th" and thread'="th'"]}\\
-  @{thm (lhs) original_priority.simps(3)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} & 
-    @{thm (rhs) original_priority.simps(3)[where thread="th" and thread'="th'"]}\\
-  @{term "original_priority th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "original_priority th s"}\\
+  @{thm (lhs) priority.simps(1)[where thread="th"]} & @{text "\<equiv>"} & 
+    @{thm (rhs) priority.simps(1)[where thread="th"]}\\
+  @{thm (lhs) priority.simps(2)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} & 
+    @{thm (rhs) priority.simps(2)[where thread="th" and thread'="th'"]}\\
+  @{thm (lhs) priority.simps(3)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} & 
+    @{thm (rhs) priority.simps(3)[where thread="th" and thread'="th'"]}\\
+  @{term "priority th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "priority th s"}\\
   \end{tabular}}
   \end{isabelle}
 
   \noindent
   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 
+  calculates the ``time'', or index, at which time a thread had its 
   priority last set.
 
   \begin{isabelle}\ \ \ \ \ %%%
   \mbox{\begin{tabular}{lcl}
-  @{thm (lhs) birthtime.simps(1)[where thread="th"]} & @{text "\<equiv>"} & 
-    @{thm (rhs) birthtime.simps(1)[where thread="th"]}\\
-  @{thm (lhs) birthtime.simps(2)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} & 
-    @{thm (rhs) birthtime.simps(2)[where thread="th" and thread'="th'"]}\\
-  @{thm (lhs) birthtime.simps(3)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} & 
-    @{thm (rhs) birthtime.simps(3)[where thread="th" and thread'="th'"]}\\
-  @{term "birthtime th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "birthtime th s"}\\
+  @{thm (lhs) last_set.simps(1)[where thread="th"]} & @{text "\<equiv>"} & 
+    @{thm (rhs) last_set.simps(1)[where thread="th"]}\\
+  @{thm (lhs) last_set.simps(2)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} & 
+    @{thm (rhs) last_set.simps(2)[where thread="th" and thread'="th'"]}\\
+  @{thm (lhs) last_set.simps(3)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} & 
+    @{thm (rhs) last_set.simps(3)[where thread="th" and thread'="th'"]}\\
+  @{term "last_set th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "last_set th s"}\\
   \end{tabular}}
   \end{isabelle}
 
@@ -286,8 +334,15 @@
   taking 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 implementation
-  this choice would translate to a quite natural FIFO-scheduling of processes with 
-  the same priority.
+  this choice would translate to a quite natural FIFO-scheduling of threads with 
+  the same priority. 
+  
+  Moylan et al.~\cite{deinheritance} considered the alternative of 
+  ``time-slicing'' threads with equal priority, but found that it does not lead to 
+  advantages in practice. On the contrary, according to their work having a policy 
+  like our FIFO-scheduling of threads with equal priority reduces the number of
+  tasks involved in the inheritance process and thus minimises the number
+  of potentially expensive thread-switches. 
 
   Next, we introduce the concept of \emph{waiting queues}. They are
   lists of threads associated with every resource. The first thread in
@@ -385,7 +440,7 @@
   so that every thread can be in the possession of several resources, that is 
   it has potentially several incoming holding edges in the RAG, but has at most one outgoing  
   waiting edge. The reason is that when a thread asks for resource that is locked
-  already, then the process is blocked and cannot ask for another resource.
+  already, then the thread is blocked and cannot ask for another resource.
   Clearly, also every resource can only have at most one outgoing holding edge---indicating
   that the resource is locked. In this way we can always start at a thread waiting for a 
   resource and ``chase'' outgoing arrows leading to a single root of a tree. 
@@ -394,16 +449,16 @@
 
   The use of relations for representing RAGs allows us to conveniently define
   the notion of the \emph{dependants} of a thread using the transitive closure
-  operation for relations. This gives
+  operation for relations, written ~@{term "trancl DUMMY"}. This gives
 
   \begin{isabelle}\ \ \ \ \ %%%
-  @{thm cs_dependents_def}
+  @{thm cs_dependants_def}
   \end{isabelle}
 
   \noindent
   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
+  wait for a resource to be released (in the picture above this means the dependants
   of @{text "th\<^sub>0"} are @{text "th\<^sub>1"} and @{text "th\<^sub>2"}, which wait for resource @{text "cs\<^sub>1"}, 
   but also @{text "th\<^sub>3"}, 
   which cannot make any progress unless @{text "th\<^sub>2"} makes progress, which
@@ -648,7 +703,7 @@
   assumption on how different resources can be locked and released relative to each 
   other. In our model it is possible that critical sections overlap. This is in 
   contrast to Sha et al \cite{Sha90} who require that critical sections are 
-  properly nested.
+  properly nested (recall Fig.~\ref{overlap}).
 
   A valid state of PIP can then be conveniently be defined as follows:
 
@@ -785,7 +840,15 @@
   finite bound does not guarantee absence of indefinite Priority
   Inversion. For this we further have to assume that every thread
   gives up its resources after a finite amount of time. We found that
-  this assumption is awkward to formalise in our model. Therefore we
+  this assumption is awkward to formalise in our model. There are mainly 
+  two reasons: First, we do not specify what ``running'' the code of a 
+  thread means, for example by giving an operational semantics for
+  machine instructions. Therefore we cannot characterise what are ``good''
+  programs that contain for every looking request also a corresponding
+  unlocking request for a resource. (HERE)
+
+
+  Therefore we
   leave it out and let the programmer assume the responsibility to
   program threads in such a benign manner (in addition to causing no 
   circularity in the RAG). In this detail, we do not
@@ -941,8 +1004,8 @@
   %  @  {thm [display] not_thread_holdents}
   %\item When the number of @{text "P"} equals the number of @{text "V"}, the relevant 
   %  thread does not hold any critical resource, therefore no thread can depend on it
-  %  (@{text "count_eq_dependents"}):
-  %  @  {thm [display] count_eq_dependents}
+  %  (@{text "count_eq_dependants"}):
+  %  @  {thm [display] count_eq_dependants}
   %\end{enumerate}
 
   %The reason that only threads which already held some resoures
@@ -1257,7 +1320,7 @@
   @{text "then"} @{thm (concl) eq_up}.
   \end{tabular}
   \end{isabelle}
-
+ 
   \noindent
   This lemma states that if an intermediate @{term cp}-value does not change, then
   the procedure can also stop, because none of its dependent threads will
@@ -1269,7 +1332,13 @@
   be recalculated for an event. This information is provided by the lemmas we proved.
   We confirmed that our observations translate into practice by implementing
   our version of PIP on top of PINTOS, a small operating system written in C and used for teaching at 
-  Stanford University \cite{PINTOS}. To implement PIP, we only need to modify the kernel 
+  Stanford University \cite{PINTOS}. An alternative would have been the small Xv6 operating 
+  system used for teaching at MIT \cite{Xv6link,Xv6}. However this operating system implements
+  a simple round robin scheduler that lacks stubs for dealing with priorities. This
+  is inconvenient for our purposes.
+
+
+  To implement PIP in PINTOS, we only need to modify the kernel 
   functions corresponding to the events in our formal model. The events translate to the following 
   function interface in PINTOS:
 
@@ -1450,7 +1519,15 @@
   the next thread which takes over a lock is irrelevant for the correctness
   of PIP. Moreover, we eliminated a crucial restriction present in 
   the proof of Sha et al.: they require that critical sections nest properly, 
-  whereas our scheduler allows critical sections to overlap. 
+  whereas our scheduler allows critical sections to overlap. What we
+  are not able to do is to mechanically ``synthesise'' an actual implementation 
+  from our formalisation. To do so for C-code seems quite hard and is beyond 
+  current technology available for Isabelle. Also our proof-method based
+  on events is not ``computational'' in the sense of having a concrete
+  algorithm behind it: our formalisation is really more about the 
+  specification of PIP and ensuring that it has the desired properties
+  (the informal specification by Sha et al.~did not). 
+  
 
   PIP is a scheduling algorithm for single-processor systems. We are
   now living in a multi-processor world. Priority Inversion certainly




