183 whereby threads, priorities and (critical) resources are represented |
183 whereby threads, priorities and (critical) resources are represented |
184 as natural numbers. The event @{term Set} models the situation that |
184 as natural numbers. The event @{term Set} models the situation that |
185 a thread obtains a new priority given by the programmer or |
185 a thread obtains a new priority given by the programmer or |
186 user (for example via the {\tt nice} utility under UNIX). As in Paulson's work, we |
186 user (for example via the {\tt nice} utility under UNIX). As in Paulson's work, we |
187 need to define functions that allow one to make some observations |
187 need to define functions that allow one to make some observations |
188 about states. One, called @{term threads}, calculates, given a state @{text s}, the set of |
188 about states. One, called @{term threads}, calculates the set of |
189 ``live'' threads that we have seen so far: |
189 ``live'' threads that we have seen so far: |
190 |
190 |
191 \begin{isabelle}\ \ \ \ \ %%% |
191 \begin{isabelle}\ \ \ \ \ %%% |
192 \mbox{\begin{tabular}{lcl} |
192 \mbox{\begin{tabular}{lcl} |
193 @{thm (lhs) threads.simps(1)} & @{text "\<equiv>"} & |
193 @{thm (lhs) threads.simps(1)} & @{text "\<equiv>"} & |
303 |
303 |
304 \noindent |
304 \noindent |
305 An instance of a RAG is as follows: |
305 An instance of a RAG is as follows: |
306 |
306 |
307 \begin{center} |
307 \begin{center} |
|
308 \newcommand{\fnt}{\fontsize{7}{8}\selectfont} |
308 \begin{tikzpicture}[scale=1] |
309 \begin{tikzpicture}[scale=1] |
309 \draw[step=2mm] (0,0) grid (3,2); |
310 %%\draw[step=2mm] (-3,2) grid (1,-1); |
310 |
311 |
311 \draw[rounded corners=1mm, very thick] (0,0) rectangle (0.6,0.6); |
312 \node (A) at (0,0) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>0"}}; |
312 \draw[rounded corners=1mm, very thick] (3,0) rectangle (3.6,0.6); |
313 \node (B) at (2,0) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>1"}}; |
313 |
314 \node (C) at (4,0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>1"}}; |
314 \draw (0.3,0.3) node {\small$th_0$}; |
315 \node (D) at (4,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>2"}}; |
315 \draw (3.3,0.3) node {\small$th_1$}; |
316 \node (E) at (6,-0.7) [draw, circle, very thick, inner sep=0.4mm] {@{text "cs\<^isub>2"}}; |
|
317 \node (F) at (8,-0.7) [draw, rounded corners=1mm, rectangle, very thick] {@{text "th\<^isub>3"}}; |
|
318 |
|
319 \draw [->,line width=0.6mm] (A) to node [pos=0.45,sloped,above=-0.5mm] {\fnt{}holding} (B); |
|
320 \draw [->,line width=0.6mm] (C) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waiting} (B); |
|
321 \draw [->,line width=0.6mm] (D) to node [pos=0.4,sloped,above=-0.5mm] {\fnt{}waiting} (B); |
|
322 \draw [->,line width=0.6mm] (D) to node [pos=0.45,sloped,above=-0.5mm] {\fnt{}holding} (E); |
|
323 \draw [->,line width=0.6mm] (F) to node [pos=0.45,sloped,above=-0.5mm] {\fnt{}waiting} (E); |
316 \end{tikzpicture} |
324 \end{tikzpicture} |
317 \end{center} |
325 \end{center} |
318 |
326 |
319 \noindent |
327 \noindent |
320 The use of relations for representing RAGs allows us to conveniently define |
328 The use of relations for representing RAGs allows us to conveniently define |