--- 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 \<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
@@ -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 \<equiv> 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 \<equiv> 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 \<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
@@ -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).