pip: comparison Journal/Paper.thy

equal deleted inserted replaced

-:f70344294e99
+:10c16b85a839
 advantages in practice. On the contrary, according to their work having a policy
 like our FIFO-scheduling of threads with equal priority reduces the number of
 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}\ \ \ \ \ %%%
 \mbox{\begin{tabular}{@ {}l}
 @{thm cntP_def}\\
 @{thm cntV_def}
 \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
 this list (i.e.~the head, or short @{term hd}) is chosen to be the one
 that is in possession of the
 \noindent Note that forests can have trees with infinte depth and
 containing nodes with infinitely many children.  A \emph{finite
 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
 so that every thread can be in the possession of several resources, that is
 it has potentially several incoming holding edges in the RAG, but has at most one outgoing
 \begin{isabelle}\ \ \ \ \ %%%
 @{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.
 While the precedence @{term prec} of any thread is determined statically
 (for example when the thread is
 context valid_trace
 begin
 (*>*)
 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}
 @{thm [mode=IfThen] preced_unique[where ?th1.0=th\<^sub>1 and ?th2.0=th\<^sub>2]}
 \end{lemma}
 That means the precedences of @{text "th'\<^sub>1"} and @{text "th'\<^sub>2"}
 must be the same (they are the maxima in the respective RAG-subtrees). From this we can
 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(*>*)
 section {* The Correctness Proof *}
 \begin{theorem}\label{mainthm}
 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"}.
 \end{itemize}
 \end{theorem}
 %% HERE
 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}
 @{term "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))"}
 \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
+}
+Next we show that a running thread @{text "th'"} must either wait for or
+hold a resource in state @{text s}.
-\begin{proof}[of Theorem 1]
-If @{term "th \<in> running (s' @ s)"}, then there is nothing to show. So let us
+\begin{lemma}\label{notdetached}
-assume otherwise. By Lem.~\ref{thblockedE} we know there exists a thread
+If @{term "th' \<in> running (s' @ s)"} then @{term "\<not>detached s th'"}.
-@{text "th'"} that is an acestor of @{text th} in the @{text "RAG"}
+\end{lemma}
-and @{text "th'"} is running, that is we know
+\begin{proof} Let us assume @{text "th'"} is detached in state
-\begin{center}
+@{text "s"}, then, according to the definition of detached, @{text
-@{term "th' \<in> nancestors (tG (s' @ s)) th"} \quad and \quad
+"th’"} does not hold or wait for any resource. Hence the @{text
-@{term "th' \<in> running (s' @ s)"}
+cp}-value of @{text "th'"} in @{text s} is not boosted, that is
-\end{center}
+@{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
-\noindent We have that @{term "th \<noteq> th'"} since we assumed
+means @{text "th'"} will not run as long as @{text "th"} is a
-@{text th} is not running.  By Lem.~\ref{thkept}, we know that
+live thread. In turn this means @{text "th'"} cannot acquire a reseource
-@{text "th'"} is also running in state @{text s} and by
+and is still detached in state @{text "s' @ s"}.  Consequently
-Lem.~\ref{detached} that @{term "\<not>detached s th'"}.
+@{text "th'"} is also not boosted in state @{text "s' @ s"} and
-By Lem.~\ref{runningpreced} we have
+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. 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"}
 either @{term th} is either running or blocked by a thread @{term
 "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}
 then @{thm (concl) eq_pv_blocked}
 \end{lemma}
 \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
 reasonable.
 \begin{lemma}\label{runninginversion}
 @{thm running_inversion}
 \end{lemma}
 explain tRAG
-\bigskip
+\bigskip}
 Suppose the thread @{term th} is \emph{not} running in state @{term
 "t @ s"}, meaning that it should be blocked by some other thread.
 It is first shown that there is a path in the RAG leading from node
 \begin{corollary}
 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.
 It is relatively easy to see that:
 %We are grateful for the comments we received from anonymous
 %referees.
 \bibliographystyle{plain}
 \bibliography{root}
+\theendnotes
 *}
 (*<*)
 end

changeset 142	10c16b85a839
parent 141	f70344294e99
child 143	c5a65d98191a