regexp: comparison prio/Paper/Paper.thy

equal deleted inserted replaced

-:8524f94d251b
+:e820ee5f76f7
 (*<*)
 theory Paper
-imports CpsG ExtGG "~~/src/HOL/Library/LaTeXsugar"
+imports "../CpsG" "../ExtGG" "~~/src/HOL/Library/LaTeXsugar"
 begin
 ML {*
 open Printer;
 show_question_marks_default := false;
 *}
 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).\medskip
 \noindent
 {\bf Contributions:} There have been earlier formal investigations
-into PIP, but ...\cite{Faria08}
+into PIP \cite{conf/fase/JahierHR09,WellingsBSB07,Faria08}, but they
+are using model checking technology. As far as we are aware, this is
+the first formalised proof for the correctness of PIP. In contrast
+to model checking, our formalisation provides insight into why PIP
+is correct and allows us to prove stronger properties. For this Isar
+and Isabelle/HOL is an attractive tool for exploring definitions and
+keeping proofs consistent.
+For example, we find through formalization that the choice of next
+thread to take a lock when a resource is released is irrelevant for
+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
-distributed PIP
 Paulson's method has not been used outside security field, except
 work by Zhang et al.
-no clue about multi-processor case according to \cite{Steinberg10}
+How did Sha et al prove it....they did not use Paulson's method.
 *}
 section {* Formal Model of the Priority Inheritance Protocol *}
 text {*
 At the beginning, that is in the state where no thread is created yet,
 the waiting queue function will be the function that returns the
 empty list for every resource.
 \begin{isabelle}\ \ \ \ \ %%%
-@{abbrev all_unlocked}
+@{abbrev all_unlocked}\hfill\numbered{allunlocked}
 \end{isabelle}
 \noindent
 Using @{term "holding"} and @{term waiting}, we can introduce \emph{Resource Allocation Graphs}
 (RAG), which represent the dependencies between threads and resources.
 The first function is a waiting queue function (that is it takes a resource @{text "cs"} and returns the
 corresponding list of threads that wait for it), the second is a function that takes
 a thread and returns its current precedence (see \eqref{cpreced}). We assume the usual getter and
 setter methods for such records.
-In the initial state, the scheduler starts with all resources unlocked and the
+In the initial state, the scheduler starts with all resources unlocked (see \eqref{allunlocked}) and the
 current precedence of every thread is initialised with @{term "Prc 0 0"}; that means
 \mbox{@{abbrev initial_cprec}}. Therefore
 we have
 \begin{isabelle}\ \ \ \ \ %%%
 \end{tabular}
 \end{isabelle}
 \noindent
 The clause for event @{term "V th cs"} is similar, except that we need to update the waiting queue function
-so that the thread that possessed the lock is deleted from the corresponding thread list. For this we use
+so that the thread that possessed the lock is deleted from the corresponding thread list. For this
+list transformation, we use
 the auxiliary function @{term release}. A simple version of @{term release} would
 just delete this thread and return the rest, namely
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}lcl}
 \end{center}
 \noindent
 The first rule states that a thread can only be created, if it does not yet exists.
 Similarly, the second rule states that a thread can only be terminated if it was
-running and does not lock any resources anymore. The event @{text Set} can happen
+running and does not lock any resources anymore (to simplify ). The event @{text Set} can happen
 if the corresponding thread is running.
 \begin{center}
 @{thm[mode=Rule] thread_set[where thread=th]}
 \end{center}
 \noindent
-If a thread wants to lock a resource, then the thread needs to be running and
+If a thread wants to lock a resource, then the thread needs to be
-also we have to make sure that the resource lock doe not lead to a cycle in the
+running and also we have to make sure that the resource lock does
-RAG. Similarly, if a thread wants to release a lock on a resource, then it must
+not lead to a cycle in the RAG. In practice, ensuring the latter is
-be running and in the possession of that lock. This is formally given by the
+of course the responsibility of the programmer.  Here in our formal
-last two inference rules of @{term step}.
+model we just exclude such problematic cases in order to make
+some meaningful statements about PIP.\footnote{This situation is
+similar to the infamous occurs check in Prolog: in order to say
+anything meaningful about unification, we need to perform an occurs
+check; but in practice the occurs check is ommited and the
+responsibility to avoid problems rests with the programmer.}
+Similarly, if a thread wants to release a lock on a resource, then
+it must be running and in the possession of that lock. This is
+formally given by the last two inference rules of @{term step}.
 \begin{center}
 \begin{tabular}{c}
 @{thm[mode=Rule] thread_P[where thread=th]}\medskip\\
 @{thm[mode=Rule] thread_V[where thread=th]}\\
 properties that show our version of PIP is correct.
 *}
 section {* Correctness Proof *}
-text {* TO DO *}
+(*<*)
+context extend_highest_gen
+begin
+(*>*)
+print_locale extend_highest_gen
+thm extend_highest_gen_def
+thm extend_highest_gen_axioms_def
+thm highest_gen_def
+text {*
+Main lemma
+\begin{enumerate}
+\item @{term "s"} is a valid state (@{text "vt_s"}):
+@{thm  vt_s}.
+\item @{term "th"} is a living thread in @{term "s"} (@{text "threads_s"}):
+@{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}
+\begin{lemma}
+@{thm[mode=IfThen] moment_blocked}
+\end{lemma}
+\begin{theorem}
+@{thm[mode=IfThen] runing_inversion_2}
+\end{theorem}
+TO DO
+*}
+(*<*)
+end
+(*>*)
 section {* Properties for an Implementation *}
 text {* TO DO *}
 text {*
 The Priority Inheritance Protocol is a classic textbook algorithm
 used in real-time systems in order to avoid the problem of Priority
 Inversion.
+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.
 TO DO
+no clue about multi-processor case according to \cite{Steinberg10}
 *}
 text {*
 \bigskip

changeset 301	e820ee5f76f7
parent 300	8524f94d251b
child 304	bd05c5011c0f