--- a/Journal/Paper.thy Fri Oct 21 14:47:01 2016 +0100
+++ b/Journal/Paper.thy Fri Dec 09 12:51:29 2016 +0000
@@ -424,7 +424,7 @@
tasks involved in the inheritance process and thus minimises the number
of potentially expensive thread-switches.
- {\bf NEEDED?} We will also need counters for @{term P} and @{term V} events of a thread @{term th}
+ \endnote{{\bf NEEDED?} We will also need counters for @{term P} and @{term V} events of a thread @{term th}
in a state @{term s}. This can be straightforwardly defined in Isabelle as
\begin{isabelle}\ \ \ \ \ %%%
@@ -434,7 +434,7 @@
\end{tabular}}
\end{isabelle}
- \noindent using the predefined function @{const count} for lists.
+ \noindent using the predefined function @{const count} for lists.}
Next, we introduce the concept of \emph{waiting queues}. They are
lists of threads associated with every resource. The first thread in
@@ -569,16 +569,17 @@
forrest} is a forest which is well-founded and every node has
finitely many children (is only finitely branching).
+ \endnote{
\begin{isabelle}\ \ \ \ \ %%%
@{thm rtrancl_path.intros}
\end{isabelle}
\begin{isabelle}\ \ \ \ \ %%%
@{thm rpath_def}
- \end{isabelle}
+ \end{isabelle}}
- {\bf Lemma about overlapping paths}
+ \endnote{{\bf Lemma about overlapping paths}}
We will design our PIP-scheduler
@@ -619,9 +620,10 @@
@{thm cpreced_def}\hfill\numbered{cpreced}
\end{isabelle}
+ \endnote{
\begin{isabelle}\ \ \ \ \ %%%
@{thm cp_alt_def cp_alt_def1}
- \end{isabelle}
+ \end{isabelle}}
\noindent
where the dependants of @{text th} are given by the waiting queue function.
@@ -881,7 +883,7 @@
(*>*)
text {*
- In this section we prove facts that immediately follow from
+ \endnote{In this section we prove facts that immediately follow from
our definitions of valid traces.
\begin{lemma}??\label{precedunique}
@@ -917,7 +919,7 @@
infer by Lemma~\ref{precedunique} that @{text "th'\<^sub>1"}
and @{text "th'\<^sub>2"} are the same threads. However, this also means the
roots @{text "th\<^sub>1"} and @{text "th\<^sub>2"} must be the same.\qed
- \end{proof}
+ \end{proof}}
*}
(*<*)end(*>*)
@@ -1030,9 +1032,9 @@
Given the assumptions about states @{text "s"} and @{text "s' @ s"},
the thread @{text th} and the events in @{text "s'"}, then either
\begin{itemize}
- \item @{term "th \<in> running (s' @ s)"} or\medskip
+ \item[$\bullet$] @{term "th \<in> running (s' @ s)"} or\medskip
- \item there exists a thread @{term "th'"} with @{term "th' \<noteq> th"}
+ \item[$\bullet$] there exists a thread @{term "th'"} with @{term "th' \<noteq> th"}
and @{term "th' \<in> running (s' @ s)"} such that @{text "th' \<in> threads
s"}, @{text "\<not> detached s th'"} and @{term "cp (s' @ s) th' = prec
th s"}.
@@ -1074,14 +1076,14 @@
Given our assumptions (on @{text th}), the first property we can
show is that any running thread, say @{text "th'"}, has the same
- precedence of @{text th}:
+ precedence as @{text th}:
\begin{lemma}\label{runningpreced}
@{thm [mode=IfThen] running_preced_inversion}
\end{lemma}
\begin{proof}
- By definition the running thread has as current precedence the maximum of
+ By definition, the running thread has as current precedence the maximum of
all ready threads, that is
\begin{center}
@@ -1089,53 +1091,71 @@
\end{center}
\noindent
- We also know that this is equal to all threads, that is
+ We also know that this is equal to the current precedences of all threads,
+ that is
\begin{center}
@{term "cp (t @ s) th' = Max (cp (t @ s) ` treads (t @ s))"}
\end{center}
\noindent
+ This is because each ready thread, say @{text "th\<^sub>r"}, has the maximum
+ current precedence of the subtree located at @{text "th\<^sub>r"}. All these
+ subtrees together form the set of threads.
But the maximum of all threads is the @{term "cp"} of @{text "th"},
- which is the @{term preced} of @{text th}.
+ which is equal to the @{term preced} of @{text th}.\qed
\end{proof}
+ \endnote{
@{thm "th_blockedE_pretty"} -- thm-blockedE??
+ @{text "th_kept"} shows that th is a thread in s'-s
+ }
- @{text "th_kept"} shows that th is a thread in s'-s
+ Next we show that a running thread @{text "th'"} must either wait for or
+ hold a resource in state @{text s}.
+
+ \begin{lemma}\label{notdetached}
+ If @{term "th' \<in> running (s' @ s)"} then @{term "\<not>detached s th'"}.
+ \end{lemma}
-
+ \begin{proof} Let us assume @{text "th'"} is detached in state
+ @{text "s"}, then, according to the definition of detached, @{text
+ "th’"} does not hold or wait for any resource. Hence the @{text
+ cp}-value of @{text "th'"} in @{text s} is not boosted, that is
+ @{term "cp s th' = prec th s"}, and is therefore lower than the
+ precedence (as well as the @{text "cp"}-value) of @{term "th"}. This
+ means @{text "th'"} will not run as long as @{text "th"} is a
+ live thread. In turn this means @{text "th'"} cannot acquire a reseource
+ and is still detached in state @{text "s' @ s"}. Consequently
+ @{text "th'"} is also not boosted in state @{text "s' @ s"} and
+ would not run. This contradicts our assumption.\qed
+ \end{proof}
- \begin{proof}[of Theorem 1]
- If @{term "th \<in> running (s' @ s)"}, then there is nothing to show. So let us
- assume otherwise. By Lem.~\ref{thblockedE} we know there exists a thread
- @{text "th'"} that is an acestor of @{text th} in the @{text "RAG"}
- and @{text "th'"} is running, that is we know
-
- \begin{center}
- @{term "th' \<in> nancestors (tG (s' @ s)) th"} \quad and \quad
- @{term "th' \<in> running (s' @ s)"}
- \end{center}
-
- \noindent We have that @{term "th \<noteq> th'"} since we assumed
- @{text th} is not running. By Lem.~\ref{thkept}, we know that
- @{text "th'"} is also running in state @{text s} and by
- Lem.~\ref{detached} that @{term "\<not>detached s th'"}.
- By Lem.~\ref{runningpreced} we have
+ \begin{proof}[of Theorem 1] If @{term "th \<in> running (s' @ s)"},
+ then there is nothing to show. So let us assume otherwise. Since the
+ @{text "RAG"} is well-founded, we know there exists an ancestor of
+ @{text "th"} that is the root of the corrsponding subtree and
+ therefore is ready. Let us call this thread @{text "th'"}. We know
+ that @{text "th'"} has the highest precedence of all ready threads.
+ Therefore it is running. We have that @{term "th \<noteq> th'"}
+ since we assumed @{text th} is not running. By
+ Lem.~\ref{notdetached} we have that @{term "\<not>detached s th'"}.
+ If @{text "th'"} is not detached in @{text s}, that is either
+ holding or waiting for a resource, it must be that @{term "th' \<in>
+ threads s"}. By Lem.~\ref{runningpreced} we have
\begin{center}
@{term "cp (t @ s) th' = preced th s"}
\end{center}
\noindent
- This concludes the proof of Theorem 1.
+ This concludes the proof of Theorem 1.\qed
\end{proof}
-
-
+ \endnote{
In what follows we will describe properties of PIP that allow us to
prove Theorem~\ref{mainthm} and, when instructive, briefly describe
our argument. Recall we want to prove that in state @{term "s' @ s"}
@@ -1143,7 +1163,6 @@
"th'"} (@{term "th \<noteq> th'"}) which was alive in state @{term s}. We
can show that
-
\begin{lemma}
If @{thm (prem 2) eq_pv_blocked}
@@ -1153,9 +1172,9 @@
\begin{lemma}
If @{thm (prem 2) eq_pv_persist}
then @{thm (concl) eq_pv_persist}
- \end{lemma}
+ \end{lemma}}
- \subsection*{\bf OUTLINE}
+ \endnote{{\bf OUTLINE}
Since @{term "th"} is the most urgent thread, if it is somehow
blocked, people want to know why and wether this blocking is
@@ -1218,7 +1237,7 @@
\end{lemma}
explain tRAG
- \bigskip
+ \bigskip}
Suppose the thread @{term th} is \emph{not} running in state @{term
@@ -1272,10 +1291,7 @@
Using the lemma \ref{runninginversion} we can say more about the thread th'
\end{corollary}
- \subsection*{END OUTLINE}
-
-
-
+ \endnote{\subsection*{END OUTLINE}}
In what follows we will describe properties of PIP that allow us to prove
Theorem~\ref{mainthm} and, when instructive, briefly describe our argument.
@@ -2009,6 +2025,8 @@
\bibliographystyle{plain}
\bibliography{root}
+
+ \theendnotes
*}