Theory KPL_execution_group

section ‹Execution rules for groups›

theory KPL_execution_group imports 
  KPL_execution_thread
begin

text ‹Intra-group race detection›
definition group_race 
  :: "lid set ⇒ (lid ⇀ thread_state) ⇒ bool"
where "group_race T γ ≡ 
  ∃j ∈ T. ∃k ∈ T. j ≠ k ∧ 
  W (the (γ j)) ∩ (R (the (γ k)) ∪ W (the (γ k))) ≠ {}"

text ‹The constraints for the @{term "merge"} map›
inductive pre_merge 
  :: "lid set ⇒ (lid ⇀ thread_state) ⇒ nat ⇒ word ⇒ bool"
where 
  "⟦ j ∈ T ; z ∈ W (the (γ j)) ; dom γ = T ⟧ ⟹
  pre_merge T γ z (sh (the (γ j)) z)"
| "⟦ ∀j ∈ T. z ∉ W (the (γ j)) ; dom γ = T ⟧ ⟹ 
  pre_merge T γ z (sh (the (γ 0)) z)"

inductive_cases pre_merge_inv [elim!]: "pre_merge P γ z z'"

text ‹The @{term "merge"} map maps each nat to the word that 
   satisfies the above constaints. The ‹merge_is_unique›
   lemma shows that there exists exactly one such word 
   per nat, provided there are no group races.›
definition merge :: "lid set ⇒ (lid ⇀ thread_state) ⇒ nat ⇒ word"
where "merge T γ ≡ λz. The (pre_merge T γ z)"

lemma no_races_imp_no_write_overlap: 
  "¬ (group_race T γ) ⟹ 
  ∀i ∈ T. ∀j ∈ T. 
  i ≠ j ⟶ W (the (γ i)) ∩ W (the (γ j)) = {}"
unfolding group_race_def 
by blast

lemma merge_is_unique:
  assumes "dom γ = T"
  assumes "¬ (group_race T γ)"
  shows "∃!z'. pre_merge T γ z z'"
apply (insert assms)
apply (drule no_races_imp_no_write_overlap)
apply (intro allI ex_ex1I)
apply (metis pre_merge.intros)
apply clarify
proof -
  fix z1 z2
  assume a: "∀i∈dom γ. ∀j∈dom γ. i ≠ j ⟶ W (the (γ i)) ∩ W (the (γ j)) = {}"
  assume "pre_merge (dom γ) γ z z1" 
  and "pre_merge (dom γ) γ z z2"
  thus "z1 = z2"
  apply (elim pre_merge_inv)
  apply (rename_tac j1 j2)
  apply (case_tac "j1 = j2")
  apply auto[1]
  apply simp
  apply (subgoal_tac "W (the (γ j1)) ∩ W (the (γ j2)) = {}")
  apply auto[1]
  apply (auto simp add: a)
  done
qed
 
text ‹The rules of Figure 5, plus an additional rule for
  equality abstraction (Fig 7a), plus an additional rule for
  adversarial abstraction (Fig 7b)›
inductive step_g
  :: "abs_level ⇒ gid ⇒ (gid ⇀ lid set) ⇒ (group_state × pred_stmt) ⇒ group_state option ⇒ bool"
where
  G_Race:
  "⟦ ∀j ∈ the (T i). step_t a (the (γ ⇩t⇩s j), (s, p)) (the (γ' ⇩t⇩s j)) ; 
    group_race (the (T i)) ((γ' :: group_state)⇩t⇩s) ⟧
  ⟹ step_g a i T (γ, (Basic s, p)) None"
| G_Basic:
  "⟦ ∀j ∈ the (T i). step_t a (the (γ ⇩t⇩s j), (s, p)) (the (γ' ⇩t⇩s j)) ; 
    ¬ (group_race (the (T i)) (γ' ⇩t⇩s)) ;
    R_group γ' = R_group γ ∪ (⋃j ∈ the (T i). ({j} × R (the (γ' ⇩t⇩s j)))) ;
    W_group γ' = W_group γ ∪ (⋃j ∈ the (T i). ({j} × W (the (γ' ⇩t⇩s j)))) ⟧
  ⟹ step_g a i T (γ, (Basic s, p)) (Some γ')"
| G_No_Op:
  "∀j ∈ the (T i). ¬ (eval_bool p (the (γ ⇩t⇩s j)))
  ⟹ step_g a i T (γ, (Barrier, p)) (Some γ)"
| G_Divergence:
  "⟦ j ≠ k ; j ∈ the (T i) ; k ∈ the (T i) ;
   eval_bool p (the (γ ⇩t⇩s j)) ; ¬ (eval_bool p (the (γ ⇩t⇩s k))) ⟧
  ⟹ step_g a i T (γ, (Barrier, p)) None"
| G_Sync:
  "⟦ ∀j ∈ the (T i). eval_bool p (the (γ ⇩t⇩s j)) ;
    ∀j ∈ the (T i). the (γ' ⇩t⇩s j) = (the (γ ⇩t⇩s j)) (| 
    sh := merge P (γ ⇩t⇩s), R := {}, W := {} |) ⟧ 
  ⟹ step_g No_Abst i T (γ, (Barrier, p)) (Some γ')"
| G_Sync_Eq:
  "⟦ ∀j ∈ the (T i). eval_bool p (the (γ ⇩t⇩s j)) ;
    ∀j ∈ the (T i). the (γ' ⇩t⇩s j) = (the (γ ⇩t⇩s j)) (| 
    sh := sh', R := {}, W := {} |) ⟧ 
  ⟹ step_g Eq_Abst i T (γ, (Barrier, p)) (Some γ')"
| G_Sync_Adv:
  "⟦ ∀j ∈ the (T i). eval_bool p (the (γ ⇩t⇩s j)) ;
    ∀j ∈ the (T i). ∃sh'. the (γ' ⇩t⇩s j) = (the (γ ⇩t⇩s j)) (| 
    sh := sh', R := {}, W := {} |) ⟧ 
  ⟹ step_g Adv_Abst i T (γ, (Barrier, p)) (Some γ')"

text ‹Rephrasing ‹G_No_Op› to make it more usable›
lemma G_No_Op_helper:
  "⟦ ∀j ∈ the (T i). ¬ (eval_bool p (the (γ ⇩t⇩s j))) ; γ = γ' ⟧
  ⟹ step_g a i T (γ, (Barrier, p)) (Some γ')"
by (simp add: step_g.G_No_Op)


end