Session GPU_Kernel_PL

Theory Misc

section ‹General purpose definitions and lemmas›

theory Misc imports 
  Main
begin

text ‹A handy abbreviation when working with maps›
abbreviation make_map :: "'a set  'b  ('a  'b)" ("[ _ |=> _ ]")
where
  "[ks |=> v]  λk. if k  ks then Some v else None"

text ‹Projecting the components of a triple›
definition "fst3  fst"
definition "snd3  fst  snd"
definition "thd3  snd  snd"

lemma fst3_simp [simp]: "fst3 (a,b,c) = a" by (simp add: fst3_def)
lemma snd3_simp [simp]: "snd3 (a,b,c) = b" by (simp add: snd3_def)
lemma thd3_simp [simp]: "thd3 (a,b,c) = c" by (simp add: thd3_def)

end

Theory KPL_syntax

section ‹Syntax of KPL›

theory KPL_syntax imports 
  Misc
begin

text‹Locations of local variables›
typedecl V 

text ‹C strings›
typedecl name

text ‹Procedure names›
typedecl proc_name

text ‹Local-id, group-id›
type_synonym lid = nat
type_synonym gid = nat

text ‹Fully-qualified thread-id›
type_synonym tid = "gid × lid"

text ‹Let @{term "(G,T)"} range over threadsets›
type_synonym threadset = "gid set × (gid  lid set)"

text ‹Returns the set of tids in a threadset›
fun tids :: "threadset  tid set"
where
  "tids (G,T) = {(i,j) | i j. i  G  j  the (T i)}"

type_synonym word = nat  (* should really be machine words *)

datatype loc =
  Name name
| Var V

text ‹Local expressions›
datatype local_expr =
  Loc loc
| Gid
| Lid
| eTrue
| eConj local_expr local_expr  (infixl "∧*" 50)
| eNot local_expr              ("¬*")

text ‹Basic statements›
datatype basic_stmt =
  Assign loc local_expr
| Read loc local_expr
| Write local_expr local_expr

text ‹Statements›
datatype stmt =
  Basic basic_stmt
| Seq stmt stmt (infixl ";;" 50)
| Local name stmt
| If local_expr stmt stmt
| While local_expr stmt
| WhileDyn local_expr stmt
| Call proc_name local_expr
| Barrier
| Break
| Continue
| Return

text ‹Procedures comprise a procedure name, parameter name, and a body statement›
record proc = 
  proc_name :: proc_name
  param :: name
  body :: stmt

text ‹Kernels›
record kernel = 
  groups :: nat
  threads :: nat
  procs :: "proc list"
  main :: stmt

end

Theory KPL_wellformedness

section ‹Well-formedness of KPL kernels›

theory KPL_wellformedness imports 
  KPL_syntax
begin

text ‹
  Well-formed local expressions. @{term "wf_local_expr ns e"} 
  means that 
  \begin{itemize} 
  \item @{term e} does not mention any internal locations, and
  \item any name mentioned by @{term e} is in the set @{term ns}.
  \end{itemize}
›
fun wf_local_expr :: "name set  local_expr  bool"
where
  "wf_local_expr ns (Loc (Var j)) = False"
| "wf_local_expr ns (Loc (Name n)) = (n  ns)"
| "wf_local_expr ns (e1 ∧* e2) =
  (wf_local_expr ns e1  wf_local_expr ns e2)"
| "wf_local_expr ns (¬* e) = wf_local_expr ns e"
| "wf_local_expr ns _ = True"

text ‹
  Well-formed basic statements. @{term "wf_basic_stmt ns b"} 
  means that 
  \begin{itemize}
  \item @{term b} does not mention any internal locations, and
  \item any name mentioned by @{term b} is in the set @{term ns}.
  \end{itemize}
›
fun wf_basic_stmt :: "name set  basic_stmt  bool"
where
  "wf_basic_stmt ns (Assign x e) = wf_local_expr ns e"
| "wf_basic_stmt ns (Read x e) = wf_local_expr ns e"
| "wf_basic_stmt ns (Write e1 e2) = 
  (wf_local_expr ns e1  wf_local_expr ns e2)"

text ‹
  Well-formed statements. @{term "wf_stmt ns F S"} means:
  \begin{itemize}
  \item @{term S} only calls procedures whose name is in @{term F},
  \item @{term S} does not contain @{term WhileDyn}, 
  \item @{term S} does not mention internal variables, 
  \item @{term S} only mentions names in @{term ns}, and
  \item @{term S} does not declare the same name twice, e.g. @{term "Local x (Local x foo)"}.
  \end{itemize}
›
fun wf_stmt :: "name set  proc_name set  stmt  bool"
where
  "wf_stmt ns F (Basic b) = wf_basic_stmt ns b"
| "wf_stmt ns F (S1 ;; S2) = (wf_stmt ns F S1  wf_stmt ns F S2)"
| "wf_stmt ns F (Local n S) = (n  ns  wf_stmt ({n}  ns) F S)"
| "wf_stmt ns F (If e S1 S2) = 
  (wf_local_expr ns e  wf_stmt ns F S1  wf_stmt ns F S2)"
| "wf_stmt ns F (While e S) = 
  (wf_local_expr ns e  wf_stmt ns F S)"
| "wf_stmt ns F (WhileDyn _ _) = False"
| "wf_stmt ns F (Call f e) = (f  F  wf_local_expr ns e)"
| "wf_stmt _ _ _ = True"

text @{term "no_return S"} holds if @{term S} does not contain a @{term Return} statement›
fun no_return :: "stmt  bool"
where
  "no_return (S1 ;; S2) = (no_return S1  no_return S2)"
| "no_return (Local n S) = no_return S"
| "no_return (If e S1 S2) = (no_return S1  no_return S2)"
| "no_return (While e S) = (no_return S)"
| "no_return Return = False"
| "no_return _ = True"

text ‹Well-formed kernel›
definition wf_kernel :: "kernel  bool"
where
  "wf_kernel P 
  let F = set (map proc_name (procs P)) in
 
  ― ‹The main statement must not refer to ‹any› variable, except those it locally defines.›
  wf_stmt {} F (main P)

  ― ‹The main statement contains no return statement.›
 no_return (main P)
 
  ― ‹A procedure body may refer only to its argument.›
 list_all (λf. wf_stmt {param f} F (body f)) (procs P)"


end

Theory KPL_state

section ‹Thread, group and kernel states›

theory KPL_state imports 
  KPL_syntax
begin

text ‹Thread state›
record thread_state =
  (* We use "V + bool" to indicate that the domain of
     l is extended with two extra values. Let's say
     that "l (Inr True)" returns the gid, and that
     "l (Inr False)" returns the lid. *)
  l :: "V + bool  word" 
  sh :: "nat  word"
  R :: "nat set"
  W :: "nat set"

abbreviation "GID  Inr True"
abbreviation "LID  Inr False"

text ‹Group state›
record group_state = 
  thread_states :: "lid  thread_state" ("_ ts" [1000] 1000)
  R_group :: "(lid × nat) set"
  W_group :: "(lid × nat) set"

text ‹Valid group state›
fun valid_group_state :: "(gid  lid set)  gid  group_state  bool"
where
  "valid_group_state T i γ = (
  dom (γ ts) = the (T i) 
  (j  the (T i).
  l (the (γ ts j)) GID = i 
  l (the (γ ts j)) LID = j))"

text ‹Predicated statements›
type_synonym pred_stmt = "stmt × local_expr"
type_synonym pred_basic_stmt = "basic_stmt × local_expr"

text ‹Kernel state›
type_synonym kernel_state = 
  "(gid  group_state) × pred_stmt list × V list"

text ‹Valid kernel state›
fun valid_kernel_state :: "threadset  kernel_state  bool"
where
  "valid_kernel_state (G,T) (κ, ss, _) = (
  dom κ = G 
  (i  G. valid_group_state T i (the (κ i))))"

text ‹Valid initial kernel state›
fun valid_initial_kernel_state :: "stmt  threadset  kernel_state  bool"
where
  "valid_initial_kernel_state S (G,T) (κ, ss, vs) = ( 
  valid_kernel_state (G,T) (κ, ss, vs) 
  (ss = [(S, eTrue)]) 
  (i  G. R_group (the (κ i)) = {}  W_group (the (κ i)) = {}) 
  (i  G. j  the (T i). R (the ((the (κ i))ts j)) = {}
     W (the ((the (κ i))ts j)) = {}) 
  (i  G. j  the (T i). v :: V. 
    l (the ((the (κ i))ts j)) (Inl v) = 0) 
  (i  G. i'  G. j  the (T i). j'  the (T i').
    sh (the ((the (κ i))ts j)) = 
    sh (the ((the (κ i'))ts j'))) 
  (vs = []))"

end

Theory KPL_execution_thread

section ‹Execution rules for threads›

theory KPL_execution_thread imports 
  KPL_state
begin

text ‹Evaluate a local expression down to a word›
fun eval_word :: "local_expr  thread_state  word"
where
  "eval_word (Loc (Var v)) τ = l τ (Inl v)"
(* eval_word (Loc (Name n)) τ = undefined *)
| "eval_word Lid τ = l τ LID"
| "eval_word Gid τ = l τ GID"
| "eval_word eTrue τ = 1"
| "eval_word (e1 ∧* e2) τ = 
  (eval_word e1 τ * eval_word e2 τ)"
| "eval_word (¬* e) τ = (if eval_word e τ = 0 then 1 else 0)"

text ‹Evaluate a local expression down to a boolean›
fun eval_bool :: "local_expr  thread_state  bool"
where
  "eval_bool e τ = (eval_word e τ  0)"

text ‹Abstraction level: none, equality abstraction, or adversarial abstraction›
datatype abs_level = No_Abst | Eq_Abst | Adv_Abst

text ‹The rules of Figure 4, plus two additional rules 
  for adversarial abstraction (Fig 7b)›
inductive step_t 
  :: "abs_level  (thread_state × pred_basic_stmt)  thread_state  bool"  
where
  T_Disabled: 
  "¬ (eval_bool p τ)  step_t a (τ, (b, p)) τ"
| T_Assign: 
  " eval_bool p τ ; l' = (l τ) (Inl v := eval_word e τ)  
   step_t a (τ, (Assign (Var v) e, p)) (τ (| l := l' |))"
| T_Read: 
  " eval_bool p τ ; l' = (l τ) (Inl v := sh τ (eval_word e τ)) ;
  R' = R τ  { eval_word e τ } ; a  {No_Abst, Eq_Abst}  
   step_t a (τ, (Read (Var v) e, p)) (τ (| l := l', R := R' |))"
| T_Write: 
  " eval_bool p τ ; 
  sh' = (sh τ) (eval_word e1 τ := eval_word e2 τ) ;
  W' = W τ  { eval_word e1 τ } ; a  {No_Abst, Eq_Abst}  
   step_t a (τ, (Write e1 e2, p)) (τ (| sh := sh', W := W' |))"
| T_Read_Adv:
  " eval_bool p τ ; l' = (l τ) (Inl v := asterisk) ;
  R' = R τ  { eval_word e τ }  
   step_t Adv_Abst (τ, (Read (Var v) e, p)) (τ (| l := l', R := R' |))"
| T_Write_Adv:
  " eval_bool p τ ; W' = W τ  { eval_word e1 τ }  
   step_t Adv_Abst (τ, (Write e1 e2, p)) (τ (| ⌦‹sh := sh',› W := W' |))"

text ‹Rephrasing T_Assign› to make it more usable›
lemma T_Assign_helper: 
  " eval_bool p τ ; l' = (l τ) (Inl v := eval_word e τ) ; τ' = τ (| l := l' |)  
   step_t a (τ, (Assign (Var v) e, p)) τ'"
by (auto simp add: step_t.T_Assign)

text ‹Rephrasing T_Read› to make it more usable›
lemma T_Read_helper: 
  " eval_bool p τ ; l' = (l τ) (Inl v := sh τ (eval_word e τ)) ;
  R' = R τ  { eval_word e τ } ; a  {No_Abst, Eq_Abst} ; 
  τ' = τ (| l := l', R := R' |)  
   step_t a (τ, (Read (Var v) e, p)) τ'"
by (auto simp add: step_t.T_Read)

text ‹Rephrasing T_Write› to make it more usable›
lemma T_Write_helper:
  " eval_bool p τ ; 
  sh' = (sh τ) (eval_word e1 τ := eval_word e2 τ) ;
  W' = W τ  { eval_word e1 τ } ; a  {No_Abst, Eq_Abst} ;
  τ' = τ (| sh := sh', W := W' |)  
   step_t a (τ, (Write e1 e2, p)) τ'"
by (auto simp add: step_t.T_Write)

end

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: "idom γ. jdom γ. 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 (γ ts j), (s, p)) (the (γ' ts j)) ; 
    group_race (the (T i)) ((γ' :: group_state)ts) 
   step_g a i T (γ, (Basic s, p)) None"
| G_Basic:
  " j  the (T i). step_t a (the (γ ts j), (s, p)) (the (γ' ts j)) ; 
    ¬ (group_race (the (T i)) (γ' ts)) ;
    R_group γ' = R_group γ  (j  the (T i). ({j} × R (the (γ' ts j)))) ;
    W_group γ' = W_group γ  (j  the (T i). ({j} × W (the (γ' ts j)))) 
   step_g a i T (γ, (Basic s, p)) (Some γ')"
| G_No_Op:
  "j  the (T i). ¬ (eval_bool p (the (γ ts 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 (γ ts j)) ; ¬ (eval_bool p (the (γ ts k))) 
   step_g a i T (γ, (Barrier, p)) None"
| G_Sync:
  " j  the (T i). eval_bool p (the (γ ts j)) ;
    j  the (T i). the (γ' ts j) = (the (γ ts j)) (| 
    sh := merge P (γ ts), R := {}, W := {} |)  
   step_g No_Abst i T (γ, (Barrier, p)) (Some γ')"
| G_Sync_Eq:
  " j  the (T i). eval_bool p (the (γ ts j)) ;
    j  the (T i). the (γ' ts j) = (the (γ ts 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 (γ ts j)) ;
    j  the (T i). sh'. the (γ' ts j) = (the (γ ts 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 (γ ts j))) ; γ = γ' 
   step_g a i T (γ, (Barrier, p)) (Some γ')"
by (simp add: step_g.G_No_Op)


end

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

Theory Kernel_programming_language

(* 
Title:       Kernel_programming_language.thy
Author:      John Wickerson
Date:        2 April 2014
Description: 
  This theory file accompanies the article "The Design and 
  Implementation of a Verification Technique for GPU Kernels" 
  by Adam Betts, Nathan Chong, Alastair F. Donaldson, Jeroen
  Ketema, Shaz Qadeer, Paul Thomson and John Wickerson. It
  formalises all of the definitions provided in Sections 3
  and 4. 
*)

theory Kernel_programming_language imports
(* 1. SOME GENERAL PURPOSE STUFF *)
  Misc
(* 2. SYNTAX OF KPL *)
  KPL_syntax
(* 3. WELL-FORMEDNESS OF KPL KERNELS *)
  KPL_wellformedness
(* 4. THREAD, GROUP, AND KERNEL STATES *)
  KPL_state
(* 5. EXECUTION RULES FOR THREADS *)
  KPL_execution_thread
(* 6. EXECUTION RULES FOR GROUPS *)
  KPL_execution_group
(* 7. EXECUTION RULES FOR KERNELS *)
  KPL_execution_kernel
begin 

end