164 ``proved'' correct, is actually \emph{flawed}. |
164 ``proved'' correct, is actually \emph{flawed}. |
165 |
165 |
166 Yodaiken \cite{Yodaiken02} and also Moylan et |
166 Yodaiken \cite{Yodaiken02} and also Moylan et |
167 al.~\cite{deinheritance} point to a subtlety that had been |
167 al.~\cite{deinheritance} point to a subtlety that had been |
168 overlooked in the informal proof by Sha et al. They specify PIP in |
168 overlooked in the informal proof by Sha et al. They specify PIP in |
169 \cite{Sha90} so that after the thread (whose priority has been |
169 \cite[Section III]{Sha90} so that after the thread (whose priority has been |
170 raised) completes its critical section and releases the lock, it |
170 raised) completes its critical section and releases the lock, it |
171 ``{\it returns to its original priority level}''. This leads them to |
171 ``{\it returns to its original priority level}''. This leads them to |
172 believe that an implementation of PIP is ``{\it rather |
172 believe that an implementation of PIP is ``{\it rather |
173 straightforward}''~\cite{Sha90}. Unfortunately, as Yodaiken and |
173 straightforward}''~\cite{Sha90}. Unfortunately, as Yodaiken and |
174 Moylan et al.~point out, this behaviour is too simplistic. Moylan et |
174 Moylan et al.~point out, this behaviour is too simplistic. Moylan et |
810 @{thm readys_def}\\ |
810 @{thm readys_def}\\ |
811 @{thm running_def} |
811 @{thm running_def} |
812 \end{tabular} |
812 \end{tabular} |
813 \end{isabelle} |
813 \end{isabelle} |
814 |
814 |
815 \noindent |
815 \noindent In the second definition @{term "DUMMY ` DUMMY"} stands |
816 %%In the second definition @{term "DUMMY ` DUMMY"} stands for the image of a set under a function. |
816 for the image of a set under a function. Note that in the initial |
817 Note that in the initial state, that is where the list of events is empty, the set |
817 state, that is where the list of events is empty, the set @{term |
818 @{term threads} is empty and therefore there is neither a thread ready nor running. |
818 threads} is empty and therefore there is neither a thread ready nor |
819 If there is one or more threads ready, then there can only be \emph{one} thread |
819 running. If there is one or more threads ready, then there can only |
820 running, namely the one whose current precedence is equal to the maximum of all ready |
820 be \emph{one} thread running, namely the one whose current |
821 threads. We use sets to capture both possibilities. |
821 precedence is equal to the maximum of all ready threads. We use sets |
822 We can now also conveniently define the set of resources that are locked by a thread in a |
822 to capture both possibilities. We can now also conveniently define |
823 given state and also when a thread is detached in a state (meaning the thread neither |
823 the set of resources that are locked by a thread in a given state |
824 holds nor waits for a resource---in the RAG this would correspond to an |
824 and also when a thread is detached in a state (meaning the thread |
825 isolated node without any incoming and outgoing edges, see Figure~\ref{RAGgraph}): |
825 neither holds nor waits for a resource---in the RAG this would |
|
826 correspond to an isolated node without any incoming and outgoing |
|
827 edges, see Figure~\ref{RAGgraph}): |
826 |
828 |
827 \begin{isabelle}\ \ \ \ \ %%% |
829 \begin{isabelle}\ \ \ \ \ %%% |
828 \begin{tabular}{@ {}l} |
830 \begin{tabular}{@ {}l} |
829 @{thm holdents_def}\\ |
831 @{thm holdents_def}\\ |
830 @{thm detached_def} |
832 @{thm detached_def} |
991 ``proved''. As Yodaiken \cite{Yodaiken02} and Moylan et |
993 ``proved''. As Yodaiken \cite{Yodaiken02} and Moylan et |
992 al.~\cite{deinheritance} pointed out: If a low-priority thread |
994 al.~\cite{deinheritance} pointed out: If a low-priority thread |
993 possesses locks to two resources for which two high-priority threads |
995 possesses locks to two resources for which two high-priority threads |
994 are waiting for, then lowering the priority prematurely after giving |
996 are waiting for, then lowering the priority prematurely after giving |
995 up only one lock, can cause indefinite Priority Inversion for one of |
997 up only one lock, can cause indefinite Priority Inversion for one of |
996 the high-priority threads, invalidating their two bounds. |
998 the high-priority threads, invalidating their two bounds (recall the |
|
999 counter example described in the Introduction). |
997 |
1000 |
998 Even when fixed, their proof idea does not seem to go through for |
1001 Even when fixed, their proof idea does not seem to go through for |
999 us, because of the way we have set up our formal model of PIP. One |
1002 us, because of the way we have set up our formal model of PIP. One |
1000 reason is that we allow critical sections, which start with a @{text |
1003 reason is that we allow critical sections, which start with a @{text |
1001 P}-event and finish with a corresponding @{text V}-event, to |
1004 P}-event and finish with a corresponding @{text V}-event, to |
1007 @{text "s' @ s"}) in which @{text th} is still alive, either @{text |
1010 @{text "s' @ s"}) in which @{text th} is still alive, either @{text |
1008 th} is running or it is blocked by a thread that was alive in the |
1011 th} is running or it is blocked by a thread that was alive in the |
1009 state @{text s} and was waiting for or in the possession of a lock |
1012 state @{text s} and was waiting for or in the possession of a lock |
1010 in @{text s}. Since in @{text s}, as in every state, the set of |
1013 in @{text s}. Since in @{text s}, as in every state, the set of |
1011 alive threads is finite, @{text th} can only be blocked a finite |
1014 alive threads is finite, @{text th} can only be blocked a finite |
1012 number of times. This is independent of how many threads of lower |
1015 number of threads. This is independent of how many threads of lower |
1013 priority are created in @{text "s'"}. We will actually prove a |
1016 priority are created in @{text "s'"}. We will actually prove a |
1014 stronger statement where we also provide the current precedence of |
1017 stronger statement where we also provide the current precedence of |
1015 the blocking thread. |
1018 the blocking thread. |
1016 |
1019 |
1017 However, this correctness criterion hinges upon a number of |
1020 However, this correctness criterion hinges upon a number of |