--- a/Journal/Paper.thy Tue May 02 14:42:52 2017 +0100
+++ b/Journal/Paper.thy Thu May 04 15:21:18 2017 +0100
@@ -46,8 +46,10 @@
preced ("prec") and
preceds ("precs") and
cpreced ("cprec") and
+ cpreceds ("cprecs") and
wq_fun ("wq") and
- cprec_fun ("cp'_fun") and
+ cp ("cprec") and
+ (*cprec_fun ("cp_fun") and*)
holdents ("resources") and
DUMMY ("\<^raw:\mbox{$\_\!\_$}>") and
cntP ("c\<^bsub>P\<^esub>") and
@@ -667,7 +669,7 @@
threads, we deal correctly with the problem in the informal
algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is
lowered prematurely (see Introduction). We again introduce an abbreviation for current
- precedeces of a set of threads, written @{text "cpreceds wq s ths"}.
+ precedeces of a set of threads, written @{text "cprecs wq s ths"}.
\begin{isabelle}\ \ \ \ \ %%%
@{thm cpreceds_def}
@@ -1085,11 +1087,10 @@
the highest precedence in the state @{text s}, is either running in
state @{term "s' @ s"}, or can only be blocked in the state @{text
"s' @ s"} by a thread @{text th'} that already existed in @{text s}
- and requested a resource or had a lock on at least one resource---that means
+ and is waiting for a resource or had a lock on at least one resource---that means
the thread was not \emph{detached} in @{text s}. As we shall see
shortly, that means there are only finitely many threads that can
- block @{text th} in this way and then they need to run with the same
- precedence as @{text th}.
+ block @{text th} in this way.
%% HERE
@@ -1115,7 +1116,7 @@
that is
\begin{center}
- @{term "cp (t @ s) th' = Max (cp (t @ s) ` treads (t @ s))"}
+ @{term "cp (t @ s) th' = Max (cp (t @ s) ` threads (t @ s))"}
\end{center}
\noindent
@@ -1143,13 +1144,14 @@
@{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
+ @{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
+ means @{text "th'"} will not run as long as @{text "th"} is a live
+ thread. In turn this means @{text "th'"} cannot take any action in
+ state @{text "s' @ s"} to change its current status; therefore
+ @{text "th'"} 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}
@@ -1176,85 +1178,87 @@
%\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
+
+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_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}}
+ \begin{lemma}
+ If @{thm (prem 2) eq_pv_persist}
+ then @{thm (concl) eq_pv_persist}
+ \end{lemma}
+ %%%}
% \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'".
+ in other words
+ th -> cs1 -> th1 -> cs2 -> th2 -> ... -> csn -> thn -> cs -> th'.
+
+ We says that th is blocked by @{text "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
+ THEN
- %@ {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
- % @{term "th'"} which blocks @{term th}, we need to know more about it.
- % To see what kind of thread can block @{term th}.
+ 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}.
- % From these two lemmas we can see the correctness of PIP, which is
- % that: the blockage of th is reasonable and under control.
+ 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:
+ Lemmas we want to describe:
- % \begin{lemma}
- % @ {thm running_cntP_cntV_inv}
- % \end{lemma}
+ \begin{lemma}
+ @{thm running_cntP_cntV_inv}
+ \end{lemma}
-% \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}.
+ \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}
+ \begin{lemma}\label{runninginversion}
+ @{thm running_inversion}
+ \end{lemma}
-% explain tRAG
+ explain tRAG
%}