# Theory FWWellform

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

section ‹Wellformedness conditions for the multithreaded state›

theory FWWellform
imports
FWLocking
FWWait
FWCondAction
begin

text‹Well-formedness property: Locks are held by real threads›

definition
lock_thread_ok :: "('l, 't) locks ⇒ ('l, 't,'x) thread_info ⇒ bool"
where [code del]:
"lock_thread_ok ls ts ≡ ∀l t. has_lock (ls \$ l) t ⟶ (∃xw. ts t = ⌊xw⌋)"

"lock_thread_ok ls ts = finfun_All ((λl. case l of None ⇒ True | ⌊(t, n)⌋ ⇒ (ts t ≠ None)) ∘\$ ls)"
by(simp add: lock_thread_ok_def finfun_All_All has_lock_has_locks_conv has_locks_iff o_def)

"(⋀l t. has_lock (ls \$ l) t ⟹ ∃xw. ts t = ⌊xw⌋) ⟹ lock_thread_ok ls ts"

"⟦ lock_thread_ok ls ts; has_lock (ls \$ l) t ⟧ ⟹ ∃xw. ts t = ⌊xw⌋"

"⟦ lock_thread_ok ls ts; has_locks (ls \$ l) t = Suc n ⟧ ⟹ ∃xw. ts t = ⌊xw⌋"
by(auto elim: lock_thread_okD[where l=l] simp del: split_paired_Ex)

"⟦ lock_thread_ok ls ts; ∀l t. has_lock (ls \$ l) t ⟶ (∃xw. ts t = ⌊xw⌋) ⟹ P ⟧ ⟹ P"
by(auto simp add: lock_thread_ok_def simp del: split_paired_Ex)

"lock_thread_ok ls ts ⟹ lock_thread_ok ls (ts(t ↦ xw))"

assumes "lock_thread_ok ls ts"
and "has_lock (ls \$ l) t"
obtains x ln' where "ts t = ⌊(x, ln')⌋"
using assms

assumes lto: "lock_thread_ok ls ts"
and tst: "ts t = ⌊xw⌋"
shows "lock_thread_ok (redT_updLs ls t las) ts"
fix L T
assume ru: "has_lock (redT_updLs ls t las \$ L) T"
show "∃xw. ts T = ⌊xw⌋"
proof(cases "t = T")
case True
thus ?thesis using tst lto
next
case False
with ru have "has_lock (ls \$ L) T"
thus ?thesis using lto
by(auto elim!: lock_thread_okE simp del: split_paired_Ex)
qed
qed

assumes lto: "lock_thread_ok ls ts"
shows "lock_thread_ok ls (redT_updTs ts nts)"
fix l t
assume "has_lock (ls \$ l) t"
with lto have "∃xw. ts t = ⌊xw⌋"
by(auto elim!: lock_thread_okE simp del: split_paired_Ex)
thus "∃xw. redT_updTs ts nts t = ⌊xw⌋"
by(auto intro: redT_updTs_Some1 simp del: split_paired_Ex)
qed

assumes "lock_thread_ok ls ts"
and "has_lock (ls \$ l) t"
obtains xw where "ts t = ⌊xw⌋"
using assms

"⟦ lock_thread_ok ls ts; ts t = None ⟧ ⟹ has_locks (ls \$ l) t = 0"
by(rule ccontr)(auto dest: lock_thread_okD)

"⟦lock_thread_ok ls ts; ts t = ⌊xw⌋; thread_oks ts tas⟧
⟹ lock_thread_ok (redT_updLs ls t las) ((redT_updTs ts tas)(t ↦ xw'))"
apply(clarsimp simp del: split_paired_Ex)
apply(drule has_lock_upd_locks_implies_has_lock, simp)
apply(erule exE)
by(rule redT_updTs_Some1)

fixes ln
shows "⟦ lock_thread_ok ls ts; ts t = ⌊(x, ln)⌋ ⟧ ⟹ lock_thread_ok (acquire_all ls t ln) (ts(t ↦ xw))"

text ‹Well-formedness condition: Wait sets contain only real threads›

definition wset_thread_ok :: "('w, 't) wait_sets ⇒ ('l, 't, 'x) thread_info ⇒ bool"
where "wset_thread_ok ws ts ≡ ∀t. ts t = None ⟶ ws t = None"

"(⋀t. ts t = None ⟹ ws t = None) ⟹ wset_thread_ok ws ts"

"⟦ wset_thread_ok ws ts; ts t = None ⟧ ⟹ ws t = None"

"wset_thread_ok ws ts ⟷ dom ws ⊆ dom ts"

"wset_thread_ok ls ts ⟹ wset_thread_ok ls (ts(t ↦ xw))"
by(auto intro!: wset_thread_okI dest: wset_thread_okD split: if_split_asm)

"wset_thread_ok ws ts ⟹ wset_thread_ok (ws(t := None)) (ts(t := None))"
by(auto intro!: wset_thread_okI dest: wset_thread_okD split: if_split_asm)

"wset_thread_ok ws ts ⟹ wset_thread_ok (ws(t := wo)) (ts(t ↦ xln))"
by(auto intro!: wset_thread_okI dest: wset_thread_okD split: if_split_asm)

"⟦ wset_thread_ok ws ts; ts t = ⌊xln⌋ ⟧ ⟹ wset_thread_ok (ws(t := w)) ts"

"wset_thread_ok ws ts ⟹ wset_thread_ok (λt. if ws t = ⌊w t⌋ then ⌊w' t⌋ else ws t) ts"

assumes wto: "wset_thread_ok ws ts"
shows "wset_thread_ok ws (redT_updTs ts nts)"
fix t
assume "redT_updTs ts nts t = None"
hence "ts t = None" by(rule redT_updTs_None)
with wto show "ws t = None" by(rule wset_thread_okD)
qed

"⟦ wset_thread_ok ws ts; redT_updW t ws wa ws'; ts t = ⌊xln⌋ ⟧ ⟹ wset_thread_ok ws' ts"

"⟦ wset_thread_ok ws ts; redT_updWs t ws was ws'; ts t = ⌊xln⌋ ⟧ ⟹ wset_thread_ok ws' ts"
unfolding redT_updWs_def apply(rotate_tac 1)
by(induct rule: rtrancl3p_converse_induct)(auto intro: redT_updW_preserve_wset_thread_ok)

text ‹Well-formedness condition: Wait sets contain only non-final threads›

definition wset_final_ok :: "('w, 't) wait_sets ⇒ ('l, 't, 'x) thread_info ⇒ bool"
where "wset_final_ok ws ts ⟷ (∀t ∈ dom ws. ∃x ln. ts t = ⌊(x, ln)⌋ ∧ ¬ final x)"

lemma wset_final_okI:
"(⋀t w. ws t = ⌊w⌋ ⟹ ∃x ln. ts t = ⌊(x, ln)⌋ ∧ ¬ final x) ⟹ wset_final_ok ws ts"
unfolding wset_final_ok_def by(blast)

lemma wset_final_okD:
"⟦ wset_final_ok ws ts; ws t = ⌊w⌋ ⟧ ⟹ ∃x ln. ts t = ⌊(x, ln)⌋ ∧ ¬ final x"
unfolding wset_final_ok_def by(blast)

lemma wset_final_okE:
assumes "wset_final_ok ws ts" "ws t = ⌊w⌋"
and "⋀x ln. ts t = ⌊(x, ln)⌋ ⟹ ¬ final x ⟹ thesis"
shows thesis
using assms by(blast dest: wset_final_okD)