correct RAG
authorurbanc
Sun, 12 Feb 2012 11:30:17 +0000
changeset 300 8524f94d251b
parent 299 4fcd802eba59
child 301 e820ee5f76f7
correct RAG
prio/Paper/Paper.thy
prio/paper.pdf
--- a/prio/Paper/Paper.thy	Sun Feb 12 05:06:59 2012 +0000
+++ b/prio/Paper/Paper.thy	Sun Feb 12 11:30:17 2012 +0000
@@ -138,7 +138,7 @@
   Unfortunately, as Yodaiken points out, this behaviour is too
   simplistic.  Consider the case where the low priority thread $L$
   locks \emph{two} resources, and two high-priority threads $H$ and
-  $H'$ each wait for one of them.  If $L$ then releases one resource
+  $H'$ each wait for one of them.  If $L$ releases one resource
   so that $H$, say, can proceed, then we still have Priority Inversion
   with $H'$ (which waits for the other resource). The correct
   behaviour for $L$ is to revert to the highest remaining priority of
@@ -146,9 +146,11 @@
   correctness of a high-level specification of PIP in a theorem prover
   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).
+  of threads, i.e.~\emph{traces}, that could possibly happen).\medskip
 
-  There have been earlier formal investigations into PIP, but ...\cite{Faria08}
+  \noindent
+  {\bf Contributions:} There have been earlier formal investigations 
+  into PIP, but ...\cite{Faria08}
 
   vt (valid trace) was introduced earlier, cite
   
@@ -321,11 +323,11 @@
   \node (E1) at (6, 0.2) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>3"}};
   \node (F) at (8,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>3"}};
 
-  \draw [->,line width=0.6mm] (A) to node [pos=0.45,sloped,above=-0.5mm] {\fnt{}holding}  (B);
+  \draw [<-,line width=0.6mm] (A) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding}  (B);
   \draw [->,line width=0.6mm] (C) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waiting}  (B);
   \draw [->,line width=0.6mm] (D) to node [pos=0.4,sloped,below=-0.5mm] {\fnt{}waiting}  (B);
-  \draw [->,line width=0.6mm] (D) to node [pos=0.45,sloped,below=-0.5mm] {\fnt{}holding}  (E);
-  \draw [->,line width=0.6mm] (D) to node [pos=0.45,sloped,above=-0.5mm] {\fnt{}holding}  (E1);
+  \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,below=-0.5mm] {\fnt{}holding}  (E);
+  \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding}  (E1);
   \draw [->,line width=0.6mm] (F) to node [pos=0.45,sloped,below=-0.5mm] {\fnt{}waiting}  (E);
   \end{tikzpicture}
   \end{center}
@@ -416,10 +418,10 @@
   \end{isabelle}
 
   \noindent 
-  More interesting are the cases when a resource, say @{text cs}, is locked or released. In this case
-  we need to calculate a new waiting queue function. For the event @{term P}, we have to update
+  More interesting are the cases when a resource, say @{text cs}, is locked or released. In these cases
+  we need to calculate a new waiting queue function. For the event @{term "P th cs"}, we have to update
   the function so that the new thread list for @{text cs} is old thread list plus the thread @{text th} 
-  appended to the end of that list (remember the head of this list is seen to be in the possession of the
+  appended to the end of that list (remember the head of this list is seen to be in the possession of this
   resource).
 
   \begin{isabelle}\ \ \ \ \ %%%
@@ -432,7 +434,7 @@
   \end{isabelle}
 
   \noindent
-  The clause for event @{term V} is similar, except that we need to update the waiting queue function
+  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
   the auxiliary function @{term release}. A simple version of @{term release} would
   just delete this thread and return the rest, namely
@@ -445,9 +447,9 @@
   \end{isabelle}
 
   \noindent
-  In practice, however, often the thread with the highest precedence will get the
+  In practice, however, often the thread with the highest precedence in the list will get the
   lock next. We have implemented this choice, but later found out that the choice 
-  about which thread is chosen next is actually irrelevant for the correctness of PIP.
+  of which thread is chosen next is actually irrelevant for the correctness of PIP.
   Therefore we prove the stronger result where @{term release} is defined as
 
   \begin{isabelle}\ \ \ \ \ %%%
@@ -471,9 +473,9 @@
   \end{tabular}
   \end{isabelle}
 
-  Having the scheduler function @{term schs} at our disposal, we can ``lift'' the notions
-  @{term waiting}, @{term holding}, @{term depend} and @{term cp} such that they only depend 
-  on states.
+  Having the scheduler function @{term schs} at our disposal, we can ``lift'', or
+  overload, the notions
+  @{term waiting}, @{term holding}, @{term depend} and @{term cp} to operate on states only.
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}rcl}
@@ -485,8 +487,8 @@
   \end{isabelle}
 
   \noindent
-  With these abbreviations we can introduce for states 
-  the notion of threads being @{term readys} (i.e.~threads
+  With these abbreviations we can introduce 
+  the notion of threads being @{term readys} in a state (i.e.~threads
   that do not wait for any resource) and the running thread.
 
   \begin{isabelle}\ \ \ \ \ %%%
@@ -503,7 +505,8 @@
   @{term threads} is empty and therefore there is no thread ready nor a 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 can also define the set of resources that are locked by a thread in any
+  threads. We use the set-comprehension to capture both possibilites.
+  We can now also define the set of resources that are locked by a thread in any
   given state.
 
   \begin{isabelle}\ \ \ \ \ %%%
@@ -574,7 +577,14 @@
 
 section {* Conclusion *}
 
-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.
+
+  TO DO 
+
+*}
 
 text {*
   \bigskip
Binary file prio/paper.pdf has changed