# Theory FWState

```(*  Title:      JinjaThreads/Framework/FWState.thy
Author:     Andreas Lochbihler
*)

section ‹State of the multithreaded semantics›

theory FWState
imports
"../Basic/Auxiliary"
begin

datatype lock_action =
Lock
| Unlock
| UnlockFail
| ReleaseAcquire

datatype 't conditional_action =
Join 't
| Yield

datatype ('t, 'w) wait_set_action =
Suspend 'w
| Notify 'w
| NotifyAll 'w
| WakeUp 't
| Notified
| WokenUp

datatype 't interrupt_action
= IsInterrupted 't bool
| Interrupt 't
| ClearInterrupt 't

type_synonym 'l lock_actions = "'l ⇒f lock_action list"

translations
(type) "'l lock_actions" <= (type) "'l ⇒f lock_action list"

type_synonym
"'l lock_actions × ('t,'x,'m) new_thread_action list ×
't conditional_action list × ('t, 'w) wait_set_action list ×
't interrupt_action list × 'o list"
(* pretty printing for thread_action type *)
print_translation ‹
let
fun tr'
[Const (@{type_syntax finfun}, _) \$ l \$
(Const (@{type_syntax list}, _) \$ Const (@{type_syntax lock_action}, _)),
Const (@{type_syntax "prod"}, _) \$
(Const (@{type_syntax list}, _) \$ (Const (@{type_syntax new_thread_action}, _) \$ t1 \$ x \$ m)) \$
(Const (@{type_syntax "prod"}, _) \$
(Const (@{type_syntax list}, _) \$ (Const (@{type_syntax conditional_action}, _) \$ t2)) \$
(Const (@{type_syntax "prod"}, _) \$
(Const (@{type_syntax list}, _) \$ (Const (@{type_syntax wait_set_action}, _) \$ t3 \$ w)) \$
(Const (@{type_syntax "prod"}, _) \$
(Const (@{type_syntax "list"}, _) \$ (Const (@{type_syntax "interrupt_action"}, _) \$ t4)) \$
(Const (@{type_syntax "list"}, _) \$ o1))))] =
if t1 = t2 andalso t2 = t3 andalso t3 = t4 then Syntax.const @{type_syntax thread_action} \$ l \$ t1 \$ x \$ m \$ w \$ o1
else raise Match;
in [(@{type_syntax "prod"}, K tr')]
end
›

definition locks_a :: "('l,'t,'x,'m,'w,'o) thread_action ⇒ 'l lock_actions" ("⦃_⦄⇘l⇙"  1000) where
"locks_a ≡ fst"

definition thr_a :: "('l,'t,'x,'m,'w,'o) thread_action ⇒ ('t,'x,'m) new_thread_action list" ("⦃_⦄⇘t⇙"  1000) where
"thr_a ≡ fst o snd"

definition cond_a :: "('l,'t,'x,'m,'w,'o) thread_action ⇒ 't conditional_action list" ("⦃_⦄⇘c⇙"  1000) where
"cond_a = fst o snd o snd"

definition wset_a :: "('l,'t,'x,'m,'w,'o) thread_action ⇒ ('t, 'w) wait_set_action list" ("⦃_⦄⇘w⇙"  1000) where
"wset_a = fst o snd o snd o snd"

definition interrupt_a :: "('l,'t,'x,'m,'w,'o) thread_action ⇒ 't interrupt_action list" ("⦃_⦄⇘i⇙"  1000) where
"interrupt_a = fst o snd o snd o snd o snd"

definition obs_a :: "('l,'t,'x,'m,'w,'o) thread_action ⇒ 'o list" ("⦃_⦄⇘o⇙"  1000) where
"obs_a ≡ snd o snd o snd o snd o snd"

lemma locks_a_conv [simp]: "locks_a (ls, ntsjswss) = ls"

lemma thr_a_conv [simp]: "thr_a (ls, nts, jswss) = nts"

lemma cond_a_conv [simp]: "cond_a (ls, nts, js, wws) = js"

lemma wset_a_conv [simp]: "wset_a (ls, nts, js, wss, isobs) = wss"

lemma interrupt_a_conv [simp]: "interrupt_a (ls, nts, js, ws, is, obs) = is"

lemma obs_a_conv [simp]: "obs_a (ls, nts, js, wss, is, obs) = obs"

fun ta_update_locks :: "('l,'t,'x,'m,'w,'o) thread_action ⇒ lock_action ⇒ 'l ⇒ ('l,'t,'x,'m,'w,'o) thread_action" where
"ta_update_locks (ls, nts, js, wss, obs) lta l = (ls(l \$:= ls \$ l @ [lta]), nts, js, wss, obs)"

"ta_update_NewThread (ls, nts, js, wss, is, obs) nt = (ls, nts @ [nt], js, wss, is, obs)"

where
"ta_update_Conditional (ls, nts, js, wss, is, obs) j = (ls, nts, js @ [j], wss, is, obs)"

fun ta_update_wait_set :: "('l,'t,'x,'m,'w,'o) thread_action ⇒ ('t, 'w) wait_set_action ⇒ ('l,'t,'x,'m,'w,'o) thread_action" where
"ta_update_wait_set (ls, nts, js, wss, is, obs) ws = (ls, nts, js, wss @ [ws], is, obs)"

where
"ta_update_interrupt (ls, nts, js, wss, is, obs) i = (ls, nts, js, wss, is @ [i], obs)"

where
"ta_update_obs (ls, nts, js, wss, is, obs) ob = (ls, nts, js, wss, is, obs @ [ob])"

abbreviation empty_ta :: "('l,'t,'x,'m,'w,'o) thread_action" where
"empty_ta ≡ (K\$ [], [], [], [], [], [])"

notation (input) empty_ta ("ε")

text ‹
Pretty syntax for specifying thread actions:
Write ‹⦃ Lock→l, Unlock→l, Suspend w, Interrupt t⦄› instead of
@{term "((K\$ [])(l \$:= [Lock, Unlock]), [], [Suspend w], [Interrupt t], [])"}.

Automatically coerce basic thread actions into that type and then dispatch to the right
update function by pattern matching.
by the specific ones, i.e. constructors.
To avoid ambiguities with observable actions, the observable actions must be of sort ‹obs_action›,
which the basic thread action types are not.
›

class obs_action

= LockAction "lock_action × 'l"
| ConditionalAction "'t conditional_action"
| WaitSetAction "('t, 'w) wait_set_action"
| InterruptAction "'t interrupt_action"
| ObsAction 'o

setup ‹
›

where

nonterminal ta_let and ta_lets
syntax
"_ta_snoc" :: "ta_lets ⇒ ta_let ⇒ ta_lets" ("_,/ _")
"_ta_block" :: "ta_lets ⇒ 'a" ("⦃_⦄"  1000)
"_ta_empty" :: "ta_lets" ("")
"_ta_single" :: "ta_let ⇒ ta_lets" ("_")
"_ta_inject" :: "logic ⇒ ta_let" ("(_)")
"_ta_lock" :: "logic ⇒ logic ⇒ ta_let" ("_→_")

translations
"_ta_block _ta_empty" == "CONST empty_ta"
"_ta_block (_ta_single bta)" == "_ta_block (_ta_snoc _ta_empty bta)"
"_ta_inject bta" == "CONST inject_thread_action bta"
"_ta_lock la l" == "CONST inject_thread_action (CONST Pair la l)"

lemma ta_upd_proj_simps [simp]:
shows ta_obs_proj_simps:
"⦃ta_update_obs ta obs⦄⇘l⇙ = ⦃ta⦄⇘l⇙" "⦃ta_update_obs ta obs⦄⇘t⇙ = ⦃ta⦄⇘t⇙" "⦃ta_update_obs ta obs⦄⇘w⇙ = ⦃ta⦄⇘w⇙"
"⦃ta_update_obs ta obs⦄⇘c⇙ = ⦃ta⦄⇘c⇙" "⦃ta_update_obs ta obs⦄⇘i⇙ = ⦃ta⦄⇘i⇙" "⦃ta_update_obs ta obs⦄⇘o⇙ = ⦃ta⦄⇘o⇙ @ [obs]"
and ta_lock_proj_simps:
"⦃ta_update_locks ta x l⦄⇘l⇙ = (let ls = ⦃ta⦄⇘l⇙ in ls(l \$:= ls \$ l @ [x]))"
"⦃ta_update_locks ta x l⦄⇘t⇙ = ⦃ta⦄⇘t⇙" "⦃ta_update_locks ta x l⦄⇘w⇙ = ⦃ta⦄⇘w⇙" "⦃ta_update_locks ta x l⦄⇘c⇙ = ⦃ta⦄⇘c⇙"
"⦃ta_update_locks ta x l⦄⇘i⇙ = ⦃ta⦄⇘i⇙" "⦃ta_update_locks ta x l⦄⇘o⇙ = ⦃ta⦄⇘o⇙"
"⦃ta_update_NewThread ta t⦄⇘l⇙ = ⦃ta⦄⇘l⇙" "⦃ta_update_NewThread ta t⦄⇘t⇙ = ⦃ta⦄⇘t⇙ @ [t]" "⦃ta_update_NewThread ta t⦄⇘w⇙ = ⦃ta⦄⇘w⇙"
and ta_wset_proj_simps:
"⦃ta_update_wait_set ta w⦄⇘l⇙ = ⦃ta⦄⇘l⇙" "⦃ta_update_wait_set ta w⦄⇘t⇙ = ⦃ta⦄⇘t⇙" "⦃ta_update_wait_set ta w⦄⇘w⇙ = ⦃ta⦄⇘w⇙ @ [w]"
"⦃ta_update_wait_set ta w⦄⇘c⇙ = ⦃ta⦄⇘c⇙" "⦃ta_update_wait_set ta w⦄⇘i⇙ = ⦃ta⦄⇘i⇙" "⦃ta_update_wait_set ta w⦄⇘o⇙ = ⦃ta⦄⇘o⇙"
and ta_cond_proj_simps:
"⦃ta_update_Conditional ta c⦄⇘l⇙ = ⦃ta⦄⇘l⇙" "⦃ta_update_Conditional ta c⦄⇘t⇙ = ⦃ta⦄⇘t⇙" "⦃ta_update_Conditional ta c⦄⇘w⇙ = ⦃ta⦄⇘w⇙"
"⦃ta_update_Conditional ta c⦄⇘c⇙ = ⦃ta⦄⇘c⇙ @ [c]" "⦃ta_update_Conditional ta c⦄⇘i⇙ = ⦃ta⦄⇘i⇙" "⦃ta_update_Conditional ta c⦄⇘o⇙ = ⦃ta⦄⇘o⇙"
and ta_interrupt_proj_simps:
"⦃ta_update_interrupt ta i⦄⇘l⇙ = ⦃ta⦄⇘l⇙" "⦃ta_update_interrupt ta i⦄⇘t⇙ = ⦃ta⦄⇘t⇙" "⦃ta_update_interrupt ta i⦄⇘c⇙ = ⦃ta⦄⇘c⇙"
"⦃ta_update_interrupt ta i⦄⇘w⇙ = ⦃ta⦄⇘w⇙" "⦃ta_update_interrupt ta i⦄⇘i⇙ = ⦃ta⦄⇘i⇙ @ [i]" "⦃ta_update_interrupt ta i⦄⇘o⇙ = ⦃ta⦄⇘o⇙"
by(cases ta, simp)+

by(simp_all)

lemmas ta_upd_simps =
ta_update_wait_set.simps ta_update_interrupt.simps ta_update_obs.simps

declare ta_upd_simps [simp del]

hide_const (open)
LockAction NewThreadAction ConditionalAction WaitSetAction InterruptAction ObsAction

datatype wake_up_status =
WSNotified
| WSWokenUp

datatype 'w wait_set_status =
InWS 'w
| PostWS wake_up_status

type_synonym 't lock = "('t × nat) option"
type_synonym ('l,'t) locks = "'l ⇒f 't lock"
type_synonym 'l released_locks = "'l ⇒f nat"
type_synonym ('l,'t,'x) thread_info = "'t ⇀ ('x × 'l released_locks)"
type_synonym ('w,'t) wait_sets = "'t ⇀ 'w wait_set_status"
type_synonym 't interrupts = "'t set"
type_synonym ('l,'t,'x,'m,'w) state = "('l,'t) locks × (('l,'t,'x) thread_info × 'm) × ('w,'t) wait_sets × 't interrupts"

translations
(type) "('l, 't) locks" <= (type) "'l ⇒f ('t × nat) option"
(type) "('l, 't, 'x) thread_info" <= (type) "'t ⇀ ('x × ('l ⇒f nat))"

(* pretty printing for state type *)
print_translation ‹
let
fun tr'
[Const (@{type_syntax finfun}, _) \$ l1 \$
(Const (@{type_syntax option}, _) \$
(Const (@{type_syntax "prod"}, _) \$ t1 \$ Const (@{type_syntax nat}, _))),
Const (@{type_syntax "prod"}, _) \$
(Const (@{type_syntax "prod"}, _) \$
(Const (@{type_syntax fun}, _) \$ t2 \$
(Const (@{type_syntax option}, _) \$
(Const (@{type_syntax "prod"}, _) \$ x \$
(Const (@{type_syntax finfun}, _) \$ l2 \$ Const (@{type_syntax nat}, _))))) \$
m) \$
(Const (@{type_syntax prod}, _) \$
(Const (@{type_syntax fun}, _) \$ t3 \$
(Const (@{type_syntax option}, _) \$ (Const (@{type_syntax wait_set_status}, _) \$ w))) \$
(Const (@{type_syntax fun}, _) \$ t4 \$ (Const (@{type_syntax bool}, _))))] =
if t1 = t2 andalso t1 = t3 andalso t1 = t4 andalso l1 = l2
then Syntax.const @{type_syntax state} \$ l1 \$ t1 \$ x \$ m \$ w
else raise Match;
in [(@{type_syntax "prod"}, K tr')]
end
›
typ "('l,'t,'x,'m,'w) state"

abbreviation no_wait_locks :: "'l ⇒f nat"
where "no_wait_locks ≡ (K\$ 0)"

lemma neq_no_wait_locks_conv:
"⋀ln. ln ≠ no_wait_locks ⟷ (∃l. ln \$ l > 0)"

lemma neq_no_wait_locksE:
fixes ln assumes "ln ≠ no_wait_locks" obtains l where "ln \$ l > 0"
using assms

text ‹
Use type variables for components instead of @{typ "('l,'t,'x,'m,'w) state"} in types for state projections
to allow to reuse them for refined state implementations for code generation.
›

definition locks :: "('locks × ('thread_info × 'm) × 'wsets × 'interrupts) ⇒ 'locks" where
"locks lstsmws ≡ fst lstsmws"

definition thr :: "('locks × ('thread_info × 'm) × 'wsets × 'interrupts) ⇒ 'thread_info" where
"thr lstsmws ≡ fst (fst (snd lstsmws))"

definition shr :: "('locks × ('thread_info × 'm) × 'wsets × 'interrupts) ⇒ 'm" where
"shr lstsmws ≡ snd (fst (snd lstsmws))"

definition wset :: "('locks × ('thread_info × 'm) × 'wsets × 'interrupts) ⇒ 'wsets" where
"wset lstsmws ≡ fst (snd (snd lstsmws))"

definition interrupts :: "('locks × ('thread_info × 'm) × 'wsets × 'interrupts) ⇒ 'interrupts" where
"interrupts lstsmws ≡ snd (snd (snd lstsmws))"

lemma locks_conv [simp]: "locks (ls, tsmws) = ls"

lemma thr_conv [simp]: "thr (ls, (ts, m), ws) = ts"

lemma shr_conv [simp]: "shr (ls, (ts, m), ws, is) = m"

lemma wset_conv [simp]: "wset (ls, (ts, m), ws, is) = ws"

lemma interrupts_conv [simp]: "interrupts (ls, (ts, m), ws, is) = is"

where

"NewThread t x h = convert_new_thread_action f nta ⟷ (∃x'. nta = NewThread t x' h ∧ x = f x')"
"convert_new_thread_action f nta = NewThread t x h ⟷ (∃x'. nta = NewThread t x' h ∧ x = f x')"
by(cases nta, auto)+

"⟦ ⋀t x m. nta = NewThread t x m ⟹ nta' = NewThread t (f x) m;
⋀t b. nta = ThreadExists t b ⟹ nta' = ThreadExists t b ⟧
⟹ convert_new_thread_action f nta = nta'"
apply(cases nta)
apply fastforce+
done

apply(cases ta)
done

"inj (convert_new_thread_action f) = inj f"
apply(rule iffI)
apply(rule injI)
apply(drule_tac x="NewThread undefined x undefined" in injD)
apply auto
apply(rule injI)
apply(case_tac x)
apply(auto dest: injD)
done

"convert_new_thread_action (λx. x) = (id :: ('t, 'x, 'm) new_thread_action ⇒ ('t, 'x, 'm) new_thread_action)" (is ?thesis2)
proof -
show ?thesis1 by(rule ext)(case_tac x, simp_all)
qed

definition convert_extTA :: "('x ⇒ 'x') ⇒ ('l,'t,'x,'m,'w,'o) thread_action ⇒ ('l,'t,'x','m,'w,'o) thread_action"
where "convert_extTA f ta = (⦃ta⦄⇘l⇙, map (convert_new_thread_action f) ⦃ta⦄⇘t⇙, snd (snd ta))"

lemma convert_extTA_simps [simp]:
"convert_extTA f ε = ε"
"⦃convert_extTA f ta⦄⇘l⇙ = ⦃ta⦄⇘l⇙"
"⦃convert_extTA f ta⦄⇘t⇙ = map (convert_new_thread_action f) ⦃ta⦄⇘t⇙"
"⦃convert_extTA f ta⦄⇘c⇙ = ⦃ta⦄⇘c⇙"
"⦃convert_extTA f ta⦄⇘w⇙ = ⦃ta⦄⇘w⇙"
"⦃convert_extTA f ta⦄⇘i⇙ = ⦃ta⦄⇘i⇙"
"convert_extTA f (las, tas, was, cas, is, obs) = (las, map (convert_new_thread_action f) tas, was, cas, is, obs)"
apply(cases ta, simp)+
done

lemma convert_extTA_eq_conv:
"convert_extTA f ta = ta' ⟷
⦃ta⦄⇘l⇙ = ⦃ta'⦄⇘l⇙ ∧ ⦃ta⦄⇘c⇙ = ⦃ta'⦄⇘c⇙ ∧ ⦃ta⦄⇘w⇙ = ⦃ta'⦄⇘w⇙ ∧ ⦃ta⦄⇘o⇙ = ⦃ta'⦄⇘o⇙ ∧ ⦃ta⦄⇘i⇙ = ⦃ta'⦄⇘i⇙ ∧ length ⦃ta⦄⇘t⇙ = length ⦃ta'⦄⇘t⇙ ∧
(∀n < length ⦃ta⦄⇘t⇙. convert_new_thread_action f (⦃ta⦄⇘t⇙ ! n) = ⦃ta'⦄⇘t⇙ ! n)"
apply(cases ta, cases ta')
done

lemma convert_extTA_compose [simp]:
"convert_extTA f (convert_extTA g ta) = convert_extTA (f o g) ta"

lemma obs_a_convert_extTA [simp]: "obs_a (convert_extTA f ta) = obs_a ta"
by(cases ta) simp

datatype 'o action =
NormalAction 'o

instance action :: (type) obs_action
proof qed

where
"convert_obs_initial ta = (⦃ta⦄⇘l⇙, ⦃ta⦄⇘t⇙, ⦃ta⦄⇘c⇙, ⦃ta⦄⇘w⇙, ⦃ta⦄⇘i⇙, map NormalAction ⦃ta⦄⇘o⇙)"

lemma inj_NormalAction [simp]: "inj NormalAction"
by(rule injI) auto

lemma convert_obs_initial_inject [simp]:
"convert_obs_initial ta = convert_obs_initial ta' ⟷ ta = ta'"
by(cases ta)(cases ta', auto simp add: convert_obs_initial_def)

lemma convert_obs_initial_empty_TA [simp]:
"convert_obs_initial ε = ε"

lemma convert_obs_initial_eq_empty_TA [simp]:
"convert_obs_initial ta = ε ⟷ ta = ε"
"ε = convert_obs_initial ta ⟷ ta = ε"
by(case_tac [!] ta)(auto simp add: convert_obs_initial_def)

lemma convert_obs_initial_simps [simp]:
"⦃convert_obs_initial ta⦄⇘o⇙ = map NormalAction ⦃ta⦄⇘o⇙"
"⦃convert_obs_initial ta⦄⇘l⇙ = ⦃ta⦄⇘l⇙"
"⦃convert_obs_initial ta⦄⇘t⇙ = ⦃ta⦄⇘t⇙"
"⦃convert_obs_initial ta⦄⇘c⇙ = ⦃ta⦄⇘c⇙"
"⦃convert_obs_initial ta⦄⇘w⇙ = ⦃ta⦄⇘w⇙"
"⦃convert_obs_initial ta⦄⇘i⇙ = ⦃ta⦄⇘i⇙"

type_synonym
('l,'t,'x,'m,'w,'o) semantics =
"'t ⇒ 'x × 'm ⇒ ('l,'t,'x,'m,'w,'o) thread_action ⇒ 'x × 'm ⇒ bool"

(* pretty printing for semantics *)
print_translation ‹
let
fun tr'
[t4,
Const (@{type_syntax fun}, _) \$
(Const (@{type_syntax "prod"}, _) \$ x1 \$ m1) \$
(Const (@{type_syntax fun}, _) \$
(Const (@{type_syntax "prod"}, _) \$
(Const (@{type_syntax finfun}, _) \$ l \$
(Const (@{type_syntax list}, _) \$ Const (@{type_syntax lock_action}, _))) \$
(Const (@{type_syntax "prod"}, _) \$
(Const (@{type_syntax list}, _) \$ (Const (@{type_syntax new_thread_action}, _) \$ t1 \$ x2 \$ m2)) \$
(Const (@{type_syntax "prod"}, _) \$
(Const (@{type_syntax list}, _) \$ (Const (@{type_syntax conditional_action}, _) \$ t2)) \$
(Const (@{type_syntax "prod"}, _) \$
(Const (@{type_syntax list}, _) \$ (Const (@{type_syntax wait_set_action}, _) \$ t3 \$ w)) \$
(Const (@{type_syntax prod}, _) \$
(Const (@{type_syntax list}, _) \$ (Const (@{type_syntax interrupt_action}, _) \$ t5)) \$
(Const (@{type_syntax list}, _) \$ o1)))))) \$
(Const (@{type_syntax fun}, _) \$ (Const (@{type_syntax "prod"}, _) \$ x3 \$ m3) \$
Const (@{type_syntax bool}, _)))] =
if x1 = x2 andalso x1 = x3 andalso m1 = m2 andalso m1 = m3
andalso t1 = t2 andalso t2 = t3 andalso t3 = t4 andalso t4 = t5
then Syntax.const @{type_syntax semantics} \$ l \$ t1 \$ x1 \$ m1 \$ w \$ o1
else raise Match;
in [(@{type_syntax fun}, K tr')]
end
›
typ "('l,'t,'x,'m,'w,'o) semantics"

end
```