# HG changeset patch # User Christian Urban # Date 1356187829 0 # Node ID 105715a0a807acdd16be515027e75b2d5a247c20 # Parent 9764023f719e83bdf6672be7f66f3afe68c4f78a updated diff -r 9764023f719e -r 105715a0a807 Journal/Paper.thy --- a/Journal/Paper.thy Sat Dec 22 01:58:45 2012 +0000 +++ b/Journal/Paper.thy Sat Dec 22 14:50:29 2012 +0000 @@ -302,6 +302,8 @@ \noindent In this definition we assume @{text "set"} converts a list into a set. + Note that in the first definition the condition about @{text "th \ set (wq cs)"} does not follow + from @{text "th = hd (set (wq cs))"}, since the head of an empty list is undefined in Isabelle/HOL. At the beginning, that is in the state where no thread is created yet, the waiting queue function will be the function that returns the empty list for every resource. @@ -380,6 +382,7 @@ Clearly, also every resource can only have at most one outgoing holding edge---indicating that the resource is locked. In this way we can always start at a thread waiting for a resource and ``chase'' outgoing arrows leading to a single root of a tree. + The use of relations for representing RAGs allows us to conveniently define @@ -527,7 +530,7 @@ \begin{tabular}{@ {}l} @{thm (lhs) schs.simps(6)} @{text "\"}\\ \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\ - \hspace{5mm}@{text "let"} @{text "new_wq = release (wq cs)"} @{text "in"}\\ + \hspace{5mm}@{text "let"} @{text "new_wq = wq(cs := release (wq cs))"} @{text "in"}\\ \hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|)"} \end{tabular} \end{isabelle} @@ -1289,7 +1292,13 @@ an unlocked resource is given next to the waiting thread with the highest precedence is realised in our implementation by priority queues. We implemented them as \emph{Braun trees} \cite{Paulson96}, which provide efficient @{text "O(log n)"}-operations - for accessing and updating. Apart from having to implement relatively complex data\-structures in C + for accessing and updating. In the code we shall describe below, we use the function + @{ML_text "queue_insert"}, for inserting a new element into a priority queue, and + @{ML_text "queue_update"}, for updating the position of an element that is already + in a queue. Both functions take an extra argument that specifies the + comparison function used for organising the priority queue. + + Apart from having to implement relatively complex data\-structures in C using pointers, our experience with the implementation has been very positive: our specification and formalisation of PIP translates smoothly to an efficent implementation in PINTOS. Let us illustrate this with the C-code for the function @{ML_text "lock_acquire"}, @@ -1297,7 +1306,6 @@ locking of a resource by the current running thread. The convention in the PINTOS code is to use the terminology \emph{locks} rather than resources. A lock is represented as a pointer to the structure {\tt lock} (Line 1). - Lines 2 to 4 are taken from the original code of @{ML_text "lock_acquire"} in PINTOS. They contain diagnostic code: first, there is a check that @@ -1308,7 +1316,7 @@ current thread does not ask twice for a lock. These assertions are supposed to be satisfied because of the assumptions in PINTOS about how this code is called. If not, then the assertions indicate a bug in PINTOS and the result will be - a \emph{kernel panic}. + a ``kernel panic''. @@ -1347,7 +1355,7 @@ intr_set_level(old_level); } \end{lstlisting} - \caption{Our version of the {\tt lock\_release} function for the small operating + \caption{Our version of the {\tt lock\_acquire} function for the small operating system PINTOS. It implements the operation corresponding to a @{text P}-event.\label{code}} \end{figure} @@ -1366,7 +1374,7 @@ to prove for @{text P}, we need to ``chase'' all the dependants in the RAG (Resource Allocation Graph) and update their current precedence; however we only have to do this as long as there is change in the - current precedence from one thread at hand to another. + current precedence. The ``chase'' is implemented in the while-loop in Lines 13 to 24. To initialise the loop, we @@ -1395,8 +1403,9 @@ Similar operations need to be implementated for the @{ML_text lock_release} function, which we however do not show. The reader should note though that we did \emph{not} verify our C-code. This is in contrast, for example, to the work on seL4, which actually verified in Isabelle/HOL - that their C-code satisfies its specification \cite{sel4}. - Our verification however provided us with the justification for designing + that their C-code satisfies its specification, thought this specification does not contain + anything about PIP \cite{sel4}. + Our verification of PIP however provided us with the justification for designing the C-code. It gave us confidence that leaving the ``chase'' early, whenever there is no change in the calculated current precedence, does not break the correctness of the algorithm. @@ -1444,7 +1453,7 @@ PIP is a scheduling algorithm for single-processor systems. We are now living in a multi-processor world. Priority Inversion certainly - occurs also there, see for example \cite{Brandenburg11, Davis11} + occurs also there, see for example \cite{Brandenburg11, Davis11}. However, there is very little ``foundational'' work about PIP-algorithms on multi-processor systems. We are not aware of any correctness proofs, not even informal ones. There is an diff -r 9764023f719e -r 105715a0a807 Journal/document/root.tex --- a/Journal/document/root.tex Sat Dec 22 01:58:45 2012 +0000 +++ b/Journal/document/root.tex Sat Dec 22 14:50:29 2012 +0000 @@ -47,7 +47,7 @@ \begin{document} \renewcommand{\thefootnote}{$\star$} -\footnotetext[1]{This is a revised and expanded version of \cite{ZhangUrbanWu12}.} +\footnotetext[1]{This is a revised, corrected and expanded version of \cite{ZhangUrbanWu12}.} \renewcommand{\thefootnote}{\arabic{footnote}} \title{Priority Inheritance Protocol Proved Correct} diff -r 9764023f719e -r 105715a0a807 Paper/Paper.thy --- a/Paper/Paper.thy Sat Dec 22 01:58:45 2012 +0000 +++ b/Paper/Paper.thy Sat Dec 22 14:50:29 2012 +0000 @@ -499,7 +499,7 @@ \begin{tabular}{@ {}l} @{thm (lhs) schs.simps(6)} @{text "\"}\\ \hspace{5mm}@{text "let"} @{text "wq = wq_fun (schs s)"} @{text "in"}\\ - \hspace{5mm}@{text "let"} @{text "new_wq = release (wq cs)"} @{text "in"}\\ + \hspace{5mm}@{text "let"} @{text "new_wq = wq(cs := release (wq cs))"} @{text "in"}\\ \hspace{8mm}@{term "(|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|)"} \end{tabular} \end{isabelle} diff -r 9764023f719e -r 105715a0a807 PrioGDef.thy --- a/PrioGDef.thy Sat Dec 22 01:58:45 2012 +0000 +++ b/PrioGDef.thy Sat Dec 22 14:50:29 2012 +0000 @@ -169,6 +169,7 @@ cs_dependents_def: "dependents (wq::cs \ thread list) th \ {th' . (Th th', Th th) \ (depend wq)^+}" + text {* The data structure used by the operating system for scheduling is referred to as {\em schedule state}. It is represented as a record consisting of diff -r 9764023f719e -r 105715a0a807 journal.pdf Binary file journal.pdf has changed