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