# HG changeset patch # User Christian Urban # Date 1517927911 0 # Node ID 5191a09d9928dc5558eeef7e35fa0bc28f29124e # Parent fe3dbfd9123b81fb59a180cfb3041a5d57257ac0 updated diff -r fe3dbfd9123b -r 5191a09d9928 Journal/Paper.thy --- a/Journal/Paper.thy Mon Jan 15 11:35:56 2018 +0000 +++ b/Journal/Paper.thy Tue Feb 06 14:38:31 2018 +0000 @@ -210,7 +210,7 @@ computing the priority to be restored solely from this log is not explained in \cite{Liu00} but left as an ``{\it excercise}'' to the reader. As we shall see, a correct version of PIP does not need to - maintain this (potentially expensive) data structure at + maintain this (potentially expensive) log data structure at all. Surprisingly also the widely read and frequently updated textbook \cite{Silberschatz13} gives the wrong specification. On Page 254 the authors write: ``{\it Upon releasing the lock, the [low-priority] thread will revert to its original @@ -229,12 +229,8 @@ Sha et al. Unfortunately, this informal proof is too vague to be useful for formalising the correctness of PIP and the specification leaves out nearly all details in order to implement PIP - efficiently.\medskip\smallskip % %The advantage of formalising the - %correctness of a high-level specification of PIP in a theorem - prover %is that such issues clearly show up and cannot be overlooked - as in %informal reasoning (since we have to analyse all possible - behaviours %of threads, i.e.~\emph{traces}, that could possibly - happen). + efficiently.\medskip\smallskip + \noindent {\bf Contributions:} There have been earlier formal investigations into PIP \cite{Faria08,Jahier09,Wellings07}, but they @@ -245,7 +241,7 @@ is correct and allows us to prove stronger properties that, as we will show, can help with an efficient implementation of PIP. We illustrate this with an implementation of PIP in the educational - PINTOS operating system \cite{PINTOS}. For example, we found by + operating system PINTOS \cite{PINTOS}. For example, we found by ``playing'' with the formalisation that the choice of the next thread to take over a lock when a resource is released is irrelevant for PIP being correct---a fact that has not been mentioned in the @@ -568,15 +564,8 @@ for example in Figure~\ref{RAGgraph}. Because of the @{text RAG}s, we will need to formalise some results - about graphs. While there are a few formalisations for graphs already - implemented in Isabelle, we choose to introduce our own library of - graphs for PIP. The justification for this is that we wanted to have - a more general theory of graphs which is capable of representing - potentially infinite graphs (in the sense of infinitely branching - and infinite size): the property that our @{text RAG}s are actually - forests of finitely branching trees having only a finite depth - should be something we can \emph{prove} for our model of PIP---it - should not be an assumption we build already into our model. It + about graphs. + It seems for our purposes the most convenient representation of graphs are binary relations given by sets of pairs shown in \eqref{pairs}. The pairs stand for the edges in graphs. This @@ -585,7 +574,17 @@ terms of relations amongst threads and resources. Also, we can easily re-use the standard notions for transitive closure operations @{term "trancl DUMMY"} and @{term "rtrancl DUMMY"}, as well as relation - composition for our graphs. A \emph{forest} is defined in our + composition for our graphs. + While there are a few formalisations for graphs already + implemented in Isabelle, we choose to introduce our own library of + graphs for PIP. The justification for this is that we wanted to have + a more general theory of graphs which is capable of representing + potentially infinite graphs (in the sense of infinitely branching + and infinite size): the property that our @{text RAG}s are actually + forests of finitely branching trees having only a finite depth + should be something we can \emph{prove} for our model of PIP---it + should not be an assumption we build already into our model. + A \emph{forest} is defined in our representation as the relation @{text rel} that is \emph{single valued} and \emph{acyclic}: @@ -613,7 +612,7 @@ containing nodes with infinitely many children. A \emph{finite forest} is a forest whose underlying relation is well-founded\footnote{For \emph{well-founded} we use the quite natural - definition from Isabelle.} + definition from Isabelle/HOL.} and every node has finitely many children (is only finitely branching). @@ -630,7 +629,7 @@ %\endnote{{\bf Lemma about overlapping paths}} - The locking mechanism of PIP ensures that for each thread node, + The locking mechanism ensures that for each thread node, there can be many incoming holding edges in the @{text RAG}, but at most one out going waiting edge. The reason is that when a thread asks for a resource that is locked already, then the thread is blocked and @@ -663,7 +662,7 @@ ensure that the resulting @{text RAG} and @{text TDG} are not circular. In practice, the programmer has to ensure this. Our model will enforce that critical resources can only be requested provided no circularity can arise (but - they can overlap, see Fig~\ref{overlap}). + critical sections can overlap, see Fig~\ref{overlap}). Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a state @{text s}. It is defined as @@ -677,7 +676,7 @@ While the precedence @{term prec} of any thread is determined statically (for example when the thread is created), the point of the current precedence is to dynamically - increase this precedence, if needed according to PIP. Therefore the + boost this precedence, if needed according to PIP. Therefore the current precedence of @{text th} is given as the maximum of the precedences of all threads in its subtree (which includes by definition @{text th} itself). Since the notion of current precedence is defined as the @@ -705,7 +704,7 @@ resource @{text "cs"} and returns the corresponding list of threads that lock or wait for it); the second is a function that takes a thread and returns its current precedence (see - the definition in \eqref{cpreced}). We assume the usual getter and setter methods for + the @{text wq} in \eqref{cpreced}). We assume the usual getter and setter methods for such records. In the initial state, the scheduler starts with all resources unlocked (the corresponding @@ -727,7 +726,7 @@ this waiting queue function @{text wq} is unchanged in the next schedule state---because none of these events lock or release any resource; for calculating the next @{term "cprec_fun"}, we use @{text wq} and - @{term cpreced}. This gives the following three clauses for @{term schs}: + @{term cpreced} defined above. This gives the following three clauses for @{term schs}: \begin{isabelle}\ \ \ \ \ %%% \begin{tabular}{@ {}l} @@ -1045,9 +1044,8 @@ state @{text s} and was waiting for or in the possession of a lock in @{text s}. Since in @{text s}, as in every state, the set of alive threads is finite, @{text th} can only be blocked by a finite - number of threads. We will actually prove a - stronger statement where we also provide the current precedence of - the blocking thread. + number of threads. + However, the theorem we are going to prove hinges upon a number of natural assumptions about the states @{text s} and @{text "s' @ s"}, the @@ -1166,7 +1164,8 @@ % @{text "th_kept"} shows that th is a thread in s'-s % } - Given our assumptions (on @{text th}), the first property we show + The next lemma is part of the proof for Theorem~1: + Given our assumptions (on~@{text th}), the first property we show that a running thread @{text "th'"} must either wait for or hold a resource in state @{text s}. @@ -1177,9 +1176,9 @@ \begin{proof} Let us assume otherwise, that is @{text "th'"} is detached in state @{text "s"}, then, according to the definition of detached, @{text "th'"} does not hold or wait for any resource. Hence the @{text - cp}-value of @{text "th'"} in @{text s} is not boosted, that is + cprec}-value of @{text "th'"} in @{text s} is not boosted, that is @{term "cp s th' = prec th' s"}, and is therefore lower than the - precedence (as well as the @{text "cp"}-value) of @{term "th"}. This + precedence (as well as the @{text "cprec"}-value) of @{term "th"}. This means @{text "th'"} will not run as long as @{text "th"} is a live thread. In turn this means @{text "th'"} cannot take any action in state @{text "s' @ s"} to change its current status; therefore @@ -1647,8 +1646,8 @@ this concept of active or hibernating threads in our model. In fact we can dispense with the first assumption altogether and allow that in our model we can create new threads or exit existing threads - arbitrarily. Consequently, the avoidance of indefinite priority - inversion we are trying to establish is in our model not true, + arbitrarily. Consequently, the absence of indefinite priority + inversion we are trying to establish in our model is not true, unless we stipulate an upper bound on the number of threads that have been created during the time leading to any future state after @{term s}. Otherwise our PIP scheduler could be ``swamped'' with @@ -1671,9 +1670,9 @@ "s' @ s"} after @{text s}. Instead, we need to put this bound on the @{text "Create"} events for all valid states after @{text s}. This ensures that no matter which ``future'' state is reached, the - number of @{text "Create"}-events is finite. We use @{text "es @ s"} - to stand for \emph{future states} after @{text s}---it is @{text s} - extended with some list @{text es} of events. + number of @{text "Create"}-events is finite. This bound @{text BC} is assumed + with respect to all future states @{text "es @ s"} + of @{text s}, not just a single one. For our second assumption about giving up resources after a finite amount of ``time'', let us introduce the following definition about @@ -1687,7 +1686,7 @@ state @{text s}. According to our definiton of @{text "detached"}, this means a thread in @{text "blockers"} either holds or waits for some resource in state @{text s} . Our Thm.~1 implies that any of - those threads can all potentially block @{text th} after state + such threads can all potentially block @{text th} after state @{text s}. We need to make the following assumption about the threads in the @{text "blockers"}-set: @@ -1779,9 +1778,12 @@ \end{array} \end{equation} - \noindent Second by Thm~\ref{mainthm}, the events are either the - actions of @{text th} or @{text "Create"}-events or actions of the - threads in blockers. That is + \noindent + The actions in @{text es} can be partitioned into the actions of @{text th} and the + actions of threads other than @{text th}. The latter can further be divided + into actions of existing threads and the actions to create new + ones. Moreover, the actions of existing threads other than @{text th} + are by Thm 1 the actions of blockers. This gives rise to % \begin{equation}\label{secondeq} \begin{array}{lcl} @@ -1889,14 +1891,9 @@ a standard scheduling operation and implemented in most operating systems. - %\begin{proof}[of Lemma~\ref{childrenlem}] - %Test - %\end{proof} - - Of course the main work for implementing PIP involves the - scheduler and coding how it should react to events. Below we - outline how our formalisation guides this implementation for each - kind of events.\smallskip + Below we + outline how our formalisation guides the efficient calculation of @{text cprecs} + in response to each kind of events.\smallskip *} text {* @@ -2013,7 +2010,7 @@ \begin{isabelle}\ \ \ \ \ %%% @{text "If"} @{text "th'' \ th"} and - @{text "th'' \ th'"} + @{text "th'' \ th'"} \;\;@{text then}\;\; @{thm (concl) valid_trace_v_n.cp_kept[where ?th1.0="th''"]} \hfill\numbered{fone} \end{isabelle} @@ -2096,7 +2093,7 @@ \noindent That means we have to add a waiting edge to the @{text RAG}. Furthermore the current precedence for all threads that are - not ancestors of @{text "th"} are unchanged. For the ancestors of + not ancestors of @{text "th"} (in the new @{text RAG} or @{text TDG}) are unchanged. For the ancestors of @{text th} we need to follow the edges in the @{text TDG} and recompute the @{term "cprecs"}. Whereas in all other event we might have to make @@ -2247,7 +2244,7 @@ The waiting queue is referenced in the usual C-way as @{ML_text "&lock->wq"}. Next, we record that the current thread is waiting for the lock (Line 10). Thus we established two pointers: one in the waiting queue of the lock pointing to the - current thread, and the other from the currend thread pointing to the lock. + current thread, and the other from the current thread pointing to the lock. According to our specification in Section~\ref{model} and the properties we were able to prove for @{text P}, we need to ``chase'' all the ancestor threads in the @{text RAG} and update their diff -r fe3dbfd9123b -r 5191a09d9928 Journal/document/root.tex --- a/Journal/document/root.tex Mon Jan 15 11:35:56 2018 +0000 +++ b/Journal/document/root.tex Tue Feb 06 14:38:31 2018 +0000 @@ -83,7 +83,7 @@ solution proposed earlier. We also generalise the scheduling problem to the practically relevant case where critical sections can overlap. Our formalisation in Isabelle/HOL is based on Paulson's - inductive approach to verifying protocols. The formalisation not + inductive approach to protocol verification. The formalisation not only uncovers facts overlooked in the literature, but also helps with an efficient implementation of this protocol. Earlier implementations were criticised as too inefficient. Our diff -r fe3dbfd9123b -r 5191a09d9928 PIPDefs.thy --- a/PIPDefs.thy Mon Jan 15 11:35:56 2018 +0000 +++ b/PIPDefs.thy Tue Feb 06 14:38:31 2018 +0000 @@ -269,7 +269,7 @@ *} abbreviation - "all_unlocked \ \_::cs. ([]::thread list)" + "all_unlocked \ \cs::cs. ([]::thread list)" text {* diff -r fe3dbfd9123b -r 5191a09d9928 journal.pdf Binary file journal.pdf has changed