Theory FWLiftingSem

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

section ‹Semantic properties of lifted predicates›

theory FWLiftingSem
imports
  FWSemantics
  FWLifting
begin

context multithreaded_base begin

lemma redT_preserves_ts_inv_ok:
  " s -tta s'; ts_inv_ok (thr s) I 
   ts_inv_ok (thr s') (upd_invs I P tat)"
by(erule redT.cases)(fastforce intro: ts_inv_ok_upd_invs ts_inv_ok_upd_ts redT_updTs_Some)+

lemma RedT_preserves_ts_inv_ok:
  " s -▹ttas→* s'; ts_inv_ok (thr s) I 
   ts_inv_ok (thr s') (upd_invs I Q (concat (map (thr_a  snd) ttas)))"
by(induct rule: RedT_induct)(auto intro: redT_preserves_ts_inv_ok)

lemma redT_upd_inv_ext:
  fixes I :: "'t  'i"
  shows " s -tta s'; ts_inv_ok (thr s) I   I m upd_invs I P tat"
by(erule redT.cases, auto intro: ts_inv_ok_inv_ext_upd_invs)

lemma RedT_upd_inv_ext:
  fixes I :: "'t  'i"
  shows " s -▹ttas→* s'; ts_inv_ok (thr s) I 
          I m upd_invs I P (concat (map (thr_a  snd) ttas))"
proof(induct rule: RedT_induct)
  case refl thus ?case by simp
next
  case (step S TTAS S' T TA S'')
  hence "ts_inv_ok (thr S') (upd_invs I P (concat (map (thr_a  snd) TTAS)))"
    by -(rule RedT_preserves_ts_inv_ok)
  hence "upd_invs I P (concat (map (thr_a  snd) TTAS)) m upd_invs (upd_invs I P (concat (map (thr_a  snd) TTAS))) P TAt" 
    using step by -(rule redT_upd_inv_ext)
  with step show ?case by(auto elim!: map_le_trans simp add: comp_def)
qed

end

locale lifting_inv = multithreaded final r convert_RA
  for final :: "'x  bool" 
  and r :: "('l,'t,'x,'m,'w,'o) semantics" ("_  _ -_ _" [50,0,0,50] 80) 
  and convert_RA :: "'l released_locks  'o list"
  +
  fixes P :: "'i  't  'x  'm  bool"
  assumes invariant_red: " t  x, m -ta x', m'; P i t x m   P i t x' m'"
  and invariant_NewThread: " t  x, m -ta x', m'; P i t x m; NewThread t'' x'' m'  set tat  
                             i''. P i'' t'' x'' m'"
  and invariant_other: " t  x, m -ta x', m'; P i t x m; P i'' t'' x'' m   P i'' t'' x'' m'"
begin

lemma redT_updTs_invariant:
  fixes ln
  assumes tsiP: "ts_inv P I ts m"
  and red: "t  x, m -ta x', m'"
  and tao: "thread_oks ts tat"
  and tst: "ts t = (x, ln)"
  shows "ts_inv P (upd_invs I P tat) ((redT_updTs ts tat)(t  (x', ln'))) m'"
proof(rule ts_invI)
  fix T X LN
  assume XLN: "((redT_updTs ts tat)(t  (x', ln'))) T = (X, LN)"
  from tsiP ts t = (x, ln) obtain i where "I t = i" "P i t x m" 
    by(auto dest: ts_invD)
  show "i. upd_invs I P tat T = i  P i T X m'"
  proof(cases "T = t")
    case True
    from red P i t x m have "P i t x' m'" by(rule invariant_red)
    moreover from I t = i ts t = (x, ln) tao 
    have "upd_invs I P tat t = i"
      by(simp add: upd_invs_Some)
    ultimately show ?thesis using True XLN by simp
  next
    case False
    show ?thesis
    proof(cases "ts T")
      case None
      with XLN tao False have "m'. NewThread T X m'  set tat"
        by(auto dest: redT_updTs_new_thread)
      with red have nt: "NewThread T X m'  set tat" by(auto dest: new_thread_memory)
      with red P i t x m have "i''. P i'' T X m'" by(rule invariant_NewThread)
      hence "P (SOME i. P i T X m') T X m'" by(rule someI_ex)
      with nt tao show ?thesis by(auto intro: SOME_new_thread_upd_invs) 
    next
      case (Some a)
      obtain X' LN' where [simp]: "a = (X', LN')" by(cases a)
      with ts T = a have esT: "ts T = (X', LN')" by simp
      hence "redT_updTs ts tat T = (X', LN')"
        using thread_oks ts tat by(auto intro: redT_updTs_Some)
      moreover from esT tsiP obtain i' where "I T = i'" "P i' T X' m"
        by(auto dest: ts_invD)
      from red P i t x m P i' T X' m
      have "P i' T X' m'" by(rule invariant_other)
      moreover from I T = i' esT tao have "upd_invs I P tat T = i'"
        by(simp add: upd_invs_Some)
      ultimately show ?thesis using XLN False by simp
    qed
  qed
qed

theorem redT_invariant:
  assumes redT: "s -tta s'"
  and esinvP: "ts_inv P I (thr s) (shr s)"
  shows "ts_inv P (upd_invs I P tat) (thr s') (shr s')"
using redT
proof(cases rule: redT_elims)
  case acquire thus ?thesis using esinvP 
    by(auto intro!: ts_invI split: if_split_asm dest: ts_invD)
next
  case (normal x x' m')
  with esinvP
  have "ts_inv P (upd_invs I P tat) ((redT_updTs (thr s) tat)(t  (x', redT_updLns (locks s) t no_wait_locks tal))) m'"
    by(auto intro: redT_updTs_invariant)
  thus ?thesis using normal by simp
qed

theorem RedT_invariant:
  assumes RedT: "s -▹ttas→* s'"
  and esinvQ: "ts_inv P I (thr s) (shr s)"
  shows "ts_inv P (upd_invs I P (concat (map (thr_a  snd) ttas))) (thr s') (shr s')"
using RedT esinvQ
proof(induct rule: RedT_induct)
  case refl thus ?case by(simp (no_asm))
next
  case (step S TTAS S' T TA S'')
  note IH = ts_inv P I (thr S) (shr S)  ts_inv P (upd_invs I P (concat (map (thr_a  snd) TTAS))) (thr S') (shr S')
  with ts_inv P I (thr S) (shr S)
  have "ts_inv P (upd_invs I P (concat (map (thr_a  snd) TTAS))) (thr S') (shr S')" by blast
  with S' -TTA S'' 
  have "ts_inv P (upd_invs (upd_invs I P (concat (map (thr_a  snd) TTAS))) P TAt) (thr S'') (shr S'')"
    by(rule redT_invariant)
  thus ?case by(simp add: comp_def)
qed

lemma invariant3p_ts_inv: "invariant3p redT {s. I. ts_inv P I (thr s) (shr s)}"
by(auto intro!: invariant3pI dest: redT_invariant)

end

locale lifting_wf = multithreaded final r convert_RA
  for final :: "'x  bool" 
  and r :: "('l,'t,'x,'m,'w,'o) semantics" ("_  _ -_ _" [50,0,0,50] 80) 
  and convert_RA :: "'l released_locks  'o list"
  +
  fixes P :: "'t  'x  'm  bool"
  assumes preserves_red: " t  x, m -ta x', m'; P t x m   P t x' m'"
  and preserves_NewThread: " t  x, m -ta x', m'; P t x m; NewThread t'' x'' m'  set tat  
                             P t'' x'' m'"
  and preserves_other: " t  x, m -ta x', m'; P t x m; P t'' x'' m   P t'' x'' m'"
begin

lemma lifting_inv: "lifting_inv final r (λ_ :: unit. P)"
by(unfold_locales)(blast intro: preserves_red preserves_NewThread preserves_other)+

lemma redT_updTs_preserves:
  fixes ln
  assumes esokQ: "ts_ok P ts m"
  and red: "t  x, m -ta x', m'"
  and "ts t = (x, ln)"
  and "thread_oks ts tat"
  shows "ts_ok P ((redT_updTs ts tat)(t  (x', ln'))) m'"
proof -
  interpret lifting_inv final r convert_RA "λ_ :: unit. P" by(rule lifting_inv)
  from esokQ obtain I :: "'t  unit" where "ts_inv (λ_. P) I ts m" by(rule ts_ok_into_ts_inv_const)
  hence "ts_inv (λ_. P) (upd_invs I (λ_. P) tat) ((redT_updTs ts tat)(t  (x', ln'))) m'"
    using red thread_oks ts tat ts t = (x, ln) by(rule redT_updTs_invariant)
  thus ?thesis by(rule ts_inv_const_into_ts_ok)
qed

theorem redT_preserves:
  assumes redT: "s -tta s'"
  and esokQ: "ts_ok P (thr s) (shr s)"
  shows "ts_ok P (thr s') (shr s')"
proof -
  interpret lifting_inv final r convert_RA "λ_ :: unit. P" by(rule lifting_inv)
  from esokQ obtain I :: "'t  unit" where "ts_inv (λ_. P) I (thr s) (shr s)" by(rule ts_ok_into_ts_inv_const)
  with redT have "ts_inv (λ_. P) (upd_invs I (λ_. P) tat) (thr s') (shr s')" by(rule redT_invariant)
  thus ?thesis by(rule ts_inv_const_into_ts_ok)
qed

theorem RedT_preserves:
  " s -▹ttas→* s'; ts_ok P (thr s) (shr s)   ts_ok P (thr s') (shr s')"
by(erule (1) RedT_lift_preserveD)(fastforce elim: redT_preserves)

lemma invariant3p_ts_ok: "invariant3p redT {s. ts_ok P (thr s) (shr s)}"
by(auto intro!: invariant3pI intro: redT_preserves)

end

lemma lifting_wf_Const [intro!]: 
  assumes "multithreaded final r"
  shows "lifting_wf final r (λt x m. k)"
proof -
  interpret multithreaded final r using assms .
  show ?thesis by unfold_locales blast+
qed

end