regexp: comparison prio/Paper/Paper.thy

equal deleted inserted replaced

-:677364c67cc8
+:e9bafb20004d
 \it{}``Priority inheritance is neither efficient nor reliable. Implementations
 are either incomplete (and unreliable) or surprisingly complex and intrusive.''
 \end{quote}
 \noindent
-He suggests avoiding PIP altogether by not allowing critical
+He suggests avoiding PIP altogether by designing the system so that no
-sections to be preempted. Unfortunately, this solution does not
+priority inversion may happen in the first place. However, such ideal designs may
-help in real-time systems with hard deadlines for high-priority
+not always be achievable in practice.
-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
 efficient implementation of PIP in the educational PINTOS operating
 system \cite{PINTOS}.  For example, we found by ``playing'' with the
 formalisation that the choice of the next thread to take over a lock
 when a resource is released is irrelevant for PIP being correct---a
 fact that has not been mentioned in the literature and not been used
-in the reference implementation of PIP in PINTOS.  This is important
+in the reference implementation of PIP in PINTOS.  This fact, however, is important
 for an efficient implementation of PIP, because we can give the lock
 to the thread with the highest priority so that it terminates more
 quickly.
 *}
 that do not wait for any resource) and the running thread.
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm readys_def}\\
-@{thm runing_def}\\
+@{thm runing_def}
 \end{tabular}
 \end{isabelle}
 \noindent
 In the second definition @{term "DUMMY ` DUMMY"} stands for the image of a set under a function.
 @{term threads} is empty and therefore there is neither a thread ready nor 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 sets to capture both possibilities.
 We can now also conveniently define the set of resources that are locked by a thread in a
-given state
+given state and also when a thread is detached that state (meaning the thread neither
+holds nor waits for a resource):
-\begin{isabelle}\ \ \ \ \ %%%
-@{thm holdents_def}
+\begin{isabelle}\ \ \ \ \ %%%
-\end{isabelle}
+\begin{tabular}{@ {}l}
+@{thm holdents_def}\\
-\noindent
-and also when a thread is detached
-\begin{isabelle}\ \ \ \ \ %%%
 @{thm detached_def}
-\end{isabelle}
+\end{tabular}
+\end{isabelle}
-\noindent
-which means that @{text th} neither holds nor waits for a resource in @{text s}.
+\noindent
+The second definition states that @{text th}  in @{text s}.
 Finally we can define what a \emph{valid state} is in our model of PIP. For
 example we cannot expect to be able to exit a thread, if it was not
 created yet.
 These validity constraints on states are characterised by the
 {\bf Assumptions on the states {\boldmath@{text s}} and
 {\boldmath@{text "s' @ s"}:}} We need to require that @{text "s"} and
 @{text "s' @ s"} are valid states:
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{l}
-@{term "vt s"}\\
+@{term "vt s"}, @{term "vt (s' @ s)"}
-@{term "vt (s' @ s)"}
 \end{tabular}
 \end{isabelle}
 \end{quote}
 \begin{quote}
 systems.
 Of course the main work for implementing PIP involves the
 scheduler and coding how it should react to events.  Below we
 outline how our formalisation guides this implementation for each
-kind of event.\smallskip
+kind of events.\smallskip
 *}
 (*<*)
 context step_create_cps
 begin
 \noindent
 That means we have to add a waiting edge to the @{text RAG}. Furthermore
 the current precedence for all threads that are not dependants of @{text th}
 are unchanged. For the others we need to follow the edges
-in the @{text RAG} and recompute the @{term "cp"}. However, like in the
+in the @{text RAG} and recompute the @{term "cp"}. To do this we can start from @{term "th"}
-case of @{text Set}, this operation can stop often earlier, namely when intermediate
+and follow the @{term "depend"}-edges to recompute  using Lemma~\ref{childrenlem}
-values do not change.
+the @{term "cp"} of every
+thread encountered on the way. Since the @{term "depend"}
+is loop free, this procedure will always stop. The following lemma shows, however,
+that this procedure can actually stop often earlier without having to consider all
+dependants.
+\begin{isabelle}\ \ \ \ \ %%%
+\begin{tabular}{@ {}l}
+%%@ {t hm[mode=IfThen] eq_up_self}\\
+@{text "If"} @{thm (prem 1) eq_up}, @{thm (prem 2) eq_up} and @{thm (prem 3) eq_up}\\
+@{text "then"} @{thm (concl) eq_up}.
+\end{tabular}
+\end{isabelle}
+\noindent
+This lemma 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.
 *}
 (*<*)
 end
 (*>*)
 text {*
 PVS of the Priority Ceiling Protocol done by Dutertre
 \cite{dutertre99b}---another solution to the Priority Inversion
 problem, which however needs static analysis of programs in order to
 avoid it. There have been earlier formal investigations
 into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model
-checking techniques. In this way they are limited to validating
+checking techniques. The results obtained by them apply,
-one particular implementation. In contrast, our paper is a good
+however, only to systems with a fixed size, such as a fixed number of
+events and threads. In contrast, our result applies to systems of arbitrary
+size. Moreover, our result is a good
 witness for one of the major reasons to be interested in machine checked
 reasoning: gaining deeper understanding of the subject matter.
 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 span over 770 lines of code. The properties relevant
-for an implementation require 2000 lines. The code of our formalisation
+for an implementation require 2000 lines.
-can be downloaded from
+%The code of our formalisation
-\url{http://www.inf.kcl.ac.uk/staff/urbanc/pip.html}.\medskip
+%can be downloaded from
+%\url{http://www.inf.kcl.ac.uk/staff/urbanc/pip.html}.\medskip
 \noindent
 {\bf Acknowledgements:}
 We are grateful for the comments we received from anonymous
 referees.

changeset 355	e9bafb20004d
parent 354	677364c67cc8
child 358	b10f8db1e907