pip: comparison Journal/Paper.thy

equal deleted inserted replaced

-:f1d82f6c05a3
+:a8ceb68bfeb0
 *)
 (*<*)
 context valid_trace
 begin
 (*>*)
+(*<*)
 text {*
 \endnote{In this section we prove facts that immediately follow from
 our definitions of valid traces.
 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(*>*)
 section {* The Correctness Proof *}
 (*<*)
 %\begin{lemma}
 %If @{thm (prem 2) eq_pv_persist}
 %then @{thm (concl) eq_pv_persist}
 %\end{lemma}}
-\endnote{{\bf OUTLINE}
+%  \endnote{{\bf OUTLINE}
-Since @{term "th"} is the most urgent thread, if it is somehow
+%  Since @{term "th"} is the most urgent thread, if it is somehow
-blocked, people want to know why and wether this blocking is
+%  blocked, people want to know why and wether this blocking is
-reasonable.
+%  reasonable.
-@{thm [source] th_blockedE} @{thm th_blockedE}
+%  @{thm [source] th_blockedE} @{thm th_blockedE}
-if @{term "th"} is blocked, then there is a path leading from
+%  if @{term "th"} is blocked, then there is a path leading from
-@{term "th"} to @{term "th'"}, which means:
+%  @{term "th"} to @{term "th'"}, which means:
-there is a chain of demand leading from @{term th} to @{term th'}.
+%  there is a chain of demand leading from @{term th} to @{term th'}.
 %%% in other words
 %%% th -> cs1 -> th1 -> cs2 -> th2 -> ... -> csn -> thn -> cs -> th'.
 %%%
 %%% We says that th is blocked by "th'".
-THEN
+%  THEN
-@{thm [source] vat_t.th_chain_to_ready} @{thm vat_t.th_chain_to_ready}
+%  @ {thm [source] vat_t.th_chain_to_ready} @ {thm vat_t.th_chain_to_ready}
-It is basic propery with non-trival proof.
+%  It is basic propery with non-trival proof.
-THEN
+%  THEN
-@{thm [source] max_preced} @{thm max_preced}
+%  @ {thm [source] max_preced} @ {thm max_preced}
-which says @{term "th"} holds the max precedence.
+%  which says @{term "th"} holds the max precedence.
-THEN
+%  THEN
-@{thm [source] th_cp_max th_cp_preced th_kept}
+%  @ {thm [source] th_cp_max th_cp_preced th_kept}
-@{thm th_cp_max th_cp_preced th_kept}
+%  @ {thm th_cp_max th_cp_preced th_kept}
-THENTHEN
+%  THENTHEN
-(here) %@ {thm [source] running_inversion_4} @  {thm running_inversion_4}
+%@ {thm [source] running_inversion_4} @  {thm running_inversion_4}
-which explains what the @{term "th'"} looks like. Now, we have found the
+% which explains what the @{term "th'"} looks like. Now, we have found the
-@{term "th'"} which blocks @{term th}, we need to know more about it.
+% @{term "th'"} which blocks @{term th}, we need to know more about it.
-To see what kind of thread can block @{term th}.
+% To see what kind of thread can block @{term th}.
-From these two lemmas we can see the correctness of PIP, which is
+% From these two lemmas we can see the correctness of PIP, which is
-that: the blockage of th is reasonable and under control.
+% that: the blockage of th is reasonable and under control.
-Lemmas we want to describe:
+% Lemmas we want to describe:
+% \begin{lemma}
+% @ {thm running_cntP_cntV_inv}
-\begin{lemma}
+% \end{lemma}
-@{thm running_cntP_cntV_inv}
-\end{lemma}
+%  \noindent
+%  Remember we do not have the well-nestedness restriction in our
-\noindent
+%  proof, which means the difference between the counters @{const cntV}
-Remember we do not have the well-nestedness restriction in our
+%  and @{const cntP} can be larger than @{term 1}.
-proof, which means the difference between the counters @{const cntV}
-and @{const cntP} can be larger than @{term 1}.
+%  \begin{lemma}\label{runninginversion}
+%  @ {thm running_inversion}
-\begin{lemma}\label{runninginversion}
+%  \end{lemma}
-@{thm running_inversion}
-\end{lemma}
+%  explain tRAG
+%}
-explain tRAG
-\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.
-Suppose the thread @{term th} is \emph{not} running in state @{term
+%  It is first shown that there is a path in the RAG leading from node
-"t @ s"}, meaning that it should be blocked by some other thread.
+%  @ {term th} to another thread @ {text "th'"}, which is also in the
-It is first shown that there is a path in the RAG leading from node
+%  @ {term readys}-set.  Since @ {term readys}-set is non-empty, there
-@{term th} to another thread @{text "th'"}, which is also in the
+%  must be one in it which holds the highest @ {term cp}-value, which,
-@{term readys}-set.  Since @{term readys}-set is non-empty, there
+%  by definition, is currently the @ {term running}-thread.  However, we
-must be one in it which holds the highest @{term cp}-value, which,
+%  are going to show in the next lemma slightly more: this running
-by definition, is currently the @{term running}-thread.  However, we
+%  thread is exactly @ {term "th'"}.
-are going to show in the next lemma slightly more: this running
-thread is exactly @{term "th'"}.
+%  \begin{lemma}
+%  There exists a thread @{text "th'"}
-\begin{lemma}
+%  such that @{thm (no_quants) th_blockedE_pretty}.
-There exists a thread @{text "th'"}
+%  \end{lemma}
-such that @{thm (no_quants) th_blockedE_pretty}.
-\end{lemma}
+%  \begin{proof}
+%  We know that @{term th} cannot be in @{term readys}, because it has
-\begin{proof}
+%  the highest precedence and therefore must be running. This violates our
-We know that @{term th} cannot be in @{term readys}, because it has
+%  assumption. So by ?? we have that there must be a @{term "th'"} such that
-the highest precedence and therefore must be running. This violates our
+%  @{term "th' \<in> readys (t @ s)"} and @{term "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+"}.
-assumption. So by ?? we have that there must be a @{term "th'"} such that
+%  We are going to first show that this @{term "th'"} must be running. For this we
-@{term "th' \<in> readys (t @ s)"} and @{term "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+"}.
+%  need to show that @{term th'} holds the highest @{term cp}-value.
-We are going to first show that this @{term "th'"} must be running. For this we
+%  By ?? we know that the @{term "cp"}-value of @{term "th'"} must
-need to show that @{term th'} holds the highest @{term cp}-value.
+%  be the highest all precedences of all thread nodes in its @{term tRAG}-subtree.
-By ?? we know that the @{term "cp"}-value of @{term "th'"} must
+%  That is
-be the highest all precedences of all thread nodes in its @{term tRAG}-subtree.
-That is
+%  \begin{center}
+%  @ {term "cp (t @ s) th' = Max (the_preced (t @ s) `
-\begin{center}
+%    (the_thread ` subtree (tRAG (t @ s)) (Th th')))"}
-@{term "cp (t @ s) th' = Max (the_preced (t @ s) `
+%  \end{center}
-(the_thread ` subtree (tRAG (t @ s)) (Th th')))"}
-\end{center}
+%  But since @{term th} is in this subtree the right-hand side is equal
+%  to @{term "preced th (t @ s)"}.
-But since @{term th} is in this subtree the right-hand side is equal
-to @{term "preced th (t @ s)"}.
 %Let me distinguish between cp (current precedence) and assigned precedence (the precedence the
 %thread ``normally'' has).
 %So we want to show what the cp of th' is in state t @ s.
 %We look at all the assingned precedences in the subgraph starting from th'
 %so cp of th' in t @ s has this (assigned) precedence of th
 %We know that cp (t @ s) th'
 %is the Maximum of the threads in the subgraph starting from th'
 %this happens to be the precedence of th
 %th has the highest precedence of all threads
-\end{proof}
+%  \end{proof}
-\begin{corollary}
+%  \begin{corollary}
-Using the lemma \ref{runninginversion} we can say more about the thread th'
+%  Using the lemma \ref{runninginversion} we can say more about the thread th'
-\end{corollary}
+%  \end{corollary}
-\endnote{\subsection*{END OUTLINE}}
+%  \endnote{\subsection*{END OUTLINE}}
-In what follows we will describe properties of PIP that allow us to prove
+%  In what follows we will describe properties of PIP that allow us to prove
-Theorem~\ref{mainthm} and, when instructive, briefly describe our argument.
+%  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{isabelle}\ \ \ \ \ %%%
-\begin{tabular}{@ {}l}
+%  \begin{tabular}{@ {}l}
-@{text "running s \<subseteq> ready s \<subseteq> threads s"}\\
+%  @ {text "running s \<subseteq> ready s \<subseteq> threads s"}\\
-@{thm[mode=IfThen]  finite_threads}
+%  @ {thm[mode=IfThen]  finite_threads}
-\end{tabular}
+%  \end{tabular}
-\end{isabelle}
+%  \end{isabelle}
-\noindent
+%  \noindent
-The second property is by induction on @{term vt}. The next three
+%  The second property is by induction on @{term vt}. The next three
-properties are:
+%  properties are:
-\begin{isabelle}\ \ \ \ \ %%%
+%  \begin{isabelle}\ \ \ \ \ %%%
-\begin{tabular}{@ {}l}
+%  \begin{tabular}{@ {}l}
-HERE??
+%  HERE??
 %@ {thm[mode=IfThen] waiting_unique[of _ _ "cs1" "cs2"]}\\
 %@ {thm[mode=IfThen] held_unique[of _ "th1" _ "th2"]}\\
 %@ {thm[mode=IfThen] running_unique[of _ "th1" "th2"]}
-\end{tabular}
+%  \end{tabular}
-\end{isabelle}
+%  \end{isabelle}
-\noindent
+%  \noindent
-The first property states that every waiting thread can only wait for a single
+%  The first property states that every waiting thread can only wait for a single
-resource (because it gets suspended after requesting that resource); the second
+%  resource (because it gets suspended after requesting that resource); the second
-that every resource can only be held by a single thread;
+%  that every resource can only be held by a single thread;
-the third property establishes that in every given valid state, there is
+%  the third property establishes that in every given valid state, there is
-at most one running thread. We can also show the following properties
+%  at most one running thread. We can also show the following properties
-about the @{term RAG} in @{text "s"}.
+%  about the @{term RAG} in @{text "s"}.
-\begin{isabelle}\ \ \ \ \ %%%
+%  \begin{isabelle}\ \ \ \ \ %%%
-\begin{tabular}{@ {}l}
+%  \begin{tabular}{@ {}l}
-HERE?? %@{text If}~@ {thm (prem 1) acyclic_RAG}~@{text "then"}:\\
+%  HERE?? %@{text If}~@ {thm (prem 1) acyclic_RAG}~@{text "then"}:\\
-\hspace{5mm}@{thm (concl) acyclic_RAG},
+%  \hspace{5mm}@{thm (concl) acyclic_RAG},
-@{thm (concl) finite_RAG} and
+%  @{thm (concl) finite_RAG} and
-%@ {thm (concl) wf_dep_converse},\\
+%  %@ {thm (concl) wf_dep_converse},\\
-%\hspace{5mm}@{text "if"}~@ {thm (prem 2) dm_RAG_threads}~@{text "then"}~@{thm (concl) dm_RAG_threads}
+%  %\hspace{5mm}@{text "if"}~@ {thm (prem 2) dm_RAG_threads}~@{text "then"}~@{thm (concl) dm_RAG_threads}
-and\\
+%  and\\
-%\hspace{5mm}@{text "if"}~@ {thm (prem 2) range_in}~@{text "then"}~% @ {thm (concl) range_in}.
+%  %\hspace{5mm}@{text "if"}~@ {thm (prem 2) range_in}~@{text "then"}~% @ {thm (concl) range_in}.
-\end{tabular}
+%  \end{tabular}
-\end{isabelle}
+%  \end{isabelle}
-\noindent
+%  \noindent
-The acyclicity property follows from how we restricted the events in
+%  The acyclicity property follows from how we restricted the events in
-@{text step}; similarly the finiteness and well-foundedness property.
+%  @{text step}; similarly the finiteness and well-foundedness property.
-The last two properties establish that every thread in a @{text "RAG"}
+%  The last two properties establish that every thread in a @{text "RAG"}
-(either holding or waiting for a resource) is a live thread.
+%  (either holding or waiting for a resource) is a live thread.
-The key lemma in our proof of Theorem~\ref{mainthm} is as follows:
+%  The key lemma in our proof of Theorem~\ref{mainthm} is as follows:
-\begin{lemma}\label{mainlem}
+%  \begin{lemma}\label{mainlem}
-Given the assumptions about states @{text "s"} and @{text "s' @ s"},
+%  Given the assumptions about states @{text "s"} and @{text "s' @ s"},
-the thread @{text th} and the events in @{text "s'"},
+%  the thread @{text th} and the events in @{text "s'"},
-if @{term "th' \<in> threads (s' @ s)"}, @{text "th' \<noteq> th"} and @{text "detached (s' @ s) th'"}\\
+%  if @{term "th' \<in> threads (s' @ s)"}, @{text "th' \<noteq> th"} and @{text "detached (s' @ s) th'"}\\
-then @{text "th' \<notin> running (s' @ s)"}.
+%  then @{text "th' \<notin> running (s' @ s)"}.
-\end{lemma}
+%  \end{lemma}
-\noindent
+%  \noindent
-The point of this lemma is that a thread different from @{text th} (which has the highest
+%  The point of this lemma is that a thread different from @{text th} (which has the highest
-precedence in @{text s}) and not holding any resource, cannot be running
+%  precedence in @{text s}) and not holding any resource, cannot be running
-in the state @{text "s' @ s"}.
+%  in the state @{text "s' @ s"}.
-\begin{proof}
+%  \begin{proof}
-Since thread @{text "th'"} does not hold any resource, no thread can depend on it.
+%  Since thread @{text "th'"} does not hold any resource, no thread can depend on it.
-Therefore its current precedence @{term "cp (s' @ s) th'"} equals its own precedence
+%  Therefore its current precedence @{term "cp (s' @ s) th'"} equals its own precedence
-@{term "prec th' (s' @ s)"}. Since @{text "th"} has the highest precedence in the
+%  @{term "prec th' (s' @ s)"}. Since @{text "th"} has the highest precedence in the
-state @{text "(s' @ s)"} and precedences are distinct among threads, we have
+%  state @{text "(s' @ s)"} and precedences are distinct among threads, we have
-@{term "prec th' (s' @s ) < prec th (s' @ s)"}. From this
+%  @{term "prec th' (s' @s ) < prec th (s' @ s)"}. From this
-we have @{term "cp (s' @ s) th' < prec th (s' @ s)"}.
+%  we have @{term "cp (s' @ s) th' < prec th (s' @ s)"}.
-Since @{text "prec th (s' @ s)"} is already the highest
+%  Since @{text "prec th (s' @ s)"} is already the highest
-@{term "cp (s' @ s) th"} can not be higher than this and can not be lower either (by
+%  @{term "cp (s' @ s) th"} can not be higher than this and can not be lower either (by
-definition of @{term "cp"}). Consequently, we have @{term "prec th (s' @ s) = cp (s' @ s) th"}.
+%  definition of @{term "cp"}). Consequently, we have @{term "prec th (s' @ s) = cp (s' @ s) th"}.
-Finally we have @{term "cp (s' @ s) th' < cp (s' @ s) th"}.
+%  Finally we have @{term "cp (s' @ s) th' < cp (s' @ s) th"}.
-By defintion of @{text "running"}, @{text "th'"} can not be running in state
+%  By defintion of @{text "running"}, @{text "th'"} can not be running in state
-@{text "s' @ s"}, as we had to show.\qed
+%  @{text "s' @ s"}, as we had to show.\qed
-\end{proof}
+%  \end{proof}
-\noindent
+%  \noindent
-Since @{text "th'"} is not able to run in state @{text "s' @ s"}, it is not able to
+%  Since @{text "th'"} is not able to run in state @{text "s' @ s"}, it is not able to
-issue a @{text "P"} or @{text "V"} event. Therefore if @{text "s' @ s"} is extended
+%  issue a @{text "P"} or @{text "V"} event. Therefore if @{text "s' @ s"} is extended
-one step further, @{text "th'"} still cannot hold any resource. The situation will
+%  one step further, @{text "th'"} still cannot hold any resource. The situation will
-not change in further extensions as long as @{text "th"} holds the highest precedence.
+%  not change in further extensions as long as @{text "th"} holds the highest precedence.
-From this lemma we can deduce Theorem~\ref{mainthm}: that @{text th} can only be
+%  From this lemma we can deduce Theorem~\ref{mainthm}: that @{text th} can only be
-blocked by a thread @{text th'} that
+%  blocked by a thread @{text th'} that
-held some resource in state @{text s} (that is not @{text "detached"}). And furthermore
+%  held some resource in state @{text s} (that is not @{text "detached"}). And furthermore
-that the current precedence of @{text th'} in state @{text "(s' @ s)"} must be equal to the
+%  that the current precedence of @{text th'} in state @{text "(s' @ s)"} must be equal to the
-precedence of @{text th} in @{text "s"}.
+%  precedence of @{text th} in @{text "s"}.
-We show this theorem by induction on @{text "s'"} using Lemma~\ref{mainlem}.
+%  We show this theorem by induction on @{text "s'"} using Lemma~\ref{mainlem}.
-This theorem gives a stricter bound on the threads that can block @{text th} than the
+%  This theorem gives a stricter bound on the threads that can block @{text th} than the
-one obtained by Sha et al.~\cite{Sha90}:
+%  one obtained by Sha et al.~\cite{Sha90}:
-only threads that were alive in state @{text s} and moreover held a resource.
+%  only threads that were alive in state @{text s} and moreover held a resource.
-This means our bound is in terms of both---alive threads in state @{text s}
+%  This means our bound is in terms of both---alive threads in state @{text s}
-and number of critical resources. Finally, the theorem establishes that the blocking threads have the
+%  and number of critical resources. Finally, the theorem establishes that the blocking threads have the
-current precedence raised to the precedence of @{text th}.
+%  current precedence raised to the precedence of @{text th}.
-We can furthermore prove that under our assumptions no deadlock exists in the state @{text "s' @ s"}
+%  We can furthermore prove that under our assumptions no deadlock exists in the state @{text "s' @ s"}
-by showing that @{text "running (s' @ s)"} is not empty.
+%  by showing that @{text "running (s' @ s)"} is not empty.
-\begin{lemma}
+%  \begin{lemma}
-Given the assumptions about states @{text "s"} and @{text "s' @ s"},
+%  Given the assumptions about states @{text "s"} and @{text "s' @ s"},
-the thread @{text th} and the events in @{text "s'"},
+%  the thread @{text th} and the events in @{text "s'"},
-@{term "running (s' @ s) \<noteq> {}"}.
+%  @{term "running (s' @ s) \<noteq> {}"}.
-\end{lemma}
+%  \end{lemma}
-\begin{proof}
+%  \begin{proof}
-If @{text th} is blocked, then by following its dependants graph, we can always
+%  If @{text th} is blocked, then by following its dependants graph, we can always
-reach a ready thread @{text th'}, and that thread must have inherited the
+%  reach a ready thread @{text th'}, and that thread must have inherited the
-precedence of @{text th}.\qed
+%  precedence of @{text th}.\qed
-\end{proof}
+%  \end{proof}
 %The following lemmas show how every node in RAG can be chased to ready threads:
 %\begin{enumerate}
 %\item Every node in RAG can be chased to a ready thread (@{text "chain_building"}):
 %Since there are only finite many threads live and holding some resource at any moment,
 %if every such thread can release all its resources in finite duration, then after finite
 %duration, none of them may block @{term "th"} anymore. So, no priority inversion may happen
 %then.
-NOTE: about bounds in sha et al and ours: they prove a bound on the length of individual
+% NOTE: about bounds in sha et al and ours: they prove a bound on the length of individual
-blocages. We prove a bound for the overall-blockage.
+% blocages. We prove a bound for the overall-blockage.
-There are low priority threads,
+% There are low priority threads,
-which do not hold any resources,
+% which do not hold any resources,
-such thread will not block th.
+% such thread will not block th.
-Their Theorem 3 does not exclude such threads.
+% Their Theorem 3 does not exclude such threads.
-There are resources, which are not held by any low prioirty threads,
+% There are resources, which are not held by any low prioirty threads,
-such resources can not cause blockage of th neither. And similiary,
+% such resources can not cause blockage of th neither. And similiary,
-theorem 6 does not exlude them.
+% theorem 6 does not exlude them.
-Our one bound excudle them by using a different formaulation. "
+% Our one bound excudle them by using a different formaulation. "
 *}
 (*<*)
 end
 (*>*)
-text {*
+(*text {*
 explan why Thm1 roughly corresponds to Sha's Thm 3
-*}
+*}*)
 section {* A Finite Bound on Priority Inversion *}
 (*<*)
 context extend_highest_gen

changeset 162	a8ceb68bfeb0
parent 161	f1d82f6c05a3
child 163	2ec13cfbb81c