44 of a clever system design). The reason for the shutdowns was that |
44 of a clever system design). The reason for the shutdowns was that |
45 the scheduling software fell victim of Priority Inversion: a low |
45 the scheduling software fell victim of Priority Inversion: a low |
46 priority task locking a resource prevented a high priority process |
46 priority task locking a resource prevented a high priority process |
47 from running in time leading to a system reset. Once the problem was found, |
47 from running in time leading to a system reset. Once the problem was found, |
48 it was rectified by enabling the \emph{Priority Inheritance Protocol} |
48 it was rectified by enabling the \emph{Priority Inheritance Protocol} |
49 (PIP) \cite{Sha90} in the scheduling software. |
49 (PIP) \cite{Sha90}\footnote{Sha et al.~call it the |
|
50 \emph{Basic Priority Inheritance Protocol}.} in the scheduling software. |
50 |
51 |
51 The idea behind PIP is to let the process $L$ temporarily |
52 The idea behind PIP is to let the process $L$ temporarily |
52 inherit the high priority from $H$ until $L$ leaves the critical |
53 inherit the high priority from $H$ until $L$ leaves the critical |
53 section by unlocking the resource. This solves the problem of $H$ |
54 section by unlocking the resource. This solves the problem of $H$ |
54 having to wait indefinitely, because $L$ cannot, for example, be |
55 having to wait indefinitely, because $L$ cannot be |
55 blocked by processes having priority $M$. While a few other |
56 blocked by processes having priority $M$. While a few other |
56 solutions exist for the Priority Inversion problem, PIP is one that is widely deployed |
57 solutions exist for the Priority Inversion problem, PIP is one that is widely deployed |
57 and implemented. This includes VxWorks (a proprietary real-time OS |
58 and implemented. This includes VxWorks (a proprietary real-time OS |
58 used in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, |
59 used in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, |
59 Honda's ASIMO robot, etc.), but also the POSIX 1003.1c Standard |
60 Honda's ASIMO robot, etc.), but also the POSIX 1003.1c Standard |
105 again at PIP from a more abstract level (but still concrete enough |
106 again at PIP from a more abstract level (but still concrete enough |
106 to inform an implementation) and makes PIP an ideal candidate for a |
107 to inform an implementation) and makes PIP an ideal candidate for a |
107 formal verification. One reason, of course, is that the original |
108 formal verification. One reason, of course, is that the original |
108 presentation of PIP \cite{Sha90}, despite being informally |
109 presentation of PIP \cite{Sha90}, despite being informally |
109 ``proved'' correct, is actually \emph{flawed}. Yodaiken |
110 ``proved'' correct, is actually \emph{flawed}. Yodaiken |
110 \cite{Yodaiken02} points to a subtlety that had been overlooked by |
111 \cite{Yodaiken02} points to a subtlety that had been overlooked in |
111 Sha et al. They specify in \cite{Sha90} that after the process whose |
112 the informal proof by Sha et al. They specify in \cite{Sha90} that after the process (whose |
112 priority has been raised completes its critical section and releases |
113 priority has been raised) completes its critical section and releases |
113 the lock, it ``returns to its original priority level.'' This leads |
114 the lock, it ``returns to its original priority level.'' This leads |
114 them to believe that an implementation of PIP is ``rather |
115 them to believe that an implementation of PIP is ``rather |
115 straightforward'' \cite{Sha90}. Unfortunately, as Yodaiken pointed |
116 straightforward'' \cite{Sha90}. Unfortunately, as Yodaiken pointed |
116 out, this behaviour is too simplistic. Consider the case where the |
117 out, this behaviour is too simplistic. Consider the case where the |
117 low priority process $L$ locks \emph{two} resources, and two |
118 low priority process $L$ locks \emph{two} resources, and two |
118 high-priority processes $H$ and $H'$ each wait for one of |
119 high-priority processes $H$ and $H'$ each wait for one of |
119 them. If $L$ then releases one resource so that $H$, say, can |
120 them. If $L$ then releases one resource so that $H$, say, can |
120 proceed, then we still have Priority Inversion with $H'$. The correct |
121 proceed, then we still have Priority Inversion with $H'$ (which waits for |
121 behaviour for $L$ |
122 the other resource). The correct behaviour for $L$ |
122 is to revert to the highest remaining priority of processes which it |
123 is to revert to the highest remaining priority of processes that it |
123 blocks. The advantage of a formalisation of PIP in a theorem prover |
124 blocks. The advantage of a formalisation of the correctness of PIP |
124 is that such issues clearly show up and cannot be overlooked as in |
125 in a theorem prover is that such issues clearly show up and cannot |
125 informal reasoning. |
126 be overlooked as in informal reasoning (since we have to analyse all |
|
127 \emph{traces} that could possibly happen). |
126 |
128 |
127 There have been earlier formal investigations into PIP, but ...\cite{Faria08} |
129 There have been earlier formal investigations into PIP, but ...\cite{Faria08} |
128 |
130 *} |
|
131 |
|
132 section {* Preliminaries *} |
|
133 |
|
134 text {* |
|
135 Our formal model of PIP is based on Paulson's inductive approach to protocol |
|
136 verification, where the state of the system is modelled as a list of events |
|
137 that happened so far. \emph{Events} will use |
|
138 |
|
139 To define events, the identifiers of {\em threads}, |
|
140 {\em priority} and {\em critical resources } (abbreviated as @{text "cs"}) |
|
141 need to be represented. All three are represetned using standard |
|
142 Isabelle/HOL type @{typ "nat"}: |
|
143 *} |
|
144 |
|
145 text {* |
129 \bigskip |
146 \bigskip |
130 Priority Inversion problem has been known since 1980 |
|
131 \cite{Lampson80}, but Sha et al.~give the first |
|
132 thorough analysis and present an informal correctness proof for PIP |
|
133 .\footnote{Sha et al.~call it the |
|
134 \emph{Basic Priority Inheritance Protocol}.} |
|
135 |
|
136 POSIX.4: programming for the real world (Google eBook) |
|
137 |
|
138 However, there are further subtleties: just lowering the priority |
|
139 of the process $L$ to its low priority, as proposed in ???, is |
|
140 incorrect.\bigskip |
|
141 |
|
142 |
|
143 |
|
144 very little on implementations, not to mention implementations informed by |
|
145 formal correctness proofs. |
|
146 |
|
147 |
|
148 |
|
149 The priority inversion phenomenon was first published in \cite{Lampson80}. |
147 The priority inversion phenomenon was first published in \cite{Lampson80}. |
150 The two protocols widely used to eliminate priority inversion, namely |
148 The two protocols widely used to eliminate priority inversion, namely |
151 PI (Priority Inheritance) and PCE (Priority Ceiling Emulation), were proposed |
149 PI (Priority Inheritance) and PCE (Priority Ceiling Emulation), were proposed |
152 in \cite{Sha90}. PCE is less convenient to use because it requires |
150 in \cite{Sha90}. PCE is less convenient to use because it requires |
153 static analysis of programs. Therefore, PI is more commonly used in |
151 static analysis of programs. Therefore, PI is more commonly used in |