# HG changeset patch # User urbanc # Date 1329111713 0 # Node ID e44c4055d430d13c357c57cc5ba3748db9644507 # Parent a401d2dff7d09b1f8c0a95b2c2af3b2fc0d794f3 more on the paper diff -r a401d2dff7d0 -r e44c4055d430 prio/Paper/Paper.thy --- a/prio/Paper/Paper.thy Mon Feb 13 04:22:52 2012 +0000 +++ b/prio/Paper/Paper.thy Mon Feb 13 05:41:53 2012 +0000 @@ -509,7 +509,7 @@ \noindent In this definition @{term "DUMMY ` DUMMY"} stands for the image of a set under a function. Note that in the initial state, that is where the list of events is empty, the set - @{term threads} is empty and therefore there is no thread ready nor a running. + @{term threads} is empty and therefore there is neither a thread ready nor running. If there is one or more threads ready, then there can only be \emph{one} thread running, namely the one whose current precedence is equal to the maximum of all ready threads. We use the set-comprehension to capture both possibilities. @@ -582,7 +582,7 @@ \noindent This completes our formal model of PIP. In the next section we present - properties that show our version of PIP is correct. + properties that show our model of PIP is correct. *} section {* Correctness Proof *} @@ -600,7 +600,7 @@ of the number of critical resources: if there are @{text m} critical resources, then a blocked job can only be blocked @{text m} times---that is a bounded number of times. - For their version of PIP, this is \emph{not} true (as pointed out by + For their version of PIP, this property is \emph{not} true (as pointed out by Yodaiken \cite{Yodaiken02}) as a high-priority thread can be blocked an unbounded number of times by creating medium-priority threads that block a thread locking a critical resource and having @@ -612,11 +612,11 @@ we show that in every future state (denoted by @{text "s' @ s"}) in which @{text th} is still active, either @{text th} is running or it is blocked by a thread that was active in the state @{text s}. Since in @{text s}, as in every - state, the set of active threads is finite, @{text th} can only blocked a - finite number of time. We will actually prove a stricter bound. However, - this correctness criterion depends on a number of assumptions about the states + state, the set of active threads is finite, @{text th} can only be blocked a + finite number of times. We will actually prove a stricter bound. However, + this correctness criterion hinges on a number of assumptions about the states @{text s} and @{text "s' @ s"}, the thread @{text th} and the events happening - in @{text s'}. + in @{text s'}. We list them next. \begin{quote} {\bf Assumptions on the states @{text s} and @{text "s' @ s"}:} In order to make @@ -645,10 +645,10 @@ \begin{quote} {\bf Assumptions on the events in @{text "s'"}:} We want to prove that @{text th} cannot - be blocked indefinitely. Of course this can by violated if threads with higher priority - than @{text th} are created in @{text s'}. Therefore we have to assume that - events in @{text s'} can only create (respectively set) threads with lower or equal - priority than @{text prio} of @{text th}. We also have to assume that @{text th} does + be blocked indefinitely. Of course this can happen if threads with higher priority + than @{text th} are continously created in @{text s'}. Therefore we have to assume that + events in @{text s'} can only create (respectively set) threads with equal or lower + priority than @{text prio} of the thread @{text th}. We also have to assume that @{text th} does not get ``exited'' in @{text "s'"}. \begin{isabelle}\ \ \ \ \ %%% \begin{tabular}{l} @@ -674,36 +674,40 @@ precedence in the state @{text s}, can only be blocked in the state @{text "s' @ s"} by a thread @{text th'} that already existed in @{text s}. As we shall see shortly, that means by only finitely many threads. Consequently, indefinite wait of - @{text th}, that is Priority Inversion, cannot occur. + @{text th}---whcih is Priority Inversion---cannot occur. + + In what follows we will describe properties of PIP that allow us to prove + Theorem~\ref{mainthm}. It is relatively easily to see that + + \begin{isabelle}\ \ \ \ \ %%% + \begin{tabular}{@ {}l} + @{text "running s \ ready s \ threads s"}\\ + @{thm[mode=IfThen] finite_threads} + \end{tabular} + \end{isabelle} + + \noindent + where the second property is by induction of @{term vt}. The next three + properties are - The following are several very basic prioprites: - \begin{enumerate} - \item All runing threads must be ready (@{text "runing_ready"}): - @{thm[display] "runing_ready"} - \item All ready threads must be living (@{text "readys_threads"}): - @{thm[display] "readys_threads"} - \item There are finite many living threads at any moment (@{text "finite_threads"}): - @{thm[display] "finite_threads"} - \item Every waiting queue does not contain duplcated elements (@{text "wq_distinct"}): - @{thm[display] "wq_distinct"} - \item All threads in waiting queues are living threads (@{text "wq_threads"}): - @{thm[display] "wq_threads"} - \item The event which can get a thread into waiting queue must be @{term "P"}-events - (@{text "block_pre"}): - @{thm[display] "block_pre"} - \item A thread may never wait for two different critical resources - (@{text "waiting_unique"}): - @{thm[display] waiting_unique[of _ _ "cs\<^isub>1" "cs\<^isub>2"]} - \item Every resource can only be held by one thread - (@{text "held_unique"}): - @{thm[display] held_unique[of _ "th\<^isub>1" _ "th\<^isub>2"]} - \item Every living thread has an unique precedence - (@{text "preced_unique"}): - @{thm[display] preced_unique[of "th\<^isub>1" _ "th\<^isub>2"]} - \end{enumerate} -*} + \begin{isabelle}\ \ \ \ \ %%% + \begin{tabular}{@ {}l} + @{thm[mode=IfThen] waiting_unique[of _ _ "cs\<^isub>1" "cs\<^isub>2"]}\\ + @{thm[mode=IfThen] held_unique[of _ "th\<^isub>1" _ "th\<^isub>2"]}\\ + @{thm[mode=IfThen] runing_unique[of _ "th\<^isub>1" "th\<^isub>2"]} + \end{tabular} + \end{isabelle} -text {* \noindent + \noindent + The first one states that every waiting thread can only wait for a single + resource (because it gets suspended after requesting that resource), and + the second that every resource can only be held by a single thread. The + third property establishes that in every given valid state, there is + at most one running thread. + + TODO + + \noindent The following lemmas show how RAG is changed with the execution of events: \begin{enumerate} \item Execution of @{term "Set"} does not change RAG (@{text "depend_set_unchanged"}): @@ -761,8 +765,6 @@ text {* \noindent Some deeper results about the system: \begin{enumerate} - \item There can only be one running thread (@{text "runing_unique"}): - @{thm [display] runing_unique[of _ "th\<^isub>1" "th\<^isub>2"]} \item The maximum of @{term "cp"} and @{term "preced"} are equal (@{text "max_cp_eq"}): @{thm [display] max_cp_eq} \item There must be one ready thread having the max @{term "cp"}-value diff -r a401d2dff7d0 -r e44c4055d430 prio/PrioG.thy --- a/prio/PrioG.thy Mon Feb 13 04:22:52 2012 +0000 +++ b/prio/PrioG.thy Mon Feb 13 05:41:53 2012 +0000 @@ -2,8 +2,15 @@ imports PrioGDef begin -lemma runing_ready: "runing s \ readys s" - by (auto simp only:runing_def readys_def) +lemma runing_ready: + shows "runing s \ readys s" + unfolding runing_def readys_def + by auto + +lemma readys_threads: + shows "readys s \ threads s" + unfolding readys_def + by auto lemma wq_v_neq: "cs \ cs' \ wq (V thread cs#s) cs' = wq s cs'" @@ -354,22 +361,20 @@ and "waiting s th cs1" and "waiting s th cs2" shows "cs1 = cs2" -proof - - from waiting_unique_pre and prems - show ?thesis - by (auto simp add: wq_def s_waiting_def) -qed +using waiting_unique_pre prems +unfolding wq_def s_waiting_def +by auto +(* not used *) lemma held_unique: - assumes "vt s" - and "holding s th1 cs" + fixes s::"state" + assumes "holding s th1 cs" and "holding s th2 cs" shows "th1 = th2" -proof - - from prems show ?thesis - unfolding s_holding_def - by auto -qed +using prems +unfolding s_holding_def +by auto + lemma birthtime_lt: "th \ threads s \ birthtime th s < length s" apply (induct s, auto) @@ -2468,42 +2473,8 @@ lemma finite_threads: assumes vt: "vt s" shows "finite (threads s)" -proof - - from vt show ?thesis - proof(induct) - case (vt_cons s e) - assume vt: "vt s" - and step: "step s e" - and ih: "finite (threads s)" - from step - show ?case - proof(cases) - case (thread_create thread prio) - assume eq_e: "e = Create thread prio" - with ih - show ?thesis by (unfold eq_e, auto) - next - case (thread_exit thread) - assume eq_e: "e = Exit thread" - with ih show ?thesis - by (unfold eq_e, auto) - next - case (thread_P thread cs) - assume eq_e: "e = P thread cs" - with ih show ?thesis by (unfold eq_e, auto) - next - case (thread_V thread cs) - assume eq_e: "e = V thread cs" - with ih show ?thesis by (unfold eq_e, auto) - next - case (thread_set thread prio) - from vt_cons thread_set show ?thesis by simp - qed - next - case vt_nil - show ?case by (auto) - qed -qed +using vt +by (induct) (auto elim: step.cases) lemma Max_f_mono: assumes seq: "A \ B" @@ -2785,14 +2756,6 @@ show ?thesis by (rule max_cp_readys_threads_pre[OF vt False]) qed -lemma readys_threads: - shows "readys s \ threads s" -proof - fix th - assume "th \ readys s" - thus "th \ threads s" - by (unfold readys_def, auto) -qed lemma eq_holding: "holding (wq s) th cs = holding s th cs" apply (unfold s_holding_def cs_holding_def wq_def, simp) diff -r a401d2dff7d0 -r e44c4055d430 prio/paper.pdf Binary file prio/paper.pdf has changed