regexp: comparison prio/Paper/Paper.thy

equal deleted inserted replaced

-:d9b0a2fd0db7
+:bd05c5011c0f
 \end{quote}
 \noindent
 He suggests to avoid PIP altogether by not allowing critical
 sections to be preempted. Unfortunately, this solution does not
-help in real-time systems with low latency \emph{requirements}.
+help in real-time systems with hard deadlines for high-priority
+threads.
 In our opinion, there is clearly a need for investigating correct
 algorithms for PIP. A few specifications for PIP exist (in English)
 and also a few high-level descriptions of implementations (e.g.~in
 the textbook \cite[Section 5.6.5]{Vahalia96}), but they help little
 informal reasoning (since we have to analyse all possible behaviours
 of threads, i.e.~\emph{traces}, that could possibly happen).\medskip
 \noindent
 {\bf Contributions:} There have been earlier formal investigations
-into PIP \cite{conf/fase/JahierHR09,WellingsBSB07,Faria08}, but they
+into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model
-are using model checking technology. As far as we are aware, this is
+checking techniques. This paper presents a formalised and
-the first formalised proof for the correctness of PIP. In contrast
+mechanically checked proof for the correctness of PIP (to our
-to model checking, our formalisation provides insight into why PIP
+knowledge the first one; an earlier informal proof by Sha et
-is correct and allows us to prove stronger properties. For this Isar
+al.~\cite{Sha90} is flawed).  In contrast to model checking, our
-and Isabelle/HOL is an attractive tool for exploring definitions and
+formalisation provides insight into why PIP is correct and allows us
-keeping proofs consistent.
+to prove stronger properties that, as we will show, inform an
+implementation.  For example, we found by ``playing'' with the formalisation
-For example, we find through formalization that the choice of next
+that the choice of the next thread to take over a lock when a
-thread to take a lock when a resource is released is irrelevant for
+resource is released is irrelevant for PIP being correct.
-the very basic property of PIP to hold.
-Despite the wide use of Priority Inheritance Protocol in real time
-operating system, it’s correctness has never been formally proved
-and mechanically checked. All existing verification are based on
-model checking technology. Full automatic verification gives little
-help to understand why the protocol is correct. And results such
-obtained only apply to models of limited size. This paper presents a
-formal verification based on theorem proving. Machine checked formal
-proof does help to get deeper understanding. We found the fact which
-is not mentioned in the literature, that the choice of next thread
-to take over when an critical resource is release does not affect
-the correctness of the protocol. The paper also shows how formal
-proof can help to construct correct and efficient implementation.
-vt (valid trace) was introduced earlier, cite
-Paulson's method has not been used outside security field, except
-work by Zhang et al.
-How did Sha et al prove it....they did not use Paulson's method.
 *}
 section {* Formal Model of the Priority Inheritance Protocol *}
 text {*
 function @{text f}.
 Note that in the initial case, that is where the list of events is empty, the set
 @{term threads} is empty and therefore there is no thread ready nor a running.
 If there is one or more threads ready, then there can only be \emph{one} thread
 running, namely the one whose current precedence is equal to the maximum of all ready
-threads. We use the set-comprehension to capture both possibilites.
+threads. We use the set-comprehension to capture both possibilities.
 We can now also define the set of resources that are locked by a thread in any
 given state.
 \begin{isabelle}\ \ \ \ \ %%%
 @{thm holdents_def}
 \end{isabelle}
 \noindent
 These resources are given by the holding edges in the RAG.
-Finally we can define what a \emph{valid state} is in our PIP. For example we cannot exptect to
+Finally we can define what a \emph{valid state} is in our PIP. For
-be able to exit a thread, if it was not created yet. These validity constraints
+example we cannot expect to be able to exit a thread, if it was not
-are characterised by the inductive predicate @{term "step"}. We give five
+created yet. These validity constraints are characterised by the
-inference rules relating a state and an event that can happen next.
+inductive predicate @{term "step"}. We give five inference rules
+relating a state and an event that can happen next.
 \begin{center}
 \begin{tabular}{c}
 @{thm[mode=Rule] thread_create[where thread=th]}\hspace{1cm}
 @{thm[mode=Rule] thread_exit[where thread=th]}
 @{thm threads_s}.
 \item @{term "th"} has the highest precedence in @{term "s"} (@{text "highest"}):
 @{thm highest}.
 \item The precedence of @{term "th"} is @{term "Prc prio tm"} (@{text "preced_th"}):
 @{thm preced_th}.
-\end{enumerate}
+\item @{term "t"} is a valid extension of @{term "s"} (@{text "vt_t"}): @{thm vt_t}.
+\item Any thread created in @{term "t"} has priority no higher than @{term "prio"}, therefore
+its precedence can not be higher than @{term "th"},  therefore
+@{term "th"} remain to be the one with the highest precedence
+(@{text "create_low"}):
+@{thm [display] create_low}
+\item Any adjustment of priority in
+@{term "t"} does not happen to @{term "th"} and
+the priority set is no higher than @{term "prio"}, therefore
+@{term "th"} remain to be the one with the highest precedence (@{text "set_diff_low"}):
+@{thm [display] set_diff_low}
+\item Since we are investigating what happens to @{term "th"}, it is assumed
+@{term "th"} does not exit during @{term "t"} (@{text "exit_diff"}):
+@{thm [display] exit_diff}
+\end{enumerate}
 \begin{lemma}
 @{thm[mode=IfThen] moment_blocked}
 \end{lemma}
 \begin{theorem}
 @{thm[mode=IfThen] runing_inversion_2}
 \end{theorem}
+\begin{theorem}
+@{thm[mode=IfThen] runing_inversion_3}
+\end{theorem}
 TO DO
 A clear and simple understanding of the problem at hand is both a
 prerequisite and a byproduct of such an effort, because everything
 has finally be reduced to the very first principle to be checked
 mechanically.
+Our formalisation and the one presented
+in \cite{Wang09} are the only ones that employ Paulson's method for
+verifying protocols which are \emph{not} security related.
 TO DO
 no clue about multi-processor case according to \cite{Steinberg10}
 practice\cite{locke-july02}. However, as pointed out in the
 literature, the analysis of priority inheritance protocol is quite
 subtle\cite{yodaiken-july02}.  A formal analysis will certainly be
 helpful for us to understand and correctly implement PI. All
 existing formal analysis of PI
-\cite{conf/fase/JahierHR09,WellingsBSB07,Faria08} are based on the
+\cite{Jahier09,Wellings07,Faria08} are based on the
 model checking technology. Because of the state explosion problem,
 model check is much like an exhaustive testing of finite models with
 limited size.  The results obtained can not be safely generalized to
 models with arbitrarily large size. Worse still, since model
 checking is fully automatic, it give little insight on why the
 the fundamental requirement of Priority Inheritance protocol. Another purpose of this paper
 is to show how this model can be used to guide a concrete implementation. As discussed in
 Section 5.6.5 of \cite{Vahalia96}, the implementation of Priority Inheritance in Solaris
 uses sophisticated linking data structure. Except discussing two scenarios to show how
 the data structure should be manipulated, a lot of details of the implementation are missing.
-In \cite{Faria08,conf/fase/JahierHR09,WellingsBSB07} the protocol is described formally
+In \cite{Faria08,Jahier09,Wellings07} the protocol is described formally
 using different notations, but little information is given on how this protocol can be
 implemented efficiently, especially there is no information on how these data structure
 should be manipulated.
 Because the scheduling of threads is based on current precedence,
 section {* Related works \label{related} *}
 text {*
 \begin{enumerate}
 \item {\em Integrating Priority Inheritance Algorithms in the Real-Time Specification for Java}
-\cite{WellingsBSB07} models and verifies the combination of Priority Inheritance (PI) and
+\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
 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{conf/fase/JahierHR09}. Gives a formal model
+\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

changeset 304	bd05c5011c0f
parent 301	e820ee5f76f7
child 305	463bed130705