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))ts 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))ts 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