28 therefore wait for $L$ to exit the critical section and release this |
28 therefore wait for $L$ to exit the critical section and release this |
29 lock. The problem is that $L$ might in turn be blocked by any |
29 lock. The problem is that $L$ might in turn be blocked by any |
30 process with priority $M$, and so $H$ sits there potentially waiting |
30 process with priority $M$, and so $H$ sits there potentially waiting |
31 indefinitely. Since $H$ is blocked by processes with lower |
31 indefinitely. Since $H$ is blocked by processes with lower |
32 priorities, the problem is called Priority Inversion. It was first |
32 priorities, the problem is called Priority Inversion. It was first |
33 described in \cite{Lampson:Redell:cacm:1980} in the context of the |
33 described in \cite{Lampson80} in the context of the |
34 Mesa programming language designed for concurrent programming. |
34 Mesa programming language designed for concurrent programming. |
35 |
35 |
36 If the problem of Priority Inversion is ignored, real-time systems |
36 If the problem of Priority Inversion is ignored, real-time systems |
37 can become unpredictable and resulting bugs can be hard to diagnose. |
37 can become unpredictable and resulting bugs can be hard to diagnose. |
38 The classic example where this happened is the software that |
38 The classic example where this happened is the software that |
39 controlled the Mars Pathfinder mission in 1997 |
39 controlled the Mars Pathfinder mission in 1997 |
40 \cite{Reeves-Glenn-1998}. Once the spacecraft landed, the software |
40 \cite{Reeves98}. Once the spacecraft landed, the software |
41 shut down at irregular intervals leading to loss of project time as |
41 shut down at irregular intervals leading to loss of project time as |
42 normal operation of the craft could only resume the next day (the |
42 normal operation of the craft could only resume the next day (the |
43 mission and data already collected were fortunately not lost, because |
43 mission and data already collected were fortunately not lost, because |
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{journals/tc/ShaRL90} 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 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 |
56 solutions exist for the Priority Inversion problem, PIP is one that is widely deployed |
57 \cite{Lampson:Redell:cacm:1980}, PIP is one that is widely deployed |
|
58 and implemented. This includes VxWorks (a proprietary real-time OS |
57 and implemented. This includes VxWorks (a proprietary real-time OS |
59 used in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, |
58 used in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, |
60 Honda's ASIMO robot, etc.), but also the POSIX 1003.1c Standard |
59 Honda's ASIMO robot, etc.), but also the POSIX 1003.1c Standard |
61 realised for example in libraries for FreeBSD, Solaris and Linux. |
60 realised for example in libraries for FreeBSD, Solaris and Linux. |
62 |
61 |
63 One advantage of PIP is that increasing the priority of a process |
62 One advantage of PIP is that increasing the priority of a process |
64 can be dynamically calculated by the scheduler. This is in contrast |
63 can be dynamically calculated by the scheduler. This is in contrast |
65 to, for example, \emph{Priority Ceiling}, another solution to the |
64 to, for example, \emph{Priority Ceiling} \cite{Sha90}, another |
66 Priority Inversion problem, which requires static analysis of the |
65 solution to the Priority Inversion problem, which requires static |
67 program in order to be helpful. However, there has also been strong |
66 analysis of the program in order to be helpful. However, there has |
68 criticism against PIP. For instance, PIP cannot prevent deadlocks, |
67 also been strong criticism against PIP. For instance, PIP cannot |
69 and also blocking times can be substantial (more than just the |
68 prevent deadlocks when lock dependencies are circular, and also |
70 duration of a critical section). Though, most criticism against PIP |
69 blocking times can be substantial (more than just the duration of a |
71 centres around unreliable implementations and around PIP being |
70 critical section). Though, most criticism against PIP centres |
72 too complicated and too inefficient. For example, Yodaiken writes in \cite{Yodaiken02}: |
71 around unreliable implementations and PIP being too complicated and |
|
72 too inefficient. For example, Yodaiken writes in \cite{Yodaiken02}: |
73 |
73 |
74 \begin{quote} |
74 \begin{quote} |
75 \it{}``Priority inheritance is neither efficient nor reliable. Implementations |
75 \it{}``Priority inheritance is neither efficient nor reliable. Implementations |
76 are either incomplete (and unreliable) or surprisingly complex and intrusive.'' |
76 are either incomplete (and unreliable) or surprisingly complex and intrusive.'' |
77 \end{quote} |
77 \end{quote} |
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 was a sensible solution in |
81 sections to be preempted. While this might have been a reasonable |
82 2002, in our modern multiprocessor world, this seems out of date. |
82 solution in 2002, in our modern multiprocessor world, this seems out |
83 However, there is clearly a need for investigating correct and |
83 of date. However, there is clearly a need for investigating correct |
84 efficient algorithms for PIP. A few specifications for PIP exist (in |
84 and efficient algorithms for PIP. A few specifications for PIP exist |
85 English) and also a few high-level descriptions of implementations |
85 (in English) and also a few high-level descriptions of |
86 (e.g.~in the textbook \cite[Section 5.6.5]{Vahalia96}), but they help little with |
86 implementations (e.g.~in the textbook \cite[Section |
87 actual implementations. That this is a problem in practise is proved |
87 5.6.5]{Vahalia96}), but they help little with actual |
88 by an email from Baker, who wrote on 13 July 2009 on the Linux |
88 implementations. That this is a problem in practise is proved by an |
89 Kernel mailing list: |
89 email by Baker, who wrote on 13 July 2009 on the Linux Kernel |
|
90 mailing list: |
90 |
91 |
91 \begin{quote} |
92 \begin{quote} |
92 \it{}``I observed in the kernel code (to my disgust), the Linux PIP |
93 \it{}``I observed in the kernel code (to my disgust), the Linux PIP |
93 implementation is a nightmare: extremely heavy weight, involving |
94 implementation is a nightmare: extremely heavy weight, involving |
94 maintenance of a full wait-for graph, and requiring updates for a |
95 maintenance of a full wait-for graph, and requiring updates for a |
95 range of events, including priority changes and interruptions of |
96 range of events, including priority changes and interruptions of |
96 wait operations.'' |
97 wait operations.'' |
97 \end{quote} |
98 \end{quote} |
98 |
99 |
99 \noindent |
100 \noindent |
100 This however means it is useful to look at PIP again from a more |
101 The criticism by Yodaiken, Baker and others suggests to us to look |
101 abstract level (but still concrete enough to inform an |
102 again at PIP from a more abstract level (but still concrete enough |
102 implementation) and makes PIP an ideal candidate for a formal |
103 to inform an implementation) and makes PIP an ideal candidate for a |
103 verification. One reason, of course, is that the original |
104 formal verification. One reason, of course, is that the original |
104 presentation of PIP, despite being informally ``proved'' correct, is |
105 presentation of PIP \cite{Sha90}, despite being |
105 flawed. Yodaiken \cite{Yodaiken02} points to a subtlety that has |
106 informally ``proved'' correct, is actually \emph{flawed}. Yodaiken |
106 been overlooked by Sha et al. |
107 \cite{Yodaiken02} points to a subtlety that had been overlooked by |
|
108 Sha et al. They write in \cite{Sha90} |
107 |
109 |
108 But this is too |
110 But this is too |
109 simplistic. Consider |
111 simplistic. Consider |
110 Priority Inversion problem has been known since 1980 |
112 Priority Inversion problem has been known since 1980 |
111 \cite{Lampson:Redell:cacm:1980}, but Sha et al.~give the first |
113 \cite{Lampson80}, but Sha et al.~give the first |
112 thorough analysis and present an informal correctness proof for PIP |
114 thorough analysis and present an informal correctness proof for PIP |
113 .\footnote{Sha et al.~call it the |
115 .\footnote{Sha et al.~call it the |
114 \emph{Basic Priority Inheritance Protocol}.} |
116 \emph{Basic Priority Inheritance Protocol}.} |
115 |
117 |
116 POSIX.4: programming for the real world (Google eBook) |
118 POSIX.4: programming for the real world (Google eBook) |
123 |
125 |
124 very little on implementations, not to mention implementations informed by |
126 very little on implementations, not to mention implementations informed by |
125 formal correctness proofs. |
127 formal correctness proofs. |
126 |
128 |
127 |
129 |
128 \noindent |
130 |
129 Priority inversion referrers to the phenomena where tasks with higher |
131 The priority inversion phenomenon was first published in \cite{Lampson80}. |
130 priority are blocked by ones with lower priority. If priority inversion |
|
131 is not controlled, there will be no guarantee the urgent tasks will be |
|
132 processed in time. As reported in \cite{Reeves-Glenn-1998}, |
|
133 priority inversion used to cause software system resets and data lose in |
|
134 JPL's Mars pathfinder project. Therefore, the avoiding, detecting and controlling |
|
135 of priority inversion is a key issue to attain predictability in priority |
|
136 based real-time systems. |
|
137 |
|
138 The priority inversion phenomenon was first published in \cite{Lampson:Redell:cacm:1980}. |
|
139 The two protocols widely used to eliminate priority inversion, namely |
132 The two protocols widely used to eliminate priority inversion, namely |
140 PI (Priority Inheritance) and PCE (Priority Ceiling Emulation), were proposed |
133 PI (Priority Inheritance) and PCE (Priority Ceiling Emulation), were proposed |
141 in \cite{journals/tc/ShaRL90}. PCE is less convenient to use because it requires |
134 in \cite{Sha90}. PCE is less convenient to use because it requires |
142 static analysis of programs. Therefore, PI is more commonly used in |
135 static analysis of programs. Therefore, PI is more commonly used in |
143 practice\cite{locke-july02}. However, as pointed out in the literature, |
136 practice\cite{locke-july02}. However, as pointed out in the literature, |
144 the analysis of priority inheritance protocol is quite subtle\cite{yodaiken-july02}. |
137 the analysis of priority inheritance protocol is quite subtle\cite{yodaiken-july02}. |
145 A formal analysis will certainly be helpful for us to understand and correctly |
138 A formal analysis will certainly be helpful for us to understand and correctly |
146 implement PI. All existing formal analysis of PI |
139 implement PI. All existing formal analysis of PI |