pip: comparison Journal/Paper.thy

equal deleted inserted replaced

-:f73b7f339314
+:6cfafcb41a3d
 Cs ("C") and
 readys ("ready") and
 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
 cntV ("c\<^bsub>V\<^esub>")
 of @{text th} in the state @{text s}. Since the notion @{term
 "dependants"} is defined as the transitive closure of all dependent
 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}
 \end{isabelle}
 \noindent This theorem ensures that the thread @{text th}, which has
 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
+block @{text th} in this way.
-precedence as @{text th}.
 %% HERE
 Given our assumptions (on @{text th}), the first property we can
 \noindent
 We also know that this is equal to the maximum of current precedences of all threads,
 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
 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
 \begin{proof} Let us assume @{text "th'"} is detached in state
 @{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
+means @{text "th'"} will not run as long as @{text "th"} is a live
-live thread. In turn this means @{text "th'"} cannot acquire a reseource
+thread. In turn this means @{text "th'"} cannot take any action in
-and is still detached in state @{text "s' @ s"}.  Consequently
+state @{text "s' @ s"} to change its current status; therefore
-@{text "th'"} is also not boosted in state @{text "s' @ s"} and
+@{text "th'"} is still detached in state @{text "s' @ s"}.
-would not run. This contradicts our assumption.\qed
+Consequently @{text "th'"} is also not boosted in state @{text "s' @
+s"} and 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
 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
+In what follows we will describe properties of PIP that allow us to
-%our argument. Recall we want to prove that in state @ {term "s' @ s"}
+prove Theorem~\ref{mainthm} and, when instructive, briefly describe
-%either @{term th} is either running or blocked by a thread @ {term
+our argument. Recall we want to prove that in state @ {term "s' @ s"}
-%"th'"} (@{term "th \<noteq> th'"}) which was alive in state @{term s}. We
+either @{term th} is either running or blocked by a thread @
-%can show that
+{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}
+\begin{lemma}
-%then @{thm (concl) eq_pv_blocked}
+If @{thm (prem 2) eq_pv_blocked}
-%\end{lemma}
+then @{thm (concl) eq_pv_blocked}
+\end{lemma}
-%\begin{lemma}
-%If @{thm (prem 2) eq_pv_persist}
+\begin{lemma}
-%then @{thm (concl) eq_pv_persist}
+If @{thm (prem 2) eq_pv_persist}
-%\end{lemma}}
+then @{thm (concl) eq_pv_persist}
+\end{lemma}
+%%%}
 %  \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
+in other words
-%%% th -> cs1 -> th1 -> cs2 -> th2 -> ... -> csn -> thn -> cs -> th'.
+th -> cs1 -> th1 -> cs2 -> th2 -> ... -> csn -> thn -> cs -> th'.
-%%%
-%%% We says that th is blocked by "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 [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
+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
+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}
+\begin{lemma}
-% @ {thm running_cntP_cntV_inv}
+@{thm running_cntP_cntV_inv}
-% \end{lemma}
+\end{lemma}
-%  \noindent
+\noindent
-%  Remember we do not have the well-nestedness restriction in our
+Remember we do not have the well-nestedness restriction in our
-%  proof, which means the difference between the counters @{const cntV}
+proof, which means the difference between the counters @{const cntV}
-%  and @{const cntP} can be larger than @{term 1}.
+and @{const cntP} can be larger than @{term 1}.
-%  \begin{lemma}\label{runninginversion}
+\begin{lemma}\label{runninginversion}
-%  @ {thm running_inversion}
+@{thm running_inversion}
-%  \end{lemma}
+\end{lemma}
-%  explain tRAG
+explain tRAG
 %}
 %  Suppose the thread @ {term th} is \emph{not} running in state @ {term
 %  "t @ s"}, meaning that it should be blocked by some other thread.

changeset 166	6cfafcb41a3d
parent 165	f73b7f339314
child 167	045371bde100