Theory FWProgress

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

header {* \isaheader{Progress theorem for the multithreaded semantics} *}

theory FWProgress imports FWDeadlock FWWellformSem begin

locale preserve_deadlocked = final_thread_wf + preserve_lock_behav begin

lemma redT_deadlocked_subset:
  assumes Red': "start_state -\<triangleright>ttas->* s"
  and Red: "s -t\<triangleright>ta-> s'"
  and t'dead: "deadlocked s t'"
  shows "deadlocked s' t'"
proof -
  from Red have tndead: "¬ deadlocked s t"
    by(auto dest: red_no_deadlock)
  with t'dead have t't: "t' ≠ t" by auto
  obtain las tas cas was obs where ta: "ta = (las, tas, cas, was, obs)" by (cases ta)
  obtain ls ts m ws where s [simp]: "s = (ls, (ts, m), ws)" by (cases s, auto)
  obtain ls' ts' m' ws' where s' [simp]: "s' = (ls', (ts', m'), ws')" by (cases s', auto)
  with s Red have "⟨ls, (ts, m), ws⟩ -t\<triangleright>ta-> ⟨ls', (ts', m'), ws'⟩" by simp
  thus "deadlocked s' t'"
  proof(cases rule: redT_elims4)
    case (normal x x' ta')
    with ta s s' Red have red: "⟨x, m⟩ -ta'-> ⟨x', m'⟩"
      and est: "ts t = ⌊(x, no_wait_locks)⌋"
      and lot: "lock_ok_las ls t las"
      and cct: "thread_oks ts tas"
      and cdt: "cond_action_oks (ls, (ts, m), ws) t cas"
      and wst: "ws t = None"
      and ws': "ws' = redT_updWs ws t was"
      and es': "ts' = redT_updTs ts \<lbrace>ta\<rbrace>t(t \<mapsto> (x', redT_updLns ls t no_wait_locks \<lbrace>ta\<rbrace>l))"
      and ls': "ls' = redT_updLs ls t las"
      and [simp]: "ta = observable_ta_of ta'"
      by auto
    from red have "¬ final x" by(auto dest: final_no_red)
    with tndead est s est wst have nafe: "¬ all_final_except s (deadlocked s)"
      by(fastsimp simp add: all_final_except_def not_final_thread_iff)
    from t'dead show ?thesis
    proof(coinduct)
      case (deadlocked t'')
      note t''dead = this
      with Red have t''t: "t'' ≠ t"
        by(auto dest: red_no_deadlock)
      from t''dead show ?case
      proof(cases rule: deadlocked_elims)
        case (lock X)
        hence est'': "ts t'' = ⌊(X, no_wait_locks)⌋"
          and msE: "⟨X, m⟩ \<wrong>"
          and csexdead: "∀LT. ⟨X, m⟩ LT \<wrong> --> (∃t'. (deadlocked s t' ∨ final_thread s t') ∧
                                                  (∃lt ∈ LT. must_wait s t'' lt t'))"
          by auto
        from t''t Red est'' s s'
        have es't'': "ts' t'' = ⌊(X, no_wait_locks)⌋"
          by(auto elim!: redT_ts_Some_inv)
        note es't'' moreover
        from msE obtain X' M' ta
          where red': "⟨X, m⟩ -ta-> ⟨X', M'⟩"
          by(auto elim: must_syncE)
        let ?LT = "collect_locks \<lbrace>ta\<rbrace>l <+> {t. Join t ∈ set \<lbrace>ta\<rbrace>c}"
        from red' have csLT: "⟨X, m⟩ ?LT \<wrong>" by(auto intro: can_syncI)
        with csexdead[rule_format] have "?LT ≠ {}" by auto
        with est'' csLT have msE': "⟨X, m'⟩ \<wrong>"
          by(rule can_lock_preserved[OF Red' Red, simplified])
        moreover
        { fix LT
          assume clL'': "⟨X, m'⟩ LT \<wrong>"
          with clL'' est'' have "∃LT'⊆LT. ⟨X, m⟩ LT' \<wrong>"
            by - (rule can_lock_devreserp[OF Red' Red, simplified shr_conv s], auto)
          then obtain LT' where clL': "⟨X, m⟩ LT' \<wrong>"
            and LL': "LT' ⊆ LT" by blast
          with csexdead obtain t' lt
            where t'dead: "deadlocked s t' ∨ final_thread s t'"
            and lt: "lt ∈ LT" and mw: "must_wait s t'' lt t'"
            by blast
          from t'dead Red s have tt': "t ≠ t'"
            by(auto dest: red_no_deadlock final_no_redT elim: final_threadE)
          from mw have "must_wait s' t'' lt t'"
          proof(induct rule: must_wait_elims)
            case (lock l)
            from lot have "lock_actions_ok (lsf l) t (lasf l)"
              by(simp add: lock_ok_las_def)
            with tt' ls' `has_lock ((locks s)f l) t'`
            have hl't': "has_lock (ls'f l) t'" by(auto)
            with `lt = Inl l` `t' ≠ t''` show ?thesis by auto
          next
            case thread
            note nftt' = `not_final_thread s t'`
            from tt' t'dead Red cct es' ta have ts't': "ts' t' = ts t'"
              by(auto elim!: deadlocked_thread_exists final_threadE intro: redT_updTs_Some simp add: observable_ta_of_def)
            from nftt' have "thr s t' ≠ None" by(auto)
            with nftt' t'dead have "deadlocked s t'"
              by(simp add: not_final_thread_final_thread_conv[symmetric])
            hence "not_final_thread s' t'"
            proof(induct rule: deadlocked_elims)
              case (lock x'')
              from `⟨x'', shr s⟩ \<wrong>` have "¬ final x''"
               by(auto elim: must_syncE)
              with `thr s t' = ⌊(x'', no_wait_locks)⌋` ts't' show ?thesis
               by(auto intro: not_final_thread.intros)
            next
              case (wait x'' ln'' w'')
              from `¬ final x` est `all_final_except s (deadlocked s)` wst
              have "deadlocked s t" by(fastsimp dest: all_final_exceptD simp add: not_final_thread_iff)
              with Red have False by(auto dest: red_no_deadlock)
              thus ?thesis ..
            next
              case (acquire x'' ln'' l'' T'')
              from `thr s t' = ⌊(x'', ln'')⌋` `0 < ln''f l''` ts't'
              show ?thesis by(auto intro: not_final_thread.intros)
            qed
            with `lt = Inr t'` show ?thesis by auto
          qed
          moreover
          { assume "final_thread s t'"
            from t'dead have "thr s t' ≠ None"
              by(auto elim: deadlocked_elims final_threadE)
            then obtain x' ln' where tst': "thr s t' = ⌊(x', ln')⌋" by auto
            with `final_thread s t'` have "final x'" 
              and "wset s t' = None" and [simp]: "ln' = no_wait_locks"
              by(auto elim: final_threadE)
            with red have "x ≠ x'" by(auto dest: final_no_red)
            with est tst' have "t ≠ t'" by auto
            with Red cct es' tst' ta have "thr s' t' = ⌊(x', ln')⌋"
              by(auto intro: redT_updTs_Some simp add: observable_ta_of_def)
            moreover from Red ws' `t ≠ t'` `wset s t' = None`
            have "ws' t' = None" by(auto simp: redT_updWs_None_implies_None)
            ultimately have "final_thread s' t'" using tst' `final x'`
              by(auto simp add: final_thread_def) }
          ultimately have "((deadlocked s t' ∨ deadlocked s' t') ∨ final_thread s' t') ∧ (∃lt ∈ LT. must_wait s' t'' lt t')"
            using t'dead `lt ∈ LT` by blast
          hence "∃t'. ((deadlocked s t' ∨ deadlocked s' t') ∨ final_thread s' t') ∧ (∃lt ∈ LT. must_wait s' t'' lt t')"
            by blast }
        moreover have "ws' t'' = None" using ws' t''t `wset s t'' = None` 
          by(auto intro: redT_updWs_None_implies_None)
        ultimately show ?thesis by(auto)
      next
        case (wait x ln w)
        from `all_final_except s (deadlocked s)` nafe have False by simp
        thus ?thesis by simp
      next
        case (acquire X ln l T)
        from t''t Red `thr s t'' = ⌊(X, ln)⌋` s s'
        have es't'': "ts' t'' = ⌊(X, ln)⌋"
          by(auto elim!: redT_ts_Some_inv)
        moreover
        from `deadlocked s T ∨ final_thread s T`
        have "T ≠ t"
        proof(rule disjE)
          assume "deadlocked s T"
          with Red show ?thesis by(auto dest: red_no_deadlock)
        next
          assume "final_thread s T"
          with Red show ?thesis
            by(auto dest!: final_no_redT simp add: final_thread_def)
        qed
        with Red `has_lock ((locks s)f l) T` have "has_lock ((locks s')f l) T"
          by(simp add: redT_has_lock_inv)
        moreover
        from ws' `T ≠ t` have wset: "ws T = None ==> ws' T = None"
          by(auto intro: redT_updWs_None_implies_None)
        { fix x
          assume "thr s T = ⌊(x, no_wait_locks)⌋"
          with `T ≠ t` Red es' cct est ta have "thr s' T = ⌊(x, no_wait_locks)⌋"
            by(auto intro: redT_updTs_Some simp add: observable_ta_of_def) }
        moreover
        hence "final_thread s T ==> final_thread s' T"
          by(auto simp add: final_thread_def intro: wset)
        ultimately show ?thesis
          using `0 < lnf l` `t'' ≠ T` `deadlocked s T ∨ final_thread s T`
          apply -
          apply(rule disjI2)
          apply(rule disjI2)
          apply(auto)
          done
      qed
    qed
  next
    case (acquire x ln n)
    note [simp] = `ta = (λf [], [], [], [], ReacquireLocks ln)` `ws' = ws` `m' = m`
    note ts' = `ts' = ts(t \<mapsto> (x, no_wait_locks))`
    note ls' = `ls' = acquire_all ls t ln`
    note tst = `ts t = ⌊(x, ln)⌋`
    from t'dead show ?thesis
    proof(coinduct)
      case (deadlocked t'')
      note t''dead = this
      with Red have t''t: "t'' ≠ t"
        by(auto dest: red_no_deadlock)
      from t''dead show ?case
      proof(cases rule: deadlocked_elims)
        case (lock X)
        hence clnml: "!!LT. ⟨X, shr s⟩ LT \<wrong>
                      ==> ∃t'. (deadlocked s t' ∨ final_thread s t') ∧ (∃lt ∈ LT. must_wait s t'' lt t')"
          by blast
        note tst'' = `thr s t'' = ⌊(X, no_wait_locks)⌋`
        with ts' t''t have ts't'': "thr s' t'' = ⌊(X, no_wait_locks)⌋" by simp
        moreover 
        { fix LT
          assume "⟨X, shr s'⟩ LT \<wrong>"
          hence "⟨X, shr s⟩ LT \<wrong>" by simp
          then obtain T lt where Tdead: "deadlocked s T ∨ final_thread s T"
            and "lt ∈ LT" and hlnft: "must_wait s t'' lt T"
            by(blast dest: clnml)
          from Tdead tst ts'
          have "deadlocked s T ∨ final_thread s' T"
            by(clarsimp simp add: final_thread_def)
          hence "(deadlocked s T ∨ deadlocked s' T) ∨ final_thread s' T" by blast
          moreover from hlnft have "must_wait s' t'' lt T"
          proof(induct rule: must_wait_elims)
            case (lock l')
            from `has_lock ((locks s)f l') T` ls'
            have "has_lock ((locks s')f l') T"
              by(auto intro: has_lock_has_lock_acquire_locks)
            with `T ≠ t''` `lt = Inl l'` show ?thesis by auto
          next
            case thread
            from Tdead have "ts T ≠ None"
              by(auto elim: deadlocked_elims final_threadE)
            moreover from Tdead have "T ≠ t"
            proof(rule disjE)
              assume "deadlocked s T"
              with Red show ?thesis by(auto dest: red_no_deadlock)
            next
              assume "final_thread s T"
              with `0 < lnf n` tst show ?thesis
               by(auto simp add: final_thread_def)
            qed
            ultimately have "not_final_thread s' T" using `not_final_thread s T` ts'
              by(auto simp add: not_final_thread_iff)
            with `lt = Inr T` show ?thesis by auto
          qed
          ultimately have "∃T. ((deadlocked s T ∨ deadlocked s' T) ∨ final_thread s' T) ∧ (∃lt ∈ LT. must_wait s' t'' lt T)"
            using `lt ∈ LT` by blast }
        moreover from `wset s t'' = None` have "wset s' t'' = None" by simp
        ultimately show ?thesis using `thr s t'' = ⌊(X, no_wait_locks)⌋` `⟨X, shr s⟩ \<wrong>` by fastsimp
      next
        case (wait X LN w)
        from `wset s t'' = ⌊w⌋` `ws t = None` have "t'' ≠ t" by auto
        have "all_final_except (ls', (ts(t \<mapsto> (x, no_wait_locks)), m), ws) (deadlocked s)"
        proof(rule all_final_exceptI)
          fix T
          assume "not_final_thread (ls', (ts(t \<mapsto> (x, no_wait_locks)), m), ws) T"
          hence "not_final_thread s T" using `ws t =  None` `ts t = ⌊(x, ln)⌋`
            by(auto simp add: not_final_thread_iff split: split_if_asm)
          with `all_final_except s (deadlocked s)` `ts t = ⌊(x, ln)⌋`
          show "deadlocked s T" by -(erule all_final_exceptD)
        qed
        hence "all_final_except s' (deadlocked s)" by(simp add: ts')
        have "all_final_except s' (λx. deadlocked s x ∨ deadlocked s' x)"
          by(blast intro: all_final_except_mono[rule_format, OF _ `all_final_except s' (deadlocked s)`])
        with t''t `thr s t'' = ⌊(X, LN)⌋` `wset s t'' = ⌊w⌋` ts' show ?thesis
          by-(rule disjI2, rule disjI1, simp)
      next
        case (acquire X LN l T)
        from `thr s t'' = ⌊(X, LN)⌋` t''t ts'
        have "thr s' t'' = ⌊(X, LN)⌋" by(simp)
        moreover from `deadlocked s T ∨ final_thread s T` ts' tst 
        have "deadlocked s T ∨ final_thread s' T"
          by(clarsimp simp add: final_thread_def)
        moreover from `has_lock ((locks s)f l) T` ls'
        have "has_lock ((locks s')f l) T"
          by(auto intro: has_lock_has_lock_acquire_locks)
        ultimately show ?thesis using `0 < LNf l` `t'' ≠ T` by blast
      qed
    qed
  qed
qed

lemma RedT_deadlocked_subset:
  "[| start_state -\<triangleright>tta->* s; deadlocked start_state t' |] ==> deadlocked s t'"
apply(induct rule: RedT_induct')
 apply(assumption)
by(insert can_lock_preserved can_lock_devreserp)(rule redT_deadlocked_subset)

end


locale progress = final_thread_wf final r + wf_progress final r start_state + wf_red final r start_state
  for final :: "'x => bool" and r :: "('l,'t,'x,'m,'w,'o) semantics" and start_state :: "('l,'t,'x,'m,'w) state" +
  fixes deadlock :: "('l,'t,'x,'m,'w) state => bool"
  assumes waiting_deadlock:
    "[| start_state -\<triangleright>ttas->* s; not_final_thread s t;
       !!t x LT. [| thr s t = ⌊(x, no_wait_locks)⌋; ¬ final x; wset s t = None; ⟨x, shr s⟩ LT \<wrong> |]
                ==> ∃t'. ∃lt ∈ LT. must_wait s t lt t';
       !!t x ln l. [| thr s t = ⌊(x, ln)⌋; wset s t = None; lnf l > 0 |] ==> ∃l'. lnf l' > 0 ∧ ¬ may_lock ((locks s)f l') t |]
     ==> deadlock s"
begin

lemma redT_progress:
  assumes Red: "start_state -\<triangleright>ttas->* s"
  assumes nfine: "not_final_thread s t"
  and ndead: "¬ deadlock s"
  shows "∃t' ta' s'. s -t'\<triangleright>ta'-> s'"
proof -
  from ndead
  have "∃t x ln l. thr s t = ⌊(x, ln)⌋ ∧ wset s t = None ∧
         (ln = no_wait_locks ∧ ¬ final x ∧ (∃LT. ⟨x, shr s⟩ LT \<wrong> ∧ (∀t'. ∀lt ∈ LT. ¬ must_wait s t lt t')) ∨
          lnf l > 0 ∧ (∀l. lnf l > 0 --> may_lock ((locks s)f l) t))"
    apply -
    apply(erule contrapos_np)
    apply(rule waiting_deadlock[OF Red nfine])
    by(blast)+
  then obtain t x ln l
    where "thr s t = ⌊(x, ln)⌋"
    and "wset s t = None"
    and a: "(ln = no_wait_locks ∧ ¬ final x ∧ 
             (∃LT. ⟨x, shr s⟩ LT \<wrong> ∧ (∀t'. ∀lt ∈ LT. ¬ must_wait s t lt t')) ∨
             lnf l > 0 ∧ (∀l. lnf l > 0 --> may_lock ((locks s)f l) t))"
    by blast

  obtain ls ts m ws where s [simp]: "s = (ls, (ts, m), ws)" by (cases s, auto)
  note conform = wf_red[OF Red, simplified]
  from `thr s t = ⌊(x, ln)⌋` have tst: "ts t = ⌊(x, ln)⌋" by simp
  from s a have a: "(ln = no_wait_locks ∧ ¬ final x ∧ 
            (∃LT. ⟨x, m⟩ LT \<wrong> ∧ (∀t'. ∀lt ∈ LT. ¬ must_wait s t lt t')) ∨
             lnf l > 0 ∧ (∀l. lnf l > 0 --> may_lock (lsf l) t))" by simp
  thus ?thesis
  proof(rule disjE)
    assume "ln = no_wait_locks ∧ ¬ final x ∧ (∃LT. ⟨x, m⟩ LT \<wrong> ∧ (∀t'. ∀lt∈LT. ¬ must_wait s t lt t'))"
    then obtain LT where [simp]: "ln = no_wait_locks" and nfine': "¬ final x"
      and cl': "⟨x, m⟩ LT \<wrong>" and mw: "!!t' lt. lt∈LT ==> ¬ must_wait s t lt t'"
      by blast
    from `thr s t = ⌊(x, ln)⌋` nfine'
    obtain x'' m'' ta' where red: "⟨x, m⟩ -ta'-> ⟨x'', m''⟩"
      by(auto intro: wf_progressE[OF Red])
    from cl'
    have "∃ta''' x''' m'''. ⟨x, m⟩ -ta'''-> ⟨x''', m'''⟩ ∧ LT = collect_locks \<lbrace>ta'''\<rbrace>l <+> {t. Join t ∈ set \<lbrace>ta'''\<rbrace>c}"
      by (fastsimp elim!: can_syncE)
    then obtain ta''' x''' m'''
      where red'': "⟨x, m⟩ -ta'''-> ⟨x''', m'''⟩"
      and L: "LT = collect_locks \<lbrace>ta'''\<rbrace>l <+> {t. Join t ∈ set \<lbrace>ta'''\<rbrace>c}"
      by blast
    from tst[simplified] red''
    obtain ta'' x'' m''
      where red': "⟨x, m⟩ -ta''-> ⟨x'', m''⟩"
      and cct: "thread_oks ts \<lbrace>ta''\<rbrace>t"
      and lot: "lock_ok_las' ls t \<lbrace>ta''\<rbrace>l"
      and collect: "collect_locks' \<lbrace>ta''\<rbrace>l ⊆ collect_locks \<lbrace>ta'''\<rbrace>l"
      and cao: "cond_action_oks' (ls, (ts, m), ws) t \<lbrace>ta'''\<rbrace>c"
      and join: "collect_cond_actions \<lbrace>ta''\<rbrace>c ⊆ collect_cond_actions \<lbrace>ta'''\<rbrace>c"
      by -(rule wf_redE[OF Red], auto)
    { fix l
      assume "Inl l ∈ LT"
      hence "∀t'. ¬ must_wait s t (Inl l) t'" by-(rule allI mw)+
      hence "∀t'. t ≠ t' --> ¬ has_lock (lsf l) t'" by(fastsimp)
      hence "may_lock (lsf l) t"
        by-(rule classical, auto simp add: not_may_lock_conv) }
    note mayl = this
    { fix t'
      assume t'LT: "Inr t' ∈ LT"
      hence "¬ not_final_thread s t' ∧ t' ≠ t"
      proof(cases "t' = t")
        case False with t'LT mw L show ?thesis by(auto)
      next
        case True with tst mw[OF t'LT, of t] nfine' L have False
          by(auto intro!: must_wait.intros simp add: not_final_thread_iff)
        thus ?thesis ..
      qed }
    note mayj = this
    from collect L mayl
    have "∀l∈collect_locks' \<lbrace>ta''\<rbrace>l. may_lock (lsf l) t" by auto
    with lot have "!!l. l ∈ collect_locks \<lbrace>ta''\<rbrace>l ==> may_lock (lsf l) t"
      by - (rule lock_ok_las'_collect_locks'_may_lock)
    with lot have "lock_ok_las ls t \<lbrace>ta''\<rbrace>l"
      by -(rule lock_ok_las'_collect_locks_lock_ok_las)
    moreover from mayj join L
    have "cond_action_oks (ls, (ts, m), ws) t \<lbrace>ta''\<rbrace>c"
      by(fastsimp intro: may_join_cond_action_oks)
    moreover note red' cct tst `wset s t = None`
    ultimately show ?thesis by(fastsimp intro: redT_normal) 
  next
    assume "0 < lnf l ∧ (∀l. 0 < lnf l --> may_lock (lsf l) t)"
    hence "0 < lnf l" "!!l. 0 < lnf l ==> may_lock (lsf l) t" by(auto)
    hence "may_acquire_all ls t ln" by(auto intro: may_acquire_allI)
    with tst `wset s t = None` `0 < lnf l`
    show ?thesis by(fastsimp intro: redT_acquire)
  qed
qed

end

lemma (in final_thread_wf) lock_thread_ok_must_wait_thread_exists:
  "[| lock_thread_ok (locks s) (thr s); must_wait s t lt t' |] ==> thr s t' ≠ None"
by(auto dest: lock_thread_okD elim!: must_wait_elims)
  

lemma (in final_thread_wf) progress_deadlock:
  assumes wf_progress: "wf_progress final r start_state"
  and wf_red: "wf_red final r start_state"
  shows "progress final r start_state deadlock"
proof(rule progress.intro[OF final_thread_wf_axioms wf_progress wf_red progress_axioms.intro])
  fix ttas s t
  assume Red: "start_state -\<triangleright>ttas->* s"
    and tst: "not_final_thread s t"
    and normal: "!!t x LT. [|thr s t = ⌊(x, no_wait_locks)⌋; ¬ final x; wset s t = None; ⟨x, shr s⟩ LT \<wrong> |]
                          ==> ∃t'. ∃lt∈LT. must_wait s t lt t'"
    and acquire: "!!t x ln l. [|thr s t = ⌊(x, ln)⌋; wset s t = None; 0 < lnf l|] ==> ∃l'. 0 < lnf l' ∧ ¬ may_lock ((locks s)f l') t"
  have lok: "lock_thread_ok (locks s) (thr s)"
    by(rule multithreaded_start.preserves_lock_thread_ok[OF wf_progress.axioms(1)[OF wf_progress] Red])
  with Red tst normal acquire show "deadlock s"
    by-(rule all_waiting_implies_deadlock,
        (blast dest: lock_thread_ok_must_wait_thread_exists[OF lok]
               intro: must_syncI[OF wf_progress.wf_progress[OF wf_progress]])+)
qed


lemmas (in final_thread_wf) progress_deadlocked'_aux = progress_deadlock[unfolded deadlock_eq_deadlocked']
lemmas (in final_thread_wf) progress_deadlocked' = progress_deadlocked'_aux


end