1 \documentclass{article}

     2 

     3 \begin{document}

     4 

     5 %%%%

     6 % Reviewer 1.

     7 \section*{Comments by Reviewer \#1}

     8 

     9 

    10 \begin{itemize}

    11 \item {\it 1.) I don't see the point of working with a more general

    12     library of possibly infinite graphs when it is clear that no

    13     (necessarily finite) evolution of the state could ever generate an

    14     infinite graph.}

    15 

    16   It seemed the most convenient approach for us and we added the following

    17   comment on page 8 about justifying our choice. There was already a

    18   comment about having finiteness as a property, rather than a built-in

    19   assumption.

    20   

    21   \begin{quote}

    22     It seems for our purposes the most convenient representation of

    23     graphs are binary relations given by sets of pairs. The pairs

    24     stand for the edges in graphs. This relation-based representation

    25     has the advantage that the notions \textit{waiting} and

    26     \textit{holding} are already defined in terms of relations

    27     amongst threads and resources.  Also, we can easily re-use the

    28     standard notions of transitive closure operations $\_*$ and $\_+$,

    29     as well as relation composition for our graphs.

    30   \end{quote}

    31 

    32 \item {\it 2.) Later, the release function is defined using Hilbert

    33     choice (Isabelle/HOL's \texttt{SOME} function) as a method for emulating

    34     non-determinism. This is horrid. The highest level generation of

    35     traces handles non-determinism beautifully; using choice at a

    36     lower level lets you keep things functional, but hides the fact

    37     that you want to model non-determinism at the lower level as

    38     well. I agree that the final theorem does imply that the way in

    39     which the new waiting list is chosen is irrelevant, but this

    40     implication is only apparent through a close reading of that

    41     definition. Better I think to lift the non-determinism and make it

    42     more apparent at the top level.}

    43 

    44   \begin{quote}

    45     We generally agree with the reviewer about the use of

    46     \texttt{SOME}, but we cannot see a way to make this nondeterminism

    47     explicit without complicating too much the topelevel rules.

    48   \end{quote}

    49 

    50 \item {\it 3. In \S 4, there is an assumption made about the number of

    51     threads allowed to be created. Given the form of theorem 2, this

    52     seems to me to be unnecessary. It's certainly extremely weird and

    53     ugly because it says that there are at most BC many thread

    54     creation events in all possible future traces (of which there are

    55     of course infinitely many). \ldots}

    56 

    57     We think this mis-reads our theorem: Although the constrains we

    58     put on thread creation prohibit the creation of higher priority

    59     threads, the creation of lower priority threads may still consume

    60     CPU time and prevent \textit{th} from accomplishing its task. That

    61     is the purpose we put in the \textit{BC} constraint to limit the

    62     overall number of thread creations. We slightly augmented the

    63     sentence on page 15 by:

    64 

    65     \begin{quote} 

    66     Otherwise our PIP scheduler could be ``swamped'' with

    67     \textit{Create}-requests of lower priority threads.

    68     \end{quote}

    69 

    70 

    71 \item {\it Why are variables corresponding to resources given the name

    72     \textit{cs}. This is confusing. \textit{rsc} or \textit{r} would be

    73     better.}

    74 

    75   \begin{quote}

    76     \textit{cs} stands for ``critical section'', which is the original name

    77     used by Sha et al to represent ``critical resources''.

    78   \end{quote}

    79 

    80 \item All other comments of the reviewer have been implemented.

    81   

    82 \end{itemize}  

    83 

    84 %%%%

    85 % Reviever 2.

    86 \section*{Comments by Reviewer \#2}

    87 

    88 \begin{itemize}

    89 \item Well-founded comment: We adpated the paragraph where \textit{acyclic}

    90   and \textit{well-founded} are used for the first time.

    91 

    92   \begin{quote}

    93     Note that forests can have trees with infinte depth and containing

    94     nodes with infinitely many children.  A \emph{finite forest} is a

    95     forest whose underlying relation is well-founded and every node

    96     has finitely many children (is only finitely branching).

    97   \end{quote}

    98 

    99   We also added a footnote that we are using the standard definition of

   100   well-foundedness from Isabelle.

   101 

   102 \item Comment about graph-library: This point was also raised by

   103   Reviewer~\#1 and we gave a better justification on page 8 (see

   104   answer to first point of Reviewer~\#1).

   105 

   106 

   107 \item {\it 20.) In the case of "Set th prio:", it is not declared what

   108     the cprec (e::s) th should be (presumably it is something like

   109     Max((prio,|s|),prec th s) or possibly just prec th (e::s) given

   110     the assumptions on Set events listed before).}

   111 

   112   We note the concern of the reviewer about the effect of the

   113   Set-operation on the \textit{cprec} value of a thread. According to

   114   equation (6) on page 11, the \textit{cprec} of a thread is

   115   determined by the precedence values in its subtree, while the Set

   116   operation only changes the precedence of the `Set' thread. If the

   117   reviewer thinks we should add this explanation again, then we are

   118   happy to do so.

   119 

   120 \end{itemize}

   121 \end{document}