30 (*>*) |
28 (*>*) |
31 |
29 |
32 section {* Introduction *} |
30 section {* Introduction *} |
33 |
31 |
34 text {* |
32 text {* |
35 Many real-time systems need to support threads involving priorities and |
33 |
36 locking of resources. Locking of resources ensures mutual exclusion |
34 Many real-time systems need to support threads involving priorities |
37 when accessing shared data or devices that cannot be |
35 and locking of resources. Locking of resources ensures mutual |
|
36 exclusion when accessing shared data or devices that cannot be |
38 preempted. Priorities allow scheduling of threads that need to |
37 preempted. Priorities allow scheduling of threads that need to |
39 finish their work within deadlines. Unfortunately, both features |
38 finish their work within deadlines. Unfortunately, both features |
40 can interact in subtle ways leading to a problem, called |
39 can interact in subtle ways leading to a problem, called |
41 \emph{Priority Inversion}. Suppose three threads having priorities |
40 \emph{Priority Inversion}. Suppose three threads having priorities |
42 $H$(igh), $M$(edium) and $L$(ow). We would expect that the thread |
41 $H$(igh), $M$(edium) and $L$(ow). We would expect that the thread |
43 $H$ blocks any other thread with lower priority and the thread itself cannot |
42 $H$ blocks any other thread with lower priority and the thread |
44 be blocked indefinitely by threads with lower priority. Alas, in a naive |
43 itself cannot be blocked indefinitely by threads with lower |
45 implementation of resource locking and priorities this property can |
44 priority. Alas, in a naive implementation of resource locking and |
46 be violated. For this let $L$ be in the |
45 priorities this property can be violated. For this let $L$ be in the |
47 possession of a lock for a resource that $H$ also needs. $H$ must |
46 possession of a lock for a resource that $H$ also needs. $H$ must |
48 therefore wait for $L$ to exit the critical section and release this |
47 therefore wait for $L$ to exit the critical section and release this |
49 lock. The problem is that $L$ might in turn be blocked by any |
48 lock. The problem is that $L$ might in turn be blocked by any thread |
50 thread with priority $M$, and so $H$ sits there potentially waiting |
49 with priority $M$, and so $H$ sits there potentially waiting |
51 indefinitely. Since $H$ is blocked by threads with lower |
50 indefinitely. Since $H$ is blocked by threads with lower priorities, |
52 priorities, the problem is called Priority Inversion. It was first |
51 the problem is called Priority Inversion. It was first described in |
53 described in \cite{Lampson80} in the context of the |
52 \cite{Lampson80} in the context of the Mesa programming language |
54 Mesa programming language designed for concurrent programming. |
53 designed for concurrent programming. |
55 |
54 |
56 If the problem of Priority Inversion is ignored, real-time systems |
55 If the problem of Priority Inversion is ignored, real-time systems |
57 can become unpredictable and resulting bugs can be hard to diagnose. |
56 can become unpredictable and resulting bugs can be hard to diagnose. |
58 The classic example where this happened is the software that |
57 The classic example where this happened is the software that |
59 controlled the Mars Pathfinder mission in 1997 \cite{Reeves98}. |
58 controlled the Mars Pathfinder mission in 1997 \cite{Reeves98}. On |
60 On Earth the software run mostly without any problem, but |
59 Earth the software run mostly without any problem, but once the |
61 once the spacecraft landed on Mars, it shut down at irregular, but frequent, |
60 spacecraft landed on Mars, it shut down at irregular, but frequent, |
62 intervals leading to loss of project time as normal operation of the |
61 intervals leading to loss of project time as normal operation of the |
63 craft could only resume the next day (the mission and data already |
62 craft could only resume the next day (the mission and data already |
64 collected were fortunately not lost, because of a clever system |
63 collected were fortunately not lost, because of a clever system |
65 design). The reason for the shutdowns was that the scheduling |
64 design). The reason for the shutdowns was that the scheduling |
66 software fell victim to Priority Inversion: a low priority thread |
65 software fell victim to Priority Inversion: a low priority thread |
67 locking a resource prevented a high priority thread from running in |
66 locking a resource prevented a high priority thread from running in |
68 time, leading to a system reset. Once the problem was found, it was |
67 time, leading to a system reset. Once the problem was found, it was |
69 rectified by enabling the \emph{Priority Inheritance Protocol} (PIP) |
68 rectified by enabling the \emph{Priority Inheritance Protocol} (PIP) |
70 \cite{Sha90}\footnote{Sha et al.~call it the \emph{Basic Priority |
69 \cite{Sha90}\footnote{Sha et al.~call it the \emph{Basic Priority |
71 Inheritance Protocol} \cite{Sha90} and others sometimes also call it |
70 Inheritance Protocol} \cite{Sha90} and others sometimes also call it |
72 \emph{Priority Boosting}, \emph{Priority Donation} or \emph{Priority Lending}.} |
71 \emph{Priority Boosting}, \emph{Priority Donation} or \emph{Priority |
73 in the scheduling software. |
72 Lending}.} in the scheduling software. |
74 |
73 |
75 The idea behind PIP is to let the thread $L$ temporarily inherit |
74 The idea behind PIP is to let the thread $L$ temporarily inherit the |
76 the high priority from $H$ until $L$ leaves the critical section |
75 high priority from $H$ until $L$ leaves the critical section |
77 unlocking the resource. This solves the problem of $H$ having to |
76 unlocking the resource. This solves the problem of $H$ having to |
78 wait indefinitely, because $L$ cannot be blocked by threads having |
77 wait indefinitely, because $L$ cannot be blocked by threads having |
79 priority $M$. While a few other solutions exist for the Priority |
78 priority $M$. While a few other solutions exist for the Priority |
80 Inversion problem, PIP is one that is widely deployed and |
79 Inversion problem, PIP is one that is widely deployed and |
81 implemented. This includes VxWorks (a proprietary real-time OS used |
80 implemented. This includes VxWorks (a proprietary real-time OS used |
82 in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, Honda's |
81 in the Mars Pathfinder mission, in Boeing's 787 Dreamliner, Honda's |
83 ASIMO robot, etc.) and ThreadX (another proprietary real-time OS |
82 ASIMO robot, etc.) and ThreadX (another proprietary real-time OS |
84 used in nearly all HP inkjet printers \cite{ThreadX}), but also |
83 used in nearly all HP inkjet printers \cite{ThreadX}), but also the |
85 the POSIX 1003.1c Standard realised for |
84 POSIX 1003.1c Standard realised for example in libraries for |
86 example in libraries for FreeBSD, Solaris and Linux. |
85 FreeBSD, Solaris and Linux. |
87 |
86 |
88 Two advantages of PIP are that it is deterministic and that increasing the priority of a thread |
87 Two advantages of PIP are that it is deterministic and that |
89 can be performed dynamically by the scheduler. |
88 increasing the priority of a thread can be performed dynamically by |
90 This is in contrast to \emph{Priority Ceiling} |
89 the scheduler. This is in contrast to \emph{Priority Ceiling} |
91 \cite{Sha90}, another solution to the Priority Inversion problem, |
90 \cite{Sha90}, another solution to the Priority Inversion problem, |
92 which requires static analysis of the program in order to prevent |
91 which requires static analysis of the program in order to prevent |
93 Priority Inversion, and also in contrast to the approach taken in the Windows NT scheduler, which avoids |
92 Priority Inversion, and also in contrast to the approach taken in |
94 this problem by randomly boosting the priority of ready low-priority threads |
93 the Windows NT scheduler, which avoids this problem by randomly |
95 (see for instance~\cite{WINDOWSNT}). |
94 boosting the priority of ready low-priority threads (see for |
96 However, there has also been strong criticism against |
95 instance~\cite{WINDOWSNT}). However, there has also been strong |
97 PIP. For instance, PIP cannot prevent deadlocks when lock |
96 criticism against PIP. For instance, PIP cannot prevent deadlocks |
98 dependencies are circular, and also blocking times can be |
97 when lock dependencies are circular, and also blocking times can be |
99 substantial (more than just the duration of a critical section). |
98 substantial (more than just the duration of a critical section). |
100 Though, most criticism against PIP centres around unreliable |
99 Though, most criticism against PIP centres around unreliable |
101 implementations and PIP being too complicated and too inefficient. |
100 implementations and PIP being too complicated and too inefficient. |
102 For example, Yodaiken writes in \cite{Yodaiken02}: |
101 For example, Yodaiken writes in \cite{Yodaiken02}: |
103 |
102 |
104 \begin{quote} |
103 \begin{quote} |
105 \it{}``Priority inheritance is neither efficient nor reliable. Implementations |
104 \it{}``Priority inheritance is neither efficient nor reliable. Implementations |
106 are either incomplete (and unreliable) or surprisingly complex and intrusive.'' |
105 are either incomplete (and unreliable) or surprisingly complex and intrusive.'' |
107 \end{quote} |
106 \end{quote} |
108 |
107 |
109 \noindent |
108 \noindent He suggests avoiding PIP altogether by designing the |
110 He suggests avoiding PIP altogether by designing the system so that no |
109 system so that no priority inversion may happen in the first |
111 priority inversion may happen in the first place. However, such ideal designs may |
110 place. However, such ideal designs may not always be achievable in |
112 not always be achievable in practice. |
111 practice. |
113 |
112 |
114 In our opinion, there is clearly a need for investigating correct |
113 In our opinion, there is clearly a need for investigating correct |
115 algorithms for PIP. A few specifications for PIP exist (in English) |
114 algorithms for PIP. A few specifications for PIP exist (in informal |
116 and also a few high-level descriptions of implementations (e.g.~in |
115 English) and also a few high-level descriptions of implementations |
117 the textbooks \cite[Section 12.3.1]{Liu00} and \cite[Section 5.6.5]{Vahalia96}), |
116 (e.g.~in the textbooks \cite[Section 12.3.1]{Liu00} and |
118 but they help little with actual implementations. That this is a problem in |
117 \cite[Section 5.6.5]{Vahalia96}), but they help little with actual |
119 practice is proved by an email by Baker, who wrote on 13 July 2009 on the Linux |
118 implementations. That this is a problem in practice is proved by an |
120 Kernel mailing list: |
119 email by Baker, who wrote on 13 July 2009 on the Linux Kernel |
|
120 mailing list: |
121 |
121 |
122 \begin{quote} |
122 \begin{quote} |
123 \it{}``I observed in the kernel code (to my disgust), the Linux PIP |
123 \it{}``I observed in the kernel code (to my disgust), the Linux PIP |
124 implementation is a nightmare: extremely heavy weight, involving |
124 implementation is a nightmare: extremely heavy weight, involving |
125 maintenance of a full wait-for graph, and requiring updates for a |
125 maintenance of a full wait-for graph, and requiring updates for a |
126 range of events, including priority changes and interruptions of |
126 range of events, including priority changes and interruptions of |
127 wait operations.'' |
127 wait operations.'' |
128 \end{quote} |
128 \end{quote} |
129 |
129 |
130 \noindent |
130 \noindent The criticism by Yodaiken, Baker and others suggests |
131 The criticism by Yodaiken, Baker and others suggests another look |
131 another look at PIP from a more abstract level (but still concrete |
132 at PIP from a more abstract level (but still concrete enough |
132 enough to inform an implementation), and makes PIP a good candidate |
133 to inform an implementation), and makes PIP a good candidate for a |
133 for a formal verification. An additional reason is that the original |
134 formal verification. An additional reason is that the original |
|
135 specification of PIP~\cite{Sha90}, despite being informally |
134 specification of PIP~\cite{Sha90}, despite being informally |
136 ``proved'' correct, is actually \emph{flawed}. |
135 ``proved'' correct, is actually \emph{flawed}. |
137 |
136 |
138 |
|
139 Yodaiken \cite{Yodaiken02} and also Moylan et |
137 Yodaiken \cite{Yodaiken02} and also Moylan et |
140 al.~\cite{deinheritance} point to a subtlety that had been |
138 al.~\cite{deinheritance} point to a subtlety that had been |
141 overlooked in the informal proof by Sha et al. They specify in |
139 overlooked in the informal proof by Sha et al. They specify PIP in |
142 \cite{Sha90} that after the thread (whose priority has been raised) |
140 \cite{Sha90} so that after the thread (whose priority has been |
143 completes its critical section and releases the lock, it ``{\it |
141 raised) completes its critical section and releases the lock, it |
144 returns to its original priority level}''. This leads them to |
142 ``{\it returns to its original priority level}''. This leads them to |
145 believe that an implementation of PIP is ``{\it rather |
143 believe that an implementation of PIP is ``{\it rather |
146 straightforward}''~\cite{Sha90}. Unfortunately, as Yodaiken and |
144 straightforward}''~\cite{Sha90}. Unfortunately, as Yodaiken and |
147 Moylan et al.~point out, this behaviour is too simplistic. Moylan et |
145 Moylan et al.~point out, this behaviour is too simplistic. Moylan et |
148 al.~write that there are ``{\it some hidden traps}''~\cite{deinheritance}. Consider the |
146 al.~write that there are ``{\it some hidden |
149 case where the low priority thread $L$ locks \emph{two} resources, |
147 traps}''~\cite{deinheritance}. Consider the case where the low |
150 and two high-priority threads $H$ and $H'$ each wait for one of |
148 priority thread $L$ locks \emph{two} resources, and two |
151 them. If $L$ releases one resource so that $H$, say, can proceed, |
149 high-priority threads $H$ and $H'$ each wait for one of them. If |
152 then we still have Priority Inversion with $H'$ (which waits for the |
150 $L$ releases one resource so that $H$, say, can proceed, then we |
153 other resource). The correct behaviour for $L$ is to switch to the |
151 still have Priority Inversion with $H'$ (which waits for the other |
154 highest remaining priority of the threads that it blocks. |
152 resource). The correct behaviour for $L$ is to switch to the highest |
155 A similar |
153 remaining priority of the threads that it blocks. A similar error |
156 error is made in the textbook \cite[Section 2.3.1]{book} which |
154 is made in the textbook \cite[Section 2.3.1]{book} which specifies |
157 specifies for a process that inherited a higher priority and exits a |
155 for a process that inherited a higher priority and exits a critical |
158 critical section ``{\it it resumes the priority it had at the point |
156 section ``{\it it resumes the priority it had at the point of entry |
159 of entry into the critical section}''. This error can also be |
157 into the critical section}''. This error can also be found in the |
160 found in the more recent textbook \cite[Page 119]{Laplante11} where the |
158 more recent textbook \cite[Page 119]{Laplante11} where the authors |
161 authors state: ``{\it when [the task] exits the critical section that caused |
159 state: ``{\it when [the task] exits the critical section that caused |
162 the block, it reverts to the priority it had when it entered that |
160 the block, it reverts to the priority it had when it entered that |
163 section}''. The textbook \cite[Page 286]{Liu00} contains a simlar |
161 section}''. The textbook \cite[Page 286]{Liu00} contains a simlar |
164 flawed specification and even goes on to develop pseudo-code based on this |
162 flawed specification and even goes on to develop pseudo-code based |
165 flawed specification. Accordingly, the operating system primitives |
163 on this flawed specification. Accordingly, the operating system |
166 for inheritance and restoration of priorities in \cite{Liu00} depend on |
164 primitives for inheritance and restoration of priorities in |
167 maintaining a data structure called \emph{inheritance log}. This log |
165 \cite{Liu00} depend on maintaining a data structure called |
168 is maintained for every thread and broadly specified as containing ``{\it |
166 \emph{inheritance log}. This log is maintained for every thread and |
169 [h]istorical information on how the thread inherited its current |
167 broadly specified as containing ``{\it [h]istorical information on |
170 priority}'' \cite[Page 527]{Liu00}. Unfortunately, the important |
168 how the thread inherited its current priority}'' \cite[Page |
171 information about actually |
169 527]{Liu00}. Unfortunately, the important information about actually |
172 computing the priority to be restored solely from this log is not explained in |
170 computing the priority to be restored solely from this log is not |
173 \cite{Liu00} but left as an ``{\it excercise}'' to the reader. |
171 explained in \cite{Liu00} but left as an ``{\it excercise}'' to the |
174 Of course, a correct version of PIP does not need to maintain |
172 reader. Of course, a correct version of PIP does not need to |
175 this (potentially expensive) data structure at all. Surprisingly |
173 maintain this (potentially expensive) data structure at |
176 also the widely read and frequently updated textbook \cite{Silberschatz13} gives |
174 all. Surprisingly also the widely read and frequently updated |
177 the wrong specification. For example on Page 254 the |
175 textbook \cite{Silberschatz13} gives the wrong specification. For |
178 authors write: ``{\it Upon releasing the lock, the [low-priority] thread |
176 example on Page 254 the authors write: ``{\it Upon releasing the |
179 will revert to its original priority.}'' The same error is also repeated |
177 lock, the [low-priority] thread will revert to its original |
180 later in this textbook. |
178 priority.}'' The same error is also repeated later in this textbook. |
181 |
179 |
182 |
180 |
183 While \cite{Laplante11,Liu00,book,Sha90,Silberschatz13} are the only formal publications we have |
181 While \cite{Laplante11,Liu00,book,Sha90,Silberschatz13} are the only formal publications we have |
184 found that specify the incorrect behaviour, it seems also many |
182 found that specify the incorrect behaviour, it seems also many |
185 informal descriptions of PIP overlook the possibility that another |
183 informal descriptions of PIP overlook the possibility that another |