470 (RAG), which represent the dependencies between threads and resources. |
470 (RAG), which represent the dependencies between threads and resources. |
471 We choose to represent RAGs as relations using pairs of the form |
471 We choose to represent RAGs as relations using pairs of the form |
472 |
472 |
473 \begin{isabelle}\ \ \ \ \ %%% |
473 \begin{isabelle}\ \ \ \ \ %%% |
474 @{term "(Th th, Cs cs)"} \hspace{5mm}{\rm and}\hspace{5mm} |
474 @{term "(Th th, Cs cs)"} \hspace{5mm}{\rm and}\hspace{5mm} |
475 @{term "(Cs cs, Th th)"} |
475 @{term "(Cs cs, Th th)"}\hfill\numbered{pairs} |
476 \end{isabelle} |
476 \end{isabelle} |
477 |
477 |
478 \noindent |
478 \noindent |
479 where the first stands for a \emph{waiting edge} and the second for a |
479 where the first stands for a \emph{waiting edge} and the second for a |
480 \emph{holding edge} (@{term Cs} and @{term Th} are constructors of a |
480 \emph{holding edge} (@{term Cs} and @{term Th} are constructors of a |
530 |
530 |
531 While there are few formalisations for graphs already implemented in |
531 While there are few formalisations for graphs already implemented in |
532 Isabelle, we choose to introduce our own library of graphs for |
532 Isabelle, we choose to introduce our own library of graphs for |
533 PIP. The reason for this is that we wanted to be able to reason with |
533 PIP. The reason for this is that we wanted to be able to reason with |
534 potentially infinite graphs (in the sense of infinitely branching |
534 potentially infinite graphs (in the sense of infinitely branching |
535 and infinite size): the property that our RAGs are forrests of |
535 and infinite size): the property that our RAGs are actually forrests |
536 finitely branching trees having only an finite depth should be a |
536 of finitely branching trees having only an finite depth should be a |
537 something we can \emph{prove} for our model of PIP---it should not |
537 something we can \emph{prove} for our model of PIP---it should not |
538 be an assumption we build already into our model. It seemed for our purposes the most convenient |
538 be an assumption we build already into our model. It seemed for our |
539 represeantation of graphs are binary relations given by |
539 purposes the most convenient represeantation of graphs are binary |
540 sets of pairs. The pairs stand for the edges in graphs. This |
540 relations given by sets of pairs from \eqref{pairs}. The pairs stand for the edges in |
541 relation-based representation is convenient since we can use the notions |
541 graphs. This relation-based representation is convenient since we |
542 of transitive closure operations @{term "trancl DUMMY"} and |
542 can use the notions of transitive closure operations @{term "trancl |
543 @{term "rtrancl DUMMY"}, as well as relation composition @{term "DUMMY O DUMMY"}. |
543 DUMMY"} and @{term "rtrancl DUMMY"}, as well as relation composition |
544 A \emph{forrest} is defined as the relation @{text rel} that is \emph{single valued} |
544 @{term "DUMMY O DUMMY"}. A \emph{forrest} is defined as the |
545 and \emph{acyclic}: |
545 relation @{text rel} that is \emph{single valued} and |
|
546 \emph{acyclic}: |
546 |
547 |
547 \begin{isabelle}\ \ \ \ \ %%% |
548 \begin{isabelle}\ \ \ \ \ %%% |
548 \begin{tabular}{@ {}l} |
549 \begin{tabular}{@ {}l} |
549 @{thm single_valued_def[where ?r="rel", THEN eq_reflection]}\\ |
550 @{thm single_valued_def[where ?r="rel", THEN eq_reflection]}\\ |
550 @{thm acyclic_def[where ?r="rel", THEN eq_reflection]} |
551 @{thm acyclic_def[where ?r="rel", THEN eq_reflection]} |
566 \noindent Note that forests can have trees with infinte depth and |
567 \noindent Note that forests can have trees with infinte depth and |
567 containing nodes with infinitely many children. A \emph{finite |
568 containing nodes with infinitely many children. A \emph{finite |
568 forrest} is a forest which is well-founded and every node has |
569 forrest} is a forest which is well-founded and every node has |
569 finitely many children (is only finitely branching). |
570 finitely many children (is only finitely branching). |
570 |
571 |
|
572 \begin{isabelle}\ \ \ \ \ %%% |
|
573 @{thm rtrancl_path.intros} |
|
574 \end{isabelle} |
|
575 |
|
576 \begin{isabelle}\ \ \ \ \ %%% |
|
577 @{thm rpath_def} |
|
578 \end{isabelle} |
|
579 |
|
580 |
|
581 {\bf Lemma about overlapping paths} |
|
582 |
571 |
583 |
572 We will design our PIP-scheduler |
584 We will design our PIP-scheduler |
573 so that every thread can be in the possession of several resources, that is |
585 so that every thread can be in the possession of several resources, that is |
574 it has potentially several incoming holding edges in the RAG, but has at most one outgoing |
586 it has potentially several incoming holding edges in the RAG, but has at most one outgoing |
575 waiting edge. The reason is that when a thread asks for resource that is locked |
587 waiting edge. The reason is that when a thread asks for resource that is locked |
603 Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a |
615 Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a |
604 state @{text s}. It is defined as |
616 state @{text s}. It is defined as |
605 |
617 |
606 \begin{isabelle}\ \ \ \ \ %%% |
618 \begin{isabelle}\ \ \ \ \ %%% |
607 @{thm cpreced_def}\hfill\numbered{cpreced} |
619 @{thm cpreced_def}\hfill\numbered{cpreced} |
|
620 \end{isabelle} |
|
621 |
|
622 \begin{isabelle}\ \ \ \ \ %%% |
|
623 @{thm cp_alt_def cp_alt_def1} |
608 \end{isabelle} |
624 \end{isabelle} |
609 |
625 |
610 \noindent |
626 \noindent |
611 where the dependants of @{text th} are given by the waiting queue function. |
627 where the dependants of @{text th} are given by the waiting queue function. |
612 While the precedence @{term prec} of any thread is determined statically |
628 While the precedence @{term prec} of any thread is determined statically |