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