44 |
44 |
45 \begin{quote} |
45 \begin{quote} |
46 We generally agree with the reviewer about the use of |
46 We generally agree with the reviewer about the use of |
47 \texttt{SOME}, but in this instance we cannot see a way to make |
47 \texttt{SOME}, but in this instance we cannot see a way to make |
48 this nondeterminism explicit without complicating the |
48 this nondeterminism explicit without complicating the |
49 topelevel rules about \textit{PIP} on page 12. By using |
49 toplevel rules about \textit{PIP} on page 12. By using |
50 \texttt{SOME}, we can leave implicit the order of the waiting |
50 \texttt{SOME}, we can leave implicit the order of the waiting |
51 queue returned by release (which corresponds to the original |
51 queue returned by release (which corresponds to the original |
52 system call from Sha et al). If we represent the non-determinism |
52 system call from Sha et al). If we represent the non-determinism |
53 explicitly, we would need to add another argument to $V$ |
53 explicitly, we would need to add another argument to $V$ |
54 specifying which thread is the next one that obtains the lock and |
54 specifying which thread is the next one that obtains the lock and |
94 %%%% |
94 %%%% |
95 % Reviever 2. |
95 % Reviever 2. |
96 \section*{Comments by Reviewer \#2} |
96 \section*{Comments by Reviewer \#2} |
97 |
97 |
98 \begin{itemize} |
98 \begin{itemize} |
99 \item {\it Well-founded comment:} We adpated the paragraph where |
99 \item {\it Well-founded comment:} We updated the paragraph where |
100 \textit{acyclic} and \textit{well-founded} are used for the first |
100 \textit{acyclic} and \textit{well-founded} are used for the first |
101 time. |
101 time. |
102 |
102 |
103 \begin{quote} |
103 \begin{quote} |
104 Note that forests can have trees with infinte depth and containing |
104 Note that forests can have trees with infinite depth and containing |
105 nodes with infinitely many children. A \emph{finite forest} is a |
105 nodes with infinitely many children. A \emph{finite forest} is a |
106 forest whose underlying relation is well-founded and every node |
106 forest whose underlying relation is well-founded and every node |
107 has finitely many children (is only finitely branching). |
107 has finitely many children (is only finitely branching). |
108 |
108 |
109 |
109 |
139 \item {\it The verification is at the model level, instead of code level:...} |
139 \item {\it The verification is at the model level, instead of code level:...} |
140 |
140 |
141 \begin{quote} |
141 \begin{quote} |
142 The verification is indeed on the level of the algorithm. A |
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 |
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 |
144 paper. For example, it would require a formalised semantics for C |
145 (as for example given in the seL4-project). This and interfacing |
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 |
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 |
147 whether their results would actually sufficient for the code we |
148 wrote. |
148 wrote. |
149 |
149 |
150 In light of this, we have made it clearer in the abstract and in a |
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 |
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 |
152 we added the following sentence in Section 5 before we describe the |
172 |
172 |
173 \item{\it The authors should have provided URL of their mechanized |
173 \item{\it The authors should have provided URL of their mechanized |
174 proofs for the review process.} |
174 proofs for the review process.} |
175 |
175 |
176 \begin{quote} |
176 \begin{quote} |
177 As is costumn, we have given a link to the sources. |
177 As is custom, we have given a link to the sources. |
178 It is mentioned in the last |
178 It is mentioned in the last |
179 sentence of the conclusion. |
179 sentence of the conclusion. |
180 |
180 |
181 The code of our formalisation can be downloaded from the Mercurial |
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}. |
182 repository at \url{http://talisker.inf.kcl.ac.uk/cgi-bin/repos.cgi/pip}. |
183 \end{quote} |
183 \end{quote} |
184 |
184 |
185 \item{\it It is more like engineering work. It's unclear what general |
185 \item{\it It is more like engineering work. It's unclear what general |
186 principles or theories are proposed.} |
186 principles or theories are proposed.} |
187 |
187 |
188 \begin{center} |
188 \begin{quote} |
189 The general point we are making is that a `proof-by-hand' is |
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 |
190 generally worthless in this area for ensuring the correctness of |
191 an algorithm. We underline this point by listing the references |
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 |
192 [13, 14, 15, 20, 24, 25], which all repeat the error from the |
193 original paper. |
193 original paper. |
199 \begin{quote} |
199 \begin{quote} |
200 Following good experience in earlier work [27], our model of PIP |
200 Following good experience in earlier work [27], our model of PIP |
201 is based on Paulson’s inductive approach for protocol |
201 is based on Paulson’s inductive approach for protocol |
202 verification [18]. |
202 verification [18]. |
203 \end{quote} |
203 \end{quote} |
204 \end{center} |
204 \end{quote} |
|
205 |
|
206 \item{\it 1) There are some places that the authors follow the Isabelle |
|
207 syntax, which require more explanation. For instance, in the |
|
208 definitions of "threads" and "priority" in page 5, I had trouble |
|
209 understanding the underscore until I realized that the 4 cases are |
|
210 pattern matching and they have orders.} |
|
211 |
|
212 \begin{quote} |
|
213 We have added the sentence after the definition of \textit{threads}: |
|
214 |
|
215 \begin{quote} |
|
216 We use \_ to match any pattern, like in functional programming. |
|
217 \end{quote} |
|
218 \end{quote} |
|
219 |
|
220 \item{\it 2) The last assumption on page 13: the assumption seems very |
|
221 strong. If you prove Theorem 1 inductively on all s (which means |
|
222 you have to consider s of length 1), then following the assumption |
|
223 you essentially require that the highest priority task is the |
|
224 first task created.} |
|
225 |
|
226 \begin{quote} |
|
227 We feel like this mis-reads what we are proving and how we |
|
228 organised the statements. The thread \textit{th} is the thread |
|
229 with the highest priority in the state \textit{s}. It can be in |
|
230 \textit{s} at any `place'---it does not need to be the first |
|
231 one. What we prove is what happens to \textit{th} in the state |
|
232 \textit{$s' @ s$} which happens after \textit{s}. We only require |
|
233 that threads created after \textit{s} need to have a lower |
|
234 priority. |
|
235 \end{quote} |
|
236 |
|
237 \item{\it 3) 2nd line of the proofs of Lemma 1: th should be th' ?} |
|
238 |
|
239 \begin{quote} |
|
240 Yes, we corrected this error. |
|
241 \end{quote} |
|
242 |
|
243 \item{\it 4) Is your state (event traces) finite or infinite?} |
|
244 |
|
245 \begin{quote} |
|
246 Yes, they are always finite, but can be arbitrary long. |
|
247 \end{quote} |
|
248 |
|
249 \item{\it 5) Assumption at the bottom of page 15: I don't understand |
|
250 why this assumption is necessary. First, is es a finite or |
|
251 infinite trace? If es is finite, of course there's limited number |
|
252 of Create-requests. Even if it can be infinite, I don't see how |
|
253 the PIP scheduler could be "swamped" with create requests. You |
|
254 already assumed that there are no threads of precedence higher |
|
255 than th created in es. If all the newly created threads have lower |
|
256 precedence, they have no chance to run anyway (because of the low |
|
257 precedence). Then why should we care?} |
|
258 |
|
259 \begin{quote} |
|
260 Yes, \textit{es} and \textit{$es @ s$} are finite traces (finite |
|
261 list of events), but they can be arbitrarily long. |
|
262 |
|
263 This means that knowing that \text{es} is finite, does *not* bound |
|
264 the number of create events. |
|
265 |
|
266 We also understand that newly created threads have no chance to |
|
267 run (because of the lower priority), but the process of creating |
|
268 any processes consumes according to our model some time and |
|
269 therefore needs to be bounded. A Create event is not assumed to be |
|
270 `instantaneously'. |
|
271 \end{quote} |
|
272 |
|
273 \item {\it 6) The next assumption in page 16 does not look right to me |
|
274 either. What if there are no actions of th' in es at all, which |
|
275 may be caused by infinite loop inside the critical region of th' |
|
276 (but the loop does not generate any events)? In this case, the |
|
277 assumption is still satisfied because the length is 0, which is |
|
278 less than BND(th').} |
|
279 |
|
280 \begin{quote} |
|
281 We made this point clearer (it was also requested by another reviewer). |
|
282 We discuss this limitation in more depth in the first paragraph of section |
|
283 4 and already wrote that in this aspect we do not |
|
284 improve the limitations of the original paper by Sha et al. |
|
285 \end{quote} |
|
286 |
|
287 \item All other comments have been implemented. |
205 |
288 |
206 \end{document} |
289 \end{document} |