--- a/Journal/Paper.thy Tue May 20 12:49:21 2014 +0100
+++ b/Journal/Paper.thy Thu May 22 17:40:39 2014 +0100
@@ -9,23 +9,22 @@
notation (latex output)
Cons ("_::_" [78,77] 73) and
+ If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
vt ("valid'_state") and
runing ("running") and
- If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
Prc ("'(_, _')") and
holding ("holds") and
waiting ("waits") and
Th ("T") and
Cs ("C") and
readys ("ready") and
- depend ("RAG") and
preced ("prec") and
+ preceds ("precs") and
cpreced ("cprec") and
cp ("cprec") and
holdents ("resources") and
DUMMY ("\<^raw:\mbox{$\_\!\_$}>")
-
(*>*)
section {* Introduction *}
@@ -186,7 +185,7 @@
et al.~\cite{Sha90} to the practically relevant case where critical
sections can overlap; see Figure~\ref{overlap} below for an example of
this restriction. In the existing literature there is no
- proof and also no prove method that cover this generalised case.
+ proof and also no proving method that cover this generalised case.
\begin{figure}
\begin{center}
@@ -328,6 +327,14 @@
\end{isabelle}
\noindent
+ We also use the abbreviation
+
+ \begin{isabelle}\ \ \ \ \ %%%
+ @{abbrev "preceds s ths"}
+ \end{isabelle}
+
+ \noindent
+ for the set of precedences of threads @{text ths} in state @{text s}.
The point of precedences is to schedule threads not according to priorities (because what should
we do in case two threads have the same priority), but according to precedences.
Precedences allow us to always discriminate between two threads with equal priority by
@@ -390,7 +397,7 @@
as the union of the sets of waiting and holding edges, namely
\begin{isabelle}\ \ \ \ \ %%%
- @{thm cs_depend_def}
+ @{thm cs_RAG_def}
\end{isabelle}
@@ -478,7 +485,7 @@
\noindent
where the dependants of @{text th} are given by the waiting queue function.
- While the precedence @{term prec} of a thread is determined statically
+ While the precedence @{term prec} of any thread is determined statically
(for example when the thread is
created), the point of the current precedence is to let the scheduler increase this
precedence, if needed according to PIP. Therefore the current precedence of @{text th} is
@@ -486,7 +493,8 @@
threads that are dependants of @{text th}. Since the notion @{term "dependants"} is
defined as the transitive closure of all dependent threads, we deal correctly with the
problem in the informal algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is
- lowered prematurely.
+ lowered prematurely. We again introduce an abbreviation for current precedeces of
+ a set of threads, written @{term "cprecs wq s ths"}.
The next function, called @{term schs}, defines the behaviour of the scheduler. It will be defined
by recursion on the state (a list of events); this function returns a \emph{schedule state}, which
@@ -597,16 +605,18 @@
\end{tabular}
\end{isabelle}
- 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.
+ Having the scheduler function @{term schs} at our disposal, we can
+ ``lift'', or overload, the notions @{term waiting}, @{term holding},
+ @{term RAG}, @{term dependants} 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) s_depend_abv} & @{text "\<equiv>"} & @{thm (rhs) s_depend_abv}\\
- @{thm (lhs) cp_def} & @{text "\<equiv>"} & @{thm (rhs) cp_def}
+ @{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) s_RAG_abv} & @{text "\<equiv>"} & @{thm (rhs) s_RAG_abv}\\
+ @{thm (lhs) s_dependants_abv}& @{text "\<equiv>"} & @{thm (rhs) s_dependants_abv}\\
+ @{thm (lhs) cp_def} & @{text "\<equiv>"} & @{thm (rhs) cp_def}\\
\end{tabular}
\end{isabelle}
@@ -625,7 +635,7 @@
\end{isabelle}
\noindent
- In the second definition @{term "DUMMY ` DUMMY"} stands for the image of a set under a function.
+ %%In the second definition @{term "DUMMY ` DUMMY"} stands for the image of a set under a function.
Note that in the initial state, that is where the list of events is empty, the set
@{term threads} is empty and therefore there is neither a thread ready nor running.
If there is one or more threads ready, then there can only be \emph{one} thread
@@ -791,7 +801,7 @@
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{l}
@{term "th \<in> threads s"}\\
- @{term "prec th s = Max (cprec s ` threads s)"}\\
+ @{term "prec th s = Max (cprecs s (threads s))"}\\
@{term "prec th s = (prio, DUMMY)"}
\end{tabular}
\end{isabelle}
@@ -836,30 +846,30 @@
many threads that can block @{text th} in this way and then they
need to run with the same precedence as @{text th}.
- Like in the argument by Sha et al.~our
- finite bound does not guarantee absence of indefinite Priority
- Inversion. For this we further have to assume that every thread
- gives up its resources after a finite amount of time. We found that
- this assumption is awkward to formalise in our model. There are mainly
- two reasons: First, we do not specify what ``running'' the code of a
- thread means, for example by giving an operational semantics for
- machine instructions. Therefore we cannot characterise what are ``good''
+ Like in the argument by Sha et al.~our finite bound does not
+ guarantee absence of indefinite Priority Inversion. For this we
+ further have to assume that every thread gives up its resources
+ after a finite amount of time. We found that this assumption is
+ awkward to formalise in our model. There are mainly two reasons:
+ First, we do not specify what ``running'' the code of a thread
+ means, for example by giving an operational semantics for machine
+ instructions. Therefore we cannot characterise what are ``good''
programs that contain for every looking request also a corresponding
- unlocking request for a resource.
- %
- %(HERE)
- %
- Therefore we
- leave it out and let the programmer assume the responsibility to
- program threads in such a benign manner (in addition to causing no
- circularity in the RAG). In this detail, we do not
- make any progress in comparison with the work by Sha et al.
+ unlocking request for a resource. Second, we would need to specify a
+ kind of global clock that tracks the time how long a thread locks a
+ resource. But this seems difficult, because how do we conveninet
+ distinguish between a thread that ``just'' lock a resource for a
+ very long time and one that locks it forever. Therefore we decided
+ to leave it out this property and let the programmer assume the
+ responsibility to program threads in such a benign manner (in
+ addition to causing no circularity in the RAG). In this detail, we
+ do not make any progress in comparison with the work by Sha et al.
However, we are able to combine their two separate bounds into a
single theorem improving their bound.
In what follows we will describe properties of PIP that allow us to prove
Theorem~\ref{mainthm} and, when instructive, briefly describe our argument.
- It is relatively easy to see that
+ It is relatively easy to see that:
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
@@ -870,7 +880,7 @@
\noindent
The second property is by induction of @{term vt}. The next three
- properties are
+ properties are:
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
@@ -890,11 +900,11 @@
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
- @{text If}~@{thm (prem 1) acyclic_depend}~@{text "then"}:\\
- \hspace{5mm}@{thm (concl) acyclic_depend},
- @{thm (concl) finite_depend} and
+ @{text If}~@{thm (prem 1) acyclic_RAG}~@{text "then"}:\\
+ \hspace{5mm}@{thm (concl) acyclic_RAG},
+ @{thm (concl) finite_RAG} and
@{thm (concl) wf_dep_converse},\\
- \hspace{5mm}@{text "if"}~@{thm (prem 2) dm_depend_threads}~@{text "then"}~@{thm (concl) dm_depend_threads}
+ \hspace{5mm}@{text "if"}~@{thm (prem 2) dm_RAG_threads}~@{text "then"}~@{thm (concl) dm_RAG_threads}
and\\
\hspace{5mm}@{text "if"}~@{thm (prem 2) range_in}~@{text "then"}~@{thm (concl) range_in}.
\end{tabular}
@@ -1113,7 +1123,7 @@
\noindent
That means the current precedence of a thread @{text th} can be
- computed locally by considering only the children of @{text th}. In
+ computed locally by considering only the current precedences of the children of @{text th}. In
effect, it only needs to be recomputed for @{text th} when one of
its children changes its current precedence. Once the current
precedence is computed in this more efficient manner, the selection
@@ -1121,6 +1131,10 @@
a standard scheduling operation implemented in most operating
systems.
+ \begin{proof}[of Lemma~\ref{childrenlem}]
+ Test
+ \end{proof}
+
Of course the main work for implementing PIP involves the
scheduler and coding how it should react to events. Below we
outline how our formalisation guides this implementation for each
@@ -1242,7 +1256,7 @@
\begin{isabelle}\ \ \ \ \ %%%
- @{thm depend_s}
+ @{thm RAG_s}
\end{isabelle}
\noindent
@@ -1265,7 +1279,7 @@
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
- @{thm depend_s}\\
+ @{thm RAG_s}\\
@{thm eq_cp}
\end{tabular}
\end{isabelle}
@@ -1284,7 +1298,7 @@
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
- @{thm depend_s}\\
+ @{thm RAG_s}\\
@{thm eq_cp}
\end{tabular}
\end{isabelle}
@@ -1297,7 +1311,7 @@
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
- @{thm depend_s}\\
+ @{thm RAG_s}\\
@{thm[mode=IfThen] eq_cp}
\end{tabular}
\end{isabelle}