\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}