diff -r 8524f94d251b -r e820ee5f76f7 prio/Paper/Paper.thy --- a/prio/Paper/Paper.thy Sun Feb 12 11:30:17 2012 +0000 +++ b/prio/Paper/Paper.thy Sun Feb 12 14:58:47 2012 +0000 @@ -1,6 +1,6 @@ (*<*) theory Paper -imports CpsG ExtGG "~~/src/HOL/Library/LaTeXsugar" +imports "../CpsG" "../ExtGG" "~~/src/HOL/Library/LaTeXsugar" begin ML {* open Printer; @@ -149,17 +149,39 @@ 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} + {\bf Contributions:} There have been earlier formal investigations + 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 *} @@ -284,7 +306,7 @@ empty list for every resource. \begin{isabelle}\ \ \ \ \ %%% - @{abbrev all_unlocked} + @{abbrev all_unlocked}\hfill\numbered{allunlocked} \end{isabelle} \noindent @@ -383,7 +405,7 @@ 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 @@ -435,7 +457,8 @@ \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 @@ -531,7 +554,7 @@ \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} @@ -539,11 +562,19 @@ \end{center} \noindent - If a thread wants to lock a resource, then the thread needs to be running and - also we have to make sure that the resource lock doe not lead to a cycle in the - RAG. 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}. + If a thread wants to lock a resource, then the thread needs to be + running and also we have to make sure that the resource lock does + not lead to a cycle in the RAG. In practice, ensuring the latter is + of course the responsibility of the programmer. Here in our formal + 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} @@ -569,7 +600,49 @@ 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 *} @@ -582,8 +655,15 @@ 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 {*