equal
deleted
inserted
replaced
1241 on top of PINTOS, a simple instructional operating system for the x86 |
1241 on top of PINTOS, a simple instructional operating system for the x86 |
1242 architecture \cite{PINTOS}. A byproduct of our formalisation effort is that nearly all |
1242 architecture \cite{PINTOS}. A byproduct of our formalisation effort is that nearly all |
1243 design choices for the PIP scheduler are backed up with a proved |
1243 design choices for the PIP scheduler are backed up with a proved |
1244 lemma. We were also able to establish the property that the choice of |
1244 lemma. We were also able to establish the property that the choice of |
1245 the next thread which takes over a lock is irrelevant for the correctness |
1245 the next thread which takes over a lock is irrelevant for the correctness |
1246 of PIP. Earlier model checking approaches which verified particular implementations |
1246 of PIP. |
1247 of PIP \cite{Faria08,Jahier09,Wellings07} cannot |
|
1248 provide this kind of ``deep understanding'' about the principles behind |
|
1249 PIP and its correctness. |
|
1250 |
1247 |
1251 {\bf ??? rewrite the following slightly} |
1248 {\bf ??? rewrite the following slightly} |
1252 |
1249 |
1253 PIP is a scheduling algorithm for single-processor systems. We are |
1250 PIP is a scheduling algorithm for single-processor systems. We are |
1254 now living in a multi-processor world. So the question naturally |
1251 now living in a multi-processor world. So the question naturally |