regexp: comparison prio/Paper/Paper.thy

equal deleted inserted replaced

-:4fcd802eba59
+:8524f94d251b
 to its original priority level.'' This leads them to believe that an
 implementation of PIP is ``rather straightforward''~\cite{Sha90}.
 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
 the threads that it blocks. The advantage of formalising the
 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
 distributed PIP
 \node (D) at (4,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>2"}};
 \node (E) at (6,-0.7) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>2"}};
 \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.54,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,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}
 \noindent
 \hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Set th prio # s)|)"}
 \end{tabular}
 \end{isabelle}
 \noindent
-More interesting are the cases when a resource, say @{text cs}, is locked or released. In this case
+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}, we have to update
+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}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm (lhs) schs.simps(5)} @{text "\<equiv>"}\\
 \hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (P th cs # s)|)"}
 \end{tabular}
 \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
 \begin{isabelle}\ \ \ \ \ %%%
 @{term "release (DUMMY # qs)"} & @{text "\<equiv>"} & @{term "qs"}\\
 \end{tabular}
 \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}\ \ \ \ \ %%%
 \begin{tabular}{@ {}lcl}
 @{term "release []"} & @{text "\<equiv>"} & @{term "[]"}\\
 \hspace{5mm}@{text "let"} @{text "new_wq = release (wq cs)"} @{text "in"}\\
 \hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|)"}
 \end{tabular}
 \end{isabelle}
-Having the scheduler function @{term schs} at our disposal, we can ``lift'' the notions
+Having the scheduler function @{term schs} at our disposal, we can ``lift'', or
-@{term waiting}, @{term holding}, @{term depend} and @{term cp} such that they only depend
+overload, the notions
-on states.
+@{term waiting}, @{term holding}, @{term depend} and @{term cp} to operate on states only.
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}rcl}
 @{thm (lhs) s_holding_abv} & @{text "\<equiv>"} & @{thm (rhs) s_holding_abv}\\
 @{thm (lhs) s_waiting_abv} & @{text "\<equiv>"} & @{thm (rhs) s_waiting_abv}\\
 @{thm (lhs) cp_def}        & @{text "\<equiv>"} & @{thm (rhs) cp_def}
 \end{tabular}
 \end{isabelle}
 \noindent
-With these abbreviations we can introduce for states
+With these abbreviations we can introduce
-the notion of threads being @{term readys} (i.e.~threads
+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}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm readys_def}\\
 function @{text f}.
 Note that in the initial case, that is where the list of events is empty, the set
 @{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}\ \ \ \ \ %%%
 @{thm holdents_def}
 \end{isabelle}
 text {* TO DO *}
 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
 The priority inversion phenomenon was first published in
 \cite{Lampson80}.  The two protocols widely used to eliminate

changeset 300	8524f94d251b
parent 299	4fcd802eba59
child 301	e820ee5f76f7