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)"
by(simp add: redT_updLs_def)

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

lemma redT_updLs_Some_thread_idD:
  "⟦ 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)"
by(simp add: acquire_all_def)


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"
by(simp add: lock_ok_las_def)

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

lemma lock_ok_lasD:
  "lock_ok_las ls t las ⟹ lock_actions_ok (ls $ l) t (las $ l)"
by(simp add: lock_ok_las_def)

lemma lock_ok_las_code [code]:
  "lock_ok_las ls t las = finfun_All ((λ(l, la). lock_actions_ok l t la) ∘$ ($ls, las$))"
by(simp add: lock_ok_las_def finfun_All_All o_def)

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"
by(simp add: may_acquire_all_def)

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

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

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"
by(simp add: collect_locks_def)

lemma collect_locksE:
  "⟦ l ∈ collect_locks las; Lock ∈ set (las $ l) ⟹ P ⟧ ⟹ P"
by(simp add: collect_locks_def)

lemma collect_locksD:
  "l ∈ collect_locks las ⟹ Lock ∈ set (las $ l)"
by(simp add: collect_locks_def)


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"
by(simp add: collect_locks'_def)

lemma collect_locks'E:
  "⟦ l ∈ collect_locks' las; must_acquire_lock (las $ l) ⟹ P ⟧ ⟹ P"
by(simp add: collect_locks'_def)

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"
by(simp add: lock_ok_las'_def)

lemma lock_ok_las'D: "lock_ok_las' ls t las ⟹ lock_actions_ok' (ls $ l) t (las $ l)"
by(simp add: lock_ok_las'_def)

lemma not_lock_ok_las'_conv:
  "¬ lock_ok_las' ls t las ⟷ (∃l. ¬ lock_actions_ok' (ls $ l) t (las $ l))"
by(simp add: lock_ok_las'_def)

lemma lock_ok_las'_code:
    "lock_ok_las' ls t las = finfun_All ((λ(l, la). lock_actions_ok' l t la) ∘$ ($ls, las$))"
by(simp add: lock_ok_las'_def finfun_All_All o_def)


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)"
    by(auto simp add: lock_ok_las'_def)
  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