--- 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
 

--- 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}

--- 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 \<exclamdown>\<degree>Group Priority Inversion\<exclamdown>\<plusminus> 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.	<<Integrating Priority Inheritance Algorithms in the Real-Time Specification for Java>> 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.	<<Synchronous modeling and validation of priority inheritance schedulers>>. 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.	<<Solving the group priority inversion problem in a timed asynchronous system>>. 
-The notion of \<exclamdown>\<degree>Group Priority Inversion\<exclamdown>\<plusminus> is introduced. The main strategy is still inversion avoidance. 
-The method is by reordering requests in the setting of Client-Server.
-
-
-<<Examples of inaccurate specification of the protocol>>.
-
-*}
-
-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. 
-*}
-
-*)

Binary file journal.pdf has changed