--- 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'' \<noteq> th"} and
- @{text "th'' \<noteq> th'"}
+ @{text "th'' \<noteq> 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