1233 \hline |
1233 \hline |
1234 \end{tabular} |
1234 \end{tabular} |
1235 \end{center} |
1235 \end{center} |
1236 |
1236 |
1237 \noindent |
1237 \noindent |
1238 Our assumption that every event is an atomic operation is ensured by the architecture of |
1238 Our implicit assumption that every event is an atomic operation is ensured by the architecture of |
1239 PINTOS. The case where an unlocked resource is given next to the waiting thread with the |
1239 PINTOS. The case where an unlocked resource is given next to the waiting thread with the |
1240 highest precedence is realised in our implementation by priority queues. We implemented |
1240 highest precedence is realised in our implementation by priority queues. We implemented |
1241 them as \emph{Braun trees} \cite{Paulson96}, which provide efficient @{text "O(log n)"}-operations |
1241 them as \emph{Braun trees} \cite{Paulson96}, which provide efficient @{text "O(log n)"}-operations |
1242 for accessing and restructuring. Apart from having to implement complex datastructures in C |
1242 for accessing and updating. Apart from having to implement relatively complex data\-structures in C |
1243 using pointers, our experience with the implementation has been very positive: our specification |
1243 using pointers, our experience with the implementation has been very positive: our specification |
1244 and formalisation of PIP translates smoothly to an efficent implementation. |
1244 and formalisation of PIP translates smoothly to an efficent implementation in PINTOS. |
1245 *} |
1245 *} |
1246 |
1246 |
1247 section {* Conclusion *} |
1247 section {* Conclusion *} |
1248 |
1248 |
1249 text {* |
1249 text {* |
1270 explain how to use various implementations of PIP and abstractly |
1270 explain how to use various implementations of PIP and abstractly |
1271 discuss their properties, but surprisingly lack most details important for a |
1271 discuss their properties, but surprisingly lack most details important for a |
1272 programmer who wants to implement PIP (similarly Sha et al.~\cite{Sha90}). |
1272 programmer who wants to implement PIP (similarly Sha et al.~\cite{Sha90}). |
1273 That this is an issue in practice is illustrated by the |
1273 That this is an issue in practice is illustrated by the |
1274 email from Baker we cited in the Introduction. We achieved also this |
1274 email from Baker we cited in the Introduction. We achieved also this |
1275 goal: The formalisation gives the first author enough data to enable |
1275 goal: The formalisation allowed us to efficently implement our version |
1276 his undergraduate students to implement PIP (as part of their OS course) |
1276 of PIP on top of PINTOS \cite{PINTOS}, a simple instructional operating system for the x86 |
1277 on top of PINTOS, a simple instructional operating system for the x86 |
1277 architecture. It also gives the first author enough data to enable |
1278 architecture \cite{PINTOS}. A byproduct of our formalisation effort is that nearly all |
1278 his undergraduate students to implement PIP (as part of their OS course). |
|
1279 A byproduct of our formalisation effort is that nearly all |
1279 design choices for the PIP scheduler are backed up with a proved |
1280 design choices for the PIP scheduler are backed up with a proved |
1280 lemma. We were also able to establish the property that the choice of |
1281 lemma. We were also able to establish the property that the choice of |
1281 the next thread which takes over a lock is irrelevant for the correctness |
1282 the next thread which takes over a lock is irrelevant for the correctness |
1282 of PIP. |
1283 of PIP. |
1283 |
1284 |