2042 qed |
2042 qed |
2043 end |
2043 end |
2044 |
2044 |
2045 section {* RAG is acyclic *} |
2045 section {* RAG is acyclic *} |
2046 |
2046 |
2047 text {* (* ddd *) |
2047 subsection {* Uniqueness of waiting *} |
2048 The nature of the work is like this: since it starts from a very simple and basic |
2048 |
2049 model, even intuitively very `basic` and `obvious` properties need to derived from scratch. |
2049 text {* |
2050 For instance, the fact |
2050 Uniqueness of waiting is expressed by the following |
2051 that one thread can not be blocked by two critical resources at the same time |
2051 predicate over system state (or event trace). |
2052 is obvious, because only running threads can make new requests, if one is waiting for |
2052 It says a thread can only be blocked on one resource. |
2053 a critical resource and get blocked, it can not make another resource request and get |
|
2054 blocked the second time (because it is not running). |
|
2055 |
|
2056 To derive this fact, one needs to prove by contraction and |
|
2057 reason about time (or @{text "moement"}). The reasoning is based on a generic theorem |
|
2058 named @{text "p_split"}, which is about status changing along the time axis. It says if |
|
2059 a condition @{text "Q"} is @{text "True"} at a state @{text "s"}, |
|
2060 but it was @{text "False"} at the very beginning, then there must exits a moment @{text "t"} |
|
2061 in the history of @{text "s"} (notice that @{text "s"} itself is essentially the history |
|
2062 of events leading to it), such that @{text "Q"} switched |
|
2063 from being @{text "False"} to @{text "True"} and kept being @{text "True"} |
|
2064 till the last moment of @{text "s"}. |
|
2065 |
|
2066 Suppose a thread @{text "th"} is blocked |
|
2067 on @{text "cs1"} and @{text "cs2"} in some state @{text "s"}, |
|
2068 since no thread is blocked at the very beginning, by applying |
|
2069 @{text "p_split"} to these two blocking facts, there exist |
|
2070 two moments @{text "t1"} and @{text "t2"} in @{text "s"}, such that |
|
2071 @{text "th"} got blocked on @{text "cs1"} and @{text "cs2"} |
|
2072 and kept on blocked on them respectively ever since. |
|
2073 |
|
2074 Without lost of generality, we assume @{text "t1"} is earlier than @{text "t2"}. |
|
2075 However, since @{text "th"} was blocked ever since memonent @{text "t1"}, so it was still |
|
2076 in blocked state at moment @{text "t2"} and could not |
|
2077 make any request and get blocked the second time: Contradiction. |
|
2078 *} |
2053 *} |
2079 |
2054 |
|
2055 definition |
|
2056 "waiting_unique (ss::state) = |
|
2057 (\<forall> th cs1 cs2. waiting ss th cs1 \<longrightarrow> |
|
2058 waiting ss th cs2 \<longrightarrow> cs1 = cs2)" |
|
2059 |
|
2060 text {* |
|
2061 We are going to show (in the |
|
2062 lemma named @{text waiting_unique}) that |
|
2063 this property holds on any valid trace (or system state). |
|
2064 *} |
|
2065 |
|
2066 text {* |
|
2067 As a first step, we need to understand how |
|
2068 a thread is get blocked. |
|
2069 We show in the following lemmas |
|
2070 (all named @{text "waiting_inv"}) that |
|
2071 @{term P}-operation is the only cause. |
|
2072 *} |
|
2073 |
|
2074 context valid_trace_create |
|
2075 begin |
|
2076 lemma waiting_inv: |
|
2077 assumes "\<not> waiting s th' cs'" |
|
2078 and "waiting (e#s) th' cs'" |
|
2079 shows "e = P th' cs'" |
|
2080 using assms |
|
2081 by (unfold s_waiting_def, fold wq_def, simp) |
|
2082 end |
|
2083 |
|
2084 context valid_trace_set |
|
2085 begin |
|
2086 lemma waiting_inv: |
|
2087 assumes "\<not> waiting s th' cs'" |
|
2088 and "waiting (e#s) th' cs'" |
|
2089 shows "e = P th' cs'" |
|
2090 using assms |
|
2091 by (unfold s_waiting_def, fold wq_def, simp) |
|
2092 end |
|
2093 |
|
2094 context valid_trace_exit |
|
2095 begin |
|
2096 lemma waiting_inv: |
|
2097 assumes "\<not> waiting s th' cs'" |
|
2098 and "waiting (e#s) th' cs'" |
|
2099 shows "e = P th' cs'" |
|
2100 using assms |
|
2101 by (unfold s_waiting_def, fold wq_def, simp) |
|
2102 end |
|
2103 |
|
2104 context valid_trace_p |
|
2105 begin |
|
2106 |
|
2107 lemma waiting_inv: |
|
2108 assumes "\<not> waiting s th' cs'" |
|
2109 and "waiting (e#s) th' cs'" |
|
2110 shows "e = P th' cs'" |
|
2111 proof(cases "cs' = cs") |
|
2112 case True |
|
2113 moreover have "th' = th" |
|
2114 proof(rule ccontr) |
|
2115 assume otherwise: "th' \<noteq> th" |
|
2116 have "waiting s th' cs'" |
|
2117 proof - |
|
2118 from assms(2)[unfolded True s_waiting_def, |
|
2119 folded wq_def, unfolded wq_es_cs] |
|
2120 have h: "th' \<in> set (wq s cs @ [th])" |
|
2121 "th' \<noteq> hd (wq s cs @ [th])" by auto |
|
2122 from h(1) and otherwise |
|
2123 have "th' \<in> set (wq s cs)" by auto |
|
2124 hence "wq s cs \<noteq> []" by auto |
|
2125 hence "hd (wq s cs @ [th]) = hd (wq s cs)" by auto |
|
2126 with h otherwise |
|
2127 have "waiting s th' cs" |
|
2128 by (unfold s_waiting_def, fold wq_def, auto) |
|
2129 from this[folded True] show ?thesis . |
|
2130 qed |
|
2131 with assms(1) show False by simp |
|
2132 qed |
|
2133 ultimately show ?thesis using is_p by simp |
|
2134 next |
|
2135 case False |
|
2136 hence "wq (e#s) cs' = wq s cs'" by simp |
|
2137 from assms[unfolded s_waiting_def, folded wq_def, |
|
2138 unfolded this] |
|
2139 show ?thesis by simp |
|
2140 qed |
|
2141 |
|
2142 end |
|
2143 |
|
2144 context valid_trace_v_n |
|
2145 begin |
|
2146 |
|
2147 lemma waiting_inv: |
|
2148 assumes "\<not> waiting s th' cs'" |
|
2149 and "waiting (e#s) th' cs'" |
|
2150 shows "e = P th' cs'" |
|
2151 proof - |
|
2152 from assms(2) |
|
2153 show ?thesis |
|
2154 by (cases rule:waiting_esE, insert assms, auto) |
|
2155 qed |
|
2156 |
|
2157 end |
|
2158 |
|
2159 context valid_trace_v_e |
|
2160 begin |
|
2161 |
|
2162 lemma waiting_inv: |
|
2163 assumes "\<not> waiting s th' cs'" |
|
2164 and "waiting (e#s) th' cs'" |
|
2165 shows "e = P th' cs'" |
|
2166 proof - |
|
2167 from assms(2) |
|
2168 show ?thesis |
|
2169 by (cases rule:waiting_esE, insert assms, auto) |
|
2170 qed |
|
2171 |
|
2172 end |
|
2173 |
|
2174 |
|
2175 context valid_trace_e |
|
2176 begin |
|
2177 |
|
2178 lemma waiting_inv: |
|
2179 assumes "\<not> waiting s th cs" |
|
2180 and "waiting (e#s) th cs" |
|
2181 shows "e = P th cs" |
|
2182 proof(cases e) |
|
2183 case (Create th' prio') |
|
2184 then interpret vt: valid_trace_create s e th' prio' |
|
2185 by (unfold_locales, simp) |
|
2186 show ?thesis using vt.waiting_inv[OF assms] by simp |
|
2187 next |
|
2188 case (Exit th') |
|
2189 then interpret vt: valid_trace_exit s e th' |
|
2190 by (unfold_locales, simp) |
|
2191 show ?thesis using vt.waiting_inv[OF assms] by simp |
|
2192 next |
|
2193 case (Set th' prio') |
|
2194 then interpret vt: valid_trace_set s e th' prio' |
|
2195 by (unfold_locales, simp) |
|
2196 show ?thesis using vt.waiting_inv[OF assms] by simp |
|
2197 next |
|
2198 case (P th' cs') |
|
2199 then interpret vt: valid_trace_p s e th' cs' |
|
2200 by (unfold_locales, simp) |
|
2201 show ?thesis using vt.waiting_inv[OF assms] by simp |
|
2202 next |
|
2203 case (V th' cs') |
|
2204 then interpret vt_e: valid_trace_v s e th' cs' |
|
2205 by (unfold_locales, simp) |
|
2206 show ?thesis |
|
2207 proof(cases "vt_e.rest = []") |
|
2208 case True |
|
2209 then interpret vt: valid_trace_v_e s e th' cs' |
|
2210 by (unfold_locales, simp) |
|
2211 show ?thesis using vt.waiting_inv[OF assms] by simp |
|
2212 next |
|
2213 case False |
|
2214 then interpret vt: valid_trace_v_n s e th' cs' |
|
2215 by (unfold_locales, simp) |
|
2216 show ?thesis using vt.waiting_inv[OF assms] by simp |
|
2217 qed |
|
2218 qed |
|
2219 |
|
2220 lemma waiting_unique_kept: |
|
2221 assumes "waiting_unique s" |
|
2222 shows "waiting_unique (e#s)" |
|
2223 proof - |
|
2224 note h = assms[unfolded waiting_unique_def, rule_format] |
|
2225 { fix th cs1 cs2 |
|
2226 assume w1: "waiting (e#s) th cs1" |
|
2227 and w2: "waiting (e#s) th cs2" |
|
2228 have "cs1 = cs2" |
|
2229 proof(rule ccontr) |
|
2230 assume otherwise: "cs1 \<noteq> cs2" |
|
2231 show False |
|
2232 proof(cases "waiting s th cs1") |
|
2233 case True |
|
2234 from h[OF this] and otherwise |
|
2235 have "\<not> waiting s th cs2" by auto |
|
2236 from waiting_inv[OF this w2] |
|
2237 have "e = P th cs2" . |
|
2238 then interpret vt: valid_trace_p s e th cs2 |
|
2239 by (unfold_locales, simp) |
|
2240 from vt.th_not_waiting and True |
|
2241 show ?thesis by simp |
|
2242 next |
|
2243 case False |
|
2244 from waiting_inv[OF this w1] |
|
2245 have "e = P th cs1" . |
|
2246 then interpret vt: valid_trace_p s e th cs1 |
|
2247 by (unfold_locales, simp) |
|
2248 have "wq (e # s) cs2 = wq s cs2" |
|
2249 using otherwise by simp |
|
2250 from w2[unfolded s_waiting_def, folded wq_def, |
|
2251 unfolded this] |
|
2252 have "waiting s th cs2" |
|
2253 by (unfold s_waiting_def, fold wq_def, simp) |
|
2254 thus ?thesis by (simp add: vt.th_not_waiting) |
|
2255 qed |
|
2256 qed |
|
2257 } thus ?thesis by (unfold waiting_unique_def, auto) |
|
2258 qed |
|
2259 |
|
2260 end |
2080 |
2261 |
2081 context valid_trace |
2262 context valid_trace |
2082 begin |
2263 begin |
2083 |
2264 |
2084 lemma waiting_unique_pre: (* ddd *) |
2265 lemma waiting_unique |
2085 assumes h11: "thread \<in> set (wq s cs1)" |
2266 [unfolded waiting_unique_def, rule_format]: |
2086 and h12: "thread \<noteq> hd (wq s cs1)" |
2267 shows "waiting_unique s" |
2087 assumes h21: "thread \<in> set (wq s cs2)" |
2268 proof(induct rule:ind) |
2088 and h22: "thread \<noteq> hd (wq s cs2)" |
2269 case Nil |
2089 and neq12: "cs1 \<noteq> cs2" |
2270 show ?case |
2090 shows "False" |
2271 by (unfold waiting_unique_def s_waiting_def, simp) |
2091 proof - |
2272 next |
2092 let "?Q" = "\<lambda> cs s. thread \<in> set (wq s cs) \<and> thread \<noteq> hd (wq s cs)" |
2273 case (Cons s e) |
2093 from h11 and h12 have q1: "?Q cs1 s" by simp |
2274 then interpret vt: valid_trace_e s e by simp |
2094 from h21 and h22 have q2: "?Q cs2 s" by simp |
2275 show ?case using Cons(2) vt.waiting_unique_kept |
2095 have nq1: "\<not> ?Q cs1 []" by (simp add:wq_def) |
2276 by simp |
2096 have nq2: "\<not> ?Q cs2 []" by (simp add:wq_def) |
2277 qed |
2097 from p_split [of "?Q cs1", OF q1 nq1] |
2278 |
2098 obtain t1 where lt1: "t1 < length s" |
2279 end |
2099 and np1: "\<not> ?Q cs1 (moment t1 s)" |
2280 |
2100 and nn1: "(\<forall>i'>t1. ?Q cs1 (moment i' s))" by auto |
2281 subsection {* Acyclic keeping *} |
2101 from p_split [of "?Q cs2", OF q2 nq2] |
|
2102 obtain t2 where lt2: "t2 < length s" |
|
2103 and np2: "\<not> ?Q cs2 (moment t2 s)" |
|
2104 and nn2: "(\<forall>i'>t2. ?Q cs2 (moment i' s))" by auto |
|
2105 { fix s cs |
|
2106 assume q: "?Q cs s" |
|
2107 have "thread \<notin> runing s" |
|
2108 proof |
|
2109 assume "thread \<in> runing s" |
|
2110 hence " \<forall>cs. \<not> (thread \<in> set (wq_fun (schs s) cs) \<and> |
|
2111 thread \<noteq> hd (wq_fun (schs s) cs))" |
|
2112 by (unfold runing_def s_waiting_def readys_def, auto) |
|
2113 from this[rule_format, of cs] q |
|
2114 show False by (simp add: wq_def) |
|
2115 qed |
|
2116 } note q_not_runing = this |
|
2117 { fix t1 t2 cs1 cs2 |
|
2118 assume lt1: "t1 < length s" |
|
2119 and np1: "\<not> ?Q cs1 (moment t1 s)" |
|
2120 and nn1: "(\<forall>i'>t1. ?Q cs1 (moment i' s))" |
|
2121 and lt2: "t2 < length s" |
|
2122 and np2: "\<not> ?Q cs2 (moment t2 s)" |
|
2123 and nn2: "(\<forall>i'>t2. ?Q cs2 (moment i' s))" |
|
2124 and lt12: "t1 < t2" |
|
2125 let ?t3 = "Suc t2" |
|
2126 interpret ve2: valid_moment_e _ t2 using lt2 |
|
2127 by (unfold_locales, simp) |
|
2128 let ?e = ve2.next_e |
|
2129 have "t2 < ?t3" by simp |
|
2130 from nn2 [rule_format, OF this] and ve2.trace_e |
|
2131 have h1: "thread \<in> set (wq (?e#moment t2 s) cs2)" and |
|
2132 h2: "thread \<noteq> hd (wq (?e#moment t2 s) cs2)" by auto |
|
2133 have ?thesis |
|
2134 proof - |
|
2135 have "thread \<in> runing (moment t2 s)" |
|
2136 proof(cases "thread \<in> set (wq (moment t2 s) cs2)") |
|
2137 case True |
|
2138 have "?e = V thread cs2" |
|
2139 proof - |
|
2140 have eq_th: "thread = hd (wq (moment t2 s) cs2)" |
|
2141 using True and np2 by auto |
|
2142 thus ?thesis |
|
2143 using True h2 ve2.vat_moment_e.wq_out_inv by blast |
|
2144 qed |
|
2145 thus ?thesis |
|
2146 using step.cases ve2.vat_moment_e.pip_e by auto |
|
2147 next |
|
2148 case False |
|
2149 hence "?e = P thread cs2" |
|
2150 using h1 ve2.vat_moment_e.wq_in_inv by blast |
|
2151 thus ?thesis |
|
2152 using step.cases ve2.vat_moment_e.pip_e by auto |
|
2153 qed |
|
2154 moreover have "thread \<notin> runing (moment t2 s)" |
|
2155 by (rule q_not_runing[OF nn1[rule_format, OF lt12]]) |
|
2156 ultimately show ?thesis by simp |
|
2157 qed |
|
2158 } note lt_case = this |
|
2159 show ?thesis |
|
2160 proof - |
|
2161 { assume "t1 < t2" |
|
2162 from lt_case[OF lt1 np1 nn1 lt2 np2 nn2 this] |
|
2163 have ?thesis . |
|
2164 } moreover { |
|
2165 assume "t2 < t1" |
|
2166 from lt_case[OF lt2 np2 nn2 lt1 np1 nn1 this] |
|
2167 have ?thesis . |
|
2168 } moreover { |
|
2169 assume eq_12: "t1 = t2" |
|
2170 let ?t3 = "Suc t2" |
|
2171 interpret ve2: valid_moment_e _ t2 using lt2 |
|
2172 by (unfold_locales, simp) |
|
2173 let ?e = ve2.next_e |
|
2174 have "t2 < ?t3" by simp |
|
2175 from nn2 [rule_format, OF this] and ve2.trace_e |
|
2176 have h1: "thread \<in> set (wq (?e#moment t2 s) cs2)" by auto |
|
2177 have lt_2: "t2 < ?t3" by simp |
|
2178 from nn2 [rule_format, OF this] and ve2.trace_e |
|
2179 have h1: "thread \<in> set (wq (?e#moment t2 s) cs2)" and |
|
2180 h2: "thread \<noteq> hd (wq (?e#moment t2 s) cs2)" by auto |
|
2181 from nn1[rule_format, OF lt_2[folded eq_12], unfolded ve2.trace_e[folded eq_12]] |
|
2182 eq_12[symmetric] |
|
2183 have g1: "thread \<in> set (wq (?e#moment t1 s) cs1)" and |
|
2184 g2: "thread \<noteq> hd (wq (?e#moment t1 s) cs1)" by auto |
|
2185 have "?e = V thread cs2 \<or> ?e = P thread cs2" |
|
2186 using h1 h2 np2 ve2.vat_moment_e.wq_in_inv |
|
2187 ve2.vat_moment_e.wq_out_inv by blast |
|
2188 moreover have "?e = V thread cs1 \<or> ?e = P thread cs1" |
|
2189 using eq_12 g1 g2 np1 ve2.vat_moment_e.wq_in_inv |
|
2190 ve2.vat_moment_e.wq_out_inv by blast |
|
2191 ultimately have ?thesis using neq12 by auto |
|
2192 } ultimately show ?thesis using nat_neq_iff by blast |
|
2193 qed |
|
2194 qed |
|
2195 |
|
2196 text {* |
|
2197 This lemma is a simple corrolary of @{text "waiting_unique_pre"}. |
|
2198 *} |
|
2199 |
|
2200 lemma waiting_unique: |
|
2201 assumes "waiting s th cs1" |
|
2202 and "waiting s th cs2" |
|
2203 shows "cs1 = cs2" |
|
2204 using waiting_unique_pre assms |
|
2205 unfolding wq_def s_waiting_def |
|
2206 by auto |
|
2207 |
|
2208 end |
|
2209 |
|
2210 lemma (in valid_trace_v) |
|
2211 preced_es [simp]: "preced th (e#s) = preced th s" |
|
2212 by (unfold is_v preced_def, simp) |
|
2213 |
|
2214 lemma the_preced_v[simp]: "the_preced (V th cs#s) = the_preced s" |
|
2215 proof |
|
2216 fix th' |
|
2217 show "the_preced (V th cs # s) th' = the_preced s th'" |
|
2218 by (unfold the_preced_def preced_def, simp) |
|
2219 qed |
|
2220 |
|
2221 |
|
2222 lemma (in valid_trace_v) |
|
2223 the_preced_es: "the_preced (e#s) = the_preced s" |
|
2224 by (unfold is_v preced_def, simp) |
|
2225 |
|
2226 context valid_trace_p |
|
2227 begin |
|
2228 |
|
2229 lemma not_holding_s_th_cs: "\<not> holding s th cs" |
|
2230 proof |
|
2231 assume otherwise: "holding s th cs" |
|
2232 from pip_e[unfolded is_p] |
|
2233 show False |
|
2234 proof(cases) |
|
2235 case (thread_P) |
|
2236 moreover have "(Cs cs, Th th) \<in> RAG s" |
|
2237 using otherwise cs_holding_def |
|
2238 holding_eq th_not_in_wq by auto |
|
2239 ultimately show ?thesis by auto |
|
2240 qed |
|
2241 qed |
|
2242 |
|
2243 end |
|
2244 |
|
2245 |
|
2246 lemma (in valid_trace_v_n) finite_waiting_set: |
|
2247 "finite {(Th th', Cs cs) |th'. next_th s th cs th'}" |
|
2248 by (simp add: waiting_set_eq) |
|
2249 |
|
2250 lemma (in valid_trace_v_n) finite_holding_set: |
|
2251 "finite {(Cs cs, Th th') |th'. next_th s th cs th'}" |
|
2252 by (simp add: holding_set_eq) |
|
2253 |
|
2254 lemma (in valid_trace_v_e) finite_waiting_set: |
|
2255 "finite {(Th th', Cs cs) |th'. next_th s th cs th'}" |
|
2256 by (simp add: waiting_set_eq) |
|
2257 |
|
2258 lemma (in valid_trace_v_e) finite_holding_set: |
|
2259 "finite {(Cs cs, Th th') |th'. next_th s th cs th'}" |
|
2260 by (simp add: holding_set_eq) |
|
2261 |
|
2262 |
2282 |
2263 context valid_trace_v_e |
2283 context valid_trace_v_e |
2264 begin |
2284 begin |
2265 |
2285 |
2266 lemma |
2286 lemma |