--- a/Journal/Paper.thy	Wed Jan 10 00:28:27 2018 +0000
+++ b/Journal/Paper.thy	Mon Jan 15 11:35:56 2018 +0000
@@ -362,10 +362,12 @@
   \end{tabular}}
   \end{isabelle}
 
-  \noindent
-  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
+  \noindent In this definition @{term "DUMMY # DUMMY"} stands for
+  list-cons and @{term "[]"} for the empty list. We use @{term "DUMMY"}
+  to match any pattern, like in functional programming.
+  Another function
+  calculates the priority for a thread @{text "th"}, which is defined
+  as
 
   \begin{isabelle}\ \ \ \ \ %%%
   \mbox{\begin{tabular}{lcl}
@@ -1174,7 +1176,7 @@
 
   \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
+  "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
   @{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
@@ -1699,7 +1701,7 @@
   \end{quote} 
 
   \noindent By this assumption we enforce that any thread potentially
-  blocking @{term th} must become detached (that is lock no resource
+  blocking @{term th} must become detached (that is it owns no resource
   anymore) after a finite number of events in @{text "es @ s"}. Again
   we have to state this bound to hold in all valid states after @{text
   s}. The bound reflects how each thread @{text "th'"} is programmed:

Binary file answers.pdf has changed

--- a/answers.tex	Wed Jan 10 00:28:27 2018 +0000
+++ b/answers.tex	Mon Jan 15 11:35:56 2018 +0000
@@ -46,7 +46,7 @@
     We generally agree with the reviewer about the use of
     \texttt{SOME}, but in this instance we cannot see a way to make
     this nondeterminism explicit without complicating  the
-    topelevel rules about \textit{PIP} on page 12. By using
+    toplevel rules about \textit{PIP} on page 12. By using
     \texttt{SOME}, we can leave implicit the order of the waiting
     queue returned by release (which corresponds to the original
     system call from Sha et al). If we represent the non-determinism
@@ -96,12 +96,12 @@
 \section*{Comments by Reviewer \#2}
 
 \begin{itemize}
-\item {\it Well-founded comment:} We adpated the paragraph where
+\item {\it Well-founded comment:} We updated the paragraph where
   \textit{acyclic} and \textit{well-founded} are used for the first
   time.
 
   \begin{quote}
-    Note that forests can have trees with infinte depth and containing
+    Note that forests can have trees with infinite depth and containing
     nodes with infinitely many children.  A \emph{finite forest} is a
     forest whose underlying relation is well-founded and every node
     has finitely many children (is only finitely branching).
@@ -141,10 +141,10 @@
   \begin{quote}
     The verification is indeed on the level of the algorithm. A
     verification of the C-code is *well* beyond the scope of the
-    paper. For example, it would requie a formalised semantics for C
+    paper. For example, it would require a formalised semantics for C
     (as for example given in the seL4-project). This and interfacing
     with it would be a tremendous amount of work and we are not sure
-    whether their results would actally sufficient for the code we
+    whether their results would actually sufficient for the code we
     wrote.
 
     In light of this, we have made it clearer in the abstract and in a
@@ -174,7 +174,7 @@
     proofs for the review process.}
 
   \begin{quote}
-    As is costumn, we have given a link to the sources. 
+    As is custom, we have given a link to the sources. 
     It is mentioned in the last
     sentence of the conclusion.
     
@@ -185,7 +185,7 @@
 \item{\it It is more like engineering work. It's unclear what general
     principles or theories are proposed.}
 
-  \begin{center}
+  \begin{quote}
     The general point we are making is that a `proof-by-hand' is
     generally worthless in this area for ensuring the correctness of
     an algorithm. We underline this point by listing the references
@@ -201,6 +201,89 @@
       is based on Paulson’s inductive approach for protocol
       verification [18].
     \end{quote}
-  \end{center}  
+  \end{quote}
+
+\item{\it 1) There are some places that the authors follow the Isabelle
+    syntax, which require more explanation. For instance, in the
+    definitions of "threads" and "priority" in page 5, I had trouble
+    understanding the underscore until I realized that the 4 cases are
+    pattern matching and they have orders.}
+
+  \begin{quote}
+    We have added the sentence after the definition of \textit{threads}:
+
+    \begin{quote}
+    We use \_ to match any pattern, like in functional programming.
+    \end{quote}
+  \end{quote}
+
+\item{\it 2) The last assumption on page 13: the assumption seems very
+    strong. If you  prove Theorem 1 inductively on all  s (which means
+    you have to consider s of length 1), then following the assumption
+    you  essentially require  that the  highest priority  task is  the
+    first task created.}
+
+  \begin{quote}
+    We feel like this mis-reads what we are proving and how we
+    organised the statements. The thread \textit{th} is the thread
+    with the highest priority in the state \textit{s}. It can be in
+    \textit{s} at any `place'---it does not need to be the first
+    one. What we prove is what happens to \textit{th} in the state
+    \textit{$s' @ s$} which happens after \textit{s}. We only require
+    that threads created after \textit{s} need to have a lower
+    priority.
+  \end{quote}
+
+\item{\it 3) 2nd line of the proofs of Lemma 1: th should be th' ?}  
+
+  \begin{quote}
+    Yes, we corrected this error.
+  \end{quote}
+
+\item{\it 4) Is your state (event traces) finite or infinite?}
+
+  \begin{quote}
+    Yes, they are always finite, but can be arbitrary long.
+  \end{quote}
+
+\item{\it 5) Assumption at the bottom of page 15: I don't understand
+    why this assumption is necessary. First, is es a finite or
+    infinite trace? If es is finite, of course there's limited number
+    of Create-requests. Even if it can be infinite, I don't see how
+    the PIP scheduler could be "swamped" with create requests. You
+    already assumed that there are no threads of precedence higher
+    than th created in es. If all the newly created threads have lower
+    precedence, they have no chance to run anyway (because of the low
+    precedence). Then why should we care?}
+
+  \begin{quote}
+    Yes, \textit{es} and \textit{$es @ s$} are finite traces (finite
+    list of events), but they can be arbitrarily long.
+
+    This means that knowing that \text{es} is finite, does *not* bound
+    the number of create events.
+
+    We also understand that newly created threads have no chance to
+    run (because of the lower priority), but the process of creating
+    any processes consumes according to our model some time and
+    therefore needs to be bounded. A Create event is not assumed to be
+    `instantaneously'.
+  \end{quote}
+
+\item {\it 6) The next assumption in page 16 does not look right to me
+    either. What if there are no actions of th' in es at all, which
+    may be caused by infinite loop inside the critical region of th'
+    (but the loop does not generate any events)? In this case, the
+    assumption is still satisfied because the length is 0, which is
+    less than BND(th').}
+
+  \begin{quote}
+    We made this point clearer (it was also requested by another reviewer).
+    We discuss this limitation in more depth in the first paragraph of section
+    4 and already wrote that in this aspect we do not
+    improve the limitations of the original paper by Sha et al.
+  \end{quote}
+
+\item All other comments have been implemented.
   
 \end{document}
\ No newline at end of file

Binary file journal.pdf has changed