(* Title: JinjaThreads/Framework/FWWait.thy Author: Andreas Lochbihler *) section ‹Semantics of the thread actions for wait, notify and interrupt› theory FWWait imports FWState begin text ‹Update functions for the wait sets in the multithreaded state› inductive redT_updW :: "'t ⇒ ('w, 't) wait_sets ⇒ ('t,'w) wait_set_action ⇒ ('w,'t) wait_sets ⇒ bool" for t :: 't and ws :: "('w, 't) wait_sets" where "ws t' = ⌊InWS w⌋ ⟹ redT_updW t ws (Notify w) (ws(t' ↦ PostWS WSNotified))" | "(⋀t'. ws t' ≠ ⌊InWS w⌋) ⟹ redT_updW t ws (Notify w) ws" | "redT_updW t ws (NotifyAll w) (λt. if ws t = ⌊InWS w⌋ then ⌊PostWS WSNotified⌋ else ws t)" | "redT_updW t ws (Suspend w) (ws(t ↦ InWS w))" | "ws t' = ⌊InWS w⌋ ⟹ redT_updW t ws (WakeUp t') (ws(t' ↦ PostWS WSInterrupted))" | "(⋀w. ws t' ≠ ⌊InWS w⌋) ⟹ redT_updW t ws (WakeUp t') ws" | "redT_updW t ws Notified (ws(t := None))" | "redT_updW t ws WokenUp (ws(t := None))" definition redT_updWs :: "'t ⇒ ('w,'t) wait_sets ⇒ ('t,'w) wait_set_action list ⇒ ('w,'t) wait_sets ⇒ bool" where "redT_updWs t = rtrancl3p (redT_updW t)" inductive_simps redT_updW_simps [simp]: "redT_updW t ws (Notify w) ws'" "redT_updW t ws (NotifyAll w) ws'" "redT_updW t ws (Suspend w) ws'" "redT_updW t ws (WakeUp t') ws'" "redT_updW t ws WokenUp ws'" "redT_updW t ws Notified ws'" lemma redT_updW_total: "∃ws'. redT_updW t ws wa ws'" by(cases wa)(auto simp add: redT_updW.simps) lemma redT_updWs_total: "∃ws'. redT_updWs t ws was ws'" proof(induct was rule: rev_induct) case Nil thus ?case by(auto simp add: redT_updWs_def) next case (snoc wa was) then obtain ws' where "redT_updWs t ws was ws'" .. also from redT_updW_total[of t ws' wa] obtain ws'' where "redT_updW t ws' wa ws''" .. ultimately show ?case unfolding redT_updWs_def by(auto intro: rtrancl3p_step) qed lemma redT_updWs_trans: "⟦ redT_updWs t ws was ws'; redT_updWs t ws' was' ws'' ⟧ ⟹ redT_updWs t ws (was @ was') ws''" unfolding redT_updWs_def by(rule rtrancl3p_trans) lemma redT_updW_None_implies_None: "⟦ redT_updW t' ws wa ws'; ws t = None; t ≠ t' ⟧ ⟹ ws' t = None" by(auto simp add: redT_updW.simps) lemma redT_updWs_None_implies_None: assumes "redT_updWs t' ws was ws'" and "t ≠ t'" and "ws t = None" shows "ws' t = None" using ‹redT_updWs t' ws was ws'› ‹ws t = None› unfolding redT_updWs_def by induct(auto intro: redT_updW_None_implies_None[OF _ _ ‹t ≠ t'›]) lemma redT_updW_PostWS_imp_PostWS: "⟦ redT_updW t ws wa ws'; ws t'' = ⌊PostWS w⌋; t'' ≠ t ⟧ ⟹ ws' t'' = ⌊PostWS w⌋" by(auto simp add: redT_updW.simps) lemma redT_updWs_PostWS_imp_PostWS: "⟦ redT_updWs t ws was ws'; t'' ≠ t; ws t'' = ⌊PostWS w⌋ ⟧ ⟹ ws' t'' = ⌊PostWS w⌋" unfolding redT_updWs_def by(induct rule: rtrancl3p.induct)(auto dest: redT_updW_PostWS_imp_PostWS) lemma redT_updW_Some_otherD: "⟦ redT_updW t' ws wa ws'; ws' t = ⌊w⌋; t ≠ t' ⟧ ⟹ (case w of InWS w' ⇒ ws t = ⌊InWS w'⌋ | _ ⇒ ws t = ⌊w⌋ ∨ (∃w'. ws t = ⌊InWS w'⌋))" by(auto simp add: redT_updW.simps split: if_split_asm wait_set_status.split) lemma redT_updWs_Some_otherD: "⟦ redT_updWs t' ws was ws'; ws' t = ⌊w⌋; t ≠ t' ⟧ ⟹ (case w of InWS w' ⇒ ws t = ⌊InWS w'⌋ | _ ⇒ ws t = ⌊w⌋ ∨ (∃w'. ws t = ⌊InWS w'⌋))" unfolding redT_updWs_def apply(induct arbitrary: w rule: rtrancl3p.induct) apply(fastforce split: wait_set_status.splits dest: redT_updW_Some_otherD)+ done lemma redT_updW_None_SomeD: "⟦ redT_updW t ws wa ws'; ws' t' = ⌊w⌋; ws t' = None ⟧ ⟹ t = t' ∧ (∃w'. w = InWS w' ∧ wa = Suspend w')" by(auto simp add: redT_updW.simps split: if_split_asm) lemma redT_updWs_None_SomeD: "⟦ redT_updWs t ws was ws'; ws' t' = ⌊w⌋; ws t' = None ⟧ ⟹ t = t' ∧ (∃w'. Suspend w' ∈ set was)" unfolding redT_updWs_def proof(induct arbitrary: w rule: rtrancl3p.induct) case (rtrancl3p_refl ws) thus ?case by simp next case (rtrancl3p_step ws was ws' wa ws'') show ?case proof(cases "ws' t'") case None from redT_updW_None_SomeD[OF ‹redT_updW t ws' wa ws''›, OF ‹ws'' t' = ⌊w⌋› this] show ?thesis by auto next case (Some w') with ‹ws t' = None› rtrancl3p_step.hyps(2) show ?thesis by auto qed qed lemma redT_updW_neq_Some_SomeD: "⟦ redT_updW t' ws wa ws'; ws' t = ⌊InWS w⌋; ws t ≠ ⌊InWS w⌋ ⟧ ⟹ t = t' ∧ wa = Suspend w" by(auto simp add: redT_updW.simps split: if_split_asm) lemma redT_updWs_neq_Some_SomeD: "⟦ redT_updWs t ws was ws'; ws' t' = ⌊InWS w⌋; ws t' ≠ ⌊InWS w⌋ ⟧ ⟹ t = t' ∧ Suspend w ∈ set was" unfolding redT_updWs_def proof(induct rule: rtrancl3p.induct) case rtrancl3p_refl thus ?case by simp next case (rtrancl3p_step ws was ws' wa ws'') show ?case proof(cases "ws' t' = ⌊InWS w⌋") case True with ‹ws t' ≠ ⌊InWS w⌋› ‹⟦ws' t' = ⌊InWS w⌋; ws t' ≠ ⌊InWS w⌋⟧ ⟹ t = t' ∧ Suspend w ∈ set was› show ?thesis by simp next case False with ‹redT_updW t ws' wa ws''› ‹ws'' t' = ⌊InWS w⌋› have "t' = t ∧ wa = Suspend w" by(rule redT_updW_neq_Some_SomeD) thus ?thesis by auto qed qed lemma redT_updW_not_Suspend_Some: "⟦ redT_updW t ws wa ws'; ws' t = ⌊w'⌋; ws t = ⌊w⌋; ⋀w. wa ≠ Suspend w ⟧ ⟹ w' = w ∨ (∃w'' w'''. w = InWS w'' ∧ w' = PostWS w''')" by(auto simp add: redT_updW.simps split: if_split_asm) lemma redT_updWs_not_Suspend_Some: "⟦ redT_updWs t ws was ws'; ws' t = ⌊w'⌋; ws t = ⌊w⌋; ⋀w. Suspend w ∉ set was ⟧ ⟹ w' = w ∨ (∃w'' w'''. w = InWS w'' ∧ w' = PostWS w''')" unfolding redT_updWs_def proof(induct arbitrary: w rule: rtrancl3p_converse_induct) case refl thus ?case by simp next case (step ws wa ws' was ws'') note ‹ws'' t = ⌊w'⌋› moreover have "ws' t ≠ None" proof assume "ws' t = None" with ‹rtrancl3p (redT_updW t) ws' was ws''› ‹ws'' t = ⌊w'⌋› obtain w' where "Suspend w' ∈ set was" unfolding redT_updWs_def[symmetric] by(auto dest: redT_updWs_None_SomeD) with ‹Suspend w' ∉ set (wa # was)› show False by simp qed then obtain w'' where "ws' t = ⌊w''⌋" by auto moreover { fix w from ‹Suspend w ∉ set (wa # was)› have "Suspend w ∉ set was" by simp } ultimately have "w' = w'' ∨ (∃w''' w''''. w'' = InWS w''' ∧ w' = PostWS w'''')" by(rule step.hyps) moreover { fix w from ‹Suspend w ∉ set (wa # was)› have "wa ≠ Suspend w" by auto } note redT_updW_not_Suspend_Some[OF ‹redT_updW t ws wa ws'›, OF ‹ws' t = ⌊w''⌋› ‹ws t = ⌊w⌋› this] ultimately show ?case by auto qed lemma redT_updWs_WokenUp_SuspendD: "⟦ redT_updWs t ws was ws'; Notified ∈ set was ∨ WokenUp ∈ set was; ws' t = ⌊w⌋ ⟧ ⟹ ∃w. Suspend w ∈ set was" unfolding redT_updWs_def by(induct rule: rtrancl3p_converse_induct)(auto dest: redT_updWs_None_SomeD[unfolded redT_updWs_def]) lemma redT_updW_Woken_Up_same_no_Notified_Interrupted: "⟦ redT_updW t ws wa ws'; ws' t = ⌊PostWS w⌋; ws t = ⌊PostWS w⌋; ⋀w. wa ≠ Suspend w ⟧ ⟹ wa ≠ Notified ∧ wa ≠ WokenUp" by(fastforce) lemma redT_updWs_Woken_Up_same_no_Notified_Interrupted: "⟦ redT_updWs t ws was ws'; ws' t = ⌊PostWS w⌋; ws t = ⌊PostWS w⌋; ⋀w. Suspend w ∉ set was ⟧ ⟹ Notified ∉ set was ∧ WokenUp ∉ set was" unfolding redT_updWs_def proof(induct rule: rtrancl3p_converse_induct) case refl thus ?case by simp next case (step ws wa ws' was ws'') note Suspend = ‹⋀w. Suspend w ∉ set (wa # was)› note ‹ws'' t = ⌊PostWS w⌋› moreover have "ws' t = ⌊PostWS w⌋" proof(cases "ws' t") case None with ‹rtrancl3p (redT_updW t) ws' was ws''› ‹ws'' t = ⌊PostWS w⌋› obtain w where "Suspend w ∈ set was" unfolding redT_updWs_def[symmetric] by(auto dest: redT_updWs_None_SomeD) with Suspend[of w] have False by simp thus ?thesis .. next case (Some w') thus ?thesis using ‹ws t = ⌊PostWS w⌋› Suspend ‹redT_updW t ws wa ws'› by(auto simp add: redT_updW.simps split: if_split_asm) qed moreover { fix w from Suspend[of w] have "Suspend w ∉ set was" by simp } ultimately have "Notified ∉ set was ∧ WokenUp ∉ set was" by(rule step.hyps) moreover { fix w from Suspend[of w] have "wa ≠ Suspend w" by auto } with ‹redT_updW t ws wa ws'› ‹ws' t = ⌊PostWS w⌋› ‹ws t = ⌊PostWS w⌋› have "wa ≠ Notified ∧ wa ≠ WokenUp" by(rule redT_updW_Woken_Up_same_no_Notified_Interrupted) ultimately show ?case by auto qed text ‹Preconditions for wait set actions› definition wset_actions_ok :: "('w,'t) wait_sets ⇒ 't ⇒ ('t,'w) wait_set_action list ⇒ bool" where "wset_actions_ok ws t was ⟷ (if Notified ∈ set was then ws t = ⌊PostWS WSNotified⌋ else if WokenUp ∈ set was then ws t = ⌊PostWS WSWokenUp⌋ else ws t = None)" lemma wset_actions_ok_Nil [simp]: "wset_actions_ok ws t [] ⟷ ws t = None" by(simp add: wset_actions_ok_def) definition waiting :: "'w wait_set_status option ⇒ bool" where "waiting w ⟷ (∃w'. w = ⌊InWS w'⌋)" lemma not_waiting_iff: "¬ waiting w ⟷ w = None ∨ (∃w'. w = ⌊PostWS w'⌋)" apply(cases "w") apply(case_tac [2] a) apply(auto simp add: waiting_def) done lemma waiting_code [code]: "waiting None = False" "⋀w. waiting ⌊PostWS w⌋ = False" "⋀w. waiting ⌊InWS w⌋ = True" by(simp_all add: waiting_def) end