334 \begin{center} |
334 \begin{center} |
335 \newcommand{\fnt}{\fontsize{7}{8}\selectfont} |
335 \newcommand{\fnt}{\fontsize{7}{8}\selectfont} |
336 \begin{tikzpicture}[scale=1] |
336 \begin{tikzpicture}[scale=1] |
337 %%\draw[step=2mm] (-3,2) grid (1,-1); |
337 %%\draw[step=2mm] (-3,2) grid (1,-1); |
338 |
338 |
339 \node (A) at (0,0) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>0"}}; |
339 \node (A) at (0,0) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^sub>0"}}; |
340 \node (B) at (2,0) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>1"}}; |
340 \node (B) at (2,0) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^sub>1"}}; |
341 \node (C) at (4,0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>1"}}; |
341 \node (C) at (4,0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^sub>1"}}; |
342 \node (D) at (4,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>2"}}; |
342 \node (D) at (4,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^sub>2"}}; |
343 \node (E) at (6,-0.7) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>2"}}; |
343 \node (E) at (6,-0.7) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^sub>2"}}; |
344 \node (E1) at (6, 0.2) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>3"}}; |
344 \node (E1) at (6, 0.2) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^sub>3"}}; |
345 \node (F) at (8,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>3"}}; |
345 \node (F) at (8,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^sub>3"}}; |
346 |
346 |
347 \draw [<-,line width=0.6mm] (A) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding} (B); |
347 \draw [<-,line width=0.6mm] (A) to node [pos=0.54,sloped,above=-0.5mm] {\fnt{}holding} (B); |
348 \draw [->,line width=0.6mm] (C) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waiting} (B); |
348 \draw [->,line width=0.6mm] (C) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waiting} (B); |
349 \draw [->,line width=0.6mm] (D) to node [pos=0.4,sloped,below=-0.5mm] {\fnt{}waiting} (B); |
349 \draw [->,line width=0.6mm] (D) to node [pos=0.4,sloped,below=-0.5mm] {\fnt{}waiting} (B); |
350 \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,below=-0.5mm] {\fnt{}holding} (E); |
350 \draw [<-,line width=0.6mm] (D) to node [pos=0.54,sloped,below=-0.5mm] {\fnt{}holding} (E); |
364 |
364 |
365 \noindent |
365 \noindent |
366 This definition needs to account for all threads that wait for a thread to |
366 This definition needs to account for all threads that wait for a thread to |
367 release a resource. This means we need to include threads that transitively |
367 release a resource. This means we need to include threads that transitively |
368 wait for a resource being released (in the picture above this means the dependants |
368 wait for a resource being released (in the picture above this means the dependants |
369 of @{text "th\<^isub>0"} are @{text "th\<^isub>1"} and @{text "th\<^isub>2"}, which wait for resource @{text "cs\<^isub>1"}, |
369 of @{text "th\<^sub>0"} are @{text "th\<^sub>1"} and @{text "th\<^sub>2"}, which wait for resource @{text "cs\<^sub>1"}, |
370 but also @{text "th\<^isub>3"}, |
370 but also @{text "th\<^sub>3"}, |
371 which cannot make any progress unless @{text "th\<^isub>2"} makes progress, which |
371 which cannot make any progress unless @{text "th\<^sub>2"} makes progress, which |
372 in turn needs to wait for @{text "th\<^isub>0"} to finish). If there is a circle of dependencies |
372 in turn needs to wait for @{text "th\<^sub>0"} to finish). If there is a circle of dependencies |
373 in a RAG, then clearly |
373 in a RAG, then clearly |
374 we have a deadlock. Therefore when a thread requests a resource, |
374 we have a deadlock. Therefore when a thread requests a resource, |
375 we must ensure that the resulting RAG is not circular. In practice, the |
375 we must ensure that the resulting RAG is not circular. In practice, the |
376 programmer has to ensure this. |
376 programmer has to ensure this. |
377 |
377 |
761 The second property is by induction of @{term vt}. The next three |
761 The second property is by induction of @{term vt}. The next three |
762 properties are |
762 properties are |
763 |
763 |
764 \begin{isabelle}\ \ \ \ \ %%% |
764 \begin{isabelle}\ \ \ \ \ %%% |
765 \begin{tabular}{@ {}l} |
765 \begin{tabular}{@ {}l} |
766 @{thm[mode=IfThen] waiting_unique[of _ _ "cs\<^isub>1" "cs\<^isub>2"]}\\ |
766 @{thm[mode=IfThen] waiting_unique[of _ _ "cs\<^sub>1" "cs\<^sub>2"]}\\ |
767 @{thm[mode=IfThen] held_unique[of _ "th\<^isub>1" _ "th\<^isub>2"]}\\ |
767 @{thm[mode=IfThen] held_unique[of _ "th\<^sub>1" _ "th\<^sub>2"]}\\ |
768 @{thm[mode=IfThen] runing_unique[of _ "th\<^isub>1" "th\<^isub>2"]} |
768 @{thm[mode=IfThen] runing_unique[of _ "th\<^sub>1" "th\<^sub>2"]} |
769 \end{tabular} |
769 \end{tabular} |
770 \end{isabelle} |
770 \end{isabelle} |
771 |
771 |
772 \noindent |
772 \noindent |
773 The first property states that every waiting thread can only wait for a single |
773 The first property states that every waiting thread can only wait for a single |
862 %The following lemmas show how every node in RAG can be chased to ready threads: |
862 %The following lemmas show how every node in RAG can be chased to ready threads: |
863 %\begin{enumerate} |
863 %\begin{enumerate} |
864 %\item Every node in RAG can be chased to a ready thread (@{text "chain_building"}): |
864 %\item Every node in RAG can be chased to a ready thread (@{text "chain_building"}): |
865 % @ {thm [display] chain_building[rule_format]} |
865 % @ {thm [display] chain_building[rule_format]} |
866 %\item The ready thread chased to is unique (@{text "dchain_unique"}): |
866 %\item The ready thread chased to is unique (@{text "dchain_unique"}): |
867 % @ {thm [display] dchain_unique[of _ _ "th\<^isub>1" "th\<^isub>2"]} |
867 % @ {thm [display] dchain_unique[of _ _ "th\<^sub>1" "th\<^sub>2"]} |
868 %\end{enumerate} |
868 %\end{enumerate} |
869 |
869 |
870 %Some deeper results about the system: |
870 %Some deeper results about the system: |
871 %\begin{enumerate} |
871 %\begin{enumerate} |
872 %\item The maximum of @{term "cp"} and @{term "preced"} are equal (@{text "max_cp_eq"}): |
872 %\item The maximum of @{term "cp"} and @{term "preced"} are equal (@{text "max_cp_eq"}): |