57 |
57 |
58 If the problem of Priority Inversion is ignored, real-time systems |
58 If the problem of Priority Inversion is ignored, real-time systems |
59 can become unpredictable and resulting bugs can be hard to diagnose. |
59 can become unpredictable and resulting bugs can be hard to diagnose. |
60 The classic example where this happened is the software that |
60 The classic example where this happened is the software that |
61 controlled the Mars Pathfinder mission in 1997 \cite{Reeves98}. |
61 controlled the Mars Pathfinder mission in 1997 \cite{Reeves98}. |
62 Once the spacecraft landed, the software shut down at irregular |
62 On Earth the software run mostly without any problem, but |
|
63 once the spacecraft landed on Mars, it shut down at irregular |
63 intervals leading to loss of project time as normal operation of the |
64 intervals leading to loss of project time as normal operation of the |
64 craft could only resume the next day (the mission and data already |
65 craft could only resume the next day (the mission and data already |
65 collected were fortunately not lost, because of a clever system |
66 collected were fortunately not lost, because of a clever system |
66 design). The reason for the shutdowns was that the scheduling |
67 design). The reason for the shutdowns was that the scheduling |
67 software fell victim to Priority Inversion: a low priority thread |
68 software fell victim to Priority Inversion: a low priority thread |
134 to inform an implementation), and makes PIP a good candidate for a |
135 to inform an implementation), and makes PIP a good candidate for a |
135 formal verification. An additional reason is that the original |
136 formal verification. An additional reason is that the original |
136 presentation of PIP~\cite{Sha90}, despite being informally |
137 presentation of PIP~\cite{Sha90}, despite being informally |
137 ``proved'' correct, is actually \emph{flawed}. |
138 ``proved'' correct, is actually \emph{flawed}. |
138 |
139 |
139 Yodaiken \cite{Yodaiken02} points to a subtlety that had been |
140 Yodaiken \cite{Yodaiken02} and also Moylan et al.~\cite{deinheritance} |
|
141 point to a subtlety that had been |
140 overlooked in the informal proof by Sha et al. They specify in |
142 overlooked in the informal proof by Sha et al. They specify in |
141 \cite{Sha90} that after the thread (whose priority has been raised) |
143 \cite{Sha90} that after the thread (whose priority has been raised) |
142 completes its critical section and releases the lock, it ``returns |
144 completes its critical section and releases the lock, it ``returns |
143 to its original priority level.'' This leads them to believe that an |
145 to its original priority level.'' This leads them to believe that an |
144 implementation of PIP is ``rather straightforward''~\cite{Sha90}. |
146 implementation of PIP is ``rather straightforward''~\cite{Sha90}. |
145 Unfortunately, as Yodaiken points out, this behaviour is too |
147 Unfortunately, as Yodaiken and Moylan et al.~point out, this behaviour is too |
146 simplistic. Consider the case where the low priority thread $L$ |
148 simplistic. Consider the case where the low priority thread $L$ |
147 locks \emph{two} resources, and two high-priority threads $H$ and |
149 locks \emph{two} resources, and two high-priority threads $H$ and |
148 $H'$ each wait for one of them. If $L$ releases one resource |
150 $H'$ each wait for one of them. If $L$ releases one resource |
149 so that $H$, say, can proceed, then we still have Priority Inversion |
151 so that $H$, say, can proceed, then we still have Priority Inversion |
150 with $H'$ (which waits for the other resource). The correct |
152 with $H'$ (which waits for the other resource). The correct |
151 behaviour for $L$ is to switch to the highest remaining priority of |
153 behaviour for $L$ is to switch to the highest remaining priority of |
152 the threads that it blocks. While |
154 the threads that it blocks. A similar error is made in the textbook |
153 \cite{Sha90} is the only formal publication we have |
155 \cite[Section 2.3.1]{book} which specifies for a process that |
154 found that describes the incorrect behaviour, not all, but many |
156 inherited a higher priority and exits a critical section ``it resumes |
|
157 the priority it had at the point of entry into the critical section''. |
|
158 |
|
159 While \cite{book} and |
|
160 \cite{Sha90} are the only formal publication we have |
|
161 found that describe the incorrect behaviour, not all, but many |
155 informal\footnote{informal as in ``found on the Web''} |
162 informal\footnote{informal as in ``found on the Web''} |
156 descriptions of PIP overlook the possibility that another |
163 descriptions of PIP overlook the possibility that another |
157 high-priority might wait for a low-priority process to finish. |
164 high-priority might wait for a low-priority process to finish. |
158 The advantage of formalising the |
165 The advantage of formalising the |
159 correctness of a high-level specification of PIP in a theorem prover |
166 correctness of a high-level specification of PIP in a theorem prover |
681 thread is guaranteed to run eventually. The assumption is that |
688 thread is guaranteed to run eventually. The assumption is that |
682 programmers must ensure that threads are programmed in this way. However, even |
689 programmers must ensure that threads are programmed in this way. However, even |
683 taking this assumption into account, the correctness properties of |
690 taking this assumption into account, the correctness properties of |
684 Sha et al.~are |
691 Sha et al.~are |
685 \emph{not} true for their version of PIP---despite being ``proved''. As Yodaiken |
692 \emph{not} true for their version of PIP---despite being ``proved''. As Yodaiken |
686 \cite{Yodaiken02} pointed out: If a low-priority thread possesses |
693 \cite{Yodaiken02} and Moylan et al.~\cite{deinheritance} pointed out: If a low-priority thread possesses |
687 locks to two resources for which two high-priority threads are |
694 locks to two resources for which two high-priority threads are |
688 waiting for, then lowering the priority prematurely after giving up |
695 waiting for, then lowering the priority prematurely after giving up |
689 only one lock, can cause indefinite Priority Inversion for one of the |
696 only one lock, can cause indefinite Priority Inversion for one of the |
690 high-priority threads, invalidating their two bounds. |
697 high-priority threads, invalidating their two bounds. |
691 |
698 |