--- a/Journal/Paper.thy Tue Apr 25 14:05:57 2017 +0100
+++ b/Journal/Paper.thy Tue Apr 25 16:23:46 2017 +0100
@@ -909,7 +909,8 @@
(*<*)
context valid_trace
begin
-(*>*)
+ (*>*)
+(*<*)
text {*
\endnote{In this section we prove facts that immediately follow from
@@ -951,6 +952,7 @@
\end{proof}}
*}
+(*>*)
(*<*)end(*>*)
section {* The Correctness Proof *}
@@ -1184,105 +1186,103 @@
%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
- blocked, people want to know why and wether this blocking is
- reasonable.
+% Since @{term "th"} is the most urgent thread, if it is somehow
+% blocked, people want to know why and wether this blocking is
+% 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
- @{term "th"} to @{term "th'"}, which means:
- there is a chain of demand leading from @{term th} to @{term th'}.
+% if @{term "th"} is blocked, then there is a path leading from
+% @{term "th"} to @{term "th'"}, which means:
+% 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 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}
+
+% THENTHEN
+
+ %@ {thm [source] running_inversion_4} @ {thm running_inversion_4}
- THENTHEN
+ % 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.
+ % To see what kind of thread can block @{term th}.
- (here) %@ {thm [source] running_inversion_4} @ {thm running_inversion_4}
+ % From these two lemmas we can see the correctness of PIP, which is
+ % that: the blockage of th is reasonable and under control.
+
+ % Lemmas we want to describe:
- 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.
- To see what kind of thread can block @{term th}.
+ % \begin{lemma}
+ % @ {thm running_cntP_cntV_inv}
+ % \end{lemma}
- From these two lemmas we can see the correctness of PIP, which is
- that: the blockage of th is reasonable and under control.
+% \noindent
+% Remember we do not have the well-nestedness restriction in our
+% proof, which means the difference between the counters @{const cntV}
+% and @{const cntP} can be larger than @{term 1}.
- Lemmas we want to describe:
+% \begin{lemma}\label{runninginversion}
+% @ {thm running_inversion}
+% \end{lemma}
+
+% explain tRAG
+%}
-
- \begin{lemma}
- @{thm running_cntP_cntV_inv}
- \end{lemma}
+% 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
+% @ {term th} to another thread @ {text "th'"}, which is also in the
+% @ {term readys}-set. Since @ {term readys}-set is non-empty, there
+% must be one in it which holds the highest @ {term cp}-value, which,
+% by definition, is currently the @ {term running}-thread. However, we
+% are going to show in the next lemma slightly more: this running
+% thread is exactly @ {term "th'"}.
- \noindent
- Remember we do not have the well-nestedness restriction in our
- 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}
- \end{lemma}
-
- explain tRAG
- \bigskip}
+% \begin{lemma}
+% There exists a thread @{text "th'"}
+% such that @{thm (no_quants) th_blockedE_pretty}.
+% \end{lemma}
-
- 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
- @{term th} to another thread @{text "th'"}, which is also in the
- @{term readys}-set. Since @{term readys}-set is non-empty, there
- must be one in it which holds the highest @{term cp}-value, which,
- by definition, is currently the @{term running}-thread. However, we
- 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'"}
- 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
+% the highest precedence and therefore must be running. This violates our
+% assumption. So by ?? we have that there must be a @{term "th'"} such that
+% @{term "th' \<in> readys (t @ s)"} and @{term "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+"}.
+% We are going to first show that this @{term "th'"} must be running. For this we
+% need to show that @{term th'} holds the highest @{term cp}-value.
+% By ?? we know that the @{term "cp"}-value of @{term "th'"} must
+% be the highest all precedences of all thread nodes in its @{term tRAG}-subtree.
+% That is
- \begin{proof}
- We know that @{term th} cannot be in @{term readys}, because it has
- the highest precedence and therefore must be running. This violates our
- assumption. So by ?? we have that there must be a @{term "th'"} such that
- @{term "th' \<in> readys (t @ s)"} and @{term "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+"}.
- We are going to first show that this @{term "th'"} must be running. For this we
- need to show that @{term th'} holds the highest @{term cp}-value.
- By ?? we know that the @{term "cp"}-value of @{term "th'"} must
- 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) `
+% (the_thread ` subtree (tRAG (t @ s)) (Th th')))"}
+% \end{center}
- \begin{center}
- @{term "cp (t @ s) th' = Max (the_preced (t @ s) `
- (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).
@@ -1295,126 +1295,126 @@
%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}
- Using the lemma \ref{runninginversion} we can say more about the thread th'
- \end{corollary}
+% \begin{corollary}
+% Using the lemma \ref{runninginversion} we can say more about the thread th'
+% \end{corollary}
- \endnote{\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:
+% 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:
- \begin{isabelle}\ \ \ \ \ %%%
- \begin{tabular}{@ {}l}
- @{text "running s \<subseteq> ready s \<subseteq> threads s"}\\
- @{thm[mode=IfThen] finite_threads}
- \end{tabular}
- \end{isabelle}
+% \begin{isabelle}\ \ \ \ \ %%%
+% \begin{tabular}{@ {}l}
+% @ {text "running s \<subseteq> ready s \<subseteq> threads s"}\\
+% @ {thm[mode=IfThen] finite_threads}
+% \end{tabular}
+% \end{isabelle}
- \noindent
- The second property is by induction on @{term vt}. The next three
- properties are:
+% \noindent
+% The second property is by induction on @{term vt}. The next three
+% properties are:
- \begin{isabelle}\ \ \ \ \ %%%
- \begin{tabular}{@ {}l}
- HERE??
+% \begin{isabelle}\ \ \ \ \ %%%
+% \begin{tabular}{@ {}l}
+% 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{isabelle}
+% \end{tabular}
+% \end{isabelle}
- \noindent
- 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
- that every resource can only be held by a single thread;
- the third property establishes that in every given valid state, there is
- at most one running thread. We can also show the following properties
- about the @{term RAG} in @{text "s"}.
+% \noindent
+% 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
+% that every resource can only be held by a single thread;
+% the third property establishes that in every given valid state, there is
+% at most one running thread. We can also show the following properties
+% about the @{term RAG} in @{text "s"}.
- \begin{isabelle}\ \ \ \ \ %%%
- \begin{tabular}{@ {}l}
- HERE?? %@{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_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}
- \end{isabelle}
+% \begin{isabelle}\ \ \ \ \ %%%
+% \begin{tabular}{@ {}l}
+% HERE?? %@{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_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}
+% \end{isabelle}
- \noindent
- The acyclicity property follows from how we restricted the events in
- @{text step}; similarly the finiteness and well-foundedness property.
- The last two properties establish that every thread in a @{text "RAG"}
- (either holding or waiting for a resource) is a live thread.
+% \noindent
+% The acyclicity property follows from how we restricted the events in
+% @{text step}; similarly the finiteness and well-foundedness property.
+% The last two properties establish that every thread in a @{text "RAG"}
+% (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}
- Given the assumptions about states @{text "s"} and @{text "s' @ 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'"}\\
- then @{text "th' \<notin> running (s' @ s)"}.
- \end{lemma}
+% \begin{lemma}\label{mainlem}
+% Given the assumptions about states @{text "s"} and @{text "s' @ 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'"}\\
+% then @{text "th' \<notin> running (s' @ s)"}.
+% \end{lemma}
- \noindent
- 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
- in the state @{text "s' @ s"}.
+% \noindent
+% 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
+% in the state @{text "s' @ s"}.
- \begin{proof}
- 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
- @{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
- @{term "prec th' (s' @s ) < prec th (s' @ s)"}. From this
- we have @{term "cp (s' @ s) th' < prec th (s' @ s)"}.
- 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
- 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"}.
- By defintion of @{text "running"}, @{text "th'"} can not be running in state
- @{text "s' @ s"}, as we had to show.\qed
- \end{proof}
+% \begin{proof}
+% 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
+% @{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
+% @{term "prec th' (s' @s ) < prec th (s' @ s)"}. From this
+% we have @{term "cp (s' @ s) th' < prec th (s' @ s)"}.
+% 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
+% 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"}.
+% By defintion of @{text "running"}, @{text "th'"} can not be running in state
+% @{text "s' @ s"}, as we had to show.\qed
+% \end{proof}
- \noindent
- 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
- 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.
+% \noindent
+% 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
+% 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.
- From this lemma we can deduce Theorem~\ref{mainthm}: that @{text th} can only be
- blocked by a thread @{text th'} that
- 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
- precedence of @{text th} in @{text "s"}.
- 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
- one obtained by Sha et al.~\cite{Sha90}:
- 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}
- and number of critical resources. Finally, the theorem establishes that the blocking threads have the
- current precedence raised to the precedence of @{text th}.
+% From this lemma we can deduce Theorem~\ref{mainthm}: that @{text th} can only be
+% blocked by a thread @{text th'} that
+% 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
+% precedence of @{text th} in @{text "s"}.
+% 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
+% one obtained by Sha et al.~\cite{Sha90}:
+% 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}
+% and number of critical resources. Finally, the theorem establishes that the blocking threads have the
+% 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"}
- by showing that @{text "running (s' @ s)"} is not empty.
+% 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.
- \begin{lemma}
- Given the assumptions about states @{text "s"} and @{text "s' @ s"},
- the thread @{text th} and the events in @{text "s'"},
- @{term "running (s' @ s) \<noteq> {}"}.
- \end{lemma}
+% \begin{lemma}
+% Given the assumptions about states @{text "s"} and @{text "s' @ s"},
+% the thread @{text th} and the events in @{text "s'"},
+% @{term "running (s' @ s) \<noteq> {}"}.
+% \end{lemma}
- \begin{proof}
- 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
- precedence of @{text th}.\qed
- \end{proof}
+% \begin{proof}
+% 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
+% precedence of @{text th}.\qed
+% \end{proof}
%The following lemmas show how every node in RAG can be chased to ready threads:
@@ -1523,28 +1523,28 @@
%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
- blocages. We prove a bound for the overall-blockage.
+ % 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.
- There are low priority threads,
- which do not hold any resources,
- such thread will not block th.
- Their Theorem 3 does not exclude such threads.
+ % There are low priority threads,
+ % which do not hold any resources,
+ % such thread will not block th.
+ % Their Theorem 3 does not exclude such threads.
- There are resources, which are not held by any low prioirty threads,
- such resources can not cause blockage of th neither. And similiary,
- theorem 6 does not exlude them.
+ % There are resources, which are not held by any low prioirty threads,
+ % such resources can not cause blockage of th neither. And similiary,
+ % 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 *}