pip: comparison Journal/Paper.thy

equal deleted inserted replaced

-:83da37e8b1d2
+:f1d82f6c05a3
 \end{isabelle}
 \noindent
 In this definition @{term "length s"} stands for the length of the list
 of events @{text s}. Again the default value in this function is @{text 0}
-for threads that have not been created yet. An actor of an event is
+for threads that have not been created yet. An \emph{actor} of an event is
 defined as
 \begin{isabelle}\ \ \ \ \ %%%
 \mbox{\begin{tabular}{lcl}
 @{thm (lhs) actor.simps(5)} & @{text "\<equiv>"} &
 @{thm (rhs) actor.simps(5)}\\
 @{thm (lhs) actor.simps(1)} & @{text "\<equiv>"} &
 @{thm (rhs) actor.simps(1)}\\
+@{thm (lhs) actor.simps(4)} & @{text "\<equiv>"} &
+@{thm (rhs) actor.simps(4)}\\
 @{thm (lhs) actor.simps(2)} & @{text "\<equiv>"} &
 @{thm (rhs) actor.simps(2)}\\
 @{thm (lhs) actor.simps(3)} & @{text "\<equiv>"} &
 @{thm (rhs) actor.simps(3)}\\
 \end{tabular}}
 \end{isabelle}
+\noindent
+This allows us to define what actions a set of threads @{text ths} might
+perform in a list of events @{text s}, namely
+@{thm actions_of_def[THEN eq_reflection]}.
 A \emph{precedence} of a thread @{text th} in a
 state @{text s} is the pair of natural numbers defined as
 \begin{isabelle}\ \ \ \ \ %%%
 @{thm preced_def}
 \noindent Note that forrests can have trees with infinte depth and
 containing nodes with infinitely many children.  A \emph{finite
 forrest} is a forrest which is well-founded and every node has
 finitely many children (is only finitely branching).
-\endnote{
+%\endnote{
-\begin{isabelle}\ \ \ \ \ %%%
-@{thm rtrancl_path.intros}
-\end{isabelle}
 %\begin{isabelle}\ \ \ \ \ %%%
-%@{thm rpath_def}
+%@ {thm rtrancl_path.intros}
+%\end{isabelle}
+%
+%\begin{isabelle}\ \ \ \ \ %%%
+%@ {thm rpath_def}
 %\end{isabelle}
-}
+%}
 %\endnote{{\bf Lemma about overlapping paths}}
 The locking mechanism of PIP ensures that for each thread node,
 resource is locked. So if the @{text "RAG"} is well-founded and
 finite, we can always start at a thread waiting for a resource and
 ``chase'' outgoing arrows leading to a single root of a tree.
 The use of relations for representing RAGs allows us to conveniently define
-the notion of the \emph{dependants} of a thread using the transitive closure
+the notion of the \emph{dependants} of a thread
-operation for relations, written ~@{term "trancl DUMMY"}. This gives
 \begin{isabelle}\ \ \ \ \ %%%
 @{thm dependants_raw_def}
 \end{isabelle}
 \begin{isabelle}\ \ \ \ \ %%%
 @{thm cpreced_def3}\hfill\numbered{cpreced}
 \end{isabelle}
-\endnote{
+%\endnote{
-\begin{isabelle}\ \ \ \ \ %%%
+%\begin{isabelle}\ \ \ \ \ %%%
-@{thm cp_alt_def cp_alt_def1}
+%@ {thm cp_alt_def cp_alt_def1}
-\end{isabelle}}
+%\end{isabelle}
+%}
 \noindent where the dependants of @{text th} are given by the
 waiting queue function.  While the precedence @{term prec} of any
 thread is determined statically (for example when the thread is
 created), the point of the current precedence is to dynamically
 \noindent
 This concludes the proof of Theorem 1.\qed
 \end{proof}
-\endnote{
+%\endnote{
-In what follows we will describe properties of PIP that allow us to
+%In what follows we will describe properties of PIP that allow us to
-prove Theorem~\ref{mainthm} and, when instructive, briefly describe
+%prove Theorem~\ref{mainthm} and, when instructive, briefly describe
-our argument. Recall we want to prove that in state @{term "s' @ s"}
+%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
+%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
+%"th'"} (@{term "th \<noteq> th'"}) which was alive in state @{term s}. We
-can show that
+%can show that
-\begin{lemma}
+%\begin{lemma}
-If @{thm (prem 2) eq_pv_blocked}
+%If @{thm (prem 2) eq_pv_blocked}
-then @{thm (concl) eq_pv_blocked}
+%then @{thm (concl) eq_pv_blocked}
-\end{lemma}
+%\end{lemma}
-\begin{lemma}
+%\begin{lemma}
-If @{thm (prem 2) eq_pv_persist}
+%If @{thm (prem 2) eq_pv_persist}
-then @{thm (concl) eq_pv_persist}
+%then @{thm (concl) eq_pv_persist}
-\end{lemma}}
+%\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
 Proof:
 Consider the states @{text "s upto t"}. It holds that all the states where
 @{text "th"} runs and all the states where @{text "th"} does not run is
-equalt to @{text "1 + len t"}. That means
+equalt to @{text "len t"}. That means
 \begin{center}
-@{text "states where th does not run = 1 + len t - states where th runs"} (*)
+@{text "states where th does not run = len t - states where th runs"} (*)
 \end{center}
 It also holds that all the actions of @{text "th"} are less or equal to
 the states where @{text th} runs. That is
 \end{center}
 That means in $(*)$ we have
 \begin{center}
-@{text "states where th does not run \<le> 1 + len t - len (actions_of {th} t)"}
+@{text "states where th does not run \<le> len t - len (actions_of {th} t)"}
 \end{center}
 If we look at all the events that can occur in @{text "s upto t"}, we have that
 \begin{center}

changeset 161	f1d82f6c05a3
parent 158	2bb3b65fc99f
child 162	a8ceb68bfeb0