pip: comparison Journal/Paper.thy

equal deleted inserted replaced

-:d62b19b641c5
+:a5afc26b1d62
 in PINTOS.  This fact, however, is important for an efficient
 implementation of PIP, because we can give the lock to the thread
 with the highest priority so that it terminates more quickly.  We
 are also able to generalise the scheduler of Sha et
 al.~\cite{Sha90} to the practically relevant case where critical
-sections can overlap; see Figure~\ref{overlap} \emph{a)} below for
+sections can overlap; see Fig.~\ref{overlap} \emph{a)} for
 an example of this restriction. In the existing literature there is
-no proof and also no method for proving which covers this generalised
+no proof and also no proof method that covers this generalised
 case.
 \begin{figure}
 \begin{center}
 \begin{tikzpicture}[scale=1]
 @{thm actions_of_def[where ?s="s" and ?ths="ths", THEN eq_reflection]}.
 \end{isabelle}
 \noindent
 where we use Isabelle's notation for list-comprehensions. This
-notation is very similar to notation used in Haskell for list-comprehensions.
+notation is very similar to the notation used in Haskell for list-comprehensions.
 A \emph{precedence} of a thread @{text th} in a
 state @{text s} is the pair of natural numbers defined as
 \begin{isabelle}\ \ \ \ \ %%%
 @{thm preced_def}
 \caption{An instance of a Resource Allocation Graph (RAG).\label{RAGgraph}}
 \end{figure}
 \noindent
 If there is no cycle, then every @{text RAG} can be pictured as a forest of trees, as
-for example in Figure~\ref{RAGgraph}.
+for example in Fig.~\ref{RAGgraph}.
 Because of the @{text RAG}s, we will need to formalise some results
 about graphs.
 It
 seems for our purposes the most convenient representation of
 @{thm ancestors_def[where ?r="rel" and ?x="node", THEN eq_reflection]}\\
 \end{tabular}\\
 \mbox{}\hfill\numbered{children}
 \end{isabelle}
-\noindent Note that forests can have trees with infinte depth and
+\noindent Note that forests can have trees with infinite depth and
 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/HOL.}
 and every node has finitely many children (is only finitely
 \end{isabelle}
 \noindent This definition is the relation that one thread is waiting for
 another to release a resource, but the corresponding
 resource is ``hidden''.
-In Figure~\ref{RAGgraph} this means the @{text TDG} connects
+In Fig.~\ref{RAGgraph} this means the @{text TDG} connects
 @{text "th\<^sub>1"} and @{text "th\<^sub>2"} to @{text "th\<^sub>0"}, which both wait for
 resource @{text "cs\<^sub>1"} to be released; and @{text "th\<^sub>3"} to @{text "th\<^sub>2"}, which
 cannot make any progress unless @{text "th\<^sub>2"} makes progress.
 Similarly for the other threads.
 If
 In the initial state, the scheduler starts with all resources unlocked (the corresponding
 function is defined in \eqref{allunlocked}) and the
 current precedence of every thread is initialised with @{term "Prc 0 0"}; that means
 \mbox{@{abbrev initial_cprec}}. Therefore
-we have for the initial shedule state
+we have for the initial schedule state
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm (lhs) schs.simps(1)} @{text "\<equiv>"}\\
 \hspace{5mm}@{term "(|wq_fun = all_unlocked, cprec_fun = (\<lambda>_::thread. Prc 0 0)|)"}
 %%%}
 %  \endnote{{\bf OUTLINE}
 %  Since @{term "th"} is the most urgent thread, if it is somehow
-%  blocked, people want to know why and wether this blocking is
+%  blocked, people want to know why and whether this blocking is
 %  reasonable.
 %  @{thm [source] th_blockedE} @{thm th_blockedE}
 %  if @{term "th"} is blocked, then there is a path leading from
 %  THEN
 %  @{thm [source] vat_t.th_chain_to_ready} @{thm vat_t.th_chain_to_ready}
-%  It is basic propery with non-trival proof.
+%  It is basic property with non-trivial proof.
 %  THEN
 %  @{thm [source] max_preced} @{thm max_preced}
 %  to @{term "preced th (t @ s)"}.
 %Let me distinguish between cp (current precedence) and assigned precedence (the precedence the
 %thread ``normally'' has).
 %So we want to show what the cp of th' is in state t @ s.
-%We look at all the assingned precedences in the subgraph starting from th'
+%We look at all the assigned precedences in the subgraph starting from th'
 %We are looking for the maximum of these assigned precedences.
-%This subgraph must contain the thread th, which actually has the highest precednence
+%This subgraph must contain the thread th, which actually has the highest precedence
 %so cp of th' in t @ s has this (assigned) precedence of th
 %We know that cp (t @ s) th'
 %is the Maximum of the threads in the subgraph starting from th'
 %this happens to be the precedence of th
 %th has the highest precedence of all threads
 %  we have @{term "cp (s' @ s) th' < prec th (s' @ s)"}.
 %  Since @{text "prec th (s' @ s)"} is already the highest
 %  @{term "cp (s' @ s) th"} can not be higher than this and can not be lower either (by
 %  definition of @{term "cp"}). Consequently, we have @{term "prec th (s' @ s) = cp (s' @ s) th"}.
 %  Finally we have @{term "cp (s' @ s) th' < cp (s' @ s) th"}.
-%  By defintion of @{text "running"}, @{text "th'"} can not be running in state
+%  By definition of @{text "running"}, @{text "th'"} can not be running in state
 %  @{text "s' @ s"}, as we had to show.\qed
 %  \end{proof}
 %  \noindent
 %  Since @{text "th'"} is not able to run in state @{text "s' @ s"}, it is not able to
 %  thread does not hold any critical resource, therefore no thread can depend on it
 %  (@{text "count_eq_dependants"}):
 %  @  {thm [display] count_eq_dependants}
 %\end{enumerate}
-%The reason that only threads which already held some resoures
+%The reason that only threads which already held some resources
 %can be running and block @{text "th"} is that if , otherwise, one thread
-%does not hold any resource, it may never have its prioirty raised
+%does not hold any resource, it may never have its priority raised
 %and will not get a chance to run. This fact is supported by
 %lemma @{text "moment_blocked"}:
 %@   {thm [display] moment_blocked}
 %When instantiating  @{text "i"} to @{text "0"}, the lemma means threads which did not hold any
 %resource in state @{text "s"} will not have a change to run latter. Rephrased, it means
 %if every such thread can release all its resources in finite duration, then after finite
 %duration, none of them may block @{term "th"} anymore. So, no priority inversion may happen
 %then.
 % NOTE: about bounds in sha et al and ours: they prove a bound on the length of individual
-% blocages. We prove a bound for the overall-blockage.
+% blockages. We prove a bound for the overall-blockage.
 % There are low priority threads,
 % which do not hold any resources,
 % such thread will not block th.
 % Their Theorem 3 does not exclude such threads.
-% There are resources, which are not held by any low prioirty threads,
+% There are resources, which are not held by any low priority threads,
 % such resources can not cause blockage of th neither. And similiary,
-% theorem 6 does not exlude them.
+% theorem 6 does not exclude them.
-% Our one bound excudle them by using a different formaulation. "
+% Our one bound exclude them by using a different formulation. "
 *}
 (*<*)
 end
 (*>*)
 \begin{isabelle}\ \ \ \ \ %%%
 @{thm blockers_def[THEN eq_reflection]}
 \end{isabelle}
 \noindent This set contains all threads that are not detached in
-state @{text s}. According to our definiton of @{text "detached"},
+state @{text s}. According to our definition 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 only
 these 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:
 \end{proof}
 \noindent This theorem is the main conclusion we obtain for the
 Priority Inheritance Protocol. It is based on the fact that the set of
 @{text blockers} is fixed at state @{text s} when @{text th} becomes
-the thread with highest priority. Then no additional blocker of
+the thread with the highest priority. Then no additional blocker of
 @{text th} can appear after the state @{text s}. And in this way we
 can bound the number of states where the thread @{text th} with the
 highest priority is prevented from running.
 Our bound does not depend on the restriction of well-nested critical
 sections in the Priority Inheritance Protocol as imposed by Sha et al.
 \noindent
 That means the current precedence of a thread @{text th} can be
 computed by considering the static precedence of @{text th}
 and
 the current precedences of the children of @{text th}. Their
-@{text "cprec"}s, in general, need to be computed by recursively decending into
+@{text "cprec"}s, in general, need to be computed by recursively descending into
 deeper ``levels'' of the @{text TDG}.
 However, the current precedence of a thread @{text th}, say,
 only needs to be recomputed when @{text "(i)"} its static
 precedence is re-set or when @{text "(ii)"} one of
 its children changes its current precedence or when @{text "(iii)"} the children set changes
 in response to each kind of events.\smallskip
 *}
 text {*
 \noindent
-\colorbox{mygrey}{@{term "Create th prio"}:} We assume that the current state @{text s} and
+\colorbox{mygrey}{@{term "Create th prio"}:} \\ We assume that the current state @{text s} and
 the next state @{term "e#s"}, whereby \mbox{@{term "e \<equiv> Create th prio"}}, are both valid (meaning the event
 @{text "Create"} is allowed to occur in @{text s}). In this situation we can show that
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 \smallskip
 *}
 text {*
 \noindent
-\colorbox{mygrey}{@{term "Exit th"}:} We again assume that the current state @{text s} and
+\colorbox{mygrey}{@{term "Exit th"}:}\\ We again assume that the current state @{text s} and
 the next state @{term "e#s"}, whereby this time  @{term "e \<equiv> Exit th"}, are both valid. We can show that
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm (concl) valid_trace_exit.RAG_es}, and\\
 \smallskip
 *}
 text {*
 \noindent
-\colorbox{mygrey}{@{term "Set th prio"}:} We assume that @{text s} and
+\colorbox{mygrey}{@{term "Set th prio"}:}\\ We assume that @{text s} and
 @{term "e#s"} with @{term "e \<equiv> Set th prio"} are both valid. We can show that
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{@ {}l}
 @{thm (concl) valid_trace_set.RAG_es}, and\\
 \smallskip
 *}
 text {*
 \noindent
-\colorbox{mygrey}{@{term "V th cs"}:} We assume that @{text s} and
+\colorbox{mygrey}{@{term "V th cs"}:}\\ We assume that @{text s} and
 @{term "e#s"} with @{text e} being @{term "V th cs"} are both valid.
 We have to consider two
 subcases: one where there is a thread to ``take over'' the released
 resource @{text cs}, and one where there is not. Let us consider them
 in turn. Suppose in state @{text s}, the thread @{text th'} takes over
 \end{isabelle}
 *}
 text {*
 \noindent
-\colorbox{mygrey}{@{term "P th cs"}:} We assume that @{text s} and
+\colorbox{mygrey}{@{term "P th cs"}:}\\ We assume that @{text s} and
 @{term "e#s"} with @{term "e \<equiv> P th cs"} are both valid.
 We again have to analyse two subcases, namely
 the one where @{text cs} is not locked, and one where it is. We
 treat the former case
 first by showing that
 \noindent This means we need to add a holding edge to the @{text
 RAG}. However, note that while the @{text RAG} changes the corresponding
 @{text TDG} does not change. Together with the fact that the
 precedences of all threads are unchanged, no @{text cprec} value is
-changed. Therefore, no recalucation of the @{text cprec} value
+changed. Therefore, no recalculation of the @{text cprec} value
 of any thread @{text "th''"} is needed.
 *}
 text {*
 @{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
 modifications to the @{text "RAG"}, no recalculation of @{text
 cprec} depends on the @{text RAG}. This is the only case where
-the recalulation needs to take the connections in the @{text RAG} into
+the recalculation needs to take the connections in the @{text RAG} into
 account.
 To do this we can start from @{term "th"} and follow the
 @{term "children"}-edges to recompute the @{term "cp"} of every
 thread encountered on the way using Lemma~\ref{childrenlem}.
 This means the recomputation can be done locally (level-by-level)
 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.
+and formalisation of PIP translates smoothly to an efficient implementation in PINTOS.
 Let us illustrate this with the C-code for the function @{ML_text "lock_acquire"},
 shown in Figure~\ref{code}.  This function implements the operation of requesting and, if free,
 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).
 the lock (Line 28), and finally update the queue of locks the current
 thread already possesses (Line 29).
 The very last step is to enable interrupts again thus leaving the protected section.
-Similar operations need to be implementated for the @{ML_text lock_release} function, which
+Similar operations need to be implemented 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, though this specification does not contain
 anything about PIP \cite{sel4}.
 Our verification of PIP however provided us with (formally proven) insights on how to design
 explain how to use various implementations of PIP and abstractly
 discuss their properties, but surprisingly lack most details important for a
 programmer who wants to implement PIP (similarly Sha et al.~\cite{Sha90}).
 That this is an issue in practice is illustrated by the
 email from Baker we cited in the Introduction. We achieved also this
-goal: The formalisation allowed us to efficently implement our version
+goal: The formalisation allowed us to efficiently implement our version
 of PIP on top of PINTOS, a simple instructional operating system for the x86
 architecture implemented by Pfaff \cite{PINTOS}. It also gives the first author enough data to enable
 his undergraduate students to implement PIP (as part of their OS course).
 A byproduct of our formalisation effort is that nearly all
 design choices for the implementation of PIP scheduler are backed up with a proved

changeset 208	a5afc26b1d62
parent 207	d62b19b641c5