31 Cons ("_::_" [78,77] 73) and |
31 Cons ("_::_" [78,77] 73) and |
32 If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and |
32 If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and |
33 vt ("valid'_state") and |
33 vt ("valid'_state") and |
34 Prc ("'(_, _')") and |
34 Prc ("'(_, _')") and |
35 holding_raw ("holds") and |
35 holding_raw ("holds") and |
36 holding ("Holds") and |
36 holding ("holds") and |
37 waiting_raw ("waits") and |
37 waiting_raw ("waits") and |
38 waiting ("Waits") and |
38 waiting ("waits") and |
39 dependants_raw ("dependants") and |
39 dependants_raw ("dependants") and |
40 dependants ("Dependants") and |
40 dependants ("dependants") and |
|
41 RAG_raw ("RAG") and |
|
42 RAG ("RAG") and |
41 Th ("T") and |
43 Th ("T") and |
42 Cs ("C") and |
44 Cs ("C") and |
43 readys ("ready") and |
45 readys ("ready") and |
44 preced ("prec") and |
46 preced ("prec") and |
45 preceds ("precs") and |
47 preceds ("precs") and |
46 cpreced ("cprec") and |
48 cpreced ("cprec") and |
47 cp ("cprec") and |
49 wq_fun ("wq") and |
|
50 cprec_fun ("cp") and |
48 holdents ("resources") and |
51 holdents ("resources") and |
49 DUMMY ("\<^raw:\mbox{$\_\!\_$}>") and |
52 DUMMY ("\<^raw:\mbox{$\_\!\_$}>") and |
50 cntP ("c\<^bsub>P\<^esub>") and |
53 cntP ("c\<^bsub>P\<^esub>") and |
51 cntV ("c\<^bsub>V\<^esub>") |
54 cntV ("c\<^bsub>V\<^esub>") |
52 |
55 |
453 \end{isabelle} |
456 \end{isabelle} |
454 |
457 |
455 \noindent |
458 \noindent |
456 Using @{term "holding_raw"} and @{term waiting_raw}, we can introduce \emph{Resource Allocation Graphs} |
459 Using @{term "holding_raw"} and @{term waiting_raw}, we can introduce \emph{Resource Allocation Graphs} |
457 (RAG), which represent the dependencies between threads and resources. |
460 (RAG), which represent the dependencies between threads and resources. |
458 We represent RAGs as relations using pairs of the form |
461 We choose to represent RAGs as relations using pairs of the form |
459 |
462 |
460 \begin{isabelle}\ \ \ \ \ %%% |
463 \begin{isabelle}\ \ \ \ \ %%% |
461 @{term "(Th th, Cs cs)"} \hspace{5mm}{\rm and}\hspace{5mm} |
464 @{term "(Th th, Cs cs)"} \hspace{5mm}{\rm and}\hspace{5mm} |
462 @{term "(Cs cs, Th th)"} |
465 @{term "(Cs cs, Th th)"} |
463 \end{isabelle} |
466 \end{isabelle} |
522 already, then the thread is blocked and cannot ask for another resource. |
525 already, then the thread is blocked and cannot ask for another resource. |
523 Clearly, also every resource can only have at most one outgoing holding edge---indicating |
526 Clearly, also every resource can only have at most one outgoing holding edge---indicating |
524 that the resource is locked. In this way we can always start at a thread waiting for a |
527 that the resource is locked. In this way we can always start at a thread waiting for a |
525 resource and ``chase'' outgoing arrows leading to a single root of a tree. |
528 resource and ``chase'' outgoing arrows leading to a single root of a tree. |
526 |
529 |
527 |
|
528 |
|
529 The use of relations for representing RAGs allows us to conveniently define |
530 The use of relations for representing RAGs allows us to conveniently define |
530 the notion of the \emph{dependants} of a thread using the transitive closure |
531 the notion of the \emph{dependants} of a thread using the transitive closure |
531 operation for relations, written ~@{term "trancl DUMMY"}. This gives |
532 operation for relations, written ~@{term "trancl DUMMY"}. This gives |
532 |
533 |
533 \begin{isabelle}\ \ \ \ \ %%% |
534 \begin{isabelle}\ \ \ \ \ %%% |
543 cannot make any progress unless @{text "th\<^sub>2"} makes progress, |
544 cannot make any progress unless @{text "th\<^sub>2"} makes progress, |
544 which in turn needs to wait for @{text "th\<^sub>0"} to finish). If |
545 which in turn needs to wait for @{text "th\<^sub>0"} to finish). If |
545 there is a circle of dependencies in a RAG, then clearly we have a |
546 there is a circle of dependencies in a RAG, then clearly we have a |
546 deadlock. Therefore when a thread requests a resource, we must |
547 deadlock. Therefore when a thread requests a resource, we must |
547 ensure that the resulting RAG is not circular. In practice, the |
548 ensure that the resulting RAG is not circular. In practice, the |
548 programmer has to ensure this. |
549 programmer has to ensure this. Our model will assume that critical |
549 |
550 reseources can only be requested provided no circularity can arise. |
550 |
551 |
551 Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a |
552 Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a |
552 state @{text s}. It is defined as |
553 state @{text s}. It is defined as |
553 |
554 |
554 \begin{isabelle}\ \ \ \ \ %%% |
555 \begin{isabelle}\ \ \ \ \ %%% |
555 @{thm cpreced_def2}\hfill\numbered{cpreced} |
556 @{thm cpreced_def}\hfill\numbered{cpreced} |
556 \end{isabelle} |
557 \end{isabelle} |
557 |
558 |
558 \noindent |
559 \noindent |
559 where the dependants of @{text th} are given by the waiting queue function. |
560 where the dependants of @{text th} are given by the waiting queue function. |
560 While the precedence @{term prec} of any thread is determined statically |
561 While the precedence @{term prec} of any thread is determined statically |
566 defined as the transitive closure of all dependent threads, we deal correctly with the |
567 defined as the transitive closure of all dependent threads, we deal correctly with the |
567 problem in the informal algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is |
568 problem in the informal algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is |
568 lowered prematurely. We again introduce an abbreviation for current precedeces of |
569 lowered prematurely. We again introduce an abbreviation for current precedeces of |
569 a set of threads, written @{term "cprecs wq s ths"}. |
570 a set of threads, written @{term "cprecs wq s ths"}. |
570 |
571 |
|
572 \begin{isabelle}\ \ \ \ \ %%% |
|
573 @{thm cpreceds_def} |
|
574 \end{isabelle} |
|
575 |
571 The next function, called @{term schs}, defines the behaviour of the scheduler. It will be defined |
576 The next function, called @{term schs}, defines the behaviour of the scheduler. It will be defined |
572 by recursion on the state (a list of events); this function returns a \emph{schedule state}, which |
577 by recursion on the state (a list of events); this function returns a \emph{schedule state}, which |
573 we represent as a record consisting of two |
578 we represent as a record consisting of two |
574 functions: |
579 functions: |
575 |
580 |
576 \begin{isabelle}\ \ \ \ \ %%% |
581 \begin{isabelle}\ \ \ \ \ %%% |
577 @{text "\<lparr>wq_fun, cprec_fun\<rparr>"} |
582 @{text "\<lparr>wq, cp\<rparr>"} |
578 \end{isabelle} |
583 \end{isabelle} |
579 |
584 |
580 \noindent |
585 \noindent |
581 The first function is a waiting queue function (that is, it takes a |
586 The first function is a waiting queue function (that is, it takes a |
582 resource @{text "cs"} and returns the corresponding list of threads |
587 resource @{text "cs"} and returns the corresponding list of threads |