# HG changeset patch # User Christian Urban # Date 1393948176 0 # Node ID 6b1141c5e24c6df4c6fbeb31b57cf1a97606a54c # Parent da7a6ccfa7a9a701c0ddc25ae63e1f5d68b45fa4 cleaned up diff -r da7a6ccfa7a9 -r 6b1141c5e24c Journal/Paper.thy --- a/Journal/Paper.thy Tue Mar 04 15:30:24 2014 +0000 +++ b/Journal/Paper.thy Tue Mar 04 15:49:36 2014 +0000 @@ -155,7 +155,7 @@ \cite[Section 2.3.1]{book} which specifies for a process that inherited a higher priority and exits a critical section ``it resumes the priority it had at the point of entry into the critical section''. - + While \cite{book} and \cite{Sha90} are the only formal publications we have found that describe the incorrect behaviour, not all, but many @@ -1467,9 +1467,9 @@ for future work. To us, it seems sound reasoning about scheduling algorithms is fiendishly difficult - if done informally by ``pencil-and-paper''. This is proved by the flawed proof - in the paper by Sha et al.~\cite{Sha90} and also by Regehr \cite{Regehr} who - pointed out an error in a paper about Preemption + if done informally by ``pencil-and-paper''. We infer this from the flawed proof + in the paper by Sha et al.~\cite{Sha90} and also from \cite{Regehr} where Regehr + points out an error in a paper about Preemption Threshold Scheduling \cite{ThreadX}. The use of a theorem prover was invaluable to us in order to be confident about the correctness of our reasoning (no case can be overlooked). @@ -1494,7 +1494,7 @@ for an implementation require 2000 lines. The code of our formalisation can be downloaded from the Mercurial repository at - \url{http://www.inf.kcl.ac.uk/staff/urbanc/pip.html}. + \url{http://www.dcs.kcl.ac.uk/staff/urbanc/cgi-bin/repos.cgi/pip}. %\medskip diff -r da7a6ccfa7a9 -r 6b1141c5e24c Journal/document/root.tex --- a/Journal/document/root.tex Tue Mar 04 15:30:24 2014 +0000 +++ b/Journal/document/root.tex Tue Mar 04 15:49:36 2014 +0000 @@ -3,6 +3,7 @@ %\textwidth 130mm %\textheight 200mm %\renewenvironment{abstract}{\section*{Abstract}\small}{} +\pagestyle{headings} \usepackage{isabelle} \usepackage{isabellesym} \usepackage{amsmath} diff -r da7a6ccfa7a9 -r 6b1141c5e24c Paper/tt.thy --- a/Paper/tt.thy Tue Mar 04 15:30:24 2014 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,94 +0,0 @@ - -There are several works on inversion avoidance: -\begin{enumerate} -\item {\em Solving the group priority inversion problem in a timed asynchronous system}. -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 Examples of inaccurate specification of the protocol}. -\end{enumerate} - - - - - - -section{* Related works *} - -text {* -1. <> 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. -2. << Formal Development of Solutions for Real-Time Operating Systems with TLA+/TLC>>. 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. -3. <>. 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. - - -There are several works on inversion avoidance: -1. <>. -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. - - -<>. - -*} - -text {* - -\section{An overview of priority inversion and priority inheritance} - -Priority inversion refers to the phenomenon when a thread with high priority is blocked -by a thread with low priority. Priority happens when the high priority thread requests -for some critical resource already taken by the low priority thread. Since the high -priority thread has to wait for the low priority thread to complete, it is said to be -blocked by the low priority thread. Priority inversion might prevent high priority -thread from fulfill its task in time if the duration of priority inversion is indefinite -and unpredictable. Indefinite priority inversion happens when indefinite number -of threads with medium priorities is activated during the period when the high -priority thread is blocked by the low priority thread. Although these medium -priority threads can not preempt the high priority thread directly, they are able -to preempt the low priority threads and cause it to stay in critical section for -an indefinite long duration. In this way, the high priority thread may be blocked indefinitely. - -Priority inheritance is one protocol proposed to avoid indefinite priority inversion. -The basic idea is to let the high priority thread donate its priority to the low priority -thread holding the critical resource, so that it will not be preempted by medium priority -threads. The thread with highest priority will not be blocked unless it is requesting -some critical resource already taken by other threads. Viewed from a different angle, -any thread which is able to block the highest priority threads must already hold some -critical resource. Further more, it must have hold some critical resource at the -moment the highest priority is created, otherwise, it may never get change to run and -get hold. Since the number of such resource holding lower priority threads is finite, -if every one of them finishes with its own critical section in a definite duration, -the duration the highest priority thread is blocked is definite as well. The key to -guarantee lower priority threads to finish in definite is to donate them the highest -priority. In such cases, the lower priority threads is said to have inherited the -highest priority. And this explains the name of the protocol: -{\em Priority Inheritance} and how Priority Inheritance prevents indefinite delay. - -The objectives of this paper are: -\begin{enumerate} -\item Build the above mentioned idea into formal model and prove a series of properties -until we are convinced that the formal model does fulfill the original idea. -\item Show how formally derived properties can be used as guidelines for correct -and efficient implementation. -\end{enumerate}. -The proof is totally formal in the sense that every detail is reduced to the -very first principles of Higher Order Logic. The nature of interactive theorem -proving is for the human user to persuade computer program to accept its arguments. -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. The former intuitive explanation of -Priority Inheritance is just such a byproduct. -*} - -*) diff -r da7a6ccfa7a9 -r 6b1141c5e24c journal.pdf Binary file journal.pdf has changed