diff -r f70344294e99 -r 10c16b85a839 Journal/Paper.thy --- 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 \ running (s' @ s)"} or\medskip + \item[$\bullet$] @{term "th \ running (s' @ s)"} or\medskip - \item there exists a thread @{term "th'"} with @{term "th' \ th"} + \item[$\bullet$] there exists a thread @{term "th'"} with @{term "th' \ th"} and @{term "th' \ running (s' @ s)"} such that @{text "th' \ threads s"}, @{text "\ 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' \ running (s' @ s)"} then @{term "\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 \ 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' \ nancestors (tG (s' @ s)) th"} \quad and \quad - @{term "th' \ running (s' @ s)"} - \end{center} - - \noindent We have that @{term "th \ 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 "\detached s th'"}. - By Lem.~\ref{runningpreced} we have + \begin{proof}[of Theorem 1] If @{term "th \ 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 \ th'"} + since we assumed @{text th} is not running. By + Lem.~\ref{notdetached} we have that @{term "\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' \ + 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 \ 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 *}