61 |
61 |
62 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 |
63 can be dynamically calculated by the scheduler. This is in contrast |
63 can be dynamically calculated by the scheduler. This is in contrast |
64 to, for example, \emph{Priority Ceiling} \cite{Sha90}, another |
64 to, for example, \emph{Priority Ceiling} \cite{Sha90}, another |
65 solution to the Priority Inversion problem, which requires static |
65 solution to the Priority Inversion problem, which requires static |
66 analysis of the program in order to be helpful. However, there has |
66 analysis of the program in order to prevent Priority Inversion. However, there has |
67 also been strong criticism against PIP. For instance, PIP cannot |
67 also been strong criticism against PIP. For instance, PIP cannot |
68 prevent deadlocks when lock dependencies are circular, and also |
68 prevent deadlocks when lock dependencies are circular, and also |
69 blocking times can be substantial (more than just the duration of a |
69 blocking times can be substantial (more than just the duration of a |
70 critical section). Though, most criticism against PIP centres |
70 critical section). Though, most criticism against PIP centres |
71 around unreliable implementations and PIP being too complicated and |
71 around unreliable implementations and PIP being too complicated and |
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. The reason is that this precludes other high-priority |
83 of date. The reason is that this precludes other high-priority |
84 processes from running that do not make any use of the locked |
84 processes from running even when they do not make any use of the locked |
85 resource. |
85 resource. |
86 |
86 |
87 However, there is clearly a need for investigating correct |
87 However, there is clearly a need for investigating correct |
88 algorithms for PIP. A few specifications for PIP exist (in English) |
88 algorithms for PIP. A few specifications for PIP exist (in English) |
89 and also a few high-level descriptions of implementations (e.g.~in |
89 and also a few high-level descriptions of implementations (e.g.~in |
113 the lock, it ``returns to its original priority level.'' This leads |
113 the lock, it ``returns to its original priority level.'' This leads |
114 them to believe that an implementation of PIP is ``rather |
114 them to believe that an implementation of PIP is ``rather |
115 straightforward'' \cite{Sha90}. Unfortunately, as Yodaiken pointed |
115 straightforward'' \cite{Sha90}. Unfortunately, as Yodaiken pointed |
116 out, this behaviour is too simplistic. Consider the case where the |
116 out, this behaviour is too simplistic. Consider the case where the |
117 low priority process $L$ locks \emph{two} resources, and two |
117 low priority process $L$ locks \emph{two} resources, and two |
118 high-priority processes $H$ and $H'$, respectively, wait for one of |
118 high-priority processes $H$ and $H'$ each wait for one of |
119 them. If $L$ releases only one of them so that $H$, say, can |
119 them. If $L$ then releases one resource so that $H$, say, can |
120 proceed, then we still have Priority Inversion with $H'$: according |
120 proceed, then we still have Priority Inversion with $H'$. The correct |
121 to Sha et al., $L$ already dropped back to its low priority, but has not yet |
121 behaviour for $L$ |
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 |
122 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 |
123 blocks. The advantage of a formalisation of PIP in a theorem prover |
125 is that such issues clearly show up and cannot be dodged. |
124 is that such issues clearly show up and cannot be overlooked as in |
126 |
125 informal reasoning. |
127 There have been earlier formal investigations into PIP, but ... |
126 |
|
127 There have been earlier formal investigations into PIP, but ...\cite{Faria08} |
128 |
128 |
129 \bigskip |
129 \bigskip |
130 Priority Inversion problem has been known since 1980 |
130 Priority Inversion problem has been known since 1980 |
131 \cite{Lampson80}, but Sha et al.~give the first |
131 \cite{Lampson80}, but Sha et al.~give the first |
132 thorough analysis and present an informal correctness proof for PIP |
132 thorough analysis and present an informal correctness proof for PIP |