pip: comparison Journal/Paper.thy

equal deleted inserted replaced

-:550ab0f68960
+:029e1506477a
 Because of these problems, we decided in our earlier paper
 \cite{ZhangUrbanWu12} to leave out this property and let the
 programmer assume the responsibility to program threads in such a
 benign manner (in addition to causing no circularity in the
 RAG). This was also the approach taken by Sha et al.~in their paper.
-However, in this paper we can make an improvement: we can look
+However, in this paper we can make an improvement: we can look at
-at the \emph{events} that are happening once a Priority Inversion
+the \emph{events} that are happening once a Priority Inversion
 occurs. The events can be seen as a rough abstraction of the
 ``runtime behaviour'' of threads and also as an abstract notion of
-``time''.  We can then prove a more direct bound for the absence of
+``time''---when an event occured, some time must have passed.  We
-indefinite Priority Inversion.
+can then prove a more direct bound for the absence of indefinite
+Priority Inversion. This is what we shall show below.
 What we will establish in this section is that there can only be a
 finite amount of states after state @{term s} in which the thread
 @{term th} is blocked. For this to be true, Sha et al.~assume in
 their work that there is a finite pool of threads (active or
 hibernating). However, we do not have this concept of active or
-hibernating threads in our model, but we can create or exit threads
+hibernating threads in our model. Rather, in our model we can create
-arbitrarily. Consequently, in our model the avoidance of indefinite
+or exit threads arbitrarily. Consequently, the avoidance of
-priority inversion we are trying to establish is not true, unless we
+indefinite priority inversion we are trying to establish is in our
-require that there number of threads created is bounded in every
+model not true, unless we require that the number of threads
-valid future state after @{term s}. So our first assumption
+created is bounded in every valid future state after @{term s}. So
-states
+our first assumption states:
 \begin{quote} {\bf Assumption on the number of threads created in
 every valid state after the state {\boldmath@{text s}}:} Given the
 state @{text s}, in every ``future'' valid state @{text "t @ s"}, we
 require that the number of created threads is less than
-@{text "BC"}, that is @{text "len (filter isCreate (t @ s)) <
+a bound @{text "BC"}, that is
-BC"}.  \end{quote}
+\[@{text "len (filter isCreate (t @ s)) < BC"}\;.\]
-\noindent Note that it is not enough for us to just to state that there
+\end{quote}
-are only finite number of threads created in the state @{text "s' @ s"}.  Instead, we
-need to put a bound on the @{text "Create"} events for all valid
+\noindent Note that it is not enough to just to state that there are
-states after @{text s}.
+only finite number of threads created in the state @{text "s' @ s"}.
+Instead, we need to put a bound on the @{text "Create"} events for
+all valid states after @{text s}.
 For our second assumption about giving up resources after a finite
-amount of ``time'', let us introduce the following definition:
+amount of ``time'', let us introduce the following definition about
+threads that can potentially block @{text th}:
 \begin{isabelle}\ \ \ \ \ %%%
 @{thm blockers_def}
 \end{isabelle}
-\noindent This set contains all treads that can potentially block
+\noindent This set contains all treads that are not detached in
-@{text th} after state @{text s}. We need to make the following
+state @{text s} (i.e.~have a lock on a resource) and therefore can
-assumption for the threads in this set:
+potentially block @{text th} after state @{text s}. We need to make
+the following assumption about the threads in this set:
 \begin{quote}
 {\bf Assumptions on the threads {\boldmath{@{term "th' \<in> blockers"}}}:}
 For each @{text "th'"} there exists a finite bound @{text "BND(th')"}
 such that for all future
 valid states @{text "t @ s"},
 we have that if @{term "\<not>(detached (t @ s) th')"}, then
-@{text "len(actions_of th' (t @ s)) < BND(th')"}.
+\[@{text "len(actions_of th' (t @ s)) < BND(th')"}\]
 \end{quote}
-\noindent By this assumption we enforce that any thread blocking
+\noindent By this assumption we enforce that any thread potentially
-@{term th} must become detached (that is hold no resource) after a
+blocking @{term th} must become detached (that is lock no resource)
-finite number of events in @{text "t @ s"}. Again we have to require
+after a finite number of events in @{text "t @ s"}. Again we have to
-this bound to hold in all valid states after @{text s}. The bound
+require this bound to hold in all valid states after @{text s}. The
-reflects how each thread @{text "th'"} is programmed: Though we cannot
+bound reflects how each thread @{text "th'"} is programmed: Though
-express what instructions a thread is executing, the events correspond
+we cannot express what instructions a thread is executing, the
-to the system calls made by thread. Our @{text "BND(th')"} bounds
+events in our model correspond to the system calls made by thread. Our @{text
-the number of these calls.
+"BND(th')"} binds the number of these calls.
-The main reason for these two assumptions is that we can prove:
+The main reason for these two assumptions is that we can prove: the
+number of states after @{text s} in which the thread @{text th} is
+is not running (that is where PI occurs) can be bounded by the
+number of actions the threads in @{text blockers} perform and how
+many threads are newly created. This bound can be stated for all
+valid states @{term "t @ s"} that can happen after @{text s}. To
+state our bound we use the definition @{term "Postfixes t \<equiv> {p. \<exists> s'. t = s' @ p}"}.
+To state this we use the
 \begin{isabelle}\ \ \ \ \ %%%
 @{thm bound_priority_inversion}
 \end{isabelle}

changeset 157	029e1506477a
parent 156	550ab0f68960
child 158	2bb3b65fc99f