609 cannot make any progress unless @{text "th\<^sub>2"} makes progress, |
609 cannot make any progress unless @{text "th\<^sub>2"} makes progress, |
610 which in turn needs to wait for @{text "th\<^sub>0"} to finish). If |
610 which in turn needs to wait for @{text "th\<^sub>0"} to finish). If |
611 there is a circle of dependencies in a RAG, then clearly we have a |
611 there is a circle of dependencies in a RAG, then clearly we have a |
612 deadlock. Therefore when a thread requests a resource, we must |
612 deadlock. Therefore when a thread requests a resource, we must |
613 ensure that the resulting RAG is not circular. In practice, the |
613 ensure that the resulting RAG is not circular. In practice, the |
614 programmer has to ensure this. Our model will assume that critical |
614 programmer has to ensure this. Our model will enforce that critical |
615 resources can only be requested provided no circularity can arise. |
615 resources can only be requested provided no circularity can arise. |
616 |
616 |
617 Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a |
617 Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a |
618 state @{text s}. It is defined as |
618 state @{text s}. It is defined as |
619 |
619 |
620 \begin{isabelle}\ \ \ \ \ %%% |
620 \begin{isabelle}\ \ \ \ \ %%% |
621 @{thm cpreced_def}\hfill\numbered{cpreced} |
621 @{thm cpreced_def3}\hfill\numbered{cpreced} |
622 \end{isabelle} |
622 \end{isabelle} |
623 |
623 |
624 \endnote{ |
624 \endnote{ |
625 \begin{isabelle}\ \ \ \ \ %%% |
625 \begin{isabelle}\ \ \ \ \ %%% |
626 @{thm cp_alt_def cp_alt_def1} |
626 @{thm cp_alt_def cp_alt_def1} |
627 \end{isabelle}} |
627 \end{isabelle}} |
628 |
628 |
629 \noindent |
629 \noindent where the dependants of @{text th} are given by the |
630 where the dependants of @{text th} are given by the waiting queue function. |
630 waiting queue function. While the precedence @{term prec} of any |
631 While the precedence @{term prec} of any thread is determined statically |
631 thread is determined statically (for example when the thread is |
632 (for example when the thread is |
632 created), the point of the current precedence is to dynamically |
633 created), the point of the current precedence is to let the scheduler increase this |
633 increase this precedence, if needed according to PIP. Therefore the |
634 precedence, if needed according to PIP. Therefore the current precedence of @{text th} is |
634 current precedence of @{text th} is given as the maximum of the |
635 given as the maximum of the precedence @{text th} has in state @{text s} \emph{and} all |
635 precedence of @{text th} \emph{and} all threads that are dependants |
636 threads that are dependants of @{text th}. Since the notion @{term "dependants"} is |
636 of @{text th} in the state @{text s}. Since the notion @{term |
637 defined as the transitive closure of all dependent threads, we deal correctly with the |
637 "dependants"} is defined as the transitive closure of all dependent |
638 problem in the informal algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is |
638 threads, we deal correctly with the problem in the informal |
639 lowered prematurely. We again introduce an abbreviation for current precedeces of |
639 algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is |
640 a set of threads, written @{term "cprecs wq s ths"}. |
640 lowered prematurely (see Introduction). We again introduce an abbreviation for current |
|
641 precedeces of a set of threads, written @{term "cprecs wq s ths"}. |
641 |
642 |
642 \begin{isabelle}\ \ \ \ \ %%% |
643 \begin{isabelle}\ \ \ \ \ %%% |
643 @{thm cpreceds_def} |
644 @{thm cpreceds_def} |
644 \end{isabelle} |
645 \end{isabelle} |
645 |
646 |
647 by recursion on the state (a list of events); this function returns a \emph{schedule state}, which |
648 by recursion on the state (a list of events); this function returns a \emph{schedule state}, which |
648 we represent as a record consisting of two |
649 we represent as a record consisting of two |
649 functions: |
650 functions: |
650 |
651 |
651 \begin{isabelle}\ \ \ \ \ %%% |
652 \begin{isabelle}\ \ \ \ \ %%% |
652 @{text "\<lparr>wq, cp\<rparr>"} |
653 @{text "\<lparr>wq_fun, cprec_fun\<rparr>"} |
653 \end{isabelle} |
654 \end{isabelle} |
654 |
655 |
655 \noindent |
656 \noindent |
656 The first function is a waiting queue function (that is, it takes a |
657 The first function is a waiting queue function (that is, it takes a |
657 resource @{text "cs"} and returns the corresponding list of threads |
658 resource @{text "cs"} and returns the corresponding list of threads |
694 \hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Set th prio # s)|)"} |
695 \hspace{8mm}@{term "(|wq_fun = wq\<iota>, cprec_fun = cpreced wq\<iota> (Set th prio # s)|)"} |
695 \end{tabular} |
696 \end{tabular} |
696 \end{isabelle} |
697 \end{isabelle} |
697 |
698 |
698 \noindent |
699 \noindent |
699 More interesting are the cases where a resource, say @{text cs}, is locked or released. In these cases |
700 More interesting are the cases where a resource, say @{text cs}, is requested or released. In these cases |
700 we need to calculate a new waiting queue function. For the event @{term "P th cs"}, we have to update |
701 we need to calculate a new waiting queue function. For the event @{term "P th cs"}, we have to update |
701 the function so that the new thread list for @{text cs} is the old thread list plus the thread @{text th} |
702 the function so that the new thread list for @{text cs} is the old thread list plus the thread @{text th} |
702 appended to the end of that list (remember the head of this list is assigned to be in the possession of this |
703 appended to the end of that list (remember the head of this list is assigned to be in the possession of this |
703 resource). This gives the clause |
704 resource). This gives the clause |
704 |
705 |
736 @{term "release []"} & @{text "\<equiv>"} & @{term "[]"}\\ |
737 @{term "release []"} & @{text "\<equiv>"} & @{term "[]"}\\ |
737 @{term "release (DUMMY # qs)"} & @{text "\<equiv>"} & @{term "SOME qs'. distinct qs' \<and> set qs' = set qs"}\\ |
738 @{term "release (DUMMY # qs)"} & @{text "\<equiv>"} & @{term "SOME qs'. distinct qs' \<and> set qs' = set qs"}\\ |
738 \end{tabular} |
739 \end{tabular} |
739 \end{isabelle} |
740 \end{isabelle} |
740 |
741 |
741 \noindent |
742 \noindent where @{text "SOME"} stands for Hilbert's epsilon and |
742 where @{text "SOME"} stands for Hilbert's epsilon and implements an arbitrary |
743 implements an arbitrary choice for the next waiting list. It just |
743 choice for the next waiting list. It just has to be a list of distinctive threads and |
744 has to be a list of distinctive threads and contains the same |
744 contains the same elements as @{text "qs"}. This gives for @{term V} the clause: |
745 elements as @{text "qs"} (essentially @{text "qs'"} can be any |
|
746 reordering of the list @{text "qs"}). This gives for @{term V} the clause: |
745 |
747 |
746 \begin{isabelle}\ \ \ \ \ %%% |
748 \begin{isabelle}\ \ \ \ \ %%% |
747 \begin{tabular}{@ {}l} |
749 \begin{tabular}{@ {}l} |
748 @{thm (lhs) schs.simps(6)} @{text "\<equiv>"}\\ |
750 @{thm (lhs) schs.simps(6)} @{text "\<equiv>"}\\ |
749 \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\ |
751 \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\ |