881 conveniently such assumptions~\cite{Haftmann08}. Under these |
881 conveniently such assumptions~\cite{Haftmann08}. Under these |
882 assumptions we shall prove the following correctness property: |
882 assumptions we shall prove the following correctness property: |
883 |
883 |
884 \begin{theorem}\label{mainthm} |
884 \begin{theorem}\label{mainthm} |
885 Given the assumptions about states @{text "s"} and @{text "s' @ s"}, |
885 Given the assumptions about states @{text "s"} and @{text "s' @ s"}, |
886 the thread @{text th} and the events in @{text "s'"}, |
886 the thread @{text th} and the events in @{text "s'"}, then either |
887 if @{term "th' \<in> running (s' @ s)"} and @{text "th' \<noteq> th"} then |
887 \begin{itemize} |
888 @{text "th' \<in> threads s"}, @{text "\<not> detached s th'"} and |
888 \item @{term "th \<in> running (s' @ s)"} or\medskip |
889 @{term "cp (s' @ s) th' = prec th s"}. |
889 |
|
890 \item there exists a thread @{term "th'"} with @{term "th' \<noteq> th"} |
|
891 and @{term "th' \<in> running (s' @ s)"} such that @{text "th' \<in> threads |
|
892 s"}, @{text "\<not> detached s th'"} and @{term "cp (s' @ s) th' = prec |
|
893 th s"}. |
|
894 \end{itemize} |
890 \end{theorem} |
895 \end{theorem} |
891 |
896 |
892 \noindent This theorem ensures that the thread @{text th}, which has |
897 \noindent This theorem ensures that the thread @{text th}, which has |
893 the highest precedence in the state @{text s}, can only be blocked |
898 the highest precedence in the state @{text s}, is either running in |
894 in the state @{text "s' @ s"} by a thread @{text th'} that already |
899 state @{term "s' @ s"}, or can only be blocked in the state @{text |
895 existed in @{text s} and requested or had a lock on at least one |
900 "s' @ s"} by a thread @{text th'} that already existed in @{text s} |
896 resource---that means the thread was not \emph{detached} in @{text |
901 and requested or had a lock on at least one resource---that means |
897 s}. As we shall see shortly, that means there are only finitely |
902 the thread was not \emph{detached} in @{text s}. As we shall see |
898 many threads that can block @{text th} in this way and then they |
903 shortly, that means there are only finitely many threads that can |
899 need to run with the same precedence as @{text th}. |
904 block @{text th} in this way and then they need to run with the same |
|
905 precedence as @{text th}. |
900 |
906 |
901 Like in the argument by Sha et al.~our finite bound does not |
907 Like in the argument by Sha et al.~our finite bound does not |
902 guarantee absence of indefinite Priority Inversion. For this we |
908 guarantee absence of indefinite Priority Inversion. For this we |
903 further have to assume that every thread gives up its resources |
909 further have to assume that every thread gives up its resources |
904 after a finite amount of time. We found that this assumption is |
910 after a finite amount of time. We found that this assumption is |