
diff -r 83ba2d8c859a -r 2aa37de77f31 Journal/Paper.thy
--- a/Journal/Paper.thy	Thu Jan 14 00:55:54 2016 +0800
+++ b/Journal/Paper.thy	Thu Jan 14 03:29:22 2016 +0000
@@ -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
@@ -32,33 +30,34 @@
 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 +68,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 +80,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 +105,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,57 +127,55 @@
   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 




