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} in the scheduling software. |
50 |
50 |
51 The idea behind PIP is to let the process $L$ temporarily |
51 The idea behind PIP is to let the process $L$ temporarily |
52 inherit the high priority from $H$ until $L$ leaves the critical |
52 inherit the high priority from $H$ until $L$ leaves the critical |
53 section unlocking the resource. This solves the problem of $H$ |
53 section by unlocking the resource. This solves the problem of $H$ |
54 having to wait indefinitely, because $L$ cannot, for example, be |
54 having to wait indefinitely, because $L$ cannot, for example, be |
55 blocked by processes having priority $M$. While a few other |
55 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 |
56 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 |
57 and implemented. This includes VxWorks (a proprietary real-time OS |
58 used in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, |
58 used in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, |
78 |
78 |
79 \noindent |
79 \noindent |
80 He suggests to avoid PIP altogether by not allowing critical |
80 He suggests to avoid PIP altogether by not allowing critical |
81 sections to be preempted. While this might have been a reasonable |
81 sections to be preempted. While this might have been a reasonable |
82 solution in 2002, in our modern multiprocessor world, this seems out |
82 solution in 2002, in our modern multiprocessor world, this seems out |
83 of date. However, there is clearly a need for investigating correct |
83 of date. The reason is that this precludes other high-priority |
84 and efficient algorithms for PIP. A few specifications for PIP exist |
84 processes from running that do not make any use of the locked |
85 (in English) and also a few high-level descriptions of |
85 resource. |
86 implementations (e.g.~in the textbook \cite[Section |
86 |
87 5.6.5]{Vahalia96}), but they help little with actual |
87 However, there is clearly a need for investigating correct |
88 implementations. That this is a problem in practise is proved by an |
88 algorithms for PIP. A few specifications for PIP exist (in English) |
89 email by Baker, who wrote on 13 July 2009 on the Linux Kernel |
89 and also a few high-level descriptions of implementations (e.g.~in |
90 mailing list: |
90 the textbook \cite[Section 5.6.5]{Vahalia96}), but they help little |
|
91 with actual implementations. That this is a problem in practise is |
|
92 proved by an email by Baker, who wrote on 13 July 2009 on the Linux |
|
93 Kernel mailing list: |
91 |
94 |
92 \begin{quote} |
95 \begin{quote} |
93 \it{}``I observed in the kernel code (to my disgust), the Linux PIP |
96 \it{}``I observed in the kernel code (to my disgust), the Linux PIP |
94 implementation is a nightmare: extremely heavy weight, involving |
97 implementation is a nightmare: extremely heavy weight, involving |
95 maintenance of a full wait-for graph, and requiring updates for a |
98 maintenance of a full wait-for graph, and requiring updates for a |
100 \noindent |
103 \noindent |
101 The criticism by Yodaiken, Baker and others suggests to us to look |
104 The criticism by Yodaiken, Baker and others suggests to us to look |
102 again at PIP from a more abstract level (but still concrete enough |
105 again at PIP from a more abstract level (but still concrete enough |
103 to inform an implementation) and makes PIP an ideal candidate for a |
106 to inform an implementation) and makes PIP an ideal candidate for a |
104 formal verification. One reason, of course, is that the original |
107 formal verification. One reason, of course, is that the original |
105 presentation of PIP \cite{Sha90}, despite being |
108 presentation of PIP \cite{Sha90}, despite being informally |
106 informally ``proved'' correct, is actually \emph{flawed}. Yodaiken |
109 ``proved'' correct, is actually \emph{flawed}. Yodaiken |
107 \cite{Yodaiken02} points to a subtlety that had been overlooked by |
110 \cite{Yodaiken02} points to a subtlety that had been overlooked by |
108 Sha et al. They write in \cite{Sha90} |
111 Sha et al. They specify in \cite{Sha90} that after the process whose |
109 |
112 priority has been raised completes its critical section and releases |
110 But this is too |
113 the lock, it ``returns to its original priority level.'' This leads |
111 simplistic. Consider |
114 them to believe that an implementation of PIP is ``rather |
|
115 straightforward'' \cite{Sha90}. Unfortunately, as Yodaiken pointed |
|
116 out, this behaviour is too simplistic. Consider the case where the |
|
117 low priority process $L$ locks \emph{two} resources, and two |
|
118 high-priority processes $H$ and $H'$, respectively, wait for one of |
|
119 them. If $L$ releases only one of them so that $H$, say, can |
|
120 proceed, then we still have Priority Inversion with $H'$: according |
|
121 to Sha et al., $L$ already dropped back to its low priority, but has not yet |
|
122 released the lock $H'$ is waiting for. Therefore the correct behaviour for $L$ |
|
123 is to revert to the highest remaining priority of processes which it |
|
124 blocks. The advantage of a formalisation of PIP in a theorem prover |
|
125 is that such issues clearly show up and cannot be dodged. |
|
126 |
|
127 There have been earlier formal investigations into PIP, but ... |
|
128 |
|
129 \bigskip |
112 Priority Inversion problem has been known since 1980 |
130 Priority Inversion problem has been known since 1980 |
113 \cite{Lampson80}, but Sha et al.~give the first |
131 \cite{Lampson80}, but Sha et al.~give the first |
114 thorough analysis and present an informal correctness proof for PIP |
132 thorough analysis and present an informal correctness proof for PIP |
115 .\footnote{Sha et al.~call it the |
133 .\footnote{Sha et al.~call it the |
116 \emph{Basic Priority Inheritance Protocol}.} |
134 \emph{Basic Priority Inheritance Protocol}.} |