pip: comparison Journal/Paper.thy

equal deleted inserted replaced

-:2aa37de77f31
+:b6ea51cd2e88
 preced ("prec") and
 (*  preceds ("precs") and*)
 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>")
 (*>*)
 section {* Introduction *}
 example on Page 254 the authors write: ``{\it Upon releasing the
 lock, the [low-priority] thread will revert to its original
 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
+While \cite{Laplante11,Liu00,book,Sha90,Silberschatz13} are the only
-found that specify the incorrect behaviour, it seems also many
+formal publications we have found that specify the incorrect
-informal descriptions of PIP overlook the possibility that another
+behaviour, it seems also many informal descriptions of PIP overlook
-high-priority might wait for a low-priority process to finish.
+the possibility that another high-priority might wait for a
-A notable exception is the texbook \cite{buttazzo}, which gives the correct
+low-priority process to finish.  A notable exception is the texbook
-behaviour of resetting the priority of a thread to the highest remaining priority of the
+\cite{buttazzo}, which gives the correct behaviour of resetting the
-threads it blocks. This textbook also gives an informal proof for
+priority of a thread to the highest remaining priority of the
-the correctness of PIP in the style of Sha et al. Unfortunately, this informal
+threads it blocks. This textbook also gives an informal proof for
-proof is too vague to be useful for formalising the correctness of PIP
+the correctness of PIP in the style of Sha et al. Unfortunately,
-and the specification leaves out nearly all details in order
+this informal proof is too vague to be useful for formalising the
-to implement PIP efficiently.\medskip\smallskip
+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
 %is that such issues clearly show up and cannot be overlooked as in
 %informal reasoning (since we have to analyse all possible behaviours
 %of threads, i.e.~\emph{traces}, that could possibly happen).
-\noindent
+\noindent {\bf Contributions:} There have been earlier formal
-{\bf Contributions:} There have been earlier formal investigations
+investigations into PIP \cite{Faria08,Jahier09,Wellings07}, but they
-into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model
+employ model checking techniques. This paper presents a formalised
-checking techniques. This paper presents a formalised and
+and mechanically checked proof for the correctness of PIP. For this
-mechanically checked proof for the correctness of PIP. For this we
+we needed to design a new correctness criterion for PIP. In contrast
-needed to design a new correctness criterion for PIP. In contrast to model checking, our
+to model checking, our formalisation provides insight into why PIP
-formalisation provides insight into why PIP is correct and allows us
+is correct and allows us to prove stronger properties that, as we
-to prove stronger properties that, as we will show, can help with an
+will show, can help with an efficient implementation of PIP. We
-efficient implementation of PIP in the educational PINTOS operating
+illustrate this with an implementation of PIP in the educational
-system \cite{PINTOS}.  For example, we found by ``playing'' with the
+PINTOS operating system \cite{PINTOS}.  For example, we found by
-formalisation that the choice of the next thread to take over a lock
+``playing'' with the formalisation that the choice of the next
-when a resource is released is irrelevant for PIP being correct---a
+thread to take over a lock when a resource is released is irrelevant
-fact that has not been mentioned in the literature and not been used
+for PIP being correct---a fact that has not been mentioned in the
-in the reference implementation of PIP in PINTOS.  This fact, however, is important
+literature and not been used in the reference implementation of PIP
-for an efficient implementation of PIP, because we can give the lock
+in PINTOS.  This fact, however, is important for an efficient
-to the thread with the highest priority so that it terminates more
+implementation of PIP, because we can give the lock to the thread
-quickly.  We were also being able to generalise the scheduler of Sha
+with the highest priority so that it terminates more quickly.  We
-et al.~\cite{Sha90} to the practically relevant case where critical
+were also being able to generalise the scheduler of Sha et
-sections can overlap; see Figure~\ref{overlap} \emph{a)} below for an example of
+al.~\cite{Sha90} to the practically relevant case where critical
-this restriction. %In the existing literature there is no
+sections can overlap; see Figure~\ref{overlap} \emph{a)} below for
-%proof and also no proving method that cover this generalised case.
+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}
 \begin{tikzpicture}[scale=1]
 %%\draw[step=2mm] (0,0) grid (10,2);
 ``time-slicing'' threads with equal priority, but found that it does not lead to
 advantages in practice. On the contrary, according to their work having a policy
 like our FIFO-scheduling of threads with equal priority reduces the number of
 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
 that is in possession of the
 To see what kind of thread can block @{term th}.
 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:
 @{thm[mode=IfThen]  finite_threads}
 \end{tabular}
 \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}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 HERE??

changeset 76	b6ea51cd2e88
parent 75	2aa37de77f31
child 82	c0a4e840aefe