# HG changeset patch # User Christian Urban # Date 1452694858 0 # Node ID 92ca2410b3d9d1a6fbbab517da616291a599889c # Parent 1dc801552dfd1282235386ac636179cf41785ef8 further simplificaton of Moment.thy diff -r 1dc801552dfd -r 92ca2410b3d9 Journal/Paper.thy --- a/Journal/Paper.thy Wed Jan 13 13:20:45 2016 +0000 +++ b/Journal/Paper.thy Wed Jan 13 14:20:58 2016 +0000 @@ -890,10 +890,10 @@ programs that contain for every looking request also a corresponding unlocking request for a resource. Second, we would need to specify a kind of global clock that tracks the time how long a thread locks a - resource. But this seems difficult, because how do we conveninet + resource. But this seems difficult, because how do we conveniently distinguish between a thread that ``just'' lock a resource for a very long time and one that locks it forever. Therefore we decided - to leave it out this property and let the programmer assume the + 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). In this detail, we do not make any progress in comparison with the work by Sha et al. @@ -936,7 +936,7 @@ THENTHEN - @{thm [source] runing_inversion_4} @{thm runing_inversion_4} + (here) %@ {thm [source] runing_inversion_4} @ {thm runing_inversion_4} which explains what the @{term "th'"} looks like. Now, we have found the @{term "th'"} which blocks @{term th}, we need to know more about it. @@ -1166,6 +1166,20 @@ %if every such thread can release all its resources in finite duration, then after finite %duration, none of them may block @{term "th"} anymore. So, no priority inversion may happen %then. + + NOTE: about bounds in sha et al and ours: + + There are low priority threads, + which do not hold any resources, + such thread will not block th. + Their Theorem 3 does not exclude such threads. + + There are resources, which are not held by any low prioirty threads, + such resources can not cause blockage of th neither. And similiary, + theorem 6 does not exlude them. + + Our one bound excudle them by using a different formaulation. " + *} (*<*) end diff -r 1dc801552dfd -r 92ca2410b3d9 Moment.thy --- a/Moment.thy Wed Jan 13 13:20:45 2016 +0000 +++ b/Moment.thy Wed Jan 13 14:20:58 2016 +0000 @@ -5,36 +5,18 @@ definition moment :: "nat \ 'a list \ 'a list" where "moment n s = rev (take n (rev s))" -value "moment 3 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9::int]" - definition restm :: "nat \ 'a list \ 'a list" where "restm n s = rev (drop n (rev s))" -value "restm 3 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9::int]" - -definition from_to :: "nat \ nat \ 'a list \ 'a list" - where "from_to i j s = take (j - i) (drop i s)" +value "moment 3 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9::int]" +value "moment 2 [5, 4, 3, 2, 1, 0::int]" -definition down_to :: "nat \ nat \ 'a list \ 'a list" -where "down_to j i s = rev (from_to i j (rev s))" - -value "down_to 6 2 [10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0]" -value "from_to 2 6 [0, 1, 2, 3, 4, 5, 6, 7]" - -value "from_to 0 2 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9] @ - from_to 2 5 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9]" - +value "restm 3 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9::int]" lemma moment_restm_s: "(restm n s) @ (moment n s) = s" unfolding restm_def moment_def by (metis append_take_drop_id rev_append rev_rev_ident) -declare drop.simps [simp del] - -lemma length_take_le: - "n \ length s \ length (take n s) = n" -by (metis length_take min.absorb2) - lemma length_moment_le: assumes le_k: "k \ length s" shows "length (moment k s) = k" @@ -45,29 +27,12 @@ shows "length (moment k s) = (length s)" using assms unfolding moment_def by simp -lemma length_take: - "(length (take n s) = length s) \ (length (take n s) = n)" -by (metis length_take min_def) - -lemma take_conc: - assumes le_mn: "m \ n" - shows "take m s = take m (take n s)" -using assms by (metis min.absorb1 take_take) - -(* -value "down_to 2 0 [5, 4, 3, 2, 1, 0]" -value "moment 2 [5, 4, 3, 2, 1, 0]" -*) - -lemma from_to_take: "from_to 0 k s = take k s" -by (simp add:from_to_def drop.simps) - lemma moment_app [simp]: assumes ile: "i \ length s" - shows "moment i (s'@s) = moment i s" + shows "moment i (s' @ s) = moment i s" using assms unfolding moment_def by simp -lemma moment_eq [simp]: "moment (length s) (s'@s) = s" +lemma moment_eq [simp]: "moment (length s) (s' @ s) = s" unfolding moment_def by simp lemma moment_ge [simp]: "length s \ n \ moment n s = s" @@ -172,7 +137,7 @@ qed lemma p_split: - "\ s Q. \Q s; \ Q []\ \ + "\Q s; \ Q []\ \ (\ i. i < length s \ \ Q (moment i s) \ (\ i' > i. Q (moment i' s)))" proof - fix s Q @@ -183,20 +148,6 @@ by auto qed -(* -value "from_to 2 5 [0, 1, 2, 3, 4]" -value "drop 2 [0, 1, 2, 3, 4]" -*) - -(* -lemma down_to_moment: "down_to k 0 s = moment k s" -proof - - have "rev (from_to 0 k (rev s)) = rev (take k (rev s))" - using from_to_take by metis - thus ?thesis by (simp add:down_to_def moment_def) -qed -*) - lemma moment_plus_split: shows "moment (m + i) s = moment m (restm i s) @ moment i s" unfolding moment_def restm_def @@ -213,32 +164,6 @@ with moment_app show ?thesis by auto qed -lemma length_down_to_in: - assumes le_ij: "i \ j" - and le_js: "j \ length s" - shows "length (down_to j i s) = j - i" -using assms -unfolding down_to_def from_to_def -by (simp) - -lemma moment_head: - assumes le_it: "Suc i \ length t" - obtains e where "moment (Suc i) t = e#moment i t" -proof - - have "i \ Suc i" by simp - from length_down_to_in [OF this le_it] - have a: "length (down_to (Suc i) i t) = 1" by auto - then obtain e where "down_to (Suc i) i t = [e]" - apply (cases "(down_to (Suc i) i t)") by auto - moreover have "down_to (Suc i) 0 t = down_to (Suc i) i t @ down_to i 0 t" - unfolding down_to_def from_to_def rev_append[symmetric] - apply(simp del: rev_append) - by (metis One_nat_def Suc_eq_plus1_left add.commute take_add) - ultimately have eq_me: "moment (Suc i) t = e # (moment i t)" - by(simp add: moment_def down_to_def from_to_def) - from that [OF this] show ?thesis . -qed - lemma moment_plus: "Suc i \ length s \ moment (Suc i) s = (hd (moment (Suc i) s)) # (moment i s)" proof(induct s, simp+) @@ -276,3 +201,4 @@ qed end +