782 @{text "s' @ s"}, as we had to show.\qed |
782 @{text "s' @ s"}, as we had to show.\qed |
783 \end{proof} |
783 \end{proof} |
784 |
784 |
785 \noindent |
785 \noindent |
786 Since @{text "th'"} is not able to run at state @{text "s' @ s"}, it is not able to |
786 Since @{text "th'"} is not able to run at state @{text "s' @ s"}, it is not able to |
787 issue a {text "P"} or @{text "V"} event. Therefore if @{text "s' @ s"} is extended |
787 issue a @{text "P"} or @{text "V"} event. Therefore if @{text "s' @ s"} is extended |
788 one step further, @{text "th'"} still cannot hold any resource. The situation will |
788 one step further, @{text "th'"} still cannot hold any resource. The situation will |
789 not change in further extensions as long as @{text "th"} holds the highest precedence. |
789 not change in further extensions as long as @{text "th"} holds the highest precedence. |
790 |
790 |
791 From this lemma we can infer that @{text th} can only be blocked by a thread @{text th'} that |
791 From this lemma we can infer that @{text th} can only be blocked by a thread @{text th'} that |
792 held some resource in state @{text s} (that is not @{text "detached"}). And furthermore |
792 held some resource in state @{text s} (that is not @{text "detached"}). And furthermore |
799 @{term "th' \<in> running (s' @ s)"}, @{text "th' \<noteq> th"}, then |
799 @{term "th' \<in> running (s' @ s)"}, @{text "th' \<noteq> th"}, then |
800 @{text "th' \<in> threads s"}, @{text "\<not> detached s th'"} and |
800 @{text "th' \<in> threads s"}, @{text "\<not> detached s th'"} and |
801 @{term "cp (s' @ s) th' = prec th s"}. |
801 @{term "cp (s' @ s) th' = prec th s"}. |
802 \end{theorem} |
802 \end{theorem} |
803 |
803 |
|
804 \noindent |
804 We show this theorem by induction on @{text "s'"} using Lemma~\ref{mainlem}. |
805 We show this theorem by induction on @{text "s'"} using Lemma~\ref{mainlem}. |
805 This theorem gives a stricter bound on the processes that can block @{text th}: |
806 This theorem gives a stricter bound on the processes that can block @{text th}: |
806 only threads that were alive in state @{text s} and moreover held a resource. |
807 only threads that were alive in state @{text s} and moreover held a resource. |
807 Finally, the theorem establishes that the blocking threads have the |
808 Finally, the theorem establishes that the blocking threads have the |
808 current precedence raised to the precedence of @{text th}. |
809 current precedence raised to the precedence of @{text th}. |
|
810 |
|
811 We can furthermore prove that no deadlock exists in the state @{text "s' @ s"} |
|
812 by showing that @{text "running (s' @ s)"} is not empty. |
|
813 |
|
814 \begin{lemma} |
|
815 Given the assumptions about states @{text "s"} and @{text "s' @ s"}, |
|
816 the thread @{text th} and the events in @{text "s'"}, |
|
817 @{term "running (s' @ s) \<noteq> {}"}. |
|
818 \end{lemma} |
|
819 |
|
820 \begin{proof} |
|
821 If @{text th} is blocked, then by following its dependants graph, we can always |
|
822 reach a ready thread @{text th'}, and that thread must have inherited the |
|
823 precedence of @{text th}.\qed |
|
824 \end{proof} |
|
825 |
809 |
826 |
810 %The following lemmas show how every node in RAG can be chased to ready threads: |
827 %The following lemmas show how every node in RAG can be chased to ready threads: |
811 %\begin{enumerate} |
828 %\begin{enumerate} |
812 %\item Every node in RAG can be chased to a ready thread (@{text "chain_building"}): |
829 %\item Every node in RAG can be chased to a ready thread (@{text "chain_building"}): |
813 % @ {thm [display] chain_building[rule_format]} |
830 % @ {thm [display] chain_building[rule_format]} |