
diff -r f1d82f6c05a3 -r a8ceb68bfeb0 Journal/Paper.thy
--- 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 *}
 




