41 definition. Better I think to lift the non-determinism and make it |
42 definition. Better I think to lift the non-determinism and make it |
42 more apparent at the top level.} |
43 more apparent at the top level.} |
43 |
44 |
44 \begin{quote} |
45 \begin{quote} |
45 We generally agree with the reviewer about the use of |
46 We generally agree with the reviewer about the use of |
46 \texttt{SOME}, but we cannot see a way to make this nondeterminism |
47 \texttt{SOME}, but in this instance we cannot see a way to make |
47 explicit without complicating too much the topelevel rules. |
48 this nondeterminism explicit without complicating the |
48 \end{quote} |
49 topelevel rules about \textit{PIP} on page 12. By using |
49 |
50 \texttt{SOME}, we can leave implicit the order of the waiting |
50 \item {\it 3. In \S 4, there is an assumption made about the number of |
51 queue returned by release (which corresponds to the original |
|
52 system call from Sha et al). If we represent the non-determinism |
|
53 explicitly, we would need to add another argument to $V$ |
|
54 specifying which thread is the next one that obtains the lock and |
|
55 add another premise to the \textit{PIP} rule for ensuring that |
|
56 this thread is member of the waiting queue. |
|
57 \end{quote} |
|
58 |
|
59 \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 |
60 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 |
61 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 |
62 ugly because it says that there are at most BC many thread |
54 creation events in all possible future traces (of which there are |
63 creation events in all possible future traces (of which there are |
55 of course infinitely many). \ldots} |
64 of course infinitely many). \ldots} |
56 |
65 |
|
66 \begin{quote} |
57 We think this mis-reads our theorem: Although the constrains we |
67 We think this mis-reads our theorem: Although the constrains we |
58 put on thread creation prohibit the creation of higher priority |
68 put on thread creation prohibit the creation of higher priority |
59 threads, the creation of lower priority threads may still consume |
69 threads, the creation of lower priority threads may still consume |
60 CPU time and prevent \textit{th} from accomplishing its task. That |
70 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 |
71 is the purpose we put in the \textit{BC} constraint to limit the |
84 %%%% |
94 %%%% |
85 % Reviever 2. |
95 % Reviever 2. |
86 \section*{Comments by Reviewer \#2} |
96 \section*{Comments by Reviewer \#2} |
87 |
97 |
88 \begin{itemize} |
98 \begin{itemize} |
89 \item Well-founded comment: We adpated the paragraph where \textit{acyclic} |
99 \item {\it Well-founded comment:} We adpated the paragraph where |
90 and \textit{well-founded} are used for the first time. |
100 \textit{acyclic} and \textit{well-founded} are used for the first |
|
101 time. |
91 |
102 |
92 \begin{quote} |
103 \begin{quote} |
93 Note that forests can have trees with infinte depth and containing |
104 Note that forests can have trees with infinte depth and containing |
94 nodes with infinitely many children. A \emph{finite forest} is a |
105 nodes with infinitely many children. A \emph{finite forest} is a |
95 forest whose underlying relation is well-founded and every node |
106 forest whose underlying relation is well-founded and every node |
96 has finitely many children (is only finitely branching). |
107 has finitely many children (is only finitely branching). |
97 \end{quote} |
108 |
98 |
109 |
99 We also added a footnote that we are using the standard definition of |
110 We also added a footnote that we are using the standard definition of |
100 well-foundedness from Isabelle. |
111 well-foundedness from Isabelle. |
101 |
112 \end{quote} |
102 \item Comment about graph-library: This point was also raised by |
113 |
|
114 \item {\it Comment about graph-library:} This point was also raised by |
103 Reviewer~\#1 and we gave a better justification on page 8 (see |
115 Reviewer~\#1 and we gave a better justification on page 8 (see |
104 answer to first point of Reviewer~\#1). |
116 answer to first point of Reviewer~\#1). |
105 |
117 |
106 |
118 |
107 \item {\it 20.) In the case of "Set th prio:", it is not declared what |
119 \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 |
120 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 |
121 Max((prio,|s|),prec th s) or possibly just prec th (e::s) given |
110 the assumptions on Set events listed before).} |
122 the assumptions on Set events listed before).} |
111 |
123 |
112 We note the concern of the reviewer about the effect of the |
124 \begin{quote} |
|
125 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 |
126 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 |
127 equation (6) on page 11, the \textit{cprec} of a thread is |
115 determined by the precedence values in its subtree, while the Set |
128 determined by the precedence values in its subtree, while the Set |
116 operation only changes the precedence of the `Set' thread. If the |
129 operation only changes the precedence of the `Set' thread. If the |
117 reviewer thinks we should add this explanation again, then we are |
130 reviewer thinks we should add this explanation again, then we are |
118 happy to do so. |
131 happy to do so. |
|
132 \end{quote} |
119 |
133 |
120 \end{itemize} |
134 \end{itemize} |
|
135 |
|
136 \section*{Comments by Reviewer \#3} |
|
137 |
|
138 \begin{itemize} |
|
139 \item {\it The verification is at the model level, instead of code level:...} |
|
140 |
|
141 \begin{quote} |
|
142 The verification is indeed on the level of the algorithm. A |
|
143 verification of the C-code is *well* beyond the scope of the |
|
144 paper. For example, it would requie a formalised semantics for C |
|
145 (as for example given in the seL4-project). This and interfacing |
|
146 with it would be a tremendous amount of work and we are not sure |
|
147 whether their results would actally sufficient for the code we |
|
148 wrote. |
|
149 |
|
150 In light of this, we have made it clearer in the abstract and in a |
|
151 footnote on the first page that our C-code is unverified. Additionally |
|
152 we added the following sentence in Section 5 before we describe the |
|
153 C-code: |
|
154 |
|
155 \begin{quote} |
|
156 While there is no formal connection between our formalisation |
|
157 and the C-code shown below, the results of the formalisation |
|
158 clearly shine through in the design of the code. |
|
159 \end{quote} |
|
160 \end{quote} |
|
161 |
|
162 \item{\it The model cannot express the execution of instructions. As a |
|
163 result, it is difficult to express the case that the critical |
|
164 region does infinite loops without generating events for system |
|
165 calls.} |
|
166 |
|
167 \begin{quote} |
|
168 Yes, we discuss this limitation in the first paragraph of section |
|
169 4 and already wrote that in this aspect we do not |
|
170 improve the limitations of the original paper by Sha et al. |
|
171 \end{quote} |
|
172 |
|
173 \item{\it The authors should have provided URL of their mechanized |
|
174 proofs for the review process.} |
|
175 |
|
176 \begin{quote} |
|
177 As is costumn, we have given a link to the sources. |
|
178 It is mentioned in the last |
|
179 sentence of the conclusion. |
|
180 |
|
181 The code of our formalisation can be downloaded from the Mercurial |
|
182 repository at \url{http://talisker.inf.kcl.ac.uk/cgi-bin/repos.cgi/pip}. |
|
183 \end{quote} |
|
184 |
|
185 \item{\it It is more like engineering work. It's unclear what general |
|
186 principles or theories are proposed.} |
|
187 |
|
188 \begin{center} |
|
189 The general point we are making is that a `proof-by-hand' is |
|
190 generally worthless in this area for ensuring the correctness of |
|
191 an algorithm. We underline this point by listing the references |
|
192 [13, 14, 15, 20, 24, 25], which all repeat the error from the |
|
193 original paper. |
|
194 |
|
195 More specifically we extend the claims of Sha at al and give |
|
196 a machine-checked formalisation of our claims (the first such |
|
197 formalisation for PIP). We also wrote about our experiences: |
|
198 |
|
199 \begin{quote} |
|
200 Following good experience in earlier work [27], our model of PIP |
|
201 is based on Paulson’s inductive approach for protocol |
|
202 verification [18]. |
|
203 \end{quote} |
|
204 \end{center} |
|
205 |
121 \end{document} |
206 \end{document} |