--- a/Journal/Paper.thy Tue Dec 19 14:20:29 2017 +0000
+++ b/Journal/Paper.thy Wed Jan 10 00:28:17 2018 +0000
@@ -138,10 +138,9 @@
implementations and PIP being too complicated and too inefficient.
For example, Yodaiken writes in \cite{Yodaiken02}:
- \begin{quote}
- \it{}``Priority inheritance is neither efficient nor reliable. Implementations
- are either incomplete (and unreliable) or surprisingly complex and intrusive.''
- \end{quote}
+ \begin{quote} \it{}``Priority inheritance is neither efficient nor
+ reliable. Implementations are either incomplete (and unreliable) or
+ surprisingly complex and intrusive.'' \end{quote}
\noindent He suggests avoiding PIP altogether by designing the
system so that no priority inversion may happen in the first
@@ -2137,10 +2136,12 @@
be recalculated for an event. This information is provided by the lemmas we proved.
We confirmed that our observations translate into practice by implementing
our version of PIP on top of PINTOS, a small operating system written in C and used for teaching at
- Stanford University \cite{PINTOS}. An alternative would have been the small Xv6 operating
+ Stanford University \cite{PINTOS}.\footnote{An alternative would have been the small Xv6 operating
system used for teaching at MIT \cite{Xv6link,Xv6}. However this operating system implements
a simple round robin scheduler that lacks stubs for dealing with priorities. This
- is inconvenient for our purposes.
+ is inconvenient for our purposes.} While there is no formal connection between our
+ formalisation and the C-code shown below, the results of the formalisation clearly
+ shine through in the design of the code.
To implement PIP in PINTOS, we only need to modify the kernel
--- a/Journal/document/root.tex Tue Dec 19 14:20:29 2017 +0000
+++ b/Journal/document/root.tex Wed Jan 10 00:28:17 2018 +0000
@@ -52,13 +52,14 @@
\begin{document}
\renewcommand{\thefootnote}{$\star$}
\footnotetext[1]{This paper is a revised, corrected and expanded version of \cite{ZhangUrbanWu12}.
-Compared with that paper we give an actual implementation of our formalised scheduling
-algorithm in C and the operating system PINTOS. Our implementation follows closely all results
-we proved about optimisations of the Priority Inheritance Protocol.
In Section 4 we improve our previous result by proving a finite bound for Priority Inversion.
Moreover, we are giving in this paper
-more details about our proof and also surveying
-the existing literature in more depth.}
+more details about our proof and describe some of our (unverified) C-code for implementing the
+Priority Inversion
+Protocol, as well as surveying
+the existing literature in more depth.
+Our C-code follows closely all results we proved about optimisations of the Priority Inheritance Protocol.
+}
\renewcommand{\thefootnote}{\arabic{footnote}}
\title{Priority Inheritance Protocol Proved Correct$^\star$}
@@ -84,7 +85,7 @@
overlap. Our formalisation in Isabelle/HOL is based on Paulson's
inductive approach to verifying protocols. The formalisation not
only uncovers facts overlooked in the literature, but also helps
- with an efficient implementation of this protocol. Earlier correct
+ with an efficient implementation of this protocol. Earlier
implementations were criticised as too inefficient. Our
implementation builds on top of the small PINTOS operating system
used for teaching.\medskip
--- a/answers.tex Tue Dec 19 14:20:29 2017 +0000
+++ b/answers.tex Wed Jan 10 00:28:17 2018 +0000
@@ -1,4 +1,5 @@
\documentclass{article}
+\usepackage{journal/pdfsetup}
\begin{document}
@@ -43,17 +44,26 @@
\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.
+ \texttt{SOME}, but in this instance we cannot see a way to make
+ this nondeterminism explicit without complicating the
+ topelevel rules about \textit{PIP} on page 12. By using
+ \texttt{SOME}, we can leave implicit the order of the waiting
+ queue returned by release (which corresponds to the original
+ system call from Sha et al). If we represent the non-determinism
+ explicitly, we would need to add another argument to $V$
+ specifying which thread is the next one that obtains the lock and
+ add another premise to the \textit{PIP} rule for ensuring that
+ this thread is member of the waiting queue.
\end{quote}
-\item {\it 3. In \S 4, there is an assumption made about the number of
+\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}
+ \begin{quote}
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
@@ -66,10 +76,10 @@
Otherwise our PIP scheduler could be ``swamped'' with
\textit{Create}-requests of lower priority threads.
\end{quote}
-
+ \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
+ \textit{cs}? This is confusing. \textit{rsc} or \textit{r} would be
better.}
\begin{quote}
@@ -86,20 +96,22 @@
\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.
+\item {\it 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).
+
+
+ We also added a footnote that we are using the standard definition of
+ well-foundedness from Isabelle.
\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
+\item {\it 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).
@@ -109,13 +121,86 @@
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
+ \begin{quote}
+ 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{quote}
\end{itemize}
+
+\section*{Comments by Reviewer \#3}
+
+\begin{itemize}
+\item {\it The verification is at the model level, instead of code level:...}
+
+ \begin{quote}
+ The verification is indeed on the level of the algorithm. A
+ verification of the C-code is *well* beyond the scope of the
+ paper. For example, it would requie a formalised semantics for C
+ (as for example given in the seL4-project). This and interfacing
+ with it would be a tremendous amount of work and we are not sure
+ whether their results would actally sufficient for the code we
+ wrote.
+
+ In light of this, we have made it clearer in the abstract and in a
+ footnote on the first page that our C-code is unverified. Additionally
+ we added the following sentence in Section 5 before we describe the
+ C-code:
+
+ \begin{quote}
+ While there is no formal connection between our formalisation
+ and the C-code shown below, the results of the formalisation
+ clearly shine through in the design of the code.
+ \end{quote}
+ \end{quote}
+
+\item{\it The model cannot express the execution of instructions. As a
+ result, it is difficult to express the case that the critical
+ region does infinite loops without generating events for system
+ calls.}
+
+ \begin{quote}
+ Yes, we discuss this limitation in the first paragraph of section
+ 4 and already wrote that in this aspect we do not
+ improve the limitations of the original paper by Sha et al.
+ \end{quote}
+
+\item{\it The authors should have provided URL of their mechanized
+ proofs for the review process.}
+
+ \begin{quote}
+ As is costumn, we have given a link to the sources.
+ It is mentioned in the last
+ sentence of the conclusion.
+
+ The code of our formalisation can be downloaded from the Mercurial
+ repository at \url{http://talisker.inf.kcl.ac.uk/cgi-bin/repos.cgi/pip}.
+ \end{quote}
+
+\item{\it It is more like engineering work. It's unclear what general
+ principles or theories are proposed.}
+
+ \begin{center}
+ The general point we are making is that a `proof-by-hand' is
+ generally worthless in this area for ensuring the correctness of
+ an algorithm. We underline this point by listing the references
+ [13, 14, 15, 20, 24, 25], which all repeat the error from the
+ original paper.
+
+ More specifically we extend the claims of Sha at al and give
+ a machine-checked formalisation of our claims (the first such
+ formalisation for PIP). We also wrote about our experiences:
+
+ \begin{quote}
+ Following good experience in earlier work [27], our model of PIP
+ is based on Paulson’s inductive approach for protocol
+ verification [18].
+ \end{quote}
+ \end{center}
+
\end{document}
\ No newline at end of file
Binary file journal.pdf has changed