136 substantial (more than just the duration of a critical section). |
136 substantial (more than just the duration of a critical section). |
137 Though, most criticism against PIP centres around unreliable |
137 Though, most criticism against PIP centres around unreliable |
138 implementations and PIP being too complicated and too inefficient. |
138 implementations and PIP being too complicated and too inefficient. |
139 For example, Yodaiken writes in \cite{Yodaiken02}: |
139 For example, Yodaiken writes in \cite{Yodaiken02}: |
140 |
140 |
141 \begin{quote} |
141 \begin{quote} \it{}``Priority inheritance is neither efficient nor |
142 \it{}``Priority inheritance is neither efficient nor reliable. Implementations |
142 reliable. Implementations are either incomplete (and unreliable) or |
143 are either incomplete (and unreliable) or surprisingly complex and intrusive.'' |
143 surprisingly complex and intrusive.'' \end{quote} |
144 \end{quote} |
|
145 |
144 |
146 \noindent He suggests avoiding PIP altogether by designing the |
145 \noindent He suggests avoiding PIP altogether by designing the |
147 system so that no priority inversion may happen in the first |
146 system so that no priority inversion may happen in the first |
148 place. However, such ideal designs may not always be achievable in |
147 place. However, such ideal designs may not always be achievable in |
149 practice. |
148 practice. |
2135 this section closely inform an implementation of PIP, namely whether the |
2134 this section closely inform an implementation of PIP, namely whether the |
2136 @{text RAG} needs to be reconfigured or current precedences need to |
2135 @{text RAG} needs to be reconfigured or current precedences need to |
2137 be recalculated for an event. This information is provided by the lemmas we proved. |
2136 be recalculated for an event. This information is provided by the lemmas we proved. |
2138 We confirmed that our observations translate into practice by implementing |
2137 We confirmed that our observations translate into practice by implementing |
2139 our version of PIP on top of PINTOS, a small operating system written in C and used for teaching at |
2138 our version of PIP on top of PINTOS, a small operating system written in C and used for teaching at |
2140 Stanford University \cite{PINTOS}. An alternative would have been the small Xv6 operating |
2139 Stanford University \cite{PINTOS}.\footnote{An alternative would have been the small Xv6 operating |
2141 system used for teaching at MIT \cite{Xv6link,Xv6}. However this operating system implements |
2140 system used for teaching at MIT \cite{Xv6link,Xv6}. However this operating system implements |
2142 a simple round robin scheduler that lacks stubs for dealing with priorities. This |
2141 a simple round robin scheduler that lacks stubs for dealing with priorities. This |
2143 is inconvenient for our purposes. |
2142 is inconvenient for our purposes.} While there is no formal connection between our |
|
2143 formalisation and the C-code shown below, the results of the formalisation clearly |
|
2144 shine through in the design of the code. |
2144 |
2145 |
2145 |
2146 |
2146 To implement PIP in PINTOS, we only need to modify the kernel |
2147 To implement PIP in PINTOS, we only need to modify the kernel |
2147 functions corresponding to the events in our formal model. The events translate to the following |
2148 functions corresponding to the events in our formal model. The events translate to the following |
2148 function interface in PINTOS: |
2149 function interface in PINTOS: |