
diff -r fe3dbfd9123b -r 5191a09d9928 Journal/Paper.thy
--- a/Journal/Paper.thy	Mon Jan 15 11:35:56 2018 +0000
+++ b/Journal/Paper.thy	Tue Feb 06 14:38:31 2018 +0000
@@ -210,7 +210,7 @@
   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.  As we shall see, a correct version of PIP does not need to
-  maintain this (potentially expensive) data structure at
+  maintain this (potentially expensive) log data structure at
   all. Surprisingly also the widely read and frequently updated
   textbook \cite{Silberschatz13} gives the wrong specification. On Page 254 the authors write: ``{\it Upon releasing the
   lock, the [low-priority] thread will revert to its original
@@ -229,12 +229,8 @@
   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 %is that such issues clearly show up and cannot be overlooked
-  as in %informal reasoning (since we have to analyse all possible
-  behaviours %of threads, i.e.~\emph{traces}, that could possibly
-  happen).
+  efficiently.\medskip\smallskip
+
 
   \noindent {\bf Contributions:} There have been earlier formal
   investigations into PIP \cite{Faria08,Jahier09,Wellings07}, but they
@@ -245,7 +241,7 @@
   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
+  operating system PINTOS \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
@@ -568,15 +564,8 @@
   for example in Figure~\ref{RAGgraph}.
 
   Because of the @{text RAG}s, we will need to formalise some results
-  about graphs.  While there are a few formalisations for graphs already
-  implemented in Isabelle, we choose to introduce our own library of
-  graphs for PIP. The justification for this is that we wanted to have
-  a more general theory of graphs which is capable of representing
-  potentially infinite graphs (in the sense of infinitely branching
-  and infinite size): the property that our @{text RAG}s are actually
-  forests of finitely branching trees having only a finite depth
-  should be something we can \emph{prove} for our model of PIP---it
-  should not be an assumption we build already into our model. It
+  about graphs.
+  It
   seems for our purposes the most convenient representation of
   graphs are binary relations given by sets of pairs shown in
   \eqref{pairs}. The pairs stand for the edges in graphs. This
@@ -585,7 +574,17 @@
   terms of relations amongst threads and resources. Also, we can easily
   re-use the standard notions for transitive closure operations @{term
   "trancl DUMMY"} and @{term "rtrancl DUMMY"}, as well as relation
-  composition for our graphs.  A \emph{forest} is defined in our
+  composition for our graphs.
+  While there are a few formalisations for graphs already
+  implemented in Isabelle, we choose to introduce our own library of
+  graphs for PIP. The justification for this is that we wanted to have
+  a more general theory of graphs which is capable of representing
+  potentially infinite graphs (in the sense of infinitely branching
+  and infinite size): the property that our @{text RAG}s are actually
+  forests of finitely branching trees having only a finite depth
+  should be something we can \emph{prove} for our model of PIP---it
+  should not be an assumption we build already into our model.
+  A \emph{forest} is defined in our
   representation as the relation @{text rel} that is \emph{single
   valued} and \emph{acyclic}:
 
@@ -613,7 +612,7 @@
   containing nodes with infinitely many children.  A \emph{finite
   forest} is a forest whose underlying relation is
   well-founded\footnote{For \emph{well-founded} we use the quite natural
-  definition from Isabelle.}
+  definition from Isabelle/HOL.}
   and every node has finitely many children (is only finitely
   branching).
 
@@ -630,7 +629,7 @@
 
   %\endnote{{\bf Lemma about overlapping paths}}
   
-  The locking mechanism of PIP ensures that for each thread node,
+  The locking mechanism ensures that for each thread node,
   there can be many incoming holding edges in the @{text RAG}, but at most one
   out going waiting edge.  The reason is that when a thread asks for
   a resource that is locked already, then the thread is blocked and
@@ -663,7 +662,7 @@
   ensure that the resulting @{text RAG} and @{text TDG} are not circular. In practice, the
   programmer has to ensure this. Our model will enforce that critical 
   resources can only be requested provided no circularity can arise (but 
-  they can overlap, see Fig~\ref{overlap}).
+  critical sections can overlap, see Fig~\ref{overlap}).
 
   Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a 
   state @{text s}. It is defined as
@@ -677,7 +676,7 @@
   While the precedence @{term prec} of any
   thread is determined statically (for example when the thread is
   created), the point of the current precedence is to dynamically
-  increase this precedence, if needed according to PIP. Therefore the
+  boost this precedence, if needed according to PIP. Therefore the
   current precedence of @{text th} is given as the maximum of the
   precedences of all threads in its subtree (which includes by definition 
   @{text th} itself). Since the notion of current precedence is defined as the 
@@ -705,7 +704,7 @@
   resource @{text "cs"} and returns the corresponding list of threads
   that lock or wait for it); the second is a function that
   takes a thread and returns its current precedence (see
-  the definition in \eqref{cpreced}). We assume the usual getter and setter methods for
+  the @{text wq} in \eqref{cpreced}). We assume the usual getter and setter methods for
   such records.
 
   In the initial state, the scheduler starts with all resources unlocked (the corresponding 
@@ -727,7 +726,7 @@
   this waiting queue function @{text wq} is unchanged in the next schedule state---because
   none of these events lock or release any resource; 
   for calculating the next @{term "cprec_fun"}, we use @{text wq} and 
-  @{term cpreced}. This gives the following three clauses for @{term schs}:
+  @{term cpreced} defined above. This gives the following three clauses for @{term schs}:
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
@@ -1045,9 +1044,8 @@
   state @{text s} and was waiting for or in the possession of a lock
   in @{text s}. Since in @{text s}, as in every state, the set of
   alive threads is finite, @{text th} can only be blocked by a finite
-  number of threads.  We will actually prove a
-  stronger statement where we also provide the current precedence of
-  the blocking thread. 
+  number of threads.
+  
 
   However, the theorem we are going to prove hinges upon a number of
   natural assumptions about the states @{text s} and @{text "s' @ s"}, the
@@ -1166,7 +1164,8 @@
   % @{text "th_kept"} shows that th is a thread in s'-s
   % }
 
-  Given our assumptions (on @{text th}), the first property we show
+  The next lemma is part of the proof for Theorem~1:
+  Given our assumptions (on~@{text th}), the first property we show
   that a running thread @{text "th'"} must either wait for or hold a
   resource in state @{text s}.
 
@@ -1177,9 +1176,9 @@
   \begin{proof} Let us assume otherwise, that is @{text "th'"} is detached in state
   @{text "s"}, then, according to the definition of detached, @{text
   "th'"} does not hold or wait for any resource. Hence the @{text
-  cp}-value of @{text "th'"} in @{text s} is not boosted, that is
+  cprec}-value of @{text "th'"} in @{text s} is not boosted, that is
   @{term "cp s th' = prec th' s"}, and is therefore lower than the
-  precedence (as well as the @{text "cp"}-value) of @{term "th"}. This
+  precedence (as well as the @{text "cprec"}-value) of @{term "th"}. This
   means @{text "th'"} will not run as long as @{text "th"} is a live
   thread. In turn this means @{text "th'"} cannot take any action in
   state @{text "s' @ s"} to change its current status; therefore
@@ -1647,8 +1646,8 @@
   this concept of active or hibernating threads in our model.  In fact
   we can dispense with the first assumption altogether and allow that
   in our model we can create new threads or exit existing threads
-  arbitrarily. Consequently, the avoidance of indefinite priority
-  inversion we are trying to establish is in our model not true,
+  arbitrarily. Consequently, the absence of indefinite priority
+  inversion we are trying to establish in our model is not true,
   unless we stipulate an upper bound on the number of threads that
   have been created during the time leading to any future state after
   @{term s}. Otherwise our PIP scheduler could be ``swamped'' with
@@ -1671,9 +1670,9 @@
   "s' @ s"} after @{text s}.  Instead, we need to put this bound on
   the @{text "Create"} events for all valid states after @{text s}.
   This ensures that no matter which ``future'' state is reached, the
-  number of @{text "Create"}-events is finite. We use @{text "es @ s"}
-  to stand for \emph{future states} after @{text s}---it is @{text s}
-  extended with some list @{text es} of events.
+  number of @{text "Create"}-events is finite. This bound @{text BC} is assumed 
+ with respect to all future states @{text "es @ s"}
+  of @{text s}, not just a single one.
 
   For our second assumption about giving up resources after a finite
   amount of ``time'', let us introduce the following definition about
@@ -1687,7 +1686,7 @@
   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
-  those threads can all potentially block @{text th} after state
+  such 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:
 
@@ -1779,9 +1778,12 @@
   \end{array} 
   \end{equation}
 
-  \noindent Second by Thm~\ref{mainthm}, the events are either the
-  actions of @{text th} or @{text "Create"}-events or actions of the
-  threads in blockers. That is
+  \noindent 
+  The actions in @{text es} can be partitioned into the actions of @{text th} and the
+  actions of threads other than @{text th}. The latter can further be divided
+  into actions of existing threads and the actions to create new
+  ones. Moreover, the actions of existing threads other than @{text th}
+  are by Thm 1 the actions of blockers. This gives rise to 
   %
   \begin{equation}\label{secondeq}
   \begin{array}{lcl}
@@ -1889,14 +1891,9 @@
   a standard scheduling operation and implemented in most operating
   systems.
 
-  %\begin{proof}[of Lemma~\ref{childrenlem}]
-  %Test
-  %\end{proof}
-
-  Of course the main work for implementing PIP involves the
-  scheduler and coding how it should react to events.  Below we
-  outline how our formalisation guides this implementation for each
-  kind of events.\smallskip
+  Below we
+  outline how our formalisation guides the efficient calculation of @{text cprecs}
+  in response to each kind of events.\smallskip
 *}
 
 text {*
@@ -2013,7 +2010,7 @@
 
   \begin{isabelle}\ \ \ \ \ %%%
   @{text "If"} @{text "th'' \<noteq> th"} and 
-  @{text "th'' \<noteq> th'"}
+  @{text "th'' \<noteq> th'"} \;\;@{text then}\;\;
   @{thm (concl) valid_trace_v_n.cp_kept[where ?th1.0="th''"]}
   \hfill\numbered{fone}
   \end{isabelle}
@@ -2096,7 +2093,7 @@
 
   \noindent That means we have to add a waiting edge to the @{text
   RAG}. Furthermore the current precedence for all threads that are
-  not ancestors of @{text "th"} are unchanged. For the ancestors of 
+  not ancestors of @{text "th"} (in the new @{text RAG} or @{text TDG}) are unchanged. For the ancestors of 
   @{text th} we need
   to follow the edges in the @{text TDG} and recompute the @{term
   "cprecs"}. Whereas in all other event we might have to make
@@ -2247,7 +2244,7 @@
   The waiting queue is referenced in the usual C-way as @{ML_text "&lock->wq"}. 
   Next, we record that the current thread is waiting for the lock (Line 10).
   Thus we established two pointers: one in the waiting queue of the lock pointing to the 
-  current thread, and the other from the currend thread pointing to the lock.
+  current thread, and the other from the current thread pointing to the lock.
   According to our specification in Section~\ref{model} and the properties we were able 
   to prove for @{text P}, we need to ``chase'' all the ancestor threads
   in the @{text RAG} and update their




