# Theory FWLocking

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

section ‹Semantics of the thread actions for locking›

theory FWLocking
imports
FWLock
begin

definition redT_updLs :: "('l,'t) locks ⇒ 't ⇒ 'l lock_actions ⇒ ('l,'t) locks" where
"redT_updLs ls t las ≡ (λ(l, la). upd_locks l t la) ∘\$ ((\$ls, las\$))"

lemma redT_updLs_iff [simp]: "redT_updLs ls t las \$ l = upd_locks (ls \$ l) t (las \$ l)"

lemma upd_locks_empty_conv [simp]: "(λ(l, las). upd_locks l t las) ∘\$ (\$ls, K\$ []\$) = ls"
by(auto intro: finfun_ext)

"⟦ has_lock (redT_updLs ls t las \$ l) t'; t ≠ t' ⟧ ⟹ has_lock (ls \$ l) t'"
by(auto simp add: redT_updLs_def intro: has_lock_upd_locks_implies_has_lock)

definition acquire_all :: "('l, 't) locks ⇒ 't ⇒ ('l ⇒f nat) ⇒ ('l, 't) locks"
where "⋀ln. acquire_all ls t ln ≡ (λ(l, la). acquire_locks l t la) ∘\$ ((\$ls, ln\$))"

lemma acquire_all_iff [simp]:
"⋀ln. acquire_all ls t ln \$ l = acquire_locks (ls \$ l) t (ln \$ l)"

definition lock_ok_las :: "('l,'t) locks ⇒ 't ⇒ 'l lock_actions ⇒ bool" where
"lock_ok_las ls t las ≡ ∀l. lock_actions_ok (ls \$ l) t (las \$ l)"

lemma lock_ok_lasI [intro]:
"(⋀l. lock_actions_ok (ls \$ l) t (las \$ l)) ⟹ lock_ok_las ls t las"

lemma lock_ok_lasE:
"⟦ lock_ok_las ls t las; (⋀l. lock_actions_ok (ls \$ l) t (las \$ l)) ⟹ Q ⟧ ⟹ Q"

lemma lock_ok_lasD:
"lock_ok_las ls t las ⟹ lock_actions_ok (ls \$ l) t (las \$ l)"

lemma lock_ok_las_code [code]:
"lock_ok_las ls t las = finfun_All ((λ(l, la). lock_actions_ok l t la) ∘\$ (\$ls, las\$))"

lemma lock_ok_las_may_lock:
"⟦ lock_ok_las ls t las; Lock ∈ set (las \$ l) ⟧ ⟹ may_lock (ls \$ l) t"
by(erule lock_ok_lasE)(rule lock_actions_ok_Lock_may_lock)

lemma redT_updLs_may_lock [simp]:
"lock_ok_las ls t las ⟹ may_lock (redT_updLs ls t las \$ l) t = may_lock (ls \$ l) t"
by(auto dest!: lock_ok_lasD[where l=l])

lemma redT_updLs_has_locks [simp]:
"⟦ lock_ok_las ls t' las; t ≠ t' ⟧ ⟹ has_locks (redT_updLs ls t' las \$ l) t = has_locks (ls \$ l) t"
by(auto dest!: lock_ok_lasD[where l=l])

definition may_acquire_all :: "('l, 't) locks ⇒ 't ⇒ ('l ⇒f nat) ⇒ bool"
where "⋀ln. may_acquire_all ls t ln ≡ ∀l. ln \$ l > 0 ⟶ may_lock (ls \$ l) t"

lemma may_acquire_allI [intro]:
"⋀ln. (⋀l. ln \$ l > 0 ⟹ may_lock (ls \$ l) t) ⟹ may_acquire_all ls t ln"

lemma may_acquire_allE:
"⋀ln. ⟦ may_acquire_all ls t ln; ∀l. ln \$ l > 0 ⟶ may_lock (ls \$ l) t ⟹ P ⟧ ⟹ P"

lemma may_acquire_allD [dest]:
"⋀ln. ⟦ may_acquire_all ls t ln; ln \$ l > 0 ⟧ ⟹ may_lock (ls \$ l) t"

lemma may_acquire_all_has_locks_acquire_locks [simp]:
fixes ln
shows "⟦ may_acquire_all ls t ln; t ≠ t' ⟧ ⟹ has_locks (acquire_locks (ls \$ l) t (ln \$ l)) t' = has_locks (ls \$ l) t'"
by(cases "ln \$ l > 0")(auto dest: may_acquire_allD)

lemma may_acquire_all_code [code]:
"⋀ln. may_acquire_all ls t ln ⟷ finfun_All ((λ(lock, n). n > 0 ⟶ may_lock lock t) ∘\$ (\$ls, ln\$))"
by(auto simp add: may_acquire_all_def finfun_All_All o_def)

definition collect_locks :: "'l lock_actions ⇒ 'l set" where
"collect_locks las = {l. Lock ∈ set (las \$ l)}"

lemma collect_locksI:
"Lock ∈ set (las \$ l) ⟹ l ∈ collect_locks las"

lemma collect_locksE:
"⟦ l ∈ collect_locks las; Lock ∈ set (las \$ l) ⟹ P ⟧ ⟹ P"

lemma collect_locksD:
"l ∈ collect_locks las ⟹ Lock ∈ set (las \$ l)"

fun must_acquire_lock :: "lock_action list ⇒ bool" where
"must_acquire_lock [] = False"
| "must_acquire_lock (Lock # las) = True"
| "must_acquire_lock (Unlock # las) = False"
| "must_acquire_lock (_ # las) = must_acquire_lock las"

lemma must_acquire_lock_append:
"must_acquire_lock (xs @ ys) ⟷ (if Lock ∈ set xs ∨ Unlock ∈ set xs then must_acquire_lock xs else must_acquire_lock ys)"
proof(induct xs)
case Nil thus ?case by simp
next
case (Cons L Ls)
thus ?case by (cases L, simp_all)
qed

lemma must_acquire_lock_contains_lock:
"must_acquire_lock las ⟹ Lock ∈ set las"
proof(induct las)
case (Cons l las) thus ?case by(cases l) auto
qed simp

lemma must_acquire_lock_conv:
"must_acquire_lock las = (case (filter (λL. L = Lock ∨ L = Unlock) las) of [] ⇒ False | L # Ls ⇒ L = Lock)"
proof(induct las)
case Nil thus ?case by simp
next
case (Cons LA LAS) thus ?case
by(cases LA, auto split: list.split_asm)
qed

definition collect_locks' :: "'l lock_actions ⇒ 'l set" where
"collect_locks' las ≡ {l. must_acquire_lock (las \$ l)}"

lemma collect_locks'I:
"must_acquire_lock (las \$ l) ⟹ l ∈ collect_locks' las"

lemma collect_locks'E:
"⟦ l ∈ collect_locks' las; must_acquire_lock (las \$ l) ⟹ P ⟧ ⟹ P"

lemma collect_locks'_subset_collect_locks:
"collect_locks' las ⊆ collect_locks las"
by(auto simp add: collect_locks'_def collect_locks_def intro: must_acquire_lock_contains_lock)

definition lock_ok_las' :: "('l,'t) locks ⇒ 't ⇒ 'l lock_actions ⇒ bool" where
"lock_ok_las' ls t las ≡ ∀l. lock_actions_ok' (ls \$ l) t (las \$ l)"

lemma lock_ok_las'I: "(⋀l. lock_actions_ok' (ls \$ l) t (las \$ l)) ⟹ lock_ok_las' ls t las"

lemma lock_ok_las'D: "lock_ok_las' ls t las ⟹ lock_actions_ok' (ls \$ l) t (las \$ l)"

lemma not_lock_ok_las'_conv:
"¬ lock_ok_las' ls t las ⟷ (∃l. ¬ lock_actions_ok' (ls \$ l) t (las \$ l))"

lemma lock_ok_las'_code:
"lock_ok_las' ls t las = finfun_All ((λ(l, la). lock_actions_ok' l t la) ∘\$ (\$ls, las\$))"

lemma lock_ok_las'_collect_locks'_may_lock:
assumes lot': "lock_ok_las' ls t las"
and mayl: "∀l ∈ collect_locks' las. may_lock (ls \$ l) t"
and l: "l ∈ collect_locks las"
shows "may_lock (ls \$ l) t"
proof(cases "l ∈ collect_locks' las")
case True thus ?thesis using mayl by auto
next
case False
hence nmal: "¬ must_acquire_lock (las \$ l)"
by(auto intro: collect_locks'I)
from l have locklasl: "Lock ∈ set (las \$ l)"
by(rule collect_locksD)
then obtain ys zs
where las: "las \$ l = ys @ Lock # zs"
and notin: "Lock ∉ set ys"
by(auto dest: split_list_first)
from lot' have "lock_actions_ok' (ls \$ l) t (las \$ l)"
thus ?thesis
proof(induct rule: lock_actions_ok'E)
case ok
with locklasl show ?thesis
by -(rule lock_actions_ok_Lock_may_lock)
next
case (Lock YS ZS)
note LAS = ‹las \$ l = YS @ Lock # ZS›
note lao = ‹lock_actions_ok (ls \$ l) t YS›
note nml = ‹¬ may_lock (upd_locks (ls \$ l) t YS) t›
from LAS las nmal notin have "Unlock ∈ set YS"
by -(erule contrapos_np, auto simp add: must_acquire_lock_append append_eq_append_conv2 append_eq_Cons_conv)
then obtain ys' zs'
where YS: "YS = ys' @ Unlock # zs'"
and unlock: "Unlock ∉ set ys'"
by(auto dest: split_list_first)
from YS las LAS lao have lao': "lock_actions_ok (ls \$ l) t (ys' @ [Unlock])" by(auto)
hence "has_lock (upd_locks (ls \$ l) t ys') t" by simp
hence "may_lock (upd_locks (ls \$ l) t ys') t"
by(rule has_lock_may_lock)
moreover from lao' have "lock_actions_ok (ls \$ l) t ys'" by simp
ultimately show ?thesis by simp
qed
qed

lemma lock_actions_ok'_must_acquire_lock_lock_actions_ok:
"⟦ lock_actions_ok' l t Ls; must_acquire_lock Ls ⟶ may_lock l t⟧ ⟹ lock_actions_ok l t Ls"
proof(induct l t Ls rule: lock_actions_ok.induct)
case 1 thus ?case by simp
next
case (2 l t L LS) thus ?case
proof(cases "L = Lock ∨ L = Unlock")
case True
with 2 show ?thesis by(auto simp add: lock_actions_ok'_iff Cons_eq_append_conv intro: has_lock_may_lock)
qed(cases L, auto)
qed

lemma lock_ok_las'_collect_locks_lock_ok_las:
assumes lol': "lock_ok_las' ls t las"
and clml: "⋀l. l ∈ collect_locks las ⟹ may_lock (ls \$ l) t"
shows "lock_ok_las ls t las"
proof(rule lock_ok_lasI)
fix l
from lol' have "lock_actions_ok' (ls \$ l) t (las \$ l)" by(rule lock_ok_las'D)
thus "lock_actions_ok (ls \$ l) t (las \$ l)"
proof(rule lock_actions_ok'_must_acquire_lock_lock_actions_ok[OF _ impI])
assume mal: "must_acquire_lock (las \$ l)"
thus "may_lock (ls \$ l) t"
by(auto intro!: clml collect_locksI elim: must_acquire_lock_contains_lock )
qed
qed

lemma lock_ok_las'_into_lock_on_las:
"⟦lock_ok_las' ls t las; ⋀l. l ∈ collect_locks' las ⟹ may_lock (ls \$ l) t⟧ ⟹ lock_ok_las ls t las"
by (metis lock_ok_las'_collect_locks'_may_lock lock_ok_las'_collect_locks_lock_ok_las)

end
```