diff -r 336ec74969df -r fe3dbfd9123b answers.tex --- 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