50 The idea behind the \emph{Priority Inheritance Protocol} (PIP) |
50 The idea behind the \emph{Priority Inheritance Protocol} (PIP) |
51 \cite{journals/tc/ShaRL90} is to let the process $L$ temporarily |
51 \cite{journals/tc/ShaRL90} is to let the process $L$ temporarily |
52 inherit the high priority from $H$ until $L$ releases the locked |
52 inherit the high priority from $H$ until $L$ releases the locked |
53 resource. This solves the problem of $H$ having to wait |
53 resource. This solves the problem of $H$ having to wait |
54 indefinitely, because $L$ cannot, for example, be blocked by |
54 indefinitely, because $L$ cannot, for example, be blocked by |
55 processes having priority $M$. While a few other solutions to the Priority |
55 processes having priority $M$. While a few other solutions exist for the |
56 Inversion problem exists \cite{Lampson:Redell:cacm:1980}, PIP is one |
56 Priority Inversion problem \cite{Lampson:Redell:cacm:1980}, |
57 that is widely adopted and implemented [???Book] (where implemented???). |
57 PIP is one that is widely deployed and implemented, including in |
58 One advantage of PIP is that raising the priority of a process |
58 VxWorks (a proprietary real-time OS used in the Mars Pathfinder |
59 having a lock can be dynamically calculated. This is in contrast, |
59 mission, in Boeing's 787 Dreamliner, Honda's ASIMO robot, etc.), but |
60 for example, to Priority Ceiling which requires static analysis |
60 also as POSIX 1003.1c Standard, realised for example in libraries |
61 of the program in order to avoid Priority Inversion. |
61 for FreeBSD, Solaris and Linux. One advantage of PIP is that |
62 |
62 increasing the priority of a process can be dynamically |
63 However there has also been strong criticism against PIP |
63 calculated. This is in contrast to, for example, \emph{Priority Ceiling}---another |
|
64 solution to the Priority Inversion problem, which however |
|
65 requires static analysis of the program in order to be helpful. |
|
66 |
|
67 However there has also been strong criticism against using PIP. For |
|
68 example it cannot prevent deathlocks and also blocking times can be |
|
69 substantial (more than just the duration of a critical section). |
|
70 However, most criticism of PIP centres around unreliabale |
|
71 implementations of PIP and PIP being complex. For example, Y...writes: |
|
72 |
|
73 \begin{quote} |
|
74 \it{}``Priority inheritance is neither efficient nor reliable. Implementations |
|
75 are either incomplete (and unreliable) or surprisingly complex and intrusive.'' |
|
76 \end{quote} |
|
77 |
|
78 \noindent |
|
79 His solution is to avoid PIP altogether by not allowing critical sections to be |
|
80 pre-empted. While this might have been a sensible solution in 198..., in our |
|
81 modern multiprocessor world, this seems out of date. |
|
82 While there exists |
|
83 That there is a practical need |
|
84 |
|
85 Baker wrote on 13 July 2009 in the Linux Kernel mailing list: |
|
86 |
|
87 \begin{quote} |
|
88 \it{}``I observed in the kernel code |
|
89 (to my disgust), the Linux PIP implementation is a nightmare: |
|
90 extremely heavy weight, involving maintenance of a full wait-for |
|
91 graph, and requiring updates for a range of events, including |
|
92 priority changes and interruptions of wait operations.'' |
|
93 \end{quote} |
|
94 |
|
95 \noindent |
|
96 This however means it is useful to look at PIP again from a more |
|
97 abstract level (but still concrete enough to inform an efficient implementation) |
|
98 and makes it an ideal candidate for a formal verification. One reason |
|
99 is of course that the original presentation of PIP, including a correcness ``proof'', |
|
100 is flawed. Y... points out a subletly that has been overlooked by Sha et al. |
|
101 But this is too simplistic. Consider |
|
102 |
|
103 |
64 |
104 |
65 Priority Inversion problem has been known since 1980 |
105 Priority Inversion problem has been known since 1980 |
66 \cite{Lampson:Redell:cacm:1980}, but Sha et al.~give the first |
106 \cite{Lampson:Redell:cacm:1980}, but Sha et al.~give the first |
67 thorough analysis and present an informal correctness proof for PIP |
107 thorough analysis and present an informal correctness proof for PIP |
68 .\footnote{Sha et al.~call it the |
108 .\footnote{Sha et al.~call it the |
69 \emph{Basic Priority Inheritance Protocol}.} |
109 \emph{Basic Priority Inheritance Protocol}.} |
70 |
110 |
|
111 POSIX.4: programming for the real world (Google eBook) |
|
112 |
71 However, there are further subtleties: just lowering the priority |
113 However, there are further subtleties: just lowering the priority |
72 of the process $L$ to its low priority, as proposed in ???, is |
114 of the process $L$ to its low priority, as proposed in ???, is |
73 incorrect.\bigskip |
115 incorrect.\bigskip |
74 |
116 |
75 \begin{quote} |
117 |
76 \it{}``Priority inheritance is neither efficient nor reliable. Implementations |
|
77 are either incomplete (and unreliable) or surprisingly complex and intrusive.'' |
|
78 \end{quote} |
|
79 |
118 |
80 book: page 135, sec 5.6.5 |
119 book: page 135, sec 5.6.5 |
81 |
120 |
82 do you need axioms in the formalisation? |
121 |
|
122 |
|
123 |
|
124 |
|
125 very little on implementations, not to mention implementations informed by |
|
126 formal correctness proofs. |
|
127 |
83 |
128 |
84 \noindent |
129 \noindent |
85 Priority inversion referrers to the phenomena where tasks with higher |
130 Priority inversion referrers to the phenomena where tasks with higher |
86 priority are blocked by ones with lower priority. If priority inversion |
131 priority are blocked by ones with lower priority. If priority inversion |
87 is not controlled, there will be no guarantee the urgent tasks will be |
132 is not controlled, there will be no guarantee the urgent tasks will be |