163 |
163 |
164 \noindent |
164 \noindent |
165 {\bf Contributions:} There have been earlier formal investigations |
165 {\bf Contributions:} There have been earlier formal investigations |
166 into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model |
166 into PIP \cite{Faria08,Jahier09,Wellings07}, but they employ model |
167 checking techniques. This paper presents a formalised and |
167 checking techniques. This paper presents a formalised and |
168 mechanically checked proof for the correctness of PIP (to our |
168 mechanically checked proof for the correctness of PIP. For this we |
169 knowledge the first one). In contrast to model checking, our |
169 needed to design a new correctness criterion. In contrast to model checking, our |
170 formalisation provides insight into why PIP is correct and allows us |
170 formalisation provides insight into why PIP is correct and allows us |
171 to prove stronger properties that, as we will show, can help with an |
171 to prove stronger properties that, as we will show, can help with an |
172 efficient implementation of PIP in the educational PINTOS operating |
172 efficient implementation of PIP in the educational PINTOS operating |
173 system \cite{PINTOS}. For example, we found by ``playing'' with the |
173 system \cite{PINTOS}. For example, we found by ``playing'' with the |
174 formalisation that the choice of the next thread to take over a lock |
174 formalisation that the choice of the next thread to take over a lock |
352 \draw [->,line width=0.6mm] (F) to node [pos=0.45,sloped,below=-0.5mm] {\fnt{}waiting} (E); |
352 \draw [->,line width=0.6mm] (F) to node [pos=0.45,sloped,below=-0.5mm] {\fnt{}waiting} (E); |
353 \end{tikzpicture} |
353 \end{tikzpicture} |
354 \end{center} |
354 \end{center} |
355 |
355 |
356 \noindent |
356 \noindent |
|
357 We will design our scheduler |
|
358 so that every thread can be in the possession of several resources, that is |
|
359 it has potentially several incoming holding edges in the RAG, but has at most only one outgoing |
|
360 waiting edge. The reason is that when a thread asks for resource that is locked |
|
361 already, then the process is stopped and cannot ask for another resource. |
|
362 Clearly, also every resource can only have at most one outgoing holding edge---indicating |
|
363 that the resource is locked. |
|
364 |
|
365 |
357 The use of relations for representing RAGs allows us to conveniently define |
366 The use of relations for representing RAGs allows us to conveniently define |
358 the notion of the \emph{dependants} of a thread using the transitive closure |
367 the notion of the \emph{dependants} of a thread using the transitive closure |
359 operation for relations. This gives |
368 operation for relations. This gives |
360 |
369 |
361 \begin{isabelle}\ \ \ \ \ %%% |
370 \begin{isabelle}\ \ \ \ \ %%% |
1315 insert the current thread into the waiting queue of the lock (Line 9, |
1324 insert the current thread into the waiting queue of the lock (Line 9, |
1316 the waiting queue is referenced as @{ML_text "&lock-wq"}). The queues are |
1325 the waiting queue is referenced as @{ML_text "&lock-wq"}). The queues are |
1317 implemented as Braun Trees providing an heap interface, therefore |
1326 implemented as Braun Trees providing an heap interface, therefore |
1318 the function is called @{ML_text "heap_insert"}. Next we |
1327 the function is called @{ML_text "heap_insert"}. Next we |
1319 record that the current thread is waiting for the lock (Line 10). |
1328 record that the current thread is waiting for the lock (Line 10). |
|
1329 According to our specification, we need to ``chase'' the holders of locks |
|
1330 in the @{text RAG} (Resource Allocation Graph). In Lines 11 and 12 we |
|
1331 assign to the variable @{ML_text pt} the owner of the lock, and enter |
|
1332 a while-loop in Lines 13 to 24, which implements the ``chase''. |
1320 |
1333 |
1321 *} |
1334 *} |
1322 |
1335 |
1323 section {* Conclusion *} |
1336 section {* Conclusion *} |
1324 |
1337 |