pip: comparison Journal/Paper.thy

equal deleted inserted replaced

-:312497c6d6b9
+:fdba35b422a0
 priorities this property can be violated. For this let $L$ be in the
 possession of a lock for a resource that $H$ also needs. $H$ must
 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,
+indefinitely (consider the case where threads with propority $M$
-the problem is called Priority Inversion. It was first described in
+continously need to be processed). Since $H$ is blocked by threads
-\cite{Lampson80} in the context of the Mesa programming language
+with lower priorities, the problem is called Priority Inversion. It
-designed for concurrent programming.
+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.
 The classic example where this happened is the software that
 controlled the Mars Pathfinder mission in 1997 \cite{Reeves98}.  On
 \begin{isabelle}\ \ \ \ \ %%%
 \mbox{\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{7mm}}l}
 \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}}
 \end{isabelle}
 @{thm (rhs) actor.simps(3)}\\
 \end{tabular}}
 \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}\ \ \ \ \ %%%
 @{thm actions_of_def[where ?s="s" and ?ths="ths", THEN eq_reflection]}.
 \end{isabelle}
 \begin{isabelle}\ \ \ \ \ %%%
 @{abbrev "preceds ths s"}
 \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
 taking into account the time when the priority was last set. We order precedences so
 that threads with the same priority get a higher precedence if their priority has been
 @{thm waiting_raw_def[where thread="th"]}
 \end{tabular}
 \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,
 the waiting queue function will be the function that returns the
 empty list for every resource.
 resource that is locked already, then the thread is blocked and
 cannot ask for another resource.  Clearly, also every resource can
 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):
 \begin{isabelle}\ \ \ \ \ %%%
 @{thm tG_raw_def}\\
 \mbox{}\hfill\numbered{dependants}
 \end{isabelle}
-\noindent This definition represents all threads in a @{text RAG} that wait
+\noindent This definition is the relation that one thread is waiting for
-for a thread to release a resource, but the corresponding
+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
+In Figure~\ref{RAGgraph} this means the @{text TDG} connects
-@{text "th\<^sub>1"} and @{text "th\<^sub>2"}, which both wait for
+@{text "th\<^sub>1"} and @{text "th\<^sub>2"} to @{text "th\<^sub>0"}, which both wait for
-resource @{text "cs\<^sub>1"}; and @{text "th\<^sub>2"} with @{text "th\<^sub>3"}, which
+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
 there is a circle of dependencies in a @{text RAG} (and thus @{text TDG}), then clearly we have a
 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
 \begin{isabelle}\ \ \ \ \ %%%
 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
 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
 lowered prematurely (see Introduction). We again introduce an abbreviation for current
 precedeces of a set of threads, written @{text "cprecs wq s ths"}.
 \begin{center}
 @{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
 responsibility of the programmer.  In our formal model we brush
 aside these problematic cases in order to be able to make some
 \end{tabular}
 \end{center}
 \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.
 *}
 (*
 section {* Preliminaries *}
 highest precedence; we show that in every future state (denoted by
 @{text "s' @ s"}) in which @{text th} is still alive, either @{text
 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.
 However, the theorem we are going to prove hinges upon a number of
 \end{tabular}
 \end{isabelle}
 \end{quote}
 \begin{quote}
-{\bf Assumptions on the events in {\boldmath@{text "s'"}:}} We want to prove that @{text th} cannot
+{\bf Assumptions on the events in {\boldmath@{text "s'"}:}}
-be blocked indefinitely. Of course this can happen if threads with higher priority
+%We want to prove that @{text th} cannot
-than @{text th} are continuously created in @{text s'}. Therefore we have to assume that
+%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.
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{l}
 \begin{lemma}\label{notdetached}
 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
 @{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
 Like in the work by Sha et al.~our result in Thm 1 does not yet
 guarantee the absence of indefinite Priority Inversion. For this we
 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
 resource also a corresponding unlocking request.  Second, we need to
 distinghish between a thread that ``just'' locks a resource for a
 What we will establish in this section is that there can only be a
 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
 we can dispence with the first assumption altogether and allow that
 in our model we can create new threads or exit existing threads

changeset 191	fdba35b422a0
parent 190	312497c6d6b9
child 192	f933a8ad24e5