diff -r 312497c6d6b9 -r fdba35b422a0 Journal/Paper.thy --- 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\"}\\ & @{text "|"} & @{term "Exit thread"} \\ - & @{text "|"} & @{term "Set thread priority\"} & {\rm reset of the priority for} @{text thread}\\ + & @{text "|"} & @{term "Set thread priority\"} & + @{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 \ 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' \ running (s' @ s)"} and @{term "th \ th'"} then @{term "\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