Theory Phases

(*<*)
(*
 * Copyright 2015, NICTA
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(NICTA_BSD)
 *)

theory Phases
imports
  Global_Invariants_Lemmas
  Local_Invariants_Lemmas
  Tactics
begin

(*>*)
section‹Handshake phases›

text‹

Reasoning about phases, handshakes.

Tie the garbage collector's control location to the value of @{const
"gc_phase"}.

›

lemma (in gc) phase_invL_eq_imp:
  "eq_imp (λ(_::unit) s. (AT s gc, s↓ gc, tso_pending_phase gc s↓))
          phase_invL"
by (clarsimp simp: eq_imp_def inv)

lemmas gc_phase_invL_niE[nie] =
  iffD1[OF gc.phase_invL_eq_imp[simplified eq_imp_simps, rule_format, unfolded conj_explode], rotated -1]

lemma (in gc) phase_invL[intro]:
  "⦃ phase_invL ❙∧ LSTP phase_rel_inv ⦄ gc ⦃ phase_invL ⦄"
by vcg_jackhammer (fastforce dest!: phase_rel_invD simp: phase_rel_def)

lemma (in sys) gc_phase_invL[intro]:
  notes fun_upd_apply[simp]
  notes if_splits[split]
  shows
  "⦃ gc.phase_invL ⦄ sys"
by (vcg_chainsaw gc.phase_invL_def)

lemma (in mut_m) gc_phase_invL[intro]:
  "⦃ gc.phase_invL ⦄ mutator m"
by (vcg_chainsaw gc.phase_invL_def[inv])

lemma (in gc) phase_rel_inv[intro]:
  "⦃ handshake_invL ❙∧ phase_invL ❙∧ LSTP phase_rel_inv ⦄ gc ⦃ LSTP phase_rel_inv ⦄"
unfolding phase_rel_inv_def by (vcg_jackhammer (no_thin_post_inv); simp add: phase_rel_def; blast)

lemma (in sys) phase_rel_inv[intro]:
  notes gc.phase_invL_def[inv]
  notes phase_rel_inv_def[inv]
  notes fun_upd_apply[simp]
  shows
  "⦃ LSTP (phase_rel_inv ❙∧ tso_store_inv) ⦄ sys ⦃ LSTP phase_rel_inv ⦄"
proof(vcg_jackhammer (no_thin_post_inv), vcg_name_cases)
  case (tso_dequeue_store_buffer s s' p w ws) then show ?case
    apply (simp add: phase_rel_def p_not_sys split: if_splits)
    apply (elim disjE; auto split: if_splits)
    done
qed

lemma (in mut_m) phase_rel_inv[intro]:
  "⦃ handshake_invL ❙∧ LSTP (handshake_phase_inv ❙∧ phase_rel_inv) ⦄
     mutator m
   ⦃ LSTP phase_rel_inv ⦄"
unfolding phase_rel_inv_def
proof (vcg_jackhammer (no_thin_post_inv), vcg_name_cases)
  case (hs_noop_done s s') then show ?case
    by (auto dest!: handshake_phase_invD
             simp: handshake_phase_rel_def phase_rel_def hp_step_rel_def
            split: hs_phase.splits)
next case (hs_get_roots_done s s') then show ?case
    by (auto dest!: handshake_phase_invD
             simp: handshake_phase_rel_def phase_rel_def hp_step_rel_def
            split: hs_phase.splits)
next case (hs_get_work_done s s') then show ?case
    by (auto dest!: handshake_phase_invD
             simp: handshake_phase_rel_def phase_rel_def hp_step_rel_def
            split: hs_phase.splits)
qed

text‹

Connect @{const "sys_ghost_hs_phase"} with locations in the GC.

›

lemma gc_handshake_invL_eq_imp:
  "eq_imp (λ(_::unit) s. (AT s gc, s↓ gc, sys_ghost_hs_phase s↓, hs_pending (s↓ sys), ghost_hs_in_sync (s↓ sys), sys_hs_type s↓))
          gc.handshake_invL"
by (simp add: gc.handshake_invL_def eq_imp_def)

lemmas gc_handshake_invL_niE[nie] =
  iffD1[OF gc_handshake_invL_eq_imp[simplified eq_imp_simps, rule_format, unfolded conj_explode], rotated -1]

lemma (in sys) gc_handshake_invL[intro]:
  "⦃ gc.handshake_invL ⦄ sys"
by (vcg_chainsaw gc.handshake_invL_def)

lemma (in sys) handshake_phase_inv[intro]:
  "⦃ LSTP handshake_phase_inv ⦄ sys"
unfolding handshake_phase_inv_def by (vcg_jackhammer (no_thin_post_inv))

lemma (in gc) handshake_invL[intro]:
  notes fun_upd_apply[simp]
  shows
  "⦃ handshake_invL ⦄ gc"
by vcg_jackhammer fastforce+

lemma (in gc) handshake_phase_inv[intro]:
  notes fun_upd_apply[simp]
  shows
  "⦃ handshake_invL ❙∧ LSTP handshake_phase_inv ⦄ gc ⦃ LSTP handshake_phase_inv ⦄"
unfolding handshake_phase_inv_def by (vcg_jackhammer (no_thin_post_inv)) (auto simp: handshake_phase_inv_def hp_step_rel_def)

text‹

Local handshake phase invariant for the mutators.

›

lemma (in mut_m) handshake_invL_eq_imp:
  "eq_imp (λ(_::unit) s. (AT s (mutator m), s↓ (mutator m), sys_hs_type s↓, sys_hs_pending m s↓, mem_store_buffers (s↓ sys) (mutator m)))
          handshake_invL"
unfolding eq_imp_def handshake_invL_def by simp

lemmas mut_m_handshake_invL_niE[nie] =
  iffD1[OF mut_m.handshake_invL_eq_imp[simplified eq_imp_simps, rule_format, unfolded conj_explode], rotated -1]

lemma (in mut_m) handshake_invL[intro]:
  "⦃ handshake_invL ⦄ mutator m"
by vcg_jackhammer

lemma (in mut_m') handshake_invL[intro]:
  "⦃ handshake_invL ⦄ mutator m'"
by vcg_chainsaw

lemma (in gc) mut_handshake_invL[intro]:
  notes fun_upd_apply[simp]
  shows
  "⦃ handshake_invL ❙∧ mut_m.handshake_invL m ⦄ gc ⦃ mut_m.handshake_invL m ⦄"
by (vcg_chainsaw mut_m.handshake_invL_def)

lemma (in sys) mut_handshake_invL[intro]:
  notes if_splits[split]
  notes fun_upd_apply[simp]
  shows
  "⦃ mut_m.handshake_invL m ⦄ sys"
by (vcg_chainsaw mut_m.handshake_invL_def)

lemma (in mut_m) gc_handshake_invL[intro]:
  notes fun_upd_apply[simp]
  shows
  "⦃ handshake_invL ❙∧ gc.handshake_invL ⦄ mutator m ⦃ gc.handshake_invL ⦄"
by (vcg_chainsaw gc.handshake_invL_def)

lemma (in mut_m) handshake_phase_inv[intro]:
  notes fun_upd_apply[simp]
  shows
  "⦃ handshake_invL ❙∧ LSTP handshake_phase_inv ⦄ mutator m ⦃ LSTP handshake_phase_inv ⦄"
unfolding handshake_phase_inv_def by (vcg_jackhammer (no_thin_post_inv)) (auto simp: hp_step_rel_def)

text‹

Validity of @{const "sys_fM"} wrt @{const "gc_fM"} and the handshake
phase. Effectively we use @{const "gc_fM"} as ghost state. We also
include the TSO lock to rule out the GC having any pending marks
during the @{const "hp_Idle"} handshake phase.

›

lemma gc_fM_fA_invL_eq_imp:
  "eq_imp (λ(_::unit) s. (AT s gc, s↓ gc, sys_fA s↓, sys_fM s↓, sys_mem_store_buffers gc s↓))
          gc.fM_fA_invL"
by (simp add: gc.fM_fA_invL_def eq_imp_def)

lemmas gc_fM_fA_invL_niE[nie] =
  iffD1[OF gc_fM_fA_invL_eq_imp[simplified eq_imp_simps, rule_format, unfolded conj_explode], rotated -1]

context gc
begin

lemma fM_fA_invL[intro]:
  "⦃ fM_fA_invL ⦄ gc"
by vcg_jackhammer

lemma fM_rel_inv[intro]:
  notes fun_upd_apply[simp]
  shows
  "⦃ fM_fA_invL ❙∧ handshake_invL ❙∧ tso_lock_invL ❙∧ LSTP fM_rel_inv ⦄
     gc
   ⦃ LSTP fM_rel_inv ⦄"
by (vcg_jackhammer (no_thin_post_inv); simp add: fM_rel_inv_def fM_rel_def)

lemma fA_rel_inv[intro]:
  notes fun_upd_apply[simp]
  shows
  "⦃ fM_fA_invL ❙∧ handshake_invL ❙∧ LSTP fA_rel_inv ⦄
     gc
   ⦃ LSTP fA_rel_inv ⦄"
by (vcg_jackhammer (no_thin_post_inv); simp add: fA_rel_inv_def; auto simp: fA_rel_def)

end

context mut_m
begin

lemma gc_fM_fA_invL[intro]:
  "⦃ gc.fM_fA_invL ⦄ mutator m"
by (vcg_chainsaw gc.fM_fA_invL_def)

lemma fM_rel_inv[intro]:
  notes fun_upd_apply[simp]
  shows
  "⦃ LSTP fM_rel_inv ⦄ mutator m"
unfolding fM_rel_inv_def by (vcg_jackhammer (no_thin_post_inv); simp add: fM_rel_def; elim disjE; auto split: if_splits)

lemma fA_rel_inv[intro]:
  notes fun_upd_apply[simp]
  shows
  "⦃ LSTP fA_rel_inv ⦄ mutator m"
unfolding fA_rel_inv_def by (vcg_jackhammer (no_thin_post_inv); simp add: fA_rel_def; elim disjE; auto split: if_splits)

end


context gc
begin

lemma fA_neq_locs_diff_fA_tso_empty_locs:
  "fA_neq_locs - fA_tso_empty_locs = {}"
apply (simp add: fA_neq_locs_def fA_tso_empty_locs_def locset_cache)
apply (simp add: loc_defs)
done

end

context sys
begin

lemma gc_fM_fA_invL[intro]:
  "⦃ gc.fM_fA_invL ❙∧ LSTP (fA_rel_inv ❙∧ fM_rel_inv ❙∧ tso_store_inv) ⦄
     sys
   ⦃ gc.fM_fA_invL ⦄"
apply( vcg_chainsaw (no_thin) gc.fM_fA_invL_def
     ; (simp add: p_not_sys)?; (erule disjE)?; clarsimp split: if_splits )
proof(vcg_name_cases sys gc)
     case (tso_dequeue_store_buffer_mark_noop_mfence s s' ws) then show ?case by (clarsimp simp: fA_rel_inv_def fA_rel_def)
next case (tso_dequeue_store_buffer_fA_neq_locs s s' ws) then show ?case
  apply (clarsimp simp: fA_rel_inv_def fA_rel_def fM_rel_inv_def fM_rel_def)
  apply (drule (1) atS_dests(3), fastforce simp: atS_simps gc.fA_neq_locs_diff_fA_tso_empty_locs)
  done
next case (tso_dequeue_store_buffer_fA_eq_locs s s' ws) then show ?case by (clarsimp simp: fA_rel_inv_def fA_rel_def)
next case (tso_dequeue_store_buffer_idle_flip_noop_mfence s s' ws) then show ?case by (clarsimp simp: fM_rel_inv_def fM_rel_def)
next case (tso_dequeue_store_buffer_fM_eq_locs s s' ws) then show ?case by (clarsimp simp: fM_rel_inv_def fM_rel_def)
qed

lemma fM_rel_inv[intro]:
  notes fun_upd_apply[simp]
  shows
  "⦃ LSTP (fM_rel_inv ❙∧ tso_store_inv) ⦄ sys ⦃ LSTP fM_rel_inv ⦄"
apply (vcg_jackhammer (no_thin_post_inv))
apply (clarsimp simp: do_store_action_def fM_rel_inv_def fM_rel_def p_not_sys
                split: mem_store_action.splits)
apply (intro allI conjI impI; clarsimp)
done

lemma fA_rel_inv[intro]:
  notes fun_upd_apply[simp]
  shows
  "⦃ LSTP (fA_rel_inv ❙∧ tso_store_inv) ⦄ sys ⦃ LSTP fA_rel_inv ⦄"
apply (vcg_jackhammer (no_thin_post_inv))
apply (clarsimp simp: do_store_action_def fA_rel_inv_def fA_rel_def p_not_sys
                split: mem_store_action.splits)
apply (intro allI conjI impI; clarsimp)
done

end


subsubsection‹sys phase inv›

context mut_m
begin

lemma sys_phase_inv[intro]:
  notes if_split_asm[split del]
  notes fun_upd_apply[simp]
  shows
  "⦃ handshake_invL
             ❙∧ mark_object_invL
             ❙∧ mut_get_roots.mark_object_invL m
             ❙∧ mut_store_del.mark_object_invL m
             ❙∧ mut_store_ins.mark_object_invL m
        ❙∧ LSTP (fA_rel_inv ❙∧ fM_rel_inv ❙∧ handshake_phase_inv ❙∧ mutators_phase_inv ❙∧ phase_rel_inv ❙∧ sys_phase_inv ❙∧ valid_refs_inv) ⦄
     mutator m
   ⦃ LSTP sys_phase_inv ⦄"
proof( (vcg_jackhammer (no_thin_post_inv)
       ; clarsimp simp: fA_rel_inv_def fM_rel_inv_def sys_phase_inv_aux_case heap_colours_colours
                 split: hs_phase.splits if_splits )
     , vcg_name_cases )
     case (alloc s s' rb) then show ?case
      by (clarsimp simp: fA_rel_def fM_rel_def no_black_refs_def
                  dest!: handshake_phase_invD phase_rel_invD
                  split: hs_phase.splits)
next case (store_ins_mo_co_mark0 s s' y) then show ?case
      by (fastforce simp: fA_rel_def fM_rel_def hp_step_rel_def
                   dest!: handshake_phase_invD phase_rel_invD)
next case (store_ins_mo_co_mark s s' y) then show ?case
      apply -
      apply (drule spec[where x=m])
      apply (rule conjI)
       apply (clarsimp simp: hp_step_rel_def phase_rel_def conj_disj_distribR[symmetric]
                      dest!: handshake_phase_invD phase_rel_invD)
       apply (elim disjE, simp_all add: no_grey_refs_not_rootD; fail)
      apply (clarsimp simp: hp_step_rel_def phase_rel_def
                     dest!: handshake_phase_invD phase_rel_invD)
      apply (elim disjE, simp_all add: no_grey_refs_not_rootD)[1]
      apply clarsimp
      apply (elim disjE, simp_all add: no_grey_refs_not_rootD filter_empty_conv)[1]
      apply fastforce
      done
next case (store_del_mo_co_mark0 s s' y) then show ?case
      apply (clarsimp simp: hp_step_rel_def dest!: handshake_phase_invD phase_rel_invD)
      apply (metis (no_types, lifting) mut_m.no_grey_refs_not_rootD mutator_phase_inv_aux.simps(5))
      done
next case (store_del_mo_co_mark s s' y) then show ?case
      apply -
      apply (drule spec[where x=m])
      apply (rule conjI)
       apply (clarsimp simp: hp_step_rel_def phase_rel_def conj_disj_distribR[symmetric] no_grey_refs_not_rootD
                      dest!: handshake_phase_invD phase_rel_invD; fail)
      apply (clarsimp simp: hp_step_rel_def phase_rel_def
                     dest!: handshake_phase_invD phase_rel_invD)
      apply (elim disjE, simp_all add: no_grey_refs_not_rootD)
      apply clarsimp
      apply (elim disjE, simp_all add: no_grey_refs_not_rootD filter_empty_conv)
      apply fastforce
      done
next case (hs_get_roots_done s s') then show ?case
      apply (clarsimp simp: hp_step_rel_def phase_rel_def filter_empty_conv
                     dest!: handshake_phase_invD phase_rel_invD)
      apply auto
      done
next case (hs_get_roots_loop_mo_co_mark s s' y) then show ?case
      apply -
      apply (drule spec[where x=m])
      apply (rule conjI)
       apply (clarsimp simp: hp_step_rel_def phase_rel_def conj_disj_distribR[symmetric]
                      dest!: handshake_phase_invD phase_rel_invD; fail)
      apply (clarsimp simp: hp_step_rel_def phase_rel_def
                     dest!: handshake_phase_invD phase_rel_invD)
      apply (elim disjE, simp_all add: no_grey_refs_not_rootD)
      apply clarsimp
      apply (elim disjE, simp_all add: no_grey_refs_not_rootD filter_empty_conv)[1]
      apply fastforce
      done
next case (hs_get_work_done s s') then show ?case
      apply (clarsimp simp: hp_step_rel_def phase_rel_def filter_empty_conv
                     dest!: handshake_phase_invD phase_rel_invD)
      apply auto
      done
qed (clarsimp simp: hp_step_rel_def dest!: handshake_phase_invD phase_rel_invD)+

end

lemma (in gc) sys_phase_inv[intro]:
  notes fun_upd_apply[simp]
  shows
  "⦃ fM_fA_invL ❙∧ gc_W_empty_invL ❙∧ handshake_invL ❙∧ obj_fields_marked_invL
       ❙∧ phase_invL ❙∧ sweep_loop_invL
       ❙∧ LSTP (phase_rel_inv ❙∧ sys_phase_inv ❙∧ valid_W_inv ❙∧ tso_store_inv) ⦄
     gc
   ⦃ LSTP sys_phase_inv ⦄"
proof(vcg_jackhammer (no_thin_post_inv), vcg_name_cases)
     case (mark_loop_get_work_load_W s s') then show ?case by (fastforce dest!: phase_rel_invD simp: phase_rel_def no_grey_refsD filter_empty_conv)
next case (mark_loop_blacken s s') then show ?case by (meson no_grey_refsD(1))
next case (mark_loop_mo_co_W s s') then show ?case by (meson no_grey_refsD(1))
next case (mark_loop_mo_co_mark s s') then show ?case by (meson no_grey_refsD(1))
next case (mark_loop_get_roots_load_W s s') then show ?case by (fastforce dest!: phase_rel_invD simp: phase_rel_def no_grey_refsD filter_empty_conv)
next case (mark_loop_get_roots_init_type s s') then show ?case by (fastforce dest!: phase_rel_invD simp: phase_rel_def no_grey_refsD filter_empty_conv)
next case (idle_noop_init_type s s') then show ?case using black_heap_no_greys by blast
qed

lemma no_grey_refs_no_marks[simp]:
  "⟦ no_grey_refs s; valid_W_inv s ⟧ ⟹ ¬sys_mem_store_buffers p s = mw_Mark r fl # ws"
unfolding no_grey_refs_def by (metis greyI(1) list.set_intros(1) valid_W_invE(5))
(* FIXME suggests redundancy in valid_W_inv rules:  by (meson greyI(1) valid_W_invD(1)) *)

context sys
begin

lemma black_heap_dequeue_mark[iff]:
  "⟦ sys_mem_store_buffers p s = mw_Mark r fl # ws; black_heap s; valid_W_inv s ⟧
   ⟹ black_heap (s(sys := s sys⦇heap := (sys_heap s)(r := map_option (obj_mark_update (λ_. fl)) (sys_heap s r)), mem_store_buffers := (mem_store_buffers (s sys))(p := ws)⦈))"
unfolding black_heap_def by (metis colours_distinct(4) valid_W_invD(1) white_valid_ref)

lemma white_heap_dequeue_fM[iff]:
  "black_heap s↓
     ⟹ white_heap (s↓(sys := s↓ sys⦇fM := ¬ sys_fM s↓, mem_store_buffers := (mem_store_buffers (s↓ sys))(gc := ws)⦈))"
unfolding black_heap_def white_heap_def black_def white_def by clarsimp (* FIXME rules? *)

lemma black_heap_dequeue_fM[iff]:
  "⟦ white_heap s↓; no_grey_refs s↓ ⟧
     ⟹ black_heap (s↓(sys := s↓ sys⦇fM := ¬ sys_fM s↓, mem_store_buffers := (mem_store_buffers (s↓ sys))(gc := ws)⦈))"
unfolding black_heap_def white_heap_def no_grey_refs_def by auto

lemma sys_phase_inv[intro]:
  notes if_split_asm[split del]
  notes fun_upd_apply[simp]
  shows
  "⦃ LSTP (fA_rel_inv ❙∧ fM_rel_inv ❙∧ handshake_phase_inv ❙∧ mutators_phase_inv ❙∧ phase_rel_inv ❙∧ sys_phase_inv ❙∧ tso_store_inv ❙∧ valid_W_inv) ⦄
     sys
   ⦃ LSTP sys_phase_inv ⦄"
proof(vcg_jackhammer (no_thin_post_inv)
     , clarsimp simp: fA_rel_inv_def fM_rel_inv_def p_not_sys
     , vcg_name_cases)
  case (tso_dequeue_store_buffer s s' p w ws) then show ?case
    apply (clarsimp simp: do_store_action_def sys_phase_inv_aux_case
                   split: mem_store_action.splits hs_phase.splits if_splits)
    apply (clarsimp simp: fA_rel_def fM_rel_def; erule disjE; clarsimp simp: fA_rel_def fM_rel_def)+
     apply (metis (mono_tags, lifting) filter.simps(2) list.discI tso_store_invD(4))
    apply auto
    done
qed

end
(*<*)

end
(*>*)