regexp: comparison prio/Paper/Paper.thy

equal deleted inserted replaced

-:630754a81bdb
+:6a4249608ad0
 attractive (especially in light of the flawed proof by Sha et
 al.~\cite{Sha90}), we found that the formalisation can even help us
 with efficiently implementing PIP.
 For example Baker complained that calculating the current precedence
-in PIP is quite ``heavy weight'' in Linux (see our Introduction).
+in PIP is quite ``heavy weight'' in Linux (see the Introduction).
 In our model of PIP the current precedence of a thread in a state s
 depends on all its dependants---a ``global'' transitive notion,
 which is indeed heavy weight (see Def.~shown in \eqref{cpreced}).
-We can however prove how to improve upon this. For this let us
+We can however improve upon this. For this let us define the notion
-define the notion of @{term children} of a thread as
+of @{term children} of a thread @{text th} in a state @{text s} as
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm children_def2}
 \end{tabular}
 \end{isabelle}
 \noindent
-where a child is a thread that is one ``hop'' away in the @{term RAG} from the
+where a child is a thread that is one ``hop'' away from the tread
-tread @{text th} (and waiting for @{text th} to release a resource). We can prove that
+@{text th} in the @{term RAG} (and waiting for @{text th} to release
+a resource). We can prove that
 \begin{lemma}\label{childrenlem}
 @{text "If"} @{thm (prem 1) cp_rec} @{text "then"}
 \begin{center}
 @{thm (concl) cp_rec}.
 \noindent
 That means the current precedence of a thread @{text th} can be
 computed locally by considering only the children of @{text th}. In
 effect, it only needs to be recomputed for @{text th} when one of
-its children change their current precedence.  Once the current
+its children changes its current precedence.  Once the current
 precedence is computed in this more efficient manner, the selection
 of the thread with highest precedence from a set of ready threads is
 a standard scheduling operation implemented in most operating
 systems.
-Of course the main implementation work for PIP involves the scheduler
+Of course the main implementation work for PIP involves the
-and coding how it should react to the events, for example which
+scheduler and coding how it should react to events.  Below we
-datastructures need to be modified (mainly @{text RAG} and @{text cprec}).
+outline how our formalisation guides this implementation for each
-Below we outline how our formalisation guides this implementation for each
+kind of event.\smallskip
-event.\smallskip
 *}
 (*<*)
 context step_create_cps
 begin
 (*>*)
 text {*
 \noindent
-@{term "Create th prio"}: We assume that the current state @{text s'} and
+\colorbox{mygrey}{@{term "Create th prio"}:} We assume that the current state @{text s'} and
 the next state @{term "s \<equiv> Create th prio#s'"} are both valid (meaning the event
 is allowed to occur). In this situation we can show that
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
-@{thm eq_dep}\\
+@{thm eq_dep},\\
-@{thm eq_cp_th}\\
+@{thm eq_cp_th}, and\\
 @{thm[mode=IfThen] eq_cp}
 \end{tabular}
 \end{isabelle}
 \noindent
 This means we do not have recalculate the @{text RAG} and also none of the
 current precedences of the other threads. The current precedence of the created
-thread is just its precedence, that is the pair @{term "(prio, length (s::event list))"}.
+thread @{text th} is just its precedence, namely the pair @{term "(prio, length (s::event list))"}.
 \smallskip
 *}
 (*<*)
 end
 context step_exit_cps
 begin
 (*>*)
 text {*
 \noindent
-@{term "Exit th"}: We again assume that the current state @{text s'} and
+\colorbox{mygrey}{@{term "Exit th"}:} We again assume that the current state @{text s'} and
 the next state @{term "s \<equiv> Exit th#s'"} are both valid. We can show that
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
-@{thm eq_dep}\\
+@{thm eq_dep}, and\\
 @{thm[mode=IfThen] eq_cp}
 \end{tabular}
 \end{isabelle}
 \noindent
-This means also we do not have to recalculate the @{text RAG} and
+This means again we do not have to recalculate the @{text RAG} and
-not the current precedences for the other threads. Since @{term th} is not
+also not the current precedences for the other threads. Since @{term th} is not
 alive anymore in state @{term "s"}, there is no need to calculate its
 current precedence.
 \smallskip
 *}
 (*<*)
 context step_set_cps
 begin
 (*>*)
 text {*
 \noindent
-@{term "Set th prio"}: We assume that @{text s'} and
+\colorbox{mygrey}{@{term "Set th prio"}:} We assume that @{text s'} and
 @{term "s \<equiv> Set th prio#s'"} are both valid. We can show that
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
-@{thm[mode=IfThen] eq_dep}\\
+@{thm[mode=IfThen] eq_dep}, and\\
 @{thm[mode=IfThen] eq_cp}
 \end{tabular}
 \end{isabelle}
 \noindent
-The first is again telling us we do not need to change the @{text RAG}. The second
+The first property is again telling us we do not need to change the @{text RAG}. The second
-however states that only threads that are \emph{not} dependent on @{text th} have their
+however states that only threads that are \emph{not} dependants of @{text th} have their
 current precedence unchanged. For the others we have to recalculate the current
 precedence. To do this we can start from @{term "th"}
 and follow the @{term "depend"}-chains to recompute the @{term "cp"} of every
 thread encountered on the way using Lemma~\ref{childrenlem}. Since the @{term "depend"}
-is loop free, this procedure always stop. The the following two lemmas show this
+is loop free, this procedure will always stop. The following two lemmas show, however,
-procedure can actually stop often earlier.
+that this procedure can actually stop often earlier without having to consider all
+dependants.
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm[mode=IfThen] eq_up_self}\\
 @{text "If"} @{thm (prem 1) eq_up}, @{thm (prem 2) eq_up} and @{thm (prem 3) eq_up}\\
 The second states that if an intermediate @{term cp}-value does not change, then
 the procedure can also stop, because none of its dependent threads will
 have their current precedence changed.
 \smallskip
 *}
 (*<*)
 end
 context step_v_cps_nt
 begin
 (*>*)
 text {*
 \noindent
-@{term "V th cs"}: We assume that @{text s'} and
+\colorbox{mygrey}{@{term "V th cs"}:} We assume that @{text s'} and
 @{term "s \<equiv> V th cs#s'"} are both valid. We have to consider two
 subcases: one where there is a thread to ``take over'' the released
-resource @{text cs}, and where there is not. Let us consider them
+resource @{text cs}, and one where there is not. Let us consider them
 in turn. Suppose in state @{text s}, the thread @{text th'} takes over
 resource @{text cs} from thread @{text th}. We can show
 \begin{isabelle}\ \ \ \ \ %%%
 For @{text th} and @{text th'} we need to use Lemma~\ref{childrenlem} to
 recalculate their current prcedence since their children have changed. *}(*<*)end context step_v_cps_nnt begin (*>*)text {*
 \noindent
 In the other case where there is no thread that takes over @{text cs}, we can show how
 to recalculate the @{text RAG} and also show that no current precedence needs
-to be recalculated, except for @{text th} (like in the case above).
+to be recalculated.
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm depend_s}\\
 @{thm eq_cp}
 begin
 (*>*)
 text {*
 \noindent
-@{term "P th cs"}: We assume that @{text s'} and
+\colorbox{mygrey}{@{term "P th cs"}:} We assume that @{text s'} and
 @{term "s \<equiv> P th cs#s'"} are both valid. We again have to analyse two subcases, namely
 the one where @{text cs} is locked, and where it is not. We treat the second case
 first by showing that
 \begin{isabelle}\ \ \ \ \ %%%
 \end{tabular}
 \end{isabelle}
 \noindent
 This means we do not need to add a holding edge to the @{text RAG} and no
-current precedence must be recalculated (including that for @{text th}).*}(*<*)end context step_P_cps_ne begin(*>*) text {*
+current precedence needs to be recalculated.*}(*<*)end context step_P_cps_ne begin(*>*) text {*
 \noindent
 In the second case we know that resouce @{text cs} is locked. We can show that
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 \end{tabular}
 \end{isabelle}
 \noindent
 That means we have to add a waiting edge to the @{text RAG}. Furthermore
-the current precedence for all threads that are not dependent on @{text th}
+the current precedence for all threads that are not dependants of @{text th}
-are unchanged. For the others we need to follow the @{term "depend"}-chains
+are unchanged. For the others we need to follow the edges
 in the @{text RAG} and recompute the @{term "cp"}. However, like in the
-@{text Set}-event, this operation can stop often earlier, namely when intermediate
+@case of {text Set}, this operation can stop often earlier, namely when intermediate
 values do not change.
 *}
 (*<*)
 end
 (*>*)
 text {*
 \noindent
-TO DO a few sentences summarising what has been achieved.
+A pleasing result of our formalisation is that the properties in
+this section closely inform an implementation of PIP:  Whether the
+@{text RAG} needs to be reconfigured or current precedences need to
+recalculated for an event is given by a lemma we proved.
 *}
 section {* Conclusion *}
 text {*
 that a mechanically checked proof avoids the flaws that crept into their
 informal reasoning. We achieved this goal: The correctness of PIP now
 only hinges on the assumptions behind our formal model. The reasoning, which is
 sometimes quite intricate and tedious, has been checked beyond any
 reasonable doubt by Isabelle/HOL. We can also confirm that Paulson's
-inductive method to protocol verification~\cite{Paulson98} is quite
+inductive method for protocol verification~\cite{Paulson98} is quite
 suitable for our formal model and proof. The traditional application
 area of this method is security protocols.  The only other
 application of Paulson's method we know of outside this area is
 \cite{Wang09}.
 PIP is a scheduling algorithm for single-processor systems. We are
 now living in a multi-processor world. So the question naturally
 arises whether PIP has any relevance in such a world beyond
 teaching. Priority Inversion certainly occurs also in
-multi-processor systems.  However, the surprising answer, according to
+multi-processor systems.  However, the surprising answer, according
-\cite{Steinberg10}, is that except for one unsatisfactory proposal
+to \cite{Steinberg10}, is that except for one unsatisfactory
-nobody has a good idea for how PIP should be modified to work
+proposal nobody has a good idea for how PIP should be modified to
-correctly on multi-processor systems. The difficulties become clear
+work correctly on multi-processor systems. The difficulties become
-when considering that locking and releasing a resource always
+clear when considering that locking and releasing a resource always
-requires a some small amount of time. If processes work independently, then a
+requires a small amount of time. If processes work independently,
-low priority process can ``steal'' in this unguarded moment a lock for a
+then a low priority process can ``steal'' in such an unguarded
-resource that was supposed allow a high-priority process to run next. Thus
+moment a lock for a resource that was supposed allow a high-priority
-the problem of Priority Inversion is not really prevented. It seems
+process to run next. Thus the problem of Priority Inversion is not
-difficult to design a PIP-algorithm with a meaningful correctness
+really prevented. It seems difficult to design a PIP-algorithm with
-property on independent multi-processor systems.  We can imagine PIP
+a meaningful correctness property on a multi-processor systems where
-to be of use in a situation where
+processes work independently.  We can imagine PIP to be of use in
-processes are not independent, but coordinated via a master
+situations where processes are \emph{not} independent, but
-process that distributes work over some slave processes. However a
+coordinated via a master process that distributes work over some
-formal investigation of this is beyond the scope of this paper.
+slave processes. However, a formal investigation of this is beyond
-We are not aware of any proofs in this area, not even informal ones.
+the scope of this paper.  We are not aware of any proofs in this
+area, not even informal ones.
-Our formalisation consists of 6894 of readable Isabelle/Isar code, with some
-apply-scripts interspersed. The formal model is 385 lines long; the
+The most closely related work to ours is the formal verification in
-formal correctness proof 3777 lines. The properties relevant for an
+PVS for Priority Ceiling done by Dutertre \cite{dutertre99b}. His formalisation
-implementation are 1964 lines long; Auxlliary definitions and notions are
+consists of 407 lemmas and 2500 lines of ``specification'' (we do not
-768 lines.
+know whether this includes also code for proofs).  Our formalisation
+consists of around 210 lemmas and overall 6950 lines of readable Isabelle/Isar
+code with a few apply-scripts interspersed. The formal model of PIP
+is 385 lines long; the formal correctness proof 3800 lines. Some auxiliary
+definitions and proofs took 770 lines of code. The properties relevant
+for an implementation took 2000 lines.  Our code can be downloaded from
+...
+\bibliographystyle{plain}
+\bibliography{root}
 *}
 section {* Key properties \label{extension} *}
 (*<*)
 then.
 *}
 (*<*)
 end
-(*>*)
-section {* Related works \label{related} *}
-text {*
-\begin{enumerate}
-\item {\em Integrating Priority Inheritance Algorithms in the Real-Time Specification for Java}
-\cite{Wellings07} models and verifies the combination of Priority Inheritance (PI) and
-Priority Ceiling Emulation (PCE) protocols in the setting of Java virtual machine
-using extended Timed Automata(TA) formalism of the UPPAAL tool. Although a detailed
-formal model of combined PI and PCE is given, the number of properties is quite
-small and the focus is put on the harmonious working of PI and PCE. Most key features of PI
-(as well as PCE) are not shown. Because of the limitation of the model checking technique
-used there, properties are shown only for a small number of scenarios. Therefore,
-the verification does not show the correctness of the formal model itself in a
-convincing way.
-\item {\em Formal Development of Solutions for Real-Time Operating Systems with TLA+/TLC}
-\cite{Faria08}. A formal model of PI is given in TLA+. Only 3 properties are shown
-for PI using model checking. The limitation of model checking is intrinsic to the work.
-\item {\em Synchronous modeling and validation of priority inheritance schedulers}
-\cite{Jahier09}. Gives a formal model
-of PI and PCE in AADL (Architecture Analysis \& Design Language) and checked
-several properties using model checking. The number of properties shown there is
-less than here and the scale is also limited by the model checking technique.
-\item {\em The Priority Ceiling Protocol: Formalization and Analysis Using PVS}
-\cite{dutertre99b}. Formalized another protocol for Priority Inversion in the
-interactive theorem proving system PVS.
-\end{enumerate}
-There are several works on inversion avoidance:
-\begin{enumerate}
-\item {\em Solving the group priority inversion problem in a timed asynchronous system}
-\cite{Wang:2002:SGP}. The notion of Group Priority Inversion is introduced. The main
-strategy is still inversion avoidance. The method is by reordering requests
-in the setting of Client-Server.
-\item {\em A Formalization of Priority Inversion} \cite{journals/rts/BabaogluMS93}.
-Formalized the notion of Priority
-Inversion and proposes methods to avoid it.
-\end{enumerate}
-{\em Examples of inaccurate specification of the protocol ???}.
-*}
-(*<*)
 end
 (*>*)

changeset 321	6a4249608ad0
parent 320	630754a81bdb
child 322	c37b387110d0