--- a/prio/Paper/Paper.thy Tue Feb 07 01:10:34 2012 +0000
+++ b/prio/Paper/Paper.thy Wed Feb 08 16:35:49 2012 +0000
@@ -11,8 +11,9 @@
Cons ("_::_" [78,77] 73) and
vt ("valid'_state") and
runing ("running") and
- birthtime ("inception") and
+ birthtime ("last'_set") and
If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
+ Prc ("'(_, _')") and
DUMMY ("\<^raw:\mbox{$\_\!\_$}>")
(*>*)
@@ -55,11 +56,11 @@
time leading to a system reset. Once the problem was found, it was
rectified by enabling the \emph{Priority Inheritance Protocol} (PIP)
\cite{Sha90}\footnote{Sha et al.~call it the \emph{Basic Priority
- Inheritance Protocol} \cite{Sha90} and others sometimes call it
- also \emph{Priority Boosting}.} in the scheduling software.
+ Inheritance Protocol} \cite{Sha90} and others sometimes also call it
+ \emph{Priority Boosting}.} in the scheduling software.
The idea behind PIP is to let the thread $L$ temporarily inherit
- the high priority from $H$ until $L$ leaves the critical section by
+ the high priority from $H$ until $L$ leaves the critical section
unlocking the resource. This solves the problem of $H$ having to
wait indefinitely, because $L$ cannot be blocked by threads having
priority $M$. While a few other solutions exist for the Priority
@@ -89,13 +90,10 @@
\noindent
He suggests to avoid PIP altogether by not allowing critical
- sections to be preempted. While this might have been a reasonable
- solution in 2002, in our modern multiprocessor world, this seems out
- of date. The reason is that this precludes other high-priority
- threads from running even when they do not make any use of the locked
- resource.
+ sections to be preempted. Unfortunately, this solution does not
+ help in real-time systems with low latency \emph{requirements}.
- However, there is clearly a need for investigating correct
+ In our opinion, there is clearly a need for investigating correct
algorithms for PIP. A few specifications for PIP exist (in English)
and also a few high-level descriptions of implementations (e.g.~in
the textbook \cite[Section 5.6.5]{Vahalia96}), but they help little
@@ -114,7 +112,7 @@
\noindent
The criticism by Yodaiken, Baker and others suggests to us to look
again at PIP from a more abstract level (but still concrete enough
- to inform an implementation) and makes PIP an ideal candidate for a
+ to inform an implementation), and makes PIP an ideal candidate for a
formal verification. One reason, of course, is that the original
presentation of PIP~\cite{Sha90}, despite being informally
``proved'' correct, is actually \emph{flawed}.
@@ -143,36 +141,43 @@
vt (valid trace) was introduced earlier, cite
distributed PIP
+
+ Paulson's method has not been used outside security field, except
+ work by Zhang et al.
+
+ no clue about multi-processor case according to \cite{Steinberg10}
*}
section {* Formal Model of the Priority Inheritance Protocol *}
text {*
- We follow the original work by Sha et al.~\cite{Sha90} by modelling
- first a classical single CPU system where only one \emph{thread} is
- active at any given moment. We shall discuss later how to lift this
- restriction. Our model of PIP is based on Paulson's inductive
- approach to protocol verification \cite{Paulson98}, where the
- \emph{state} of a system is given by a list of events that
- happened so far. \emph{Events} fall into four categories defined as
- the datatype
+ The Priority Inheritance Protocol, short PIP, is a scheduling
+ algorithm for a single-processor system.\footnote{We shall come back
+ later to the case of PIP on multi-processor systems.} Our model of
+ PIP is based on Paulson's inductive approach to protocol
+ verification \cite{Paulson98}, where the \emph{state} of a system is
+ given by a list of events that happened so far. \emph{Events} fall
+ into five categories defined as the datatype
\begin{isabelle}\ \ \ \ \ %%%
\mbox{\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{7mm}}l}
\isacommand{datatype} event
& @{text "="} & @{term "Create thread priority"}\\
& @{text "|"} & @{term "Exit thread"} \\
- & @{text "|"} & @{term "Set thread priority"} & {\rm reset of the proprity for} @{text thread}\\
+ & @{text "|"} & @{term "Set thread priority"} & {\rm reset of the priority for} @{text thread}\\
& @{text "|"} & @{term "P thread cs"} & {\rm request of resource} @{text "cs"} {\rm by} @{text "thread"}\\
& @{text "|"} & @{term "V thread cs"} & {\rm release of resource} @{text "cs"} {\rm by} @{text "thread"}
\end{tabular}}
\end{isabelle}
\noindent
- whereby threads, priorities and (critical) resources are represented
- as natural numbers. As in Paulson's work, we need to define
- functions that allow one to make some observations about states.
- One is the ``live'' threads we have seen so far in a state:
+ whereby threads, priorities and (critical) resources are represented
+ as natural numbers. The event @{term Set} models the situation that
+ a thread obtains a new priority given by the programmer or
+ user (for example via the {\tt nice} utility under UNIX). As in Paulson's work, we
+ need to define functions that allow one to make some observations
+ about states. One, called @{term threads}, calculates the set of
+ ``live'' threads that we have seen so far in a state:
\begin{isabelle}\ \ \ \ \ %%%
\mbox{\begin{tabular}{lcl}
@@ -187,8 +192,7 @@
\end{isabelle}
\noindent
- Another is that given a thread @{text "th"}, what is the original priority was at
- its inception.
+ Another calculates the priority for a thread @{text "th"}, defined as
\begin{isabelle}\ \ \ \ \ %%%
\mbox{\begin{tabular}{lcl}
@@ -219,10 +223,42 @@
@{term "birthtime th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "birthtime th s"}\\
\end{tabular}}
\end{isabelle}
+
+ \footnote{Can Precedence be the real birth-time / or must be time precedence last set?}
+
+ \noindent
+ A \emph{precedence} of a thread @{text th} in a state @{text s} is a pair of
+ natural numbers defined as
- \begin{center}
- threads, original-priority, birth time, precedence.
- \end{center}
+ \begin{isabelle}\ \ \ \ \ %%%
+ @{thm (rhs) preced_def[where thread="th"]}
+ \end{isabelle}
+
+ \noindent
+ The point of precedences is to schedule threads not according to priorities (what should
+ we do in case two threads have the same priority), but according to precedences.
+ Precedences allow us to always discriminate two threads with equal priority by
+ tacking into account the time when the priority was last set. We order precedences so
+ that threads with the same priority get a higher precedence if their priority has been
+ set earlier, since for such threads it is more urgent to finish. In an impementation
+ this choice would translate to a quite natural a FIFO-scheduling of processes with
+ the same priority.
+
+ Next, we introduce the concept of \emph{waiting queues}. They are
+ lists of threads associated with every resource. The first thread in
+ this list is chosen to be in the one that is in possession of the
+ ``lock'' of the corresponding resource. We model waiting queues as
+ functions, below abbreviated as @{text wq}, taking a resource as
+ argument and returning a list of threads. This allows us to define
+ when a thread \emph{holds}, respectively \emph{waits}, for a
+ resource @{text cs}.
+
+ \begin{isabelle}\ \ \ \ \ %%%
+ \begin{tabular}{@ {}l}
+ @{thm cs_holding_def[where thread="th"]}\\
+ @{thm cs_waiting_def[where thread="th"]}
+ \end{tabular}
+ \end{isabelle}
@@ -937,6 +973,34 @@
section {* Conclusions \label{conclusion} *}
+text {*
+ The work in this paper only deals with single CPU configurations. The
+ "one CPU" assumption is essential for our formalisation, because the
+ main lemma fails in multi-CPU configuration. The lemma says that any
+ runing thead must be the one with the highest prioirty or already held
+ some resource when the highest priority thread was initiated. When
+ there are multiple CPUs, it may well be the case that a threads did
+ not hold any resource when the highest priority thread was initiated,
+ but that thread still runs after that moment on a separate CPU. In
+ this way, the main lemma does not hold anymore.
+
+
+ There are some works deals with priority inversion in multi-CPU
+ configurations[???], but none of them have given a formal correctness
+ proof. The extension of our formal proof to deal with multi-CPU
+ configurations is not obvious. One possibility, as suggested in paper
+ [???], is change our formal model (the defiintion of "schs") to give
+ the released resource to the thread with the highest prioirty. In this
+ way, indefinite prioirty inversion can be avoided, but for a quite
+ different reason from the one formalized in this paper (because the
+ "mail lemma" will be different). This means a formal correctness proof
+ for milt-CPU configuration would be quite different from the one given
+ in this paper. The solution of prioirty inversion problem in mult-CPU
+ configurations is a different problem which needs different solutions
+ which is outside the scope of this paper.
+
+*}
+
(*<*)
end
(*>*)
\ No newline at end of file