--- a/Journal/Paper.thy	Fri Feb 23 21:10:49 2018 +0000
+++ b/Journal/Paper.thy	Fri Jul 06 22:18:39 2018 +0100
@@ -84,8 +84,8 @@
   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 (consider the case where threads with propority $M$
-  continously need to be processed). Since $H$ is blocked by threads
+  indefinitely (consider the case where threads with priority $M$
+  continuously need to be processed). 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.
@@ -94,9 +94,9 @@
   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
+  Earth, the software ran 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
+  intervals. This led 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
   design).  The reason for the shutdowns was that the scheduling
@@ -190,7 +190,7 @@
   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
+  section that ``{\it it resumes the priority it had at the point of entry
   into the critical section}''.  This error can also be found in the
   textbook \cite[Section 16.4.1]{LiYao03} where the authors write
   about this process: ``{\it its priority is immediately lowered to the level originally assigned}'';
@@ -198,7 +198,7 @@
   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
+  section}''. The textbook \cite[Page 286]{Liu00} contains a similar
   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
@@ -208,7 +208,7 @@
   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
+  explained in \cite{Liu00} but left as an ``{\it exercise}'' to the
   reader.  As we shall see, a correct version of PIP does not need to
   maintain this (potentially expensive) log data structure at
   all. Surprisingly also the widely read and frequently updated
@@ -222,7 +222,7 @@
   incorrect behaviour, it seems also many informal descriptions of the
   PIP protocol overlook the possibility that another high-priority
   process might wait for a low-priority process to finish.  A notable
-  exception is the texbook \cite{buttazzo}, which gives the correct
+  exception is the textbook \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
@@ -249,11 +249,11 @@
   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
-  are also being able to generalise the scheduler of Sha et
+  are also 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
+  no proof and also no method for proving which covers this generalised
   case.
 
   \begin{figure}
@@ -332,7 +332,8 @@
 
   \noindent
   whereby threads, priorities and (critical) resources are represented
-  as natural numbers. The event @{term Set} models the situation that
+  as natural numbers. In what follows we shall use @{term cs} as a name for
+  critical resources. The event @{term Set} models the situation that
   a thread obtains a new priority given by the programmer or
   user (for example via the {\tt nice} utility under UNIX).  For states
   we define the following type-synonym:
@@ -787,7 +788,7 @@
 
   \noindent where @{text "SOME"} stands for Hilbert's epsilon and
   implements an arbitrary choice for the next waiting list. It just
-  has to be a list of distinctive threads and contains the same
+  has to be a list of distinct threads and contains the same
   elements as @{text "qs"} (essentially @{text "qs'"} can be any
   reordering of the list @{text "qs"}). This gives for @{term V} the clause:
  
@@ -802,7 +803,7 @@
 
   Having the scheduler function @{term schs} at our disposal, we can
   ``lift'', or overload, the notions @{term waiting}, @{term holding},
-  @{term RAG}, %%@ {term dependants} 
+  @{term RAG}, @{term "TDG"},  %%@ {term dependants} 
   and @{term cp} to operate on states only.
 
   \begin{isabelle}\ \ \ \ \ %%%
@@ -1627,7 +1628,7 @@
   \cite{ZhangUrbanWu12} to leave out this property and let the
   programmer take on the responsibility to program threads in such a
   benign manner (in addition to causing no circularity in the
-  RAG). This leave-it-to-the-programmer was also the approach taken by
+  RAG). This leave-it-to-the-programmer approach was also taken by
   Sha et al.~in their paper.  However, in this paper we can make an
   improvement by establishing a finite bound on the duration of
   Priority Inversion measured by the number of events.  The events can
@@ -1662,10 +1663,10 @@
 
   \[@{text "len (filter isCreate es) < BC"}\;\]  
   
-  wherby @{text es} is a list of events.
+  whereby @{text es} is a list of events.
   \end{quote}
 
-  \noindent Note that it is not enough to just to state that there are
+  \noindent Note that it is not enough to just state that there are
   only finite number of threads created up until a single state @{text
   "s' @ s"} after @{text s}.  Instead, we need to put this bound on
   the @{text "Create"} events for all valid states after @{text s}.
@@ -1685,8 +1686,8 @@
   \noindent This set contains all threads that are not detached in
   state @{text s}. According to our definiton of @{text "detached"},
   this means a thread in @{text "blockers"} either holds or waits for
-  some resource in state @{text s} . Our Thm.~1 implies that any of
-  such threads can all potentially block @{text th} after state
+  some resource in state @{text s} . Our Thm.~1 implies that only 
+  these threads can all potentially block @{text th} after state
   @{text s}. We need to make the following assumption about the
   threads in the @{text "blockers"}-set:
 
@@ -1716,7 +1717,7 @@
   created.  To state our bound formally, we need to make a definition
   of what we mean by intermediate states between a state @{text s} and
   a future state after @{text s}; they will be the list of states
-  starting from @{text s} upto the state \mbox{@{text "es @ s"}}. For
+  starting from @{text s} up to the state \mbox{@{text "es @ s"}}. For
   example, suppose $\textit{es} = [\textit{e}_n, \textit{e}_{n-1},
   \ldots, \textit{e}_2, \textit{e}_1]$, then the intermediate states
   from @{text s} upto @{text "es @ s"} are
@@ -1952,8 +1953,8 @@
   \noindent The first property is again telling us we do not need to
   change the @{text RAG}.  The second shows that the @{term cp}-values
   of all threads other than @{text th} are unchanged. The reason for
-  this is more subtle: Since @{text th} must be running, that is does
-  not wait for any resource to be released, it cannot be in any
+  this is more subtle: Since @{text th} must be running, then it does
+  not wait for any resource to be released and it cannot be in any
   subtree of any other thread. So all current precedences of other
   threads are unchanged.
 
@@ -2309,15 +2310,15 @@
   area of this method is security protocols. 
 
   The second goal of our formalisation is to provide a specification for actually
-  implementing PIP. Textbooks, for example \cite[Section 5.6.5]{Vahalia96},
+  implementing PIP. Textbooks, for example Vahalia \cite[Section 5.6.5]{Vahalia96},
   explain how to use various implementations of PIP and abstractly
   discuss their properties, but surprisingly lack most details important for a
   programmer who wants to implement PIP (similarly Sha et al.~\cite{Sha90}).  
   That this is an issue in practice is illustrated by the
   email from Baker we cited in the Introduction. We achieved also this
   goal: The formalisation allowed us to efficently implement our version
-  of PIP on top of PINTOS \cite{PINTOS}, a simple instructional operating system for the x86 
-  architecture. It also gives the first author enough data to enable
+  of PIP on top of PINTOS, a simple instructional operating system for the x86 
+  architecture implemented by Pfaff \cite{PINTOS}. It also gives the first author enough data to enable
   his undergraduate students to implement PIP (as part of their OS course).
   A byproduct of our formalisation effort is that nearly all
   design choices for the implementation of PIP scheduler are backed up with a proved
@@ -2337,13 +2338,13 @@
 
   PIP is a scheduling algorithm for single-processor systems. We are
   now living in a multi-processor world. Priority Inversion certainly
-  occurs also there, see for example \cite{Brandenburg11,Davis11}.  
+  occurs also there, see for example work by Brandenburg, and Davis and Burns \cite{Brandenburg11,Davis11}.  
   However, there is very little ``foundational''
   work about PIP-algorithms on multi-processor systems.  We are not
   aware of any correctness proofs, not even informal ones. There is an
   implementation of a PIP-algorithm for multi-processors as part of the
   ``real-time'' effort in Linux, including an informal description of the implemented scheduling
-  algorithm given in \cite{LINUX}.  We estimate that the formal
+  algorithm given by Rostedt in \cite{LINUX}.  We estimate that the formal
   verification of this algorithm, involving more fine-grained events,
   is a magnitude harder than the one we presented here, but still
   within reach of current theorem proving technology. We leave this
@@ -2353,12 +2354,11 @@
   if done informally by ``pencil-and-paper''. We infer this from the flawed proof
   in the paper by Sha et al.~\cite{Sha90} and also from \cite{Regehr} where Regehr 
   points out an error in a paper about Preemption 
-  Threshold Scheduling \cite{ThreadX}. The use of a theorem prover was
+  Threshold Scheduling by Wang and Saksena \cite{ThreadX}. The use of a theorem prover was
   invaluable to us in order to be confident about the correctness of our reasoning 
   (for example no corner case can be overlooked).   
   The most closely related work to ours is the formal verification in
-  PVS of the Priority Ceiling Protocol done by Dutertre
-  \cite{dutertre99b}---another solution to the Priority Inversion
+  PVS of the Priority Ceiling Protocol done by Dutertre~\cite{dutertre99b}---another solution to the Priority Inversion
   problem, which however needs static analysis of programs in order to
   avoid it. There have been earlier formal investigations
   into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model