diff -r d62b19b641c5 -r a5afc26b1d62 Journal/Paper.thy --- a/Journal/Paper.thy Fri Jul 06 22:18:39 2018 +0100 +++ b/Journal/Paper.thy Wed Jan 02 21:09:05 2019 +0000 @@ -251,9 +251,9 @@ 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} @@ -427,7 +427,7 @@ \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 @@ -562,7 +562,7 @@ \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. @@ -609,7 +609,7 @@ \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 @@ -652,7 +652,7 @@ \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. @@ -712,7 +712,7 @@ 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} @@ -1244,7 +1244,7 @@ % \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} @@ -1262,7 +1262,7 @@ % @{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 @@ -1342,9 +1342,9 @@ %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' @@ -1433,7 +1433,7 @@ % @{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} @@ -1511,9 +1511,9 @@ % @ {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} @@ -1579,18 +1579,18 @@ %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. " *} (*<*) @@ -1684,7 +1684,7 @@ \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 @@ -1837,7 +1837,7 @@ \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. @@ -1875,7 +1875,7 @@ 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 @@ -1899,7 +1899,7 @@ 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 \ 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 @@ -1920,7 +1920,7 @@ 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 \ Exit th"}, are both valid. We can show that \begin{isabelle}\ \ \ \ \ %%% @@ -1940,7 +1940,7 @@ 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 \ Set th prio"} are both valid. We can show that \begin{isabelle}\ \ \ \ \ %%% @@ -1989,7 +1989,7 @@ 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 @@ -2057,7 +2057,7 @@ 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 \ 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 @@ -2075,7 +2075,7 @@ 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. *} @@ -2100,7 +2100,7 @@ "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 @@ -2176,7 +2176,7 @@ 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 @@ -2277,7 +2277,7 @@ 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 @@ -2316,7 +2316,7 @@ 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).