--- a/Journal/Paper.thy Thu Jun 20 23:28:26 2013 -0400
+++ b/Journal/Paper.thy Tue Feb 25 20:01:47 2014 +0000
@@ -3,19 +3,9 @@
imports "../CpsG" "../ExtGG" "~~/src/HOL/Library/LaTeXsugar"
begin
-(*
-find_unused_assms CpsG
-find_unused_assms ExtGG
-find_unused_assms Moment
-find_unused_assms Precedence_ord
-find_unused_assms PrioG
-find_unused_assms PrioGDef
-*)
-ML {*
- open Printer;
- show_question_marks_default := false;
- *}
+declare [[show_question_marks = false]]
+
notation (latex output)
Cons ("_::_" [78,77] 73) and
@@ -38,9 +28,7 @@
original_priority ("priority") and
DUMMY ("\<^raw:\mbox{$\_\!\_$}>")
-(*abbreviation
- "detached s th \<equiv> cntP s th = cntV s th"
-*)
+
(*>*)
section {* Introduction *}
@@ -96,12 +84,15 @@
ASIMO robot, etc.), but also the POSIX 1003.1c Standard realised for
example in libraries for FreeBSD, Solaris and Linux.
- One advantage of PIP is that increasing the priority of a thread
- can be performed dynamically by the scheduler. This is in contrast
- to, for example, \emph{Priority Ceiling} \cite{Sha90}, another
- solution to the Priority Inversion problem, which requires static
- analysis of the program in order to prevent Priority
- Inversion. However, there has also been strong criticism against
+ Two advantages of PIP are that increasing the priority of a thread
+ can be performed dynamically by the scheduler and is deterministic.
+ This is in contrast to \emph{Priority Ceiling}
+ \cite{Sha90}, another solution to the Priority Inversion problem,
+ which requires static analysis of the program in order to prevent
+ Priority Inversion, and also to the Windows NT scheduler, which avoids
+ this problem by randomly boosting the priority of ready (low priority) threads
+ (e.g.~\cite{WINDOWSNT}).
+ However, there has also been strong criticism against
PIP. For instance, PIP cannot prevent deadlocks when lock
dependencies are circular, and also blocking times can be
substantial (more than just the duration of a critical section).
@@ -160,7 +151,10 @@
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).\medskip
+ of threads, i.e.~\emph{traces}, that could possibly happen).\footnote{While
+ \cite{Sha90} is the only formal publication we have
+ found that describes the incorrect behaviour, not all, but many
+ informal descriptions of PIP overlook the case...}\medskip
\noindent
{\bf Contributions:} There have been earlier formal investigations
@@ -335,26 +329,26 @@
\noindent
If there is no cycle, then every RAG can be pictured as a forrest of trees, for example as follows:
- \begin{figure}[h]
+ \begin{figure}[ph]
\begin{center}
\newcommand{\fnt}{\fontsize{7}{8}\selectfont}
\begin{tikzpicture}[scale=1]
%%\draw[step=2mm] (-3,2) grid (1,-1);
- \node (A) at (0,0) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>0"}};
- \node (B) at (2,0) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>1"}};
- \node (C) at (4,0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>1"}};
- \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"}};
+ \node (A) at (0,0) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^sub>0"}};
+ \node (B) at (2,0) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^sub>1"}};
+ \node (C) at (4,0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^sub>1"}};
+ \node (D) at (4,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^sub>2"}};
+ \node (E) at (6,-0.7) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^sub>2"}};
+ \node (E1) at (6, 0.2) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^sub>3"}};
+ \node (F) at (8,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^sub>3"}};
- \node (X) at (0,-2) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>4"}};
- \node (Y) at (2,-2) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>4"}};
- \node (Z) at (2,-2.9) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>5"}};
- \node (U1) at (4,-2) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>5"}};
- \node (U2) at (4,-2.9) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>6"}};
- \node (R) at (6,-2.9) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>6"}};
+ \node (X) at (0,-2) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^sub>4"}};
+ \node (Y) at (2,-2) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^sub>4"}};
+ \node (Z) at (2,-2.9) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^sub>5"}};
+ \node (U1) at (4,-2) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^sub>5"}};
+ \node (U2) at (4,-2.9) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^sub>6"}};
+ \node (R) at (6,-2.9) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^sub>6"}};
\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);
@@ -397,10 +391,10 @@
This definition needs to account for all threads that wait for a thread to
release a resource. This means we need to include threads that transitively
wait for a resource being released (in the picture above this means the dependants
- of @{text "th\<^isub>0"} are @{text "th\<^isub>1"} and @{text "th\<^isub>2"}, which wait for resource @{text "cs\<^isub>1"},
- but also @{text "th\<^isub>3"},
- which cannot make any progress unless @{text "th\<^isub>2"} makes progress, which
- in turn needs to wait for @{text "th\<^isub>0"} to finish). If there is a circle of dependencies
+ of @{text "th\<^sub>0"} are @{text "th\<^sub>1"} and @{text "th\<^sub>2"}, which wait for resource @{text "cs\<^sub>1"},
+ but also @{text "th\<^sub>3"},
+ which cannot make any progress unless @{text "th\<^sub>2"} makes progress, which
+ in turn needs to wait for @{text "th\<^sub>0"} to finish). If there is a circle of dependencies
in a RAG, then clearly
we have a deadlock. Therefore when a thread requests a resource,
we must ensure that the resulting RAG is not circular. In practice, the
@@ -638,7 +632,7 @@
\noindent
Note, however, that apart from the circularity condition, we do not make any
- assumption on how different resources can locked and released relative to each
+ assumption on how different resources can be locked and released relative to each
other. In our model it is possible that critical sections overlap. This is in
contrast to Sha et al \cite{Sha90} who require that critical sections are
properly nested.
@@ -803,9 +797,9 @@
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
- @{thm[mode=IfThen] waiting_unique[of _ _ "cs\<^isub>1" "cs\<^isub>2"]}\\
- @{thm[mode=IfThen] held_unique[of _ "th\<^isub>1" _ "th\<^isub>2"]}\\
- @{thm[mode=IfThen] runing_unique[of _ "th\<^isub>1" "th\<^isub>2"]}
+ @{thm[mode=IfThen] waiting_unique[of _ _ "cs\<^sub>1" "cs\<^sub>2"]}\\
+ @{thm[mode=IfThen] held_unique[of _ "th\<^sub>1" _ "th\<^sub>2"]}\\
+ @{thm[mode=IfThen] runing_unique[of _ "th\<^sub>1" "th\<^sub>2"]}
\end{tabular}
\end{isabelle}
@@ -904,7 +898,7 @@
%\item Every node in RAG can be chased to a ready thread (@{text "chain_building"}):
% @ {thm [display] chain_building[rule_format]}
%\item The ready thread chased to is unique (@{text "dchain_unique"}):
- % @ {thm [display] dchain_unique[of _ _ "th\<^isub>1" "th\<^isub>2"]}
+ % @ {thm [display] dchain_unique[of _ _ "th\<^sub>1" "th\<^sub>2"]}
%\end{enumerate}
%Some deeper results about the system:
@@ -1076,7 +1070,7 @@
\end{isabelle}
\noindent
- This means in an implementation we do not have recalculate the @{text RAG} and also none of the
+ This means in an implementation we do not have to recalculate the @{text RAG} and also none of the
current precedences of the other threads. The current precedence of the created
thread @{text th} is just its precedence, namely the pair @{term "(prio, length (s::event list))"}.
\smallskip
@@ -1453,7 +1447,7 @@
PIP is a scheduling algorithm for single-processor systems. We are
now living in a multi-processor world. Priority Inversion certainly
- occurs also there, see for example \cite{Brandenburg11, Davis11}.
+ occurs also there, see for example \cite{Brandenburg11,Davis11}.
However, there is very little ``foundational''
work about PIP-algorithms on multi-processor systems. We are not
aware of any correctness proofs, not even informal ones. There is an