--- a/Journal/Paper.thy Thu Jan 14 03:29:22 2016 +0000
+++ b/Journal/Paper.thy Fri Jan 15 02:05:29 2016 +0000
@@ -23,7 +23,9 @@
cpreced ("cprec") and
cp ("cprec") and
holdents ("resources") and
- DUMMY ("\<^raw:\mbox{$\_\!\_$}>")
+ DUMMY ("\<^raw:\mbox{$\_\!\_$}>") and
+ cntP ("c\<^bsub>P\<^esub>") and
+ cntV ("c\<^bsub>V\<^esub>")
(*>*)
@@ -178,17 +180,18 @@
priority.}'' The same error is also repeated later in this textbook.
- While \cite{Laplante11,Liu00,book,Sha90,Silberschatz13} are the only formal publications we have
- found that specify the incorrect behaviour, it seems also many
- informal descriptions of PIP overlook the possibility that another
- high-priority might wait for a low-priority process to finish.
- A notable exception is the texbook \cite{buttazzo}, which gives the correct
- behaviour of resetting the priority of a thread to the highest remaining priority of the
- threads it blocks. This textbook also gives an informal proof for
- the correctness of PIP in the style of Sha et al. Unfortunately, this informal
- proof is too vague to be useful for formalising the correctness of PIP
- and the specification leaves out nearly all details in order
- to implement PIP efficiently.\medskip\smallskip
+ While \cite{Laplante11,Liu00,book,Sha90,Silberschatz13} are the only
+ formal publications we have found that specify the incorrect
+ behaviour, it seems also many informal descriptions of PIP overlook
+ the possibility that another high-priority might wait for a
+ low-priority process to finish. A notable exception is the texbook
+ \cite{buttazzo}, which gives the correct behaviour of resetting the
+ priority of a thread to the highest remaining priority of the
+ threads it blocks. This textbook also gives an informal proof for
+ the correctness of PIP in the style of Sha et al. Unfortunately,
+ this informal proof is too vague to be useful for formalising the
+ correctness of PIP and the specification leaves out nearly all
+ details in order to implement PIP efficiently.\medskip\smallskip
%
%The advantage of formalising the
%correctness of a high-level specification of PIP in a theorem prover
@@ -196,27 +199,29 @@
%informal reasoning (since we have to analyse all possible behaviours
%of threads, i.e.~\emph{traces}, that could possibly happen).
- \noindent
- {\bf Contributions:} There have been earlier formal investigations
- into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model
- checking techniques. This paper presents a formalised and
- mechanically checked proof for the correctness of PIP. For this we
- needed to design a new correctness criterion for PIP. In contrast to model checking, our
- formalisation provides insight into why PIP is correct and allows us
- to prove stronger properties that, as we will show, can help with an
- efficient implementation of PIP in the educational PINTOS operating
- system \cite{PINTOS}. For example, we found by ``playing'' with the
- formalisation that the choice of the next thread to take over a lock
- when a resource is released is irrelevant for PIP being correct---a
- fact that has not been mentioned in the literature and not been used
- in the reference implementation of PIP in PINTOS. This fact, however, is important
- for an efficient implementation of PIP, because we can give the lock
- to the thread with the highest priority so that it terminates more
- quickly. We were also being able to generalise the scheduler of Sha
- et al.~\cite{Sha90} to the practically relevant case where critical
- sections can overlap; see Figure~\ref{overlap} \emph{a)} below for an example of
- this restriction. %In the existing literature there is no
- %proof and also no proving method that cover this generalised case.
+ \noindent {\bf Contributions:} There have been earlier formal
+ investigations into PIP \cite{Faria08,Jahier09,Wellings07}, but they
+ employ model checking techniques. This paper presents a formalised
+ and mechanically checked proof for the correctness of PIP. For this
+ we needed to design a new correctness criterion for PIP. In contrast
+ to model checking, our formalisation provides insight into why PIP
+ is correct and allows us to prove stronger properties that, as we
+ will show, can help with an efficient implementation of PIP. We
+ illustrate this with an implementation of PIP in the educational
+ PINTOS operating system \cite{PINTOS}. For example, we found by
+ ``playing'' with the formalisation that the choice of the next
+ thread to take over a lock when a resource is released is irrelevant
+ for PIP being correct---a fact that has not been mentioned in the
+ literature and not been used in the reference implementation of PIP
+ in PINTOS. This fact, however, is important for an efficient
+ implementation of PIP, because we can give the lock to the thread
+ with the highest priority so that it terminates more quickly. We
+ were also being able to generalise the scheduler of Sha et
+ al.~\cite{Sha90} to the practically relevant case where critical
+ sections can overlap; see Figure~\ref{overlap} \emph{a)} below for
+ an example of this restriction. In the existing literature there is
+ no proof and also no proving method that cover this generalised
+ case.
\begin{figure}
\begin{center}
@@ -382,6 +387,18 @@
tasks involved in the inheritance process and thus minimises the number
of potentially expensive thread-switches.
+ We will also need counters for @{term P} and @{term V} events of a thread @{term th}
+ in a state @{term s}. This can be straightforwardly defined in Isabelle as
+
+ \begin{isabelle}\ \ \ \ \ %%%
+ \mbox{\begin{tabular}{@ {}l}
+ @{thm cntP_def}\\
+ @{thm cntV_def}
+ \end{tabular}}
+ \end{isabelle}
+
+ \noindent using the predefined function @{const count} for lists.
+
Next, we introduce the concept of \emph{waiting queues}. They are
lists of threads associated with every resource. The first thread in
this list (i.e.~the head, or short @{term hd}) is chosen to be the one
@@ -943,8 +960,39 @@
From these two lemmas we can see the correctness of PIP, which is
that: the blockage of th is reasonable and under control.
+ Lemmas we want to describe:
+
+ \begin{lemma}
+ @{thm eq_pv_persist}
+ \end{lemma}
+
+ \begin{lemma}
+ @{thm eq_pv_blocked}
+ \end{lemma}
+
+ \begin{lemma}
+ @{thm runing_cntP_cntV_inv}
+ \end{lemma}
+
+ \noindent
+ Remember we do not have the well-nestedness restriction in our
+ proof, which means the difference between the counters @{const cntV}
+ and @{const cntP} can be larger than @{term 1}.
+
+ \begin{lemma}
+ @{thm runing_inversion}
+ \end{lemma}
+
+
+ \begin{lemma}
+ @{thm th_blockedE}
+ \end{lemma}
+
\subsection*{END OUTLINE}
+
+
+
In what follows we will describe properties of PIP that allow us to prove
Theorem~\ref{mainthm} and, when instructive, briefly describe our argument.
It is relatively easy to see that:
@@ -957,7 +1005,7 @@
\end{isabelle}
\noindent
- The second property is by induction of @{term vt}. The next three
+ The second property is by induction on @{term vt}. The next three
properties are:
\begin{isabelle}\ \ \ \ \ %%%