pip: comparison Journal/Paper.thy

equal deleted inserted replaced

-:a88af0e4731f
+:38c6acf03f68
 notation (latex output)
 Cons ("_::_" [78,77] 73) and
 If  ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
 vt ("valid'_state") and
-runing ("running") and
 Prc ("'(_, _')") and
-holding ("holds") and
+holding_raw ("holds") and
-waiting ("waits") and
+holding ("Holds") and
+waiting_raw ("waits") and
+waiting ("Waits") and
+dependants_raw ("dependants") and
+dependants ("Dependants") and
 Th ("T") and
 Cs ("C") and
 readys ("ready") and
 preced ("prec") and
-(*  preceds ("precs") and*)
+preceds ("precs") and
 cpreced ("cprec") and
 cp ("cprec") and
 holdents ("resources") and
 DUMMY  ("\<^raw:\mbox{$\_\!\_$}>") and
 cntP ("c\<^bsub>P\<^esub>") and
 \begin{isabelle}\ \ \ \ \ %%%
 \mbox{\begin{tabular}{lcl}
 @{thm (lhs) threads.simps(1)} & @{text "\<equiv>"} &
 @{thm (rhs) threads.simps(1)}\\
-@{thm (lhs) threads.simps(2)[where thread="th"]} & @{text "\<equiv>"} &
+@{thm (lhs) threads.simps(2)} & @{text "\<equiv>"} &
-@{thm (rhs) threads.simps(2)[where thread="th"]}\\
+@{thm (rhs) threads.simps(2)}\\
-@{thm (lhs) threads.simps(3)[where thread="th"]} & @{text "\<equiv>"} &
+@{thm (lhs) threads.simps(3)} & @{text "\<equiv>"} &
-@{thm (rhs) threads.simps(3)[where thread="th"]}\\
+@{thm (rhs) threads.simps(3)}\\
 @{term "threads (DUMMY#s)"} & @{text "\<equiv>"} & @{term "threads s"}\\
 \end{tabular}}
 \end{isabelle}
 \noindent
 Another function calculates the priority for a thread @{text "th"}, which is
 defined as
 \begin{isabelle}\ \ \ \ \ %%%
 \mbox{\begin{tabular}{lcl}
-@{thm (lhs) priority.simps(1)[where thread="th"]} & @{text "\<equiv>"} &
+@{thm (lhs) priority.simps(1)} & @{text "\<equiv>"} &
-@{thm (rhs) priority.simps(1)[where thread="th"]}\\
+@{thm (rhs) priority.simps(1)}\\
-@{thm (lhs) priority.simps(2)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} &
+@{thm (lhs) priority.simps(2)} & @{text "\<equiv>"} &
-@{thm (rhs) priority.simps(2)[where thread="th" and thread'="th'"]}\\
+@{thm (rhs) priority.simps(2)}\\
-@{thm (lhs) priority.simps(3)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} &
+@{thm (lhs) priority.simps(3)} & @{text "\<equiv>"} &
-@{thm (rhs) priority.simps(3)[where thread="th" and thread'="th'"]}\\
+@{thm (rhs) priority.simps(3)}\\
 @{term "priority th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "priority th s"}\\
 \end{tabular}}
 \end{isabelle}
 \noindent
 calculates the ``time'', or index, at which time a thread had its
 priority last set.
 \begin{isabelle}\ \ \ \ \ %%%
 \mbox{\begin{tabular}{lcl}
-@{thm (lhs) last_set.simps(1)[where thread="th"]} & @{text "\<equiv>"} &
+@{thm (lhs) last_set.simps(1)} & @{text "\<equiv>"} &
-@{thm (rhs) last_set.simps(1)[where thread="th"]}\\
+@{thm (rhs) last_set.simps(1)}\\
-@{thm (lhs) last_set.simps(2)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} &
+@{thm (lhs) last_set.simps(2)} & @{text "\<equiv>"} &
-@{thm (rhs) last_set.simps(2)[where thread="th" and thread'="th'"]}\\
+@{thm (rhs) last_set.simps(2)}\\
-@{thm (lhs) last_set.simps(3)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} &
+@{thm (lhs) last_set.simps(3)} & @{text "\<equiv>"} &
-@{thm (rhs) last_set.simps(3)[where thread="th" and thread'="th'"]}\\
+@{thm (rhs) last_set.simps(3)}\\
 @{term "last_set th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "last_set th s"}\\
 \end{tabular}}
 \end{isabelle}
 \noindent
 of events @{text s}. Again the default value in this function is @{text 0}
 for threads that have not been created yet. 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[where thread="th"]}
+@{thm preced_def}
 \end{isabelle}
 \noindent
 We also use the abbreviation
 \begin{isabelle}\ \ \ \ \ %%%
-???preceds s ths
+@{thm preceds_def}
 \end{isabelle}
 \noindent
 for the set of precedences of threads @{text ths} in state @{text s}.
 The point of precedences is to schedule threads not according to priorities (because what should
 when a thread \emph{holds}, respectively \emph{waits} for, a
 resource @{text cs} given a waiting queue function @{text wq}.
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
-@{thm cs_holding_raw[where thread="th"]}\\
+@{thm holding_raw_def[where thread="th"]}\\
-@{thm cs_waiting_raw[where thread="th"]}
+@{thm waiting_raw_def[where thread="th"]}
 \end{tabular}
 \end{isabelle}
 \noindent
 In this definition we assume @{text "set"} converts a list into a set.
 \begin{isabelle}\ \ \ \ \ %%%
 @{abbrev all_unlocked}\hfill\numbered{allunlocked}
 \end{isabelle}
 \noindent
-Using @{term "holding"} and @{term waiting}, we can introduce \emph{Resource Allocation Graphs}
+Using @{term "holding_raw"} and @{term waiting_raw}, we can introduce \emph{Resource Allocation Graphs}
 (RAG), which represent the dependencies between threads and resources.
 We represent RAGs as relations using pairs of the form
 \begin{isabelle}\ \ \ \ \ %%%
 @{term "(Th th, Cs cs)"} \hspace{5mm}{\rm and}\hspace{5mm}
 \emph{holding edge} (@{term Cs} and @{term Th} are constructors of a
 datatype for vertices). Given a waiting queue function, a RAG is defined
 as the union of the sets of waiting and holding edges, namely
 \begin{isabelle}\ \ \ \ \ %%%
-@{thm cs_RAG_raw}
+@{thm RAG_raw_def}
 \end{isabelle}
 \begin{figure}[t]
 \begin{center}
 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
 operation for relations, written ~@{term "trancl DUMMY"}. This gives
 \begin{isabelle}\ \ \ \ \ %%%
-@{thm cs_dependants_def}
+@{thm dependants_raw_def}
 \end{isabelle}
-\noindent
+\noindent This definition needs to account for all threads that wait
-This definition needs to account for all threads that wait for a thread to
+for a thread to release a resource. This means we need to include
-release a resource. This means we need to include threads that transitively
+threads that transitively wait for a resource to be released (in the
-wait for a resource to be released (in the picture above this means the dependants
+picture above this means the dependants of @{text "th\<^sub>0"} are
-of @{text "th\<^sub>0"} are @{text "th\<^sub>1"} and @{text "th\<^sub>2"}, which wait for resource @{text "cs\<^sub>1"},
+@{text "th\<^sub>1"} and @{text "th\<^sub>2"}, which wait for
-but also @{text "th\<^sub>3"},
+resource @{text "cs\<^sub>1"}, but also @{text "th\<^sub>3"}, which
-which cannot make any progress unless @{text "th\<^sub>2"} makes progress, which
+cannot make any progress unless @{text "th\<^sub>2"} makes progress,
-in turn needs to wait for @{text "th\<^sub>0"} to finish). If there is a circle of dependencies
+which in turn needs to wait for @{text "th\<^sub>0"} to finish). If
-in a RAG, then clearly
+there is a circle of dependencies in a RAG, then clearly we have a
-we have a deadlock. Therefore when a thread requests a resource,
+deadlock. Therefore when a thread requests a resource, we must
-we must ensure that the resulting RAG is not circular. In practice, the
+ensure that the resulting RAG is not circular. In practice, the
 programmer has to ensure this.
 Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a
 state @{text s}. It is defined as
 is then the thread with the highest current precedence of all ready threads.
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm readys_def}\\
-@{thm runing_def}
+@{thm running_def}
 \end{tabular}
 \end{isabelle}
 \noindent
 %%In the second definition @{term "DUMMY ` DUMMY"} stands for the image of a set under a function.
 @{thm [source] th_cp_max th_cp_preced th_kept}
 @{thm th_cp_max th_cp_preced th_kept}
 THENTHEN
-(here) %@ {thm [source] runing_inversion_4} @  {thm runing_inversion_4}
+(here) %@ {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}.
 Lemmas we want to describe:
 \begin{lemma}
-@{thm runing_cntP_cntV_inv}
+@{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}.
 \begin{lemma}\label{runninginversion}
-@{thm runing_inversion}
+@{thm running_inversion}
 \end{lemma}
 explain tRAG
 \bigskip
 \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] runing_unique[of _ "th1" "th2"]}
+%@ {thm[mode=IfThen] running_unique[of _ "th1" "th2"]}
 \end{tabular}
 \end{isabelle}
 \noindent
 The first property states that every waiting thread can only wait for a single
 %  (@{text "count_eq_dependants"}):
 %  @  {thm [display] count_eq_dependants}
 %\end{enumerate}
 %The reason that only threads which already held some resoures
-%can be runing and block @{text "th"} is that if , otherwise, one thread
+%can be running and block @{text "th"} is that if , otherwise, one thread
 %does not hold any resource, it may never have its prioirty raised
 %and will not get a chance to run. This fact is supported by
 %lemma @{text "moment_blocked"}:
 %@   {thm [display] moment_blocked}
 %When instantiating  @{text "i"} to @{text "0"}, the lemma means threads which did not hold any
 %  (@{text "th_cp_preced"}):
 %  @   {thm [display] th_cp_preced}
 %\end{enumerate}
 %The main theorem of this part is to characterizing the running thread during @{term "t"}
-%(@{text "runing_inversion_2"}):
+%(@{text "running_inversion_2"}):
-%@   {thm [display] runing_inversion_2}
+%@   {thm [display] running_inversion_2}
 %According to this, if a thread is running, it is either @{term "th"} or was
 %already live and held some resource
 %at moment @{text "s"} (expressed by: @{text "cntV s th' < cntP s th'"}).
 %Since there are only finite many threads live and holding some resource at any moment,

changeset 127	38c6acf03f68
parent 126	a88af0e4731f
child 130	0f124691c191