Theory KPL_execution_kernel

section ‹Execution rules for kernels›

theory KPL_execution_kernel imports 
  KPL_execution_group
begin

text ‹Inter-group race detection›
definition kernel_race 
  :: "gid set ⇒ (gid ⇀ group_state) ⇒ bool"
where "kernel_race G κ ≡ 
  ∃i ∈ G. ∃j ∈ G. i ≠ j ∧ 
  (snd ` (W_group (the (κ i)))) ∩ 
  (snd ` (R_group (the (κ j))) ∪ snd ` (W_group (the (κ j)))) ≠ {}"

text ‹Replaces top-level @{term Break} with ‹v := true››
fun belim :: "stmt ⇒ V ⇒ stmt"
where 
  "belim (Basic b) v = Basic b"
| "belim (S1 ;; S2) v = (belim S1 v ;; belim S2 v)"
| "belim (Local n S) v = Local n (belim S v)"
| "belim (If e S1 S2) v = If e (belim S1 v) (belim S2 v)"
| "belim (While e S) v = While e S" (* only top-level *)
(* belim (WhileDyn e S) v = undefined *)
| "belim (Call f e) v = Call f e"
| "belim Barrier v = Barrier"
| "belim Break v = Basic (Assign (Var v) eTrue)"
| "belim Continue v = Continue"
| "belim Return v = Return"

text ‹Replaces top-level @{term Continue} with ‹v := true››
fun celim :: "stmt ⇒ V ⇒ stmt"
where 
  "celim (Basic b) v = Basic b"
| "celim (S1 ;; S2) v = (celim S1 v ;; celim S2 v)"
| "celim (Local n S) v = Local n (celim S v)"
| "celim (If e S1 S2) v = If e (celim S1 v) (celim S2 v)"
| "celim (While e S) v = While e S" (* only top-level *)
(* celim (WhileDyn e S) v = undefined *)
| "celim (Call f e) v = Call f e"
| "celim Barrier v = Barrier"
| "celim Break v = Break"
| "celim Continue v = Basic (Assign (Var v) eTrue)"
| "celim Return v = Return"

text ‹@{term "subst_basic_stmt n v loc"} replaces @{term n} with @{term v} inside @{term loc}›
fun subst_loc :: "name ⇒ V ⇒ loc ⇒ loc"
where
  "subst_loc n v (Var w) = Var w"
| "subst_loc n v (Name m) = (if n = m then Var v else Name m)"

text ‹@{term "subst_local_expr n v e"} replaces @{term n} with @{term v} inside @{term e}›
fun subst_local_expr 
  :: "name ⇒ V ⇒ local_expr ⇒ local_expr"
where
  "subst_local_expr n v (Loc loc) = Loc (subst_loc n v loc)"
| "subst_local_expr n v Gid = Gid"
| "subst_local_expr n v Lid = Lid"
| "subst_local_expr n v eTrue = eTrue"
| "subst_local_expr n v (e1 ∧* e2) = 
  (subst_local_expr n v e1 ∧* subst_local_expr n v e2)"
| "subst_local_expr n v (¬* e) = ¬* (subst_local_expr n v e)"

text ‹@{term "subst_basic_stmt n v b"} replaces @{term n} with @{term v} inside @{term b}›
fun subst_basic_stmt :: "name ⇒ V ⇒ basic_stmt ⇒ basic_stmt"
where 
  "subst_basic_stmt n v (Assign loc e) = 
  Assign (subst_loc n v loc) (subst_local_expr n v e)"
| "subst_basic_stmt n v (Read loc e) =
  Read (subst_loc n v loc) (subst_local_expr n v e)"
| "subst_basic_stmt n v (Write e1 e2) =
  Write (subst_local_expr n v e1) (subst_local_expr n v e2)"

text ‹@{term "subst_stmt n v s t"} holds if @{term t} is the result 
  of replacing @{term n} with @{term v} inside @{term s}›
inductive subst_stmt :: "name ⇒ V ⇒ stmt ⇒ stmt ⇒ bool"
where 
  "subst_stmt n v (Basic b) (Basic (subst_basic_stmt n v b))"
| "⟦ subst_stmt n v S1 S1' ; subst_stmt n v S2 S2' ⟧ ⟹
  subst_stmt n v (S1 ;; S2) (S1' ;; S2')"
| "⟦ m ≠ n ; subst_stmt n v S S' ⟧ ⟹ 
  subst_stmt n v (Local m S) (Local m S')"
| "⟦ subst_stmt n v S1 S1' ; subst_stmt n v S2 S2' ⟧ ⟹ 
  subst_stmt n v (If e S1 S2) (If e S1' S2')"
| "subst_stmt n v S S' ⟹ subst_stmt n v (While e S) (While e S')" 
(* subst_stmt n v (WhileDyn e S) undefined *)
| "subst_stmt n v (Call f e) (Call f e)"
| "subst_stmt n v Barrier Barrier"
| "subst_stmt n v Break Break"
| "subst_stmt n v Continue Continue"
| "subst_stmt n v Return Return"

text ‹@{term "param_subst f u"} replaces @{term f}'s parameter with @{term u}›
definition param_subst :: "proc list ⇒ proc_name ⇒ V ⇒ stmt"
where "param_subst fs f u ≡ 
  let proc = THE proc. proc ∈ set fs ∧ proc_name proc = f in
  THE S'. subst_stmt (param proc) u (body proc) S'"

text ‹Replace @{term "Return"} with ‹v := true››
fun relim :: "stmt ⇒ V ⇒ stmt"
where 
  "relim (Basic b) v = Basic b"
(* Additional rule for adversarial abstraction (Fig 7b) *)
| "relim (S1 ;; S2) v = (relim S1 v ;; relim S2 v)"
| "relim (Local n S) v = Local n (relim S v)"
| "relim (If e S1 S2) v = If e (relim S1 v) (relim S2 v)"
| "relim (While e S) v = While e (relim S v)"
(* relim (WhileDyn e S) v = undefined *)
| "relim (Call f e) v = Call f e"
| "relim Barrier v = Barrier"
| "relim Break v = Break"
| "relim Continue v = Continue"
| "relim Return v = Basic (Assign (Var v) eTrue)"

text ‹Fresh variables›
definition fresh :: "V ⇒ V list ⇒ bool"
where "fresh v vs ≡ v ∉ set vs"

text ‹The rules of Figure 6›
inductive step_k
  :: "abs_level ⇒ proc list ⇒ threadset ⇒ kernel_state ⇒ kernel_state option ⇒ bool"
where
  K_Inter_Group_Race:
  "⟦ ∀i ∈ G. step_g a i T (the (κ i), (Basic b, p)) (Some (the (κ' i))) ;
     kernel_race P κ' ⟧ ⟹
  step_k a fs (G,T) (κ, (Basic b, p) # ss, vs) None"
| K_Intra_Group_Race:
  "⟦ i ∈ G; step_g a i T (the (κ i), (Basic s, p)) None ⟧ ⟹
  step_k a fs (G,T) (κ, (Basic s, p) # ss, vs) None"
| K_Basic:
  "⟦ ∀i ∈ G. step_g a i T (the (κ i), (Basic b, p)) (Some (the (κ' i))) ;
     ¬ (kernel_race G κ') ⟧ ⟹
  step_k a fs (G,T) (κ, (Basic b, p) # ss, vs) (Some (κ',ss, vs))"
| K_Divergence:
  "⟦ i ∈ G; step_g a i T (the (κ i), (Barrier, p)) None ⟧ ⟹
  step_k a fs (G,T) (κ, (Barrier, p) # ss, vs) None"
| K_Sync:
  "⟦ ∀i ∈ G. step_g a i T (the (κ i), (Barrier, p)) (Some (the (κ' i))) ;
     ¬ (kernel_race G κ') ⟧ ⟹
  step_k a fs (G,T) (κ, (Barrier, p) # ss, vs) (Some (κ',ss, vs))"
| K_Seq:
  "step_k a fs (G,T) (κ, (S1 ;; S2, p) # ss, vs) 
  (Some (κ, (S1, p) # (S2, p) # ss, vs))"
| K_Var:
  "fresh v vs ⟹ 
  step_k a fs (G,T) (κ, (Local n S, p) # ss, vs)  
  (Some (κ, (THE S'. subst_stmt n v S S', p) # ss, v # vs))"
| K_If: 
  "fresh v vs ⟹ 
  step_k a fs (G,T) (κ, (If e S1 S2, p) # ss, vs) (Some (κ, 
  (Basic (Assign (Var v) e), p) 
  # (S1, p ∧* Loc (Var v)) 
  # (S2, p ∧* ¬* (Loc (Var v))) # ss, v # vs))"
| K_Open:
  "fresh v vs ⟹
  step_k a fs (G,T) (κ, (While e S, p) # ss, vs) (Some (κ, 
  (WhileDyn e (belim S v), p ∧* ¬* (Loc (Var v))) # ss, v # vs))"
| K_Iter:
  "⟦ i ∈ G ; j ∈ the (T i) ; 
  eval_bool (p ∧* e) (the ((the (κ i))⇩t⇩s j)) ; 
  fresh u vs ; fresh v vs; u ≠ v ⟧ ⟹
  step_k a fs (G,T) (κ, (WhileDyn e S, p) # ss, vs) (Some (κ, 
  (Basic (Assign (Var u) e), p) 
  # (celim S v, p ∧* Loc (Var u) ∧* ¬* (Loc (Var v))) 
  # (WhileDyn e S, p) # ss, u # v # vs))"
| K_Done:
  "∀i ∈ G. ∀j ∈ the (T i). 
  ¬ (eval_bool (p ∧* e) (the ((the (κ i))⇩t⇩s j))) ⟹
  step_k a fs (G,T) (κ, (WhileDyn e S, p) # ss, vs) (Some (κ, ss, vs))"
| K_Call: 
  "⟦ fresh u vs ; fresh v vs ; u ≠ v ; s = param_subst fs f u ⟧ ⟹
  step_k a fs (G,T) (κ, (Call f e, p) # ss, vs ) 
  (Some (κ, (Basic (Assign (Var u) e) ;; relim s v, 
  p ∧* ¬* (Loc (Var v))) # ss, u # v # vs))"



end