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