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" (‹_ ⇩t⇩s› [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 (γ ⇩t⇩s) = the (T i) ∧
  (∀j ∈ the (T i).
  l (the (γ ⇩t⇩s j)) GID = i ∧
  l (the (γ ⇩t⇩s 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))⇩t⇩s j)) = {}
    ∧ W (the ((the (κ i))⇩t⇩s j)) = {}) ∧
  (∀i ∈ G. ∀j ∈ the (T i). ∀v :: V. 
    l (the ((the (κ i))⇩t⇩s j)) (Inl v) = 0) ∧
  (∀i ∈ G. ∀i' ∈ G. ∀j ∈ the (T i). ∀j' ∈ the (T i').
    sh (the ((the (κ i))⇩t⇩s j)) = 
    sh (the ((the (κ i'))⇩t⇩s j'))) ∧
  (vs = []))"

end