--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/answers.tex Tue Dec 19 14:20:29 2017 +0000
@@ -0,0 +1,121 @@
+\documentclass{article}
+
+\begin{document}
+
+%%%%
+% Reviewer 1.
+\section*{Comments by Reviewer \#1}
+
+
+\begin{itemize}
+\item {\it 1.) I don't see the point of working with a more general
+ library of possibly infinite graphs when it is clear that no
+ (necessarily finite) evolution of the state could ever generate an
+ infinite graph.}
+
+ It seemed the most convenient approach for us and we added the following
+ comment on page 8 about justifying our choice. There was already a
+ comment about having finiteness as a property, rather than a built-in
+ assumption.
+
+ \begin{quote}
+ It seems for our purposes the most convenient representation of
+ graphs are binary relations given by sets of pairs. The pairs
+ stand for the edges in graphs. This relation-based representation
+ has the advantage that the notions \textit{waiting} and
+ \textit{holding} are already defined in terms of relations
+ amongst threads and resources. Also, we can easily re-use the
+ standard notions of transitive closure operations $\_*$ and $\_+$,
+ as well as relation composition for our graphs.
+ \end{quote}
+
+\item {\it 2.) Later, the release function is defined using Hilbert
+ choice (Isabelle/HOL's \texttt{SOME} function) as a method for emulating
+ non-determinism. This is horrid. The highest level generation of
+ traces handles non-determinism beautifully; using choice at a
+ lower level lets you keep things functional, but hides the fact
+ that you want to model non-determinism at the lower level as
+ well. I agree that the final theorem does imply that the way in
+ which the new waiting list is chosen is irrelevant, but this
+ implication is only apparent through a close reading of that
+ definition. Better I think to lift the non-determinism and make it
+ more apparent at the top level.}
+
+ \begin{quote}
+ We generally agree with the reviewer about the use of
+ \texttt{SOME}, but we cannot see a way to make this nondeterminism
+ explicit without complicating too much the topelevel rules.
+ \end{quote}
+
+\item {\it 3. In \S 4, there is an assumption made about the number of
+ threads allowed to be created. Given the form of theorem 2, this
+ seems to me to be unnecessary. It's certainly extremely weird and
+ ugly because it says that there are at most BC many thread
+ creation events in all possible future traces (of which there are
+ of course infinitely many). \ldots}
+
+ We think this mis-reads our theorem: Although the constrains we
+ put on thread creation prohibit the creation of higher priority
+ threads, the creation of lower priority threads may still consume
+ CPU time and prevent \textit{th} from accomplishing its task. That
+ is the purpose we put in the \textit{BC} constraint to limit the
+ overall number of thread creations. We slightly augmented the
+ sentence on page 15 by:
+
+ \begin{quote}
+ Otherwise our PIP scheduler could be ``swamped'' with
+ \textit{Create}-requests of lower priority threads.
+ \end{quote}
+
+
+\item {\it Why are variables corresponding to resources given the name
+ \textit{cs}. This is confusing. \textit{rsc} or \textit{r} would be
+ better.}
+
+ \begin{quote}
+ \textit{cs} stands for ``critical section'', which is the original name
+ used by Sha et al to represent ``critical resources''.
+ \end{quote}
+
+\item All other comments of the reviewer have been implemented.
+
+\end{itemize}
+
+%%%%
+% Reviever 2.
+\section*{Comments by Reviewer \#2}
+
+\begin{itemize}
+\item Well-founded comment: We adpated 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
+ 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).
+ \end{quote}
+
+ We also added a footnote that we are using the standard definition of
+ well-foundedness from Isabelle.
+
+\item Comment about graph-library: This point was also raised by
+ Reviewer~\#1 and we gave a better justification on page 8 (see
+ answer to first point of Reviewer~\#1).
+
+
+\item {\it 20.) In the case of "Set th prio:", it is not declared what
+ the cprec (e::s) th should be (presumably it is something like
+ Max((prio,|s|),prec th s) or possibly just prec th (e::s) given
+ the assumptions on Set events listed before).}
+
+ We note the concern of the reviewer about the effect of the
+ Set-operation on the \textit{cprec} value of a thread. According to
+ equation (6) on page 11, the \textit{cprec} of a thread is
+ determined by the precedence values in its subtree, while the Set
+ operation only changes the precedence of the `Set' thread. If the
+ reviewer thinks we should add this explanation again, then we are
+ happy to do so.
+
+\end{itemize}
+\end{document}
\ No newline at end of file