1165 provide this kind of ``deep understanding'' about the principles behind |
1165 provide this kind of ``deep understanding'' about the principles behind |
1166 PIP and its correctness. |
1166 PIP and its correctness. |
1167 |
1167 |
1168 PIP is a scheduling algorithm for single-processor systems. We are |
1168 PIP is a scheduling algorithm for single-processor systems. We are |
1169 now living in a multi-processor world. So the question naturally |
1169 now living in a multi-processor world. So the question naturally |
1170 arises whether PIP has any relevance nowadays beyond |
1170 arises whether PIP has any relevance in such a world beyond |
1171 teaching. Priority inversion certainly occurs also in |
1171 teaching. Priority Inversion certainly occurs also in |
1172 multi-processor systems. The surprising answer, according to |
1172 multi-processor systems. However, the surprising answer, according to |
1173 \cite{Steinberg10}, is that except for one unsatisfactory proposal |
1173 \cite{Steinberg10}, is that except for one unsatisfactory proposal |
1174 nobody seems to have any good idea how PIP shoud be modified to work |
1174 nobody has a good idea for how PIP should be modified to work |
1175 correctly on multi-processor systems. The obstacles become clear |
1175 correctly on multi-processor systems. The difficulties become clear |
1176 when considering that locking and releasing a resource always |
1176 when considering that locking and releasing a resource always |
1177 requires some small time span. If processes are independent, then a |
1177 requires a some small amount of time. If processes work independently, then a |
1178 low priority process can always ``steal'' a the lock for such a |
1178 low priority process can ``steal'' in this unguarded moment a lock for a |
1179 resource from a high-priority process that should have run next. In |
1179 resource that was supposed allow a high-priority process to run next. Thus |
1180 effect, we have again the problem of Priority Inversions. It seems |
1180 the problem of Priority Inversion is not really prevented. It seems |
1181 difficult to design an algorithm with a meaningful property from |
1181 difficult to design a PIP-algorithm with a meaningful correctness |
1182 PIP. We can imagine PIP can be of use in a situation where |
1182 property on independent multi-processor systems. We can imagine PIP |
1183 processes are not independent, but coordinated such that a master |
1183 to be of use in a situation where |
1184 process distributes the work over some slave processes. However a |
1184 processes are not independent, but coordinated via a master |
|
1185 process that distributes work over some slave processes. However a |
1185 formal investigation of this is beyond the scope of this paper. |
1186 formal investigation of this is beyond the scope of this paper. |
1186 |
1187 We are not aware of any proofs in this area, not even informal ones. |
1187 |
1188 |
|
1189 Our formalisation consists of X lines of readable Isabelle/Isar code, with some |
|
1190 apply-scripts interspersed. The formal model is Y lines long; the |
|
1191 formal correctness proof Z lines. The properties relevant for an |
|
1192 implementation are U lines long. |
1188 |
1193 |
1189 *} |
1194 *} |
1190 |
1195 |
1191 section {* Key properties \label{extension} *} |
1196 section {* Key properties \label{extension} *} |
1192 |
1197 |