
diff -r d37703e0c5c4 -r df0334468335 Journal/Paper.thy
--- a/Journal/Paper.thy	Sat Jan 16 10:59:03 2016 +0800
+++ b/Journal/Paper.thy	Sat Jan 16 11:02:17 2016 +0800
@@ -5,10 +5,8 @@
         "~~/src/HOL/Library/LaTeXsugar"
 begin
 
-
 declare [[show_question_marks = false]]
 
-
 notation (latex output)
   Cons ("_::_" [78,77] 73) and
   If  ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
@@ -25,40 +23,43 @@
   cpreced ("cprec") and
   cp ("cprec") and
   holdents ("resources") and
-  DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")
+  DUMMY  ("\<^raw:\mbox{$\_\!\_$}>") and
+  cntP ("c\<^bsub>P\<^esub>") and
+  cntV ("c\<^bsub>V\<^esub>")
  
 (*>*)
 
 section {* Introduction *}
 
 text {*
-  Many real-time systems need to support threads involving priorities and
-  locking of resources. Locking of resources ensures mutual exclusion
-  when accessing shared data or devices that cannot be
+
+  Many real-time systems need to support threads involving priorities
+  and locking of resources. Locking of resources ensures mutual
+  exclusion when accessing shared data or devices that cannot be
   preempted. Priorities allow scheduling of threads that need to
   finish their work within deadlines.  Unfortunately, both features
   can interact in subtle ways leading to a problem, called
   \emph{Priority Inversion}. Suppose three threads having priorities
   $H$(igh), $M$(edium) and $L$(ow). We would expect that the thread
-  $H$ blocks any other thread with lower priority and the thread itself cannot
-  be blocked indefinitely by threads with lower priority. Alas, in a naive
-  implementation of resource locking and priorities this property can
-  be violated. For this let $L$ be in the
+  $H$ blocks any other thread with lower priority and the thread
+  itself cannot be blocked indefinitely by threads with lower
+  priority. Alas, in a naive implementation of resource locking and
+  priorities this property can be violated. For this let $L$ be in the
   possession of a lock for a resource that $H$ also needs. $H$ must
   therefore wait for $L$ to exit the critical section and release this
-  lock. The problem is that $L$ might in turn be blocked by any
-  thread with priority $M$, and so $H$ sits there potentially waiting
-  indefinitely. Since $H$ is blocked by threads with lower
-  priorities, the problem is called Priority Inversion. It was first
-  described in \cite{Lampson80} in the context of the
-  Mesa programming language designed for concurrent programming.
+  lock. The problem is that $L$ might in turn be blocked by any thread
+  with priority $M$, and so $H$ sits there potentially waiting
+  indefinitely. Since $H$ is blocked by threads with lower priorities,
+  the problem is called Priority Inversion. It was first described in
+  \cite{Lampson80} in the context of the Mesa programming language
+  designed for concurrent programming.
  
   If the problem of Priority Inversion is ignored, real-time systems
   can become unpredictable and resulting bugs can be hard to diagnose.
   The classic example where this happened is the software that
-  controlled the Mars Pathfinder mission in 1997 \cite{Reeves98}.
-  On Earth the software run mostly without any problem, but
-  once the spacecraft landed on Mars, it shut down at irregular, but frequent,
+  controlled the Mars Pathfinder mission in 1997 \cite{Reeves98}.  On
+  Earth the software run mostly without any problem, but once the
+  spacecraft landed on Mars, it shut down at irregular, but frequent,
   intervals leading to loss of project time as normal operation of the
   craft could only resume the next day (the mission and data already
   collected were fortunately not lost, because of a clever system
@@ -69,11 +70,11 @@
   rectified by enabling the \emph{Priority Inheritance Protocol} (PIP)
   \cite{Sha90}\footnote{Sha et al.~call it the \emph{Basic Priority
   Inheritance Protocol} \cite{Sha90} and others sometimes also call it
-  \emph{Priority Boosting}, \emph{Priority Donation} or \emph{Priority Lending}.} 
-  in the scheduling software.
+  \emph{Priority Boosting}, \emph{Priority Donation} or \emph{Priority
+  Lending}.}  in the scheduling software.
 
-  The idea behind PIP is to let the thread $L$ temporarily inherit
-  the high priority from $H$ until $L$ leaves the critical section
+  The idea behind PIP is to let the thread $L$ temporarily inherit the
+  high priority from $H$ until $L$ leaves the critical section
   unlocking the resource. This solves the problem of $H$ having to
   wait indefinitely, because $L$ cannot be blocked by threads having
   priority $M$. While a few other solutions exist for the Priority
@@ -81,21 +82,21 @@
   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 nearly all HP inkjet printers \cite{ThreadX}), but also
-  the POSIX 1003.1c Standard realised for
-  example in libraries for FreeBSD, Solaris and Linux. 
+  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.
 
-  Two advantages of PIP are that it is deterministic and that increasing the priority of a thread
-  can be performed dynamically by the scheduler.
-  This is in contrast to \emph{Priority Ceiling}
+  Two advantages of PIP are that it is deterministic and that
+  increasing the priority of a thread can be performed dynamically by
+  the scheduler.  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 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
-  PIP. For instance, PIP cannot prevent deadlocks when lock
-  dependencies are circular, and also blocking times can be
+  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 PIP. For instance, PIP cannot prevent deadlocks
+  when lock dependencies are circular, and also blocking times can be
   substantial (more than just the duration of a critical section).
   Though, most criticism against PIP centres around unreliable
   implementations and PIP being too complicated and too inefficient.
@@ -106,18 +107,19 @@
   are either incomplete (and unreliable) or surprisingly complex and intrusive.''
   \end{quote}
 
-  \noindent
-  He suggests avoiding PIP altogether by designing the system so that no 
-  priority inversion may happen in the first place. However, such ideal designs may 
-  not always be achievable in practice.
+  \noindent He suggests avoiding PIP altogether by designing the
+  system so that no priority inversion may happen in the first
+  place. However, such ideal designs may not always be achievable in
+  practice.
 
   In our opinion, there is clearly a need for investigating correct
-  algorithms for PIP. A few specifications for PIP exist (in English)
-  and also a few high-level descriptions of implementations (e.g.~in
-  the textbooks \cite[Section 12.3.1]{Liu00} and \cite[Section 5.6.5]{Vahalia96}), 
-  but they help little with actual implementations. That this is a problem in 
-  practice is proved by an email by Baker, who wrote on 13 July 2009 on the Linux
-  Kernel mailing list:
+  algorithms for PIP. A few specifications for PIP exist (in informal
+  English) and also a few high-level descriptions of implementations
+  (e.g.~in the textbooks \cite[Section 12.3.1]{Liu00} and
+  \cite[Section 5.6.5]{Vahalia96}), but they help little with actual
+  implementations. That this is a problem in practice is proved by an
+  email by Baker, who wrote on 13 July 2009 on the Linux Kernel
+  mailing list:
 
   \begin{quote}
   \it{}``I observed in the kernel code (to my disgust), the Linux PIP
@@ -127,70 +129,69 @@
   wait operations.''
   \end{quote}
 
-  \noindent
-  The criticism by Yodaiken, Baker and others suggests another look
-  at PIP from a more abstract level (but still concrete enough
-  to inform an implementation), and makes PIP a good candidate for a
-  formal verification. An additional reason is that the original
+  \noindent The criticism by Yodaiken, Baker and others suggests
+  another look at PIP from a more abstract level (but still concrete
+  enough to inform an implementation), and makes PIP a good candidate
+  for a formal verification. An additional reason is that the original
   specification of PIP~\cite{Sha90}, despite being informally
-  ``proved'' correct, is actually \emph{flawed}. 
+  ``proved'' correct, is actually \emph{flawed}.
   
-
   Yodaiken \cite{Yodaiken02} and also Moylan et
   al.~\cite{deinheritance} 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 ``{\it
-  returns to its original priority level}''. This leads them to
+  overlooked in the informal proof by Sha et al. They specify PIP in
+  \cite{Sha90} so that after the thread (whose priority has been
+  raised) 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. Moylan et
-  al.~write that there are ``{\it some hidden traps}''~\cite{deinheritance}.  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 with $H'$ (which waits for the
-  other resource). The correct 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 it resumes the priority it had at the point
-  of entry into the critical section}''.  This error can also be
-  found in the more recent textbook \cite[Page 119]{Laplante11} where the
-  authors state: ``{\it when [the task] exits the critical section that caused
+  al.~write that there are ``{\it some hidden
+  traps}''~\cite{deinheritance}.  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 with $H'$ (which waits for the other
+  resource). The correct 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 it resumes the priority it had at the point of entry
+  into the critical section}''.  This error can also be found in the
+  more recent textbook \cite[Page 119]{Laplante11} where the authors
+  state: ``{\it when [the task] exits the critical section that caused
   the block, it reverts to the priority it had when it entered that
   section}''. The textbook \cite[Page 286]{Liu00} contains a simlar
-  flawed specification and even goes on to develop pseudo-code based on this
-  flawed specification. Accordingly, the operating system primitives
-  for inheritance and restoration of priorities in \cite{Liu00} depend on
-  maintaining a  data structure called \emph{inheritance log}. This log
-  is maintained for every thread and broadly specified as containing ``{\it
-  [h]istorical information on how the thread inherited its current
-  priority}'' \cite[Page 527]{Liu00}. Unfortunately, the important
-  information about actually
-  computing the priority to be restored solely from this log is  not explained in
-  \cite{Liu00} but left as an ``{\it excercise}'' to the reader.
-  Of course, a correct version of PIP does not need to maintain
-  this (potentially expensive) data structure at all. Surprisingly
-  also the widely read and frequently updated textbook \cite{Silberschatz13} gives
-  the wrong specification. For example on Page 254 the
-  authors write: ``{\it Upon releasing the lock, the [low-priority] thread
-  will revert to its original priority.}'' The same error is also repeated
-  later in this textbook.
+  flawed specification and even goes on to develop pseudo-code based
+  on this flawed specification. Accordingly, the operating system
+  primitives for inheritance and restoration of priorities in
+  \cite{Liu00} depend on maintaining a data structure called
+  \emph{inheritance log}. This log is maintained for every thread and
+  broadly specified as containing ``{\it [h]istorical information on
+  how the thread inherited its current priority}'' \cite[Page
+  527]{Liu00}. Unfortunately, the important information about actually
+  computing the priority to be restored solely from this log is not
+  explained in \cite{Liu00} but left as an ``{\it excercise}'' to the
+  reader.  Of course, a correct version of PIP does not need to
+  maintain this (potentially expensive) data structure at
+  all. Surprisingly also the widely read and frequently updated
+  textbook \cite{Silberschatz13} gives the wrong specification. For
+  example on Page 254 the authors write: ``{\it Upon releasing the
+  lock, the [low-priority] thread will revert to its original
+  priority.}'' The same error is also repeated later in this textbook.
 
   
-  While \cite{Laplante11,Liu00,book,Sha90,Silberschatz13} are the only formal publications we have 
-  found that specify the incorrect behaviour, it seems also many
-  informal descriptions of PIP overlook the possibility that another
-  high-priority might wait for a low-priority process to finish.
-  A notable exception is the texbook \cite{buttazzo}, which gives the correct 
-  behaviour of resetting the priority of a thread to the highest remaining priority of the 
-  threads it blocks. This textbook also gives an informal proof for 
-  the correctness of PIP in the style of Sha et al. Unfortunately, this informal 
-  proof is too vague to be useful for formalising the correctness of PIP
-  and the specification leaves out nearly all details in order 
-  to implement PIP efficiently.\medskip\smallskip
+  While \cite{Laplante11,Liu00,book,Sha90,Silberschatz13} are the only
+  formal publications we have found that specify the incorrect
+  behaviour, it seems also many informal descriptions of PIP overlook
+  the possibility that another high-priority might wait for a
+  low-priority process to finish.  A notable exception is the texbook
+  \cite{buttazzo}, which gives the correct behaviour of resetting the
+  priority of a thread to the highest remaining priority of the
+  threads it blocks. This textbook also gives an informal proof for
+  the correctness of PIP in the style of Sha et al. Unfortunately,
+  this informal proof is too vague to be useful for formalising the
+  correctness of PIP and the specification leaves out nearly all
+  details in order to implement PIP efficiently.\medskip\smallskip
   %
   %The advantage of formalising the
   %correctness of a high-level specification of PIP in a theorem prover
@@ -198,27 +199,29 @@
   %informal reasoning (since we have to analyse all possible behaviours
   %of threads, i.e.~\emph{traces}, that could possibly happen).
 
-  \noindent
-  {\bf Contributions:} There have been earlier formal investigations
-  into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model
-  checking techniques. This paper presents a formalised and
-  mechanically checked proof for the correctness of PIP. For this we 
-  needed to design a new correctness criterion for PIP. In contrast to model checking, our
-  formalisation provides insight into why PIP is correct and allows us
-  to prove stronger properties that, as we will show, can help with an
-  efficient implementation of PIP in the educational PINTOS operating
-  system \cite{PINTOS}.  For example, we found by ``playing'' with the
-  formalisation that the choice of the next thread to take over a lock
-  when a resource is released is irrelevant for PIP being correct---a
-  fact that has not been mentioned in the literature and not been used
-  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 being able to generalise the scheduler of Sha
-  et al.~\cite{Sha90} to the practically relevant case where critical 
-  sections can overlap; see Figure~\ref{overlap} \emph{a)} below for an example of 
-  this restriction. %In the existing literature there is no 
-  %proof and also no proving method that cover this generalised case.
+  \noindent {\bf Contributions:} There have been earlier formal
+  investigations into PIP \cite{Faria08,Jahier09,Wellings07}, but they
+  employ model checking techniques. This paper presents a formalised
+  and mechanically checked proof for the correctness of PIP. For this
+  we needed to design a new correctness criterion for PIP. In contrast
+  to model checking, our formalisation provides insight into why PIP
+  is correct and allows us to prove stronger properties that, as we
+  will show, can help with an efficient implementation of PIP. We
+  illustrate this with an implementation of PIP in the educational
+  PINTOS operating system \cite{PINTOS}.  For example, we found by
+  ``playing'' with the formalisation that the choice of the next
+  thread to take over a lock when a resource is released is irrelevant
+  for PIP being correct---a fact that has not been mentioned in the
+  literature and not been used 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 being able to generalise the scheduler of Sha et
+  al.~\cite{Sha90} to the practically relevant case where critical
+  sections can overlap; see Figure~\ref{overlap} \emph{a)} below for
+  an example of this restriction. In the existing literature there is
+  no proof and also no proving method that cover this generalised
+  case.
 
   \begin{figure}
   \begin{center}
@@ -384,6 +387,18 @@
   tasks involved in the inheritance process and thus minimises the number
   of potentially expensive thread-switches. 
 
+  We will also need counters for @{term P} and @{term V} events of a thread @{term th}
+  in a state @{term s}. This can be straightforwardly defined in Isabelle as
+
+  \begin{isabelle}\ \ \ \ \ %%%
+  \mbox{\begin{tabular}{@ {}l}
+  @{thm cntP_def}\\
+  @{thm cntV_def}
+  \end{tabular}}
+  \end{isabelle}
+
+  \noindent using the predefined function @{const count} for lists.
+
   Next, we introduce the concept of \emph{waiting queues}. They are
   lists of threads associated with every resource. The first thread in
   this list (i.e.~the head, or short @{term hd}) is chosen to be the one 
@@ -945,8 +960,39 @@
   From these two lemmas we can see the correctness of PIP, which is
   that: the blockage of th is reasonable and under control.
 
+  Lemmas we want to describe:
+
+  \begin{lemma}
+  @{thm eq_pv_persist}
+  \end{lemma}
+
+  \begin{lemma}
+  @{thm eq_pv_blocked}
+  \end{lemma}
+
+  \begin{lemma}
+  @{thm runing_cntP_cntV_inv}
+  \end{lemma}
+
+  \noindent
+  Remember we do not have the well-nestedness restriction in our
+  proof, which means the difference between the counters @{const cntV}
+  and @{const cntP} can be larger than @{term 1}.
+
+  \begin{lemma}
+  @{thm runing_inversion}
+  \end{lemma}
+  
+
+  \begin{lemma}
+  @{thm th_blockedE}
+  \end{lemma}
+
   \subsection*{END OUTLINE}
 
+
+
+
   In what follows we will describe properties of PIP that allow us to prove 
   Theorem~\ref{mainthm} and, when instructive, briefly describe our argument. 
   It is relatively easy to see that:
@@ -959,7 +1005,7 @@
   \end{isabelle}
 
   \noindent
-  The second property is by induction of @{term vt}. The next three
+  The second property is by induction on @{term vt}. The next three
   properties are: 
 
   \begin{isabelle}\ \ \ \ \ %%%




