Theory FWWait

(*  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