Theory FWWellform

(*  Title:      JinjaThreads/Framework/FWWellform.thy
    Author:     Andreas Lochbihler
*)

section ‹Wellformedness conditions for the multithreaded state›

theory FWWellform
imports
  FWLocking
  FWThread
  FWWait
  FWCondAction
begin

text‹Well-formedness property: Locks are held by real threads›

definition
  lock_thread_ok :: "('l, 't) locks ⇒ ('l, 't,'x) thread_info ⇒ bool"
where [code del]:
  "lock_thread_ok ls ts ≡ ∀l t. has_lock (ls $ l) t ⟶ (∃xw. ts t = ⌊xw⌋)"

lemma lock_thread_ok_code [code]: 
  "lock_thread_ok ls ts = finfun_All ((λl. case l of None ⇒ True | ⌊(t, n)⌋ ⇒ (ts t ≠ None)) ∘$ ls)"
by(simp add: lock_thread_ok_def finfun_All_All has_lock_has_locks_conv has_locks_iff o_def)

lemma lock_thread_okI:
  "(⋀l t. has_lock (ls $ l) t ⟹ ∃xw. ts t = ⌊xw⌋) ⟹ lock_thread_ok ls ts"
by(auto simp add: lock_thread_ok_def)

lemma lock_thread_okD:
  "⟦ lock_thread_ok ls ts; has_lock (ls $ l) t ⟧ ⟹ ∃xw. ts t = ⌊xw⌋"
by(fastforce simp add: lock_thread_ok_def)

lemma lock_thread_okD':
  "⟦ lock_thread_ok ls ts; has_locks (ls $ l) t = Suc n ⟧ ⟹ ∃xw. ts t = ⌊xw⌋"
by(auto elim: lock_thread_okD[where l=l] simp del: split_paired_Ex)

lemma lock_thread_okE:
  "⟦ lock_thread_ok ls ts; ∀l t. has_lock (ls $ l) t ⟶ (∃xw. ts t = ⌊xw⌋) ⟹ P ⟧ ⟹ P"
by(auto simp add: lock_thread_ok_def simp del: split_paired_Ex)

lemma lock_thread_ok_upd:
  "lock_thread_ok ls ts ⟹ lock_thread_ok ls (ts(t ↦ xw))"
by(auto intro!: lock_thread_okI dest: lock_thread_okD)

lemma lock_thread_ok_has_lockE:
  assumes "lock_thread_ok ls ts"
  and "has_lock (ls $ l) t"
  obtains x ln' where "ts t = ⌊(x, ln')⌋"
using assms
by(auto dest!: lock_thread_okD)

lemma redT_updLs_preserves_lock_thread_ok:
  assumes lto: "lock_thread_ok ls ts"
  and tst: "ts t = ⌊xw⌋"
  shows "lock_thread_ok (redT_updLs ls t las) ts"
proof(rule lock_thread_okI)
  fix L T
  assume ru: "has_lock (redT_updLs ls t las $ L) T"
  show "∃xw. ts T = ⌊xw⌋"
  proof(cases "t = T")
    case True
    thus ?thesis using tst lto
      by(auto elim: lock_thread_okE)
  next
    case False
    with ru have "has_lock (ls $ L) T"
      by(rule redT_updLs_Some_thread_idD) 
    thus ?thesis using lto
      by(auto elim!: lock_thread_okE simp del: split_paired_Ex)
  qed
qed

lemma redT_updTs_preserves_lock_thread_ok:
  assumes lto: "lock_thread_ok ls ts"
  shows "lock_thread_ok ls (redT_updTs ts nts)"
proof(rule lock_thread_okI)
  fix l t
  assume "has_lock (ls $ l) t"
  with lto have "∃xw. ts t = ⌊xw⌋"
    by(auto elim!: lock_thread_okE simp del: split_paired_Ex)
  thus "∃xw. redT_updTs ts nts t = ⌊xw⌋"
    by(auto intro: redT_updTs_Some1 simp del: split_paired_Ex)
qed

lemma lock_thread_ok_has_lock:
  assumes "lock_thread_ok ls ts"
  and "has_lock (ls $ l) t"
  obtains xw where "ts t = ⌊xw⌋"
using assms
by(auto dest!: lock_thread_okD)

lemma lock_thread_ok_None_has_locks_0:
  "⟦ lock_thread_ok ls ts; ts t = None ⟧ ⟹ has_locks (ls $ l) t = 0"
by(rule ccontr)(auto dest: lock_thread_okD)

lemma redT_upds_preserves_lock_thread_ok:
  "⟦lock_thread_ok ls ts; ts t = ⌊xw⌋; thread_oks ts tas⟧
  ⟹ lock_thread_ok (redT_updLs ls t las) ((redT_updTs ts tas)(t ↦ xw'))"
apply(rule lock_thread_okI)
apply(clarsimp simp del: split_paired_Ex)
apply(drule has_lock_upd_locks_implies_has_lock, simp)
apply(drule lock_thread_okD, assumption)
apply(erule exE)
by(rule redT_updTs_Some1)

lemma acquire_all_preserves_lock_thread_ok:
  fixes ln
  shows "⟦ lock_thread_ok ls ts; ts t = ⌊(x, ln)⌋ ⟧ ⟹ lock_thread_ok (acquire_all ls t ln) (ts(t ↦ xw))"
by(rule lock_thread_okI)(auto dest!: has_lock_acquire_locks_implies_has_lock dest: lock_thread_okD)

text ‹Well-formedness condition: Wait sets contain only real threads›

definition wset_thread_ok :: "('w, 't) wait_sets ⇒ ('l, 't, 'x) thread_info ⇒ bool"
where "wset_thread_ok ws ts ≡ ∀t. ts t = None ⟶ ws t = None"

lemma wset_thread_okI:
  "(⋀t. ts t = None ⟹ ws t = None) ⟹ wset_thread_ok ws ts"
by(simp add: wset_thread_ok_def)

lemma wset_thread_okD:
  "⟦ wset_thread_ok ws ts; ts t = None ⟧ ⟹ ws t = None"
by(simp add: wset_thread_ok_def)

lemma wset_thread_ok_conv_dom:
  "wset_thread_ok ws ts ⟷ dom ws ⊆ dom ts"
by(auto simp add: wset_thread_ok_def)

lemma wset_thread_ok_upd:
  "wset_thread_ok ls ts ⟹ wset_thread_ok ls (ts(t ↦ xw))"
by(auto intro!: wset_thread_okI dest: wset_thread_okD split: if_split_asm)

lemma wset_thread_ok_upd_None:
  "wset_thread_ok ws ts ⟹ wset_thread_ok (ws(t := None)) (ts(t := None))"
by(auto intro!: wset_thread_okI dest: wset_thread_okD split: if_split_asm)

lemma wset_thread_ok_upd_Some:
  "wset_thread_ok ws ts ⟹ wset_thread_ok (ws(t := wo)) (ts(t ↦ xln))"
by(auto intro!: wset_thread_okI dest: wset_thread_okD split: if_split_asm)

lemma wset_thread_ok_upd_ws:
  "⟦ wset_thread_ok ws ts; ts t = ⌊xln⌋ ⟧ ⟹ wset_thread_ok (ws(t := w)) ts"
by(auto intro!: wset_thread_okI dest: wset_thread_okD)

lemma wset_thread_ok_NotifyAllI: 
  "wset_thread_ok ws ts ⟹ wset_thread_ok (λt. if ws t = ⌊w t⌋ then ⌊w' t⌋ else ws t) ts"
by(simp add: wset_thread_ok_def)

lemma redT_updTs_preserves_wset_thread_ok:
  assumes wto: "wset_thread_ok ws ts"
  shows "wset_thread_ok ws (redT_updTs ts nts)"
proof(rule wset_thread_okI)
  fix t
  assume "redT_updTs ts nts t = None"
  hence "ts t = None" by(rule redT_updTs_None)
  with wto show "ws t = None" by(rule wset_thread_okD)
qed

lemma redT_updW_preserve_wset_thread_ok: 
  "⟦ wset_thread_ok ws ts; redT_updW t ws wa ws'; ts t = ⌊xln⌋ ⟧ ⟹ wset_thread_ok ws' ts"
by(fastforce simp add: redT_updW.simps intro: wset_thread_okI wset_thread_ok_NotifyAllI wset_thread_ok_upd_ws dest: wset_thread_okD)

lemma redT_updWs_preserve_wset_thread_ok:
  "⟦ wset_thread_ok ws ts; redT_updWs t ws was ws'; ts t = ⌊xln⌋ ⟧ ⟹ wset_thread_ok ws' ts"
unfolding redT_updWs_def apply(rotate_tac 1)
by(induct rule: rtrancl3p_converse_induct)(auto intro: redT_updW_preserve_wset_thread_ok)

text ‹Well-formedness condition: Wait sets contain only non-final threads›

context final_thread begin

definition wset_final_ok :: "('w, 't) wait_sets ⇒ ('l, 't, 'x) thread_info ⇒ bool"
where "wset_final_ok ws ts ⟷ (∀t ∈ dom ws. ∃x ln. ts t = ⌊(x, ln)⌋ ∧ ¬ final x)"

lemma wset_final_okI:
  "(⋀t w. ws t = ⌊w⌋ ⟹ ∃x ln. ts t = ⌊(x, ln)⌋ ∧ ¬ final x) ⟹ wset_final_ok ws ts"
unfolding wset_final_ok_def by(blast)

lemma wset_final_okD:
  "⟦ wset_final_ok ws ts; ws t = ⌊w⌋ ⟧ ⟹ ∃x ln. ts t = ⌊(x, ln)⌋ ∧ ¬ final x"
unfolding wset_final_ok_def by(blast)

lemma wset_final_okE:
  assumes "wset_final_ok ws ts" "ws t = ⌊w⌋"
  and "⋀x ln. ts t = ⌊(x, ln)⌋ ⟹ ¬ final x ⟹ thesis"
  shows thesis
using assms by(blast dest: wset_final_okD)

lemma wset_final_ok_imp_wset_thread_ok:
  "wset_final_ok ws ts ⟹ wset_thread_ok ws ts"
apply(rule wset_thread_okI)
apply(rule ccontr)
apply(auto elim: wset_final_okE)
done

end

end