--- a/Journal/Paper.thy Tue Jun 07 13:51:39 2016 +0100
+++ b/Journal/Paper.thy Thu Jun 09 23:01:36 2016 +0100
@@ -31,15 +31,18 @@
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
- waiting ("waits") and
+ holding_raw ("holds") 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
@@ -330,10 +333,10 @@
\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 (rhs) threads.simps(2)[where thread="th"]}\\
- @{thm (lhs) threads.simps(3)[where thread="th"]} & @{text "\<equiv>"} &
- @{thm (rhs) threads.simps(3)[where thread="th"]}\\
+ @{thm (lhs) threads.simps(2)} & @{text "\<equiv>"} &
+ @{thm (rhs) threads.simps(2)}\\
+ @{thm (lhs) threads.simps(3)} & @{text "\<equiv>"} &
+ @{thm (rhs) threads.simps(3)}\\
@{term "threads (DUMMY#s)"} & @{text "\<equiv>"} & @{term "threads s"}\\
\end{tabular}}
\end{isabelle}
@@ -345,12 +348,12 @@
\begin{isabelle}\ \ \ \ \ %%%
\mbox{\begin{tabular}{lcl}
- @{thm (lhs) priority.simps(1)[where thread="th"]} & @{text "\<equiv>"} &
- @{thm (rhs) priority.simps(1)[where thread="th"]}\\
- @{thm (lhs) priority.simps(2)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} &
- @{thm (rhs) priority.simps(2)[where thread="th" and thread'="th'"]}\\
- @{thm (lhs) priority.simps(3)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} &
- @{thm (rhs) priority.simps(3)[where thread="th" and thread'="th'"]}\\
+ @{thm (lhs) priority.simps(1)} & @{text "\<equiv>"} &
+ @{thm (rhs) priority.simps(1)}\\
+ @{thm (lhs) priority.simps(2)} & @{text "\<equiv>"} &
+ @{thm (rhs) priority.simps(2)}\\
+ @{thm (lhs) priority.simps(3)} & @{text "\<equiv>"} &
+ @{thm (rhs) priority.simps(3)}\\
@{term "priority th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "priority th s"}\\
\end{tabular}}
\end{isabelle}
@@ -363,12 +366,12 @@
\begin{isabelle}\ \ \ \ \ %%%
\mbox{\begin{tabular}{lcl}
- @{thm (lhs) last_set.simps(1)[where thread="th"]} & @{text "\<equiv>"} &
- @{thm (rhs) last_set.simps(1)[where thread="th"]}\\
- @{thm (lhs) last_set.simps(2)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} &
- @{thm (rhs) last_set.simps(2)[where thread="th" and thread'="th'"]}\\
- @{thm (lhs) last_set.simps(3)[where thread="th" and thread'="th'"]} & @{text "\<equiv>"} &
- @{thm (rhs) last_set.simps(3)[where thread="th" and thread'="th'"]}\\
+ @{thm (lhs) last_set.simps(1)} & @{text "\<equiv>"} &
+ @{thm (rhs) last_set.simps(1)}\\
+ @{thm (lhs) last_set.simps(2)} & @{text "\<equiv>"} &
+ @{thm (rhs) last_set.simps(2)}\\
+ @{thm (lhs) last_set.simps(3)} & @{text "\<equiv>"} &
+ @{thm (rhs) last_set.simps(3)}\\
@{term "last_set th (DUMMY#s)"} & @{text "\<equiv>"} & @{term "last_set th s"}\\
\end{tabular}}
\end{isabelle}
@@ -380,14 +383,14 @@
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
@@ -432,8 +435,8 @@
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
- @{thm cs_holding_raw[where thread="th"]}\\
- @{thm cs_waiting_raw[where thread="th"]}
+ @{thm holding_raw_def[where thread="th"]}\\
+ @{thm waiting_raw_def[where thread="th"]}
\end{tabular}
\end{isabelle}
@@ -450,7 +453,7 @@
\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
@@ -466,7 +469,7 @@
as the union of the sets of waiting and holding edges, namely
\begin{isabelle}\ \ \ \ \ %%%
- @{thm cs_RAG_raw}
+ @{thm RAG_raw_def}
\end{isabelle}
@@ -528,20 +531,20 @@
operation for relations, written ~@{term "trancl DUMMY"}. This gives
\begin{isabelle}\ \ \ \ \ %%%
- @{thm cs_dependants_def}
+ @{thm dependants_raw_def}
\end{isabelle}
- \noindent
- This definition needs to account for all threads that wait for a thread to
- release a resource. This means we need to include threads that transitively
- wait for a resource to be released (in the picture above this means the dependants
- of @{text "th\<^sub>0"} are @{text "th\<^sub>1"} and @{text "th\<^sub>2"}, which wait for resource @{text "cs\<^sub>1"},
- but also @{text "th\<^sub>3"},
- which cannot make any progress unless @{text "th\<^sub>2"} makes progress, which
- in turn needs to wait for @{text "th\<^sub>0"} to finish). If there is a circle of dependencies
- in a RAG, then clearly
- we have a deadlock. Therefore when a thread requests a resource,
- we must ensure that the resulting RAG is not circular. In practice, the
+ \noindent This definition needs to account for all threads that wait
+ for a thread to release a resource. This means we need to include
+ threads that transitively wait for a resource to be released (in the
+ picture above this means the dependants of @{text "th\<^sub>0"} are
+ @{text "th\<^sub>1"} and @{text "th\<^sub>2"}, which wait for
+ resource @{text "cs\<^sub>1"}, but also @{text "th\<^sub>3"}, which
+ cannot make any progress unless @{text "th\<^sub>2"} makes progress,
+ which in turn needs to wait for @{text "th\<^sub>0"} to finish). If
+ there is a circle of dependencies in a RAG, then clearly we have a
+ deadlock. Therefore when a thread requests a resource, we must
+ ensure that the resulting RAG is not circular. In practice, the
programmer has to ensure this.
@@ -699,7 +702,7 @@
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
@{thm readys_def}\\
- @{thm runing_def}
+ @{thm running_def}
\end{tabular}
\end{isabelle}
@@ -1001,7 +1004,7 @@
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.
@@ -1015,7 +1018,7 @@
\begin{lemma}
- @{thm runing_cntP_cntV_inv}
+ @{thm running_cntP_cntV_inv}
\end{lemma}
\noindent
@@ -1024,7 +1027,7 @@
and @{const cntP} can be larger than @{term 1}.
\begin{lemma}\label{runninginversion}
- @{thm runing_inversion}
+ @{thm running_inversion}
\end{lemma}
explain tRAG
@@ -1107,7 +1110,7 @@
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}
@@ -1241,7 +1244,7 @@
%\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"}:
@@ -1296,8 +1299,8 @@
%\end{enumerate}
%The main theorem of this part is to characterizing the running thread during @{term "t"}
- %(@{text "runing_inversion_2"}):
- %@ {thm [display] runing_inversion_2}
+ %(@{text "running_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'"}).
@@ -1824,4 +1827,4 @@
(*<*)
end
-(*>*)
\ No newline at end of file
+(*>*)