--- a/Journal/Paper.thy Wed Aug 02 14:56:47 2017 +0100
+++ b/Journal/Paper.thy Fri Aug 11 16:09:02 2017 +0100
@@ -78,10 +78,11 @@
therefore wait for $L$ to exit the critical section and release this
lock. The problem is that $L$ might in turn be blocked by any thread
with priority $M$, and so $H$ sits there potentially waiting
- indefinitely. Since $H$ is blocked by threads with lower priorities,
- the problem is called Priority Inversion. It was first described in
- \cite{Lampson80} in the context of the Mesa programming language
- designed for concurrent programming.
+ indefinitely (consider the case where threads with propority $M$
+ continously need to be processed). Since $H$ is blocked by threads
+ with lower priorities, the problem is called Priority Inversion. It
+ was first described in \cite{Lampson80} in the context of the Mesa
+ programming language designed for concurrent programming.
If the problem of Priority Inversion is ignored, real-time systems
can become unpredictable and resulting bugs can be hard to diagnose.
@@ -321,7 +322,8 @@
\isacommand{datatype} event
& @{text "="} & @{term "Create thread priority\<iota>"}\\
& @{text "|"} & @{term "Exit thread"} \\
- & @{text "|"} & @{term "Set thread priority\<iota>"} & {\rm reset of the priority for} @{text thread}\\
+ & @{text "|"} & @{term "Set thread priority\<iota>"} &
+ @{text thread} {\rm resets its own priority} \\
& @{text "|"} & @{term "P thread cs"} & {\rm request of resource} @{text "cs"} {\rm by} @{text "thread"}\\
& @{text "|"} & @{term "V thread cs"} & {\rm release of resource} @{text "cs"} {\rm by} @{text "thread"}
\end{tabular}}
@@ -412,7 +414,7 @@
\end{isabelle}
\noindent
- This allows us to define what actions a set of threads @{text ths} might
+ This allows us to filter out the actions a set of threads @{text ths}
perform in a list of events @{text s}, namely
\begin{isabelle}\ \ \ \ \ %%%
@@ -437,7 +439,7 @@
\end{isabelle}
\noindent
- for the set of precedences of threads @{text ths} in state @{text s}.
+ for the precedences of a set of threads @{text ths} in state @{text s}.
The point of precedences is to schedule threads not according to priorities (because what should
we do in case two threads have the same priority), but according to precedences.
Precedences allow us to always discriminate between two threads with equal priority by
@@ -484,7 +486,7 @@
\end{isabelle}
\noindent
- In this definition we assume @{text "set"} converts a list into a set.
+ In this definition we assume that @{text "set"} converts a list into a set.
Note that in the first definition the condition about @{text "th \<in> set (wq cs)"} does not follow
from @{text "th = hd (set (wq cs))"}, since the head of an empty list is undefined in Isabelle/HOL.
At the beginning, that is in the state where no thread is created yet,
@@ -623,7 +625,8 @@
only have at most one outgoing holding edge---indicating that the
resource is locked. So if the @{text "RAG"} is well-founded and
finite, we can always start at a thread waiting for a resource and
- ``chase'' outgoing arrows leading to a single root of a tree.
+ ``chase'' outgoing arrows leading to a single root of a tree,
+ which must be a ready thread.
The use of relations for representing @{text RAG}s allows us to
conveniently define the \emph{Thread Dependants Graph} (TDG):
@@ -633,12 +636,12 @@
\mbox{}\hfill\numbered{dependants}
\end{isabelle}
- \noindent This definition represents all threads in a @{text RAG} that wait
- for a thread to release a resource, but the corresponding
+ \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 @{text "th\<^sub>0"} with
- @{text "th\<^sub>1"} and @{text "th\<^sub>2"}, which both wait for
- resource @{text "cs\<^sub>1"}; and @{text "th\<^sub>2"} with @{text "th\<^sub>3"}, which
+ In Figure~\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
@@ -646,7 +649,8 @@
deadlock. Therefore when a thread requests a resource, we must
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.
+ resources can only be requested provided no circularity can arise (but
+ they 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
@@ -662,7 +666,8 @@
created), the point of the current precedence is to dynamically
increase this precedence, if needed according to PIP. Therefore the
current precedence of @{text th} is given as the maximum of the
- precedence of @{text th} \emph{and} all threads in its subtree. Since the notion of current precedence is defined as 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
transitive closure of the dependent
threads in the @{text TDG}, we deal correctly with the problem in the informal
algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is
@@ -874,7 +879,10 @@
@{thm[mode=Rule] thread_set[where thread=th]}
\end{center}
- \noindent If a thread wants to lock a resource, then the thread
+ \noindent This is because the @{text Set} event is for a thread to change
+ its \emph{own} priority---therefore it must be running.
+
+ If a thread wants to lock a resource, then the thread
needs to be running and also we have to make sure that the resource
lock does not lead to a cycle in the RAG (the prurpose of the second
premise in the rule below). In practice, ensuring the latter is the
@@ -918,7 +926,7 @@
\noindent
This completes our formal model of PIP. In the next section we present
- a series of desirable properties derived from our model of PIP. This can
+ a series of desirable properties derived from this model of PIP. This can
be regarded as a validation of the correctness of our model.
*}
@@ -1023,7 +1031,7 @@
th} is running or it is blocked by a thread that was alive in the
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 a finite
+ 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.
@@ -1059,11 +1067,13 @@
\end{quote}
\begin{quote}
- {\bf Assumptions on the events in {\boldmath@{text "s'"}:}} We want to prove that @{text th} cannot
- be blocked indefinitely. Of course this can happen if threads with higher priority
- than @{text th} are continuously created in @{text s'}. Therefore we have to assume that
+ {\bf Assumptions on the events in {\boldmath@{text "s'"}:}}
+ %We want to prove that @{text th} cannot
+ %be blocked indefinitely. Of course this can happen if threads with higher priority
+ %than @{text th} are continuously created in @{text s'}.
+ To make sure @{text th} has the highest precedence we have to assume that
events in @{text s'} can only create (respectively set) threads with equal or lower
- priority than @{text prio} of @{text th}. We also need to assume that the
+ priority than @{text prio} of @{text th}. For the same reason, we also need to assume that the
priority of @{text "th"} does not get reset and all other reset priorities are either
less or equal. Moreover, we assume that @{text th} does
not get ``exited'' in @{text "s'"}. This can be ensured by assuming the following three implications.
@@ -1151,7 +1161,7 @@
If @{term "th' \<in> running (s' @ s)"} and @{term "th \<noteq> th'"} then @{term "\<not>detached s th'"}.
\end{lemma}
- \begin{proof} Let us assume @{text "th'"} is detached in state
+ \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
@@ -1591,7 +1601,7 @@
further need the property that every thread gives up its resources
after a finite amount of time. We found that this property is not so
straightforward to formalise in our model. There are mainly two
- reasons for this: First, we do not specify what ``running'' the code
+ reasons for this: First, we do not specify what ``running the code''
of a thread means, for example by giving an operational semantics
for machine instructions. Therefore we cannot characterise what are
``good'' programs that contain for every locking request for a
@@ -1618,7 +1628,7 @@
finite number of states after state @{term s} in which the thread
@{term th} is blocked (recall for this that a state is a list of
events). For this finiteness bound to exist, Sha et al.~informally
- make two assumtions: first, there is a finite pool of threads
+ make two assumptions: first, there is a finite pool of threads
(active or hibernating) and second, each of them giving up its
resources after a finite amount of time. However, we do not have
this concept of active or hibernating threads in our model. In fact