theory KPL_soundness imports
"$AFP/GPU_Kernel_PL/KPL_wellformedness"
"$AFP/GPU_Kernel_PL/KPL_execution_kernel"
begin
section {* Soundness of the two-thread reduction using equality-abstraction *}
fun K_Open_applies :: "kernel_state => bool"
where
"K_Open_applies (_,ss,_) = (∃ e S p.
hd ss = (While e S, p))"
fun K_Done_applies
:: "threadset => kernel_state => bool"
where
"K_Done_applies (G,T) (κ,ss,_) = (∃ e S p.
hd ss = (WhileDyn e S, p) ∧
(∀i ∈ G. ∀j ∈ the (T i).
¬ (eval_bool (p ∧* e) (the ((the (κ i))⇩t⇩s j)))))"
fun K_Iter_applies_but
:: "threadset => threadset => kernel_state => bool"
where
"K_Iter_applies_but (G,T) (G',T') K = (∃ e S κ' ss p vs.
K = (κ', (WhileDyn e S, p) # ss, vs)
∧ (∃i ∈ G. ∃j ∈ the (T i).
eval_bool (p ∧* e) (the ((the (κ' i))⇩t⇩s j)))
∧ (∀i ∈ G'. ∀j ∈ the (T' i).
¬ (eval_bool (p ∧* e) (the ((the (κ' i))⇩t⇩s j)))))"
definition executions
:: "abs_level => proc list => threadset
=> kernel_state list set"
where
"executions a fs GT ≡ { Ks :: kernel_state list. Ks ≠ [] ∧
(∀n < length Ks - 1.
step_k a fs GT (Ks ! n) (Some (Ks ! (n + 1))))}"
lemma executions_singleton:
"[K] ∈ executions a fs GT"
by (auto simp add: executions_def)
lemma executions_consI:
"[| Ks ∈ executions a fs GT ; step_k a fs GT K (Some (Ks ! 0)) |] ==>
(K # Ks) ∈ executions a fs GT"
apply (auto simp add: executions_def)
apply (case_tac n)
apply auto
done
lemma executions_consD:
"[| (K # Ks) ∈ executions a fs GT ; Ks ≠ [] |] ==> Ks ∈ executions a fs GT"
apply (auto simp add: executions_def)
apply (metis drop_0 drop_Suc length_drop nth_Cons_Suc tl_drop zero_less_diff)
done
definition wf_executions
:: "abs_level => stmt => proc list => threadset
=> kernel_state list set"
where
"wf_executions a S fs GT ≡ { Ks :: kernel_state list.
valid_initial_kernel_state S GT (Ks ! 0) ∧
Ks ∈ executions a fs GT}"
definition faulting_executions
:: "abs_level => stmt => proc list => threadset
=> kernel_state list set"
where
"faulting_executions a S fs GT ≡ { Ks :: kernel_state list.
Ks ∈ wf_executions a S fs GT ∧
step_k a fs GT (last Ks) None }"
definition error_free
:: "abs_level => stmt => proc list => threadset => bool"
where
"error_free a S fs GT ≡ faulting_executions a S fs GT = {}"
fun reductions :: "threadset => threadset set"
where
"reductions (G,T) = {(G',T') | G' T'.
((∃i. G' = {i} ∧ card (the (T' i)) = 2) ∨
(∃i1 i2. i1 ≠ i2 ∧ G' = {i1,i2} ∧ card (the (T' i1)) = 1 ∧ card (the (T' i2)) = 1))
∧ G' ⊆ G ∧ (∀i ∈ G'. the (T' i) ⊆ the (T i))}"
fun proj_g :: "lid set => group_state => group_state"
where
"proj_g T' γ = γ (|
thread_states := (thread_states γ) |` T',
R_group := {r ∈ R_group γ . fst r ∈ T'} ,
W_group := {w ∈ W_group γ . fst w ∈ T'} |)"
fun proj_k :: "threadset => (gid \<rightharpoonup> group_state) => (gid \<rightharpoonup> group_state)"
where
"proj_k (G',T') κ = (λ i. if i ∈ G' then Some (proj_g (the (T' i)) (the (κ i))) else None)"
fun proj :: "threadset => kernel_state => kernel_state"
where
"proj GT' (κ,ss,vs) = (proj_k GT' κ, ss, vs)"
lemma reduction_preserves_no_group_race:
assumes "¬ (group_race (the (T i)) ((the (κ i))⇩t⇩s))"
assumes "(G', T') ∈ reductions (G, T)"
assumes "i ∈ G'"
shows "¬ (group_race (the (T' i)) ((the (proj_k (G', T') κ i))⇩t⇩s))"
using assms
apply (unfold group_race_def)
apply clarify
apply (subgoal_tac "j ∈ the (T i)")
apply (subgoal_tac "k ∈ the (T i)")
apply auto
done
lemma reduction_preserves_no_kernel_race:
assumes "¬ kernel_race G κ"
assumes "(G', T') ∈ reductions (G, T)"
shows "¬ kernel_race G' (proj_k (G', T') κ)"
using assms
apply (unfold kernel_race_def)
apply clarify
apply (subgoal_tac "i ∈ G")
apply (subgoal_tac "j ∈ G")
apply simp
apply (fold atomize_ball)
apply (subgoal_tac "snd ` W_group (the (κ i)) ∩
(snd ` R_group (the (κ j))
∪ snd ` W_group (the (κ j))) = {}")
apply auto[1]
apply (metis (hide_lams, no_types))
apply auto
done
lemma reduction_preserves_reads:
assumes "i ∈ G'"
assumes "(G',T') ∈ reductions (G,T)"
assumes "R_group (the (κ' i)) =
R_group (the (κ i))
∪ (\<Union>j∈the (T i). {j} × R (the ((the (κ' i))⇩t⇩s j)))"
shows "R_group (the (proj_k (G', T') κ' i)) =
R_group (the (proj_k (G', T') κ i))
∪ (\<Union>j∈the (T' i). {j} ×
R (the ((the (proj_k (G', T') κ' i))⇩t⇩s j)))"
using assms by auto
lemma reduction_preserves_writes:
assumes "i ∈ G'"
assumes "(G', T') ∈ reductions (G, T)"
assumes "W_group (the (κ' i)) =
W_group (the (κ i))
∪ (\<Union>j∈the (T i). {j} × W (the ((the (κ' i))⇩t⇩s j)))"
shows "W_group (the (proj_k (G', T') κ' i)) =
W_group (the (proj_k (G', T') κ i))
∪ (\<Union>j∈the (T' i). {j} ×
W (the ((the (proj_k (G', T') κ' i))⇩t⇩s j)))"
using assms by auto
lemma reduced_step_t:
"[| step_t a τbp τ' ;
a = No_Abst ;
τbp = (the ((the (κ i))⇩t⇩s j), b, p) ;
τ' = the ((the (κ' i))⇩t⇩s j) ; i ∈ G' ;
γ' = the (proj_k (G', T') κ' i) ;
j ∈ the (T' i) |] ==>
step_t Eq_Abst (the ((the (proj_k (G', T') κ i))⇩t⇩s j), b, p)
(the (γ' ⇩t⇩s j))"
apply (induct rule: step_t.induct)
apply (auto simp add: step_t.T_Disabled T_Assign_helper T_Read_helper T_Write_helper)
done
lemma reduced_step_g:
"[| step_g a i T γbp γo ; γo = Some (the (κ' i)) ;
(G',T') ∈ reductions (G,T) ; γbp = (the (κ i), S, p) ;
i ∈ G' ; a = No_Abst |] ==>
step_g Eq_Abst i T' (the (proj_k (G', T') κ i), S, p)
(Some (the (proj_k (G',T') κ' i)))"
proof (induct rule: step_g.induct)
case (G_Basic T i a γ s pa γ')
thus ?case
apply clarify
apply (rule step_g.G_Basic)
apply (intro ballI)
apply (fold atomize_ball)[1]
apply (rule_tac a=No_Abst and τbp="(the ((the (κ i))⇩t⇩s j), s, p)"
and τ'="(the ((the (κ' i))⇩t⇩s j))" and κ=κ and i=i and j=j
and b=s and p=p and κ'=κ' and T'=T' and G'=G' in reduced_step_t)
apply (subgoal_tac "j ∈ the (T i)")
apply auto[8]
apply (rule reduction_preserves_no_group_race[of T i κ' G' T' G])
apply auto[3]
apply (rule reduction_preserves_reads, assumption+)
apply (rule reduction_preserves_writes, assumption+)
done
next
case (G_No_Op T i pa γ a)
thus ?case
apply clarify
apply (rule G_No_Op_helper)
apply auto
done
next
case (G_Sync T i pa γ γ' P)
thus ?case
apply clarify
apply (rule step_g.G_Sync_Eq)
apply (intro ballI)
apply (auto simp del: reductions.simps)[1]
apply (subgoal_tac "j ∈ the (T i)")
apply auto[2]
apply (auto simp del: reductions.simps)[1]
apply (subgoal_tac "j ∈ the (T i)")
apply auto[2]
done
qed auto
lemma reduced_step_g_error:
"[| step_g a i T γbp γo ; γo = None ;
(G',T') ∈ reductions (G,T) ; γbp = (the (κ i), S, p) ;
i ∈ G' ; a = No_Abst |] ==>
step_g Eq_Abst i T' (the (proj_k (G', T') κ i), S, p) None"
proof (induct rule: step_g.induct)
case (G_Race T i a γ s p' γ')
thus ?case
sorry
next
case (G_Divergence j k T i p' γ a)
thus ?case
sorry
qed auto
lemma reduced_step_k:
"[| step_k a fs (G,T) K Ko ;
(G',T') ∈ reductions (G,T) ;
a = No_Abst ; Ko = Some K' ;
¬ K_Iter_applies_but (G,T) (G',T') K |] ==>
step_k Eq_Abst fs (G',T') (proj (G',T') K) (Some (proj (G',T') K'))"
proof (induct rule: step_k.induct)
case (K_Basic G a T κ b p κ' fs ss vs)
thus ?case
apply clarify
apply (unfold proj.simps)
apply (rule step_k.K_Basic)
prefer 2
apply (rule reduction_preserves_no_kernel_race[of G κ' G' T' T])
apply (assumption)+
apply (intro ballI)
apply (subgoal_tac "i ∈ G")
apply (drule_tac x=i in bspec, assumption)
apply (rule_tac a=No_Abst and i=i and T=T
and γbp="(the (κ i), Basic b, p)"
and γo="Some (the (κ' i))" in reduced_step_g)
apply auto
done
next
case (K_Sync G a T κ p κ' fs ss vs)
thus ?case
apply clarify
apply (unfold proj.simps)
apply (rule step_k.K_Sync)
prefer 2
apply (rule reduction_preserves_no_kernel_race[of G κ' G' T' T])
apply assumption+
apply (intro ballI)
apply (subgoal_tac "i ∈ G")
apply (drule_tac x=i in bspec, assumption)
apply (rule_tac a=No_Abst and i=i and T=T
and γbp="(the (κ i), Barrier, p)"
and γo="Some (the (κ' i))" in reduced_step_g)
apply auto
done
next
case (K_Iter i G j T p e κ u vs v a fs S ss)
thus ?case
apply (unfold option.inject)
apply clarify
apply (unfold proj.simps)
apply (unfold K_Iter_applies_but.simps)
apply (auto simp del: eval_bool.simps reductions.simps proj_k.simps)
apply (rule step_k.K_Iter)
apply auto
done
next
case (K_Done G T p e κ a fs S ss vs)
thus ?case
apply clarify
apply (unfold proj.simps)
apply (rule step_k.K_Done)
apply fastforce
done
qed (auto simp add: step_k.K_Seq step_k.K_Var step_k.K_If step_k.K_Open step_k.K_Call)
lemma reduced_step_k_error:
"[| step_k a fs (G,T) K Ko ;
(G',T') ∈ reductions (G,T) ;
¬ K_Iter_applies_but (G,T) (G',T') K ;
Ko = None ; a = No_Abst |] ==>
step_k Eq_Abst fs (G',T') (proj (G',T') K) None"
proof (induct rule: step_k.induct)
case (K_Inter_Group_Race G a T κ b p κ' P fs ss vs)
thus ?case sorry
next
case (K_Intra_Group_Race i G a T κ s p fs ss vs)
thus ?case sorry
next
case (K_Divergence i G a T κ p fs ss vs)
thus ?case sorry
qed (auto)
definition endOfLoop :: "threadset => kernel_state => kernel_state => bool"
where
"endOfLoop GT K K' ≡ K_Done_applies GT K' ∧ snd3 K' = snd3 K"
fun dropUntil :: "('a => bool) => 'a list => 'a list"
where
"dropUntil P [] = []"
| "dropUntil P (x # xs) = (if P x then xs else dropUntil P xs)"
lemma length_dropUntil_le:
"length (dropUntil P xs) ≤ length xs"
by (induct xs, auto)
lemma executions_consD2:
"[| Ks ∈ executions a fs GT ; dropUntil P Ks ≠ [] |] ==> dropUntil P Ks ∈ executions a fs GT"
proof (induct Ks)
case (Cons K Ks)
thus ?case
apply (cases "P K")
apply (metis dropUntil.simps(2) executions_consD)
apply (metis dropUntil.simps executions_consD)
done
qed (auto)
function process
:: "threadset => threadset => kernel_state list => kernel_state list"
where
"process GT GT' [] = []"
| "process GT GT' (K # Ks) = (
if K_Iter_applies_but GT GT' K then
proj GT' K # process GT GT' (dropUntil (endOfLoop GT K) Ks)
else
proj GT' K # process GT GT' Ks)"
by pat_completeness auto
termination
apply (relation "measure(λ(_,_,xs). length xs)")
apply (auto)
apply (smt length_dropUntil_le)
done
lemma reduction_preserves_valid_initial_kernel_state:
"[| valid_initial_kernel_state S (G, T) K0 ;
(G',T') ∈ reductions (G, T) |]
==> valid_initial_kernel_state S (G', T') (proj (G', T') K0)"
sorry
lemma must_leave_loop:
"[| Ks ∈ executions No_Abst (procs P) GT ;
step_k No_Abst fs GT (last Ks) None ;
K_Iter_applies_but GT GT' Ks_head ;
Ks = Ks_head # Ks_tail |] ==>
dropUntil (endOfLoop GT Ks_head) Ks_tail ≠ []"
sorry
lemma last_dropUntil:
"dropUntil P xs ≠ [] ==> last (dropUntil P xs) = last xs"
by (induct xs, auto)
lemma process_not_empty:
"Ks ≠ [] ==> process GT GT' Ks ≠ []"
by (case_tac Ks, auto)
theorem Eq_Soundness:
assumes "wf_kernel P"
assumes "∀(G',T') ∈ reductions (G,T). error_free Eq_Abst (main P) (procs P) (G',T')"
assumes "G = {0..<(groups P)}"
assumes "T = [G |=> {0..<(threads P)}]"
shows "error_free No_Abst (main P) (procs P) (G,T)"
proof (rule ccontr)
assume "¬ (error_free No_Abst (main P) (procs P) (G,T))"
then obtain Ks where
"Ks ∈ faulting_executions No_Abst (main P) (procs P) (G,T)"
by (auto simp add: error_free_def)
hence
1: "Ks ∈ wf_executions No_Abst (main P) (procs P) (G,T)" and
2: "step_k No_Abst (procs P) (G,T) (last Ks) None"
by (auto simp add: faulting_executions_def)
hence
3: "Ks ∈ executions No_Abst (procs P) (G,T)" and
4: "valid_initial_kernel_state (main P) (G,T) (Ks ! 0)"
by (auto simp add: wf_executions_def)
hence "Ks ≠ []" by (auto simp add: executions_def)
from 2 obtain s t where "s ≠ t" and "s ∈ tids (G,T)" and "t ∈ tids (G,T)"
sorry
def G' ≡ "{fst s, fst t}"
def T' ≡ "if fst s = fst t then [fst s \<mapsto> {snd s, snd t}]
else [fst s \<mapsto> {snd s}, fst t \<mapsto> {snd t}]"
have 5: "(G', T') ∈ reductions (G, T)"
apply (simp)
apply (intro conjI)
apply (case_tac "fst s = fst t")
apply (intro disjI1)
apply (rule_tac x="fst s" in exI)
apply (intro conjI)
apply (simp add: G'_def)
apply (case_tac "snd s = snd t")
apply (metis `s ≠ t` prod_eqI)
apply (simp add: T'_def)
apply (intro disjI2)
apply (rule_tac x="fst s" in exI)
apply (rule_tac x="fst t" in exI)
apply (intro conjI)
apply assumption
apply (simp add: G'_def)
apply (simp add: T'_def)
apply (simp add: T'_def)
apply (simp add: G'_def)
apply (intro conjI)
apply (insert `s ∈ tids (G,T)`) [1]
apply (case_tac s, simp)
apply (insert `t ∈ tids (G,T)`) [1]
apply (case_tac t, simp)
apply (simp add: G'_def T'_def)
apply (intro conjI impI)
apply (insert `s ∈ tids (G,T)`) [1]
apply (case_tac s, simp)
apply (insert `t ∈ tids (G,T)`) [1]
apply (case_tac t, simp)
apply (insert `s ∈ tids (G,T)`) [1]
apply (case_tac s, simp)
apply (insert `t ∈ tids (G,T)`) [1]
apply (case_tac t, simp)
done
def Ks' ≡ "process (G,T) (G',T') Ks"
{
fix n :: nat
have
"!!Ks. [| length Ks = n ;
Ks ∈ executions No_Abst (procs P) (G,T) ;
step_k No_Abst (procs P) (G,T) (last Ks) None |] ==>
process (G,T) (G',T') Ks ∈ executions Eq_Abst (procs P) (G',T')"
proof (induct n rule: less_induct)
case (less n Ks)
hence "Ks ≠ []" and "n > 0" by (auto simp add: executions_def)
then obtain rest κ ss vs where
Ks_def: "Ks = (κ,ss,vs) # rest"
by (case_tac Ks, auto)
{
assume 8: "¬ K_Iter_applies_but (G,T) (G',T') (κ, ss, vs)"
have ?case
apply (subst Ks_def)
apply (subst process.simps)
apply (subst if_not_P)
apply (rule 8)
apply (case_tac rest)
apply (simp add: executions_singleton)
apply (rename_tac K' rest')
apply (rule executions_consI)
apply (cut_tac y="n - 1" and Ks=rest in less.hyps)
apply (simp add: `n > 0`)
apply (insert `length Ks = n` Ks_def, auto)[1]
apply (insert less.prems(2))[1]
apply (subst (asm) Ks_def)
apply (erule executions_consD)
apply simp
apply (insert less.prems(3) Ks_def)[1]
apply simp
apply assumption
apply (insert 8)
apply (simp del: K_Iter_applies_but.simps proj.simps)
apply (rule reduced_step_k)
apply (insert less.prems(2) Ks_def executions_def)[1]
apply auto[1]
apply (rule 5)
apply simp+
done
}
moreover
{
assume 8: "K_Iter_applies_but (G,T) (G',T') (κ, ss, vs)"
have ?case
apply (subst Ks_def)
apply (subst process.simps)
apply (subst if_P)
apply (rule 8)
apply (case_tac rest)
apply simp
apply (rule executions_singleton)
apply (case_tac
"dropUntil (endOfLoop (G, T) (κ, ss, vs)) rest = []")
apply (simp add: executions_singleton)
apply (rename_tac K' rest')
apply (rule executions_consI)
apply (cut_tac
y="length (dropUntil (endOfLoop (G, T) (κ, ss, vs)) rest)" and
Ks="dropUntil (endOfLoop (G,T) (κ, ss, vs)) rest" in less.hyps)
apply (subst `length Ks = n`[symmetric])
apply (subst Ks_def)
apply (subst list.size(4))
apply (thin_tac "?x")
apply (thin_tac "?x")
apply (auto simp add: length_dropUntil_le less_Suc_eq_le)[1]
apply simp
apply (insert less.prems(2))[1]
apply (subst (asm) Ks_def)
apply (rule executions_consD2)
apply (rule executions_consD)
apply assumption
apply simp
apply (rule must_leave_loop)
apply assumption
apply (subst Ks_def[symmetric])
apply (rule less.prems(3))
apply (rule 8)
apply simp
defer 1
apply assumption
defer 1
apply (insert less.prems(3))[1]
apply (unfold Ks_def)[1]
apply (unfold last.simps)
apply (subst (asm) if_not_P)
apply simp
apply (subst last_dropUntil)
apply simp
apply simp
sorry
}
ultimately show ?case
by (cases "K_Iter_applies_but (G,T) (G',T') (κ, ss, vs)", auto)
qed
}
hence "Ks' ∈ executions Eq_Abst (procs P) (G', T')"
by (auto simp add: 2 3 Ks'_def)
moreover
{
fix n
have "!!Ks. [| length Ks = n ;
Ks ∈ executions No_Abst (procs P) (G,T) ;
step_k No_Abst (procs P) (G,T) (last Ks) None |] ==>
step_k Eq_Abst (procs P) (G',T') (last (process (G,T) (G',T') Ks)) None"
proof (induct n rule: less_induct)
case (less n Ks)
hence "Ks ≠ []" and "n > 0" by (auto simp add: executions_def)
then obtain rest κ ss vs where
Ks_def: "Ks = (κ,ss,vs) # rest"
by (case_tac Ks, auto)
{
assume 8: "¬ K_Iter_applies_but (G,T) (G',T') (κ, ss, vs)"
have ?case
apply (subst Ks_def)
apply (subst process.simps)
apply (subst if_not_P)
apply (rule 8)
apply (case_tac "rest = []")
apply (insert less.prems(3))
apply (subst (asm) Ks_def)
apply (simp del: proj.simps)
apply (rule reduced_step_k_error)
apply assumption
apply (rule 5)
apply (rule 8)
apply simp
apply simp
apply (unfold Ks_def)
apply (subgoal_tac "process (G, T) (G', T') rest ≠ []")
apply (simp del: proj.simps)
apply (rule less.hyps[where y="n - 1" and Ks="rest"])
apply (simp add: `n > 0`)
apply (insert `length Ks = n`)[1]
apply (simp add: Ks_def)
defer 1
apply assumption
apply (case_tac rest, simp, simp)
apply (metis Ks_def less.prems(2) executions_consD)
done
}
moreover
{
assume 8: "K_Iter_applies_but (G,T) (G',T') (κ, ss, vs)"
have ?case
apply (subst Ks_def)
apply (subst process.simps)
apply (subst if_P)
apply (rule 8)
apply (case_tac "dropUntil (endOfLoop (G, T) (κ, ss, vs)) rest = []")
apply (subgoal_tac "dropUntil (endOfLoop (G, T) (κ, ss, vs)) rest ≠ []")
apply simp
apply (rule must_leave_loop)
prefer 4
apply simp
apply (fold Ks_def)
apply (metis 8 Ks_def less.prems(2) less.prems(3) must_leave_loop)
apply (metis 8 Ks_def less.prems(2) less.prems(3) must_leave_loop)
apply (rule 8)
apply (subgoal_tac "process (G, T) (G', T') (
dropUntil (endOfLoop (G, T) (κ, ss, vs)) rest) ≠ []")
apply (subst last.simps)
apply (subst if_not_P, assumption)
apply (rule less.hyps)
prefer 2
apply blast
apply (insert `length Ks = n`)[1]
apply (auto simp add: Ks_def)[1]
apply (smt length_dropUntil_le)
apply (rule executions_consD2)
apply (rule executions_consD)
apply (insert less.prems(2))[1]
apply (simp add: Ks_def)
apply fastforce
apply assumption
apply (metis Ks_def dropUntil.simps(1) last.simps last_dropUntil less.prems(3))
apply (rule process_not_empty)
apply assumption
done
}
ultimately show ?case
by (cases "K_Iter_applies_but (G,T) (G',T') (κ, ss, vs)", auto)
qed
}
hence "step_k Eq_Abst (procs P) (G',T') (last Ks') None"
by (auto simp add: 2 3 Ks'_def)
moreover have
"valid_initial_kernel_state (main P) (G',T') (Ks' ! 0)"
apply (unfold Ks'_def)
apply (case_tac Ks)
apply (simp add: `Ks ≠ []`)
apply (rename_tac K0 rest)
apply (simp del: valid_initial_kernel_state.simps K_Iter_applies_but.simps)
apply (rule reduction_preserves_valid_initial_kernel_state)
apply (insert 4, simp)[1]
apply (rule 5)
done
ultimately have
"Ks' ∈ faulting_executions Eq_Abst (main P) (procs P) (G',T')"
by (metis (lifting) wf_executions_def faulting_executions_def mem_Collect_eq)
hence "¬ error_free Eq_Abst (main P) (procs P) (G',T')"
by (metis elem_set error_free_def not_None_eq set_empty_eq)
with 5 and assms(2) show False by auto
qed
end