Theory FWLock

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

section ‹All about a managing a single lock›

theory FWLock
imports
  FWState
begin

fun has_locks :: "'t lock ⇒ 't ⇒ nat" where
  "has_locks None t = 0"
| "has_locks ⌊(t', n)⌋ t = (if t = t' then Suc n else 0)"

lemma has_locks_iff: 
  "has_locks l t = n ⟷
  (l = None ∧ n = 0) ∨ 
  (∃n'. l = ⌊(t, n')⌋ ∧ Suc n' = n) ∨ (∃t' n'. l = ⌊(t', n')⌋ ∧ t' ≠ t ∧ n = 0)"
by(cases l, auto)

lemma has_locksE:
  "⟦ has_locks l t = n;
     ⟦ l = None; n = 0 ⟧ ⟹ P;
     ⋀n'. ⟦ l = ⌊(t, n')⌋; Suc n' = n ⟧ ⟹ P;
     ⋀t' n'. ⟦ l = ⌊(t', n')⌋; t' ≠ t; n = 0 ⟧ ⟹ P ⟧
  ⟹ P"
by(auto simp add: has_locks_iff split: if_split_asm prod.split_asm)


inductive may_lock :: "'t lock ⇒ 't ⇒ bool" where
  "may_lock None t"
| "may_lock ⌊(t, n)⌋ t"

lemma may_lock_iff [code]:
  "may_lock l t = (case l of None ⇒ True | ⌊(t', n)⌋ ⇒ t = t')"
by(auto intro: may_lock.intros elim: may_lock.cases)

lemma may_lockI:
  "l = None ∨ (∃n. l = ⌊(t, n)⌋) ⟹ may_lock l t"
by(cases l, auto intro: may_lock.intros)

lemma may_lockE [consumes 1, case_names None Locked]:
  "⟦ may_lock l t; l = None ⟹ P; ⋀n. l = ⌊(t, n)⌋  ⟹ P ⟧ ⟹ P"
by(auto elim: may_lock.cases)

lemma may_lock_may_lock_t_eq:
  "⟦ may_lock l t; may_lock l t' ⟧ ⟹ (l = None) ∨ (t = t')"
by(auto elim!: may_lockE)

abbreviation has_lock :: "'t lock ⇒ 't ⇒ bool"
where "has_lock l t ≡ 0 < has_locks l t"

lemma has_locks_Suc_has_lock:
  "has_locks l t = Suc n ⟹ has_lock l t"
by(auto)

lemmas has_lock_has_locks_Suc = gr0_implies_Suc[where n = "has_locks l t"] for l t

lemma has_lock_has_locks_conv:
  "has_lock l t ⟷ (∃n. has_locks l t = (Suc n))"
by(auto intro: has_locks_Suc_has_lock has_lock_has_locks_Suc)

lemma has_lock_may_lock:
  "has_lock l t ⟹ may_lock l t"
by(cases l, auto intro: may_lockI)

lemma has_lock_may_lock_t_eq:
  "⟦ has_lock l t; may_lock l t' ⟧ ⟹ t = t'"
by(auto elim!: may_lockE split: if_split_asm)

lemma has_locks_has_locks_t_eq: 
  "⟦has_locks l t = Suc n; has_locks l t' = Suc n'⟧ ⟹ t = t'"
by(auto elim: has_locksE)

lemma has_lock_has_lock_t_eq:
  "⟦ has_lock l t; has_lock l t' ⟧ ⟹ t = t'"
unfolding has_lock_has_locks_conv
by(auto intro: has_locks_has_locks_t_eq)

lemma not_may_lock_conv:
  "¬ may_lock l t ⟷ (∃t'. t' ≠ t ∧ has_lock l t')"
by(cases l, auto intro: may_lock.intros elim: may_lockE)



(* State update functions for locking *)

fun lock_lock :: "'t lock ⇒ 't ⇒ 't lock" where
  "lock_lock None t = ⌊(t, 0)⌋"
| "lock_lock ⌊(t', n)⌋ t = ⌊(t', Suc n)⌋"

fun unlock_lock :: "'t lock ⇒ 't lock" where
  "unlock_lock None = None"
| "unlock_lock ⌊(t, n)⌋ = (case n of 0 ⇒ None | Suc n' ⇒ ⌊(t, n')⌋)"

fun release_all :: "'t lock ⇒ 't ⇒ 't lock" where
  "release_all None t = None"
| "release_all ⌊(t', n)⌋ t = (if t = t' then None else ⌊(t', n)⌋)"

fun acquire_locks :: "'t lock ⇒ 't ⇒ nat ⇒ 't lock" where
  "acquire_locks L t 0 = L"
| "acquire_locks L t (Suc m) = acquire_locks (lock_lock L t) t m"

lemma acquire_locks_conv:
  "acquire_locks L t n = (case L of None ⇒ (case n of 0 ⇒ None | Suc m ⇒ ⌊(t, m)⌋) | ⌊(t', m)⌋ ⇒ ⌊(t', n + m)⌋)"
by(induct n arbitrary: L)(auto)

lemma lock_lock_ls_Some:
  "∃t' n. lock_lock l t = ⌊(t', n)⌋"
by(cases l, auto)

lemma unlock_lock_SomeD:
  "unlock_lock l = ⌊(t', n)⌋ ⟹ l = ⌊(t', Suc n)⌋"
by(cases l, auto split: nat.split_asm)

lemma has_locks_Suc_lock_lock_has_locks_Suc_Suc:
  "has_locks l t = Suc n ⟹ has_locks (lock_lock l t) t = Suc (Suc n)"
by(auto elim!: has_locksE)

lemma has_locks_lock_lock_conv [simp]:
  "may_lock l t ⟹ has_locks (lock_lock l t) t = Suc (has_locks l t)"
by(auto elim: may_lockE)

lemma has_locks_release_all_conv [simp]:
  "has_locks (release_all l t) t = 0"
by(cases l, auto split: if_split_asm)

lemma may_lock_lock_lock_conv [simp]: "may_lock (lock_lock l t) t = may_lock l t"
by(cases l, auto elim!: may_lock.cases intro: may_lock.intros)

lemma has_locks_acquire_locks_conv [simp]:
  "may_lock l t ⟹ has_locks (acquire_locks l t n) t = has_locks l t + n"
by(induct n arbitrary: l, auto)

lemma may_lock_unlock_lock_conv [simp]:
  "has_lock l t ⟹ may_lock (unlock_lock l) t = may_lock l t"
by(cases l)(auto split: if_split_asm nat.splits elim!: may_lock.cases intro: may_lock.intros)

lemma may_lock_release_all_conv [simp]:
  "may_lock (release_all l t) t = may_lock l t"
by(cases l, auto split: if_split_asm intro!: may_lockI elim: may_lockE)

lemma may_lock_t_may_lock_unlock_lock_t: 
  "may_lock l t ⟹ may_lock (unlock_lock l) t"
by(auto intro: may_lock.intros elim!: may_lockE split: nat.split)


lemma may_lock_has_locks_lock_lock_0: 
  "⟦may_lock l t'; t ≠ t'⟧ ⟹ has_locks (lock_lock l t') t = 0"
by(auto elim!: may_lock.cases)

lemma has_locks_unlock_lock_conv [simp]:
  "has_lock l t ⟹ has_locks (unlock_lock l) t = has_locks l t - 1"
by(cases l)(auto split: nat.split)

lemma has_lock_lock_lock_unlock_lock_id [simp]:
  "has_lock l t ⟹ lock_lock (unlock_lock l) t = l"
by(cases l)(auto split: if_split_asm nat.split)

lemma may_lock_unlock_lock_lock_lock_id [simp]:
  "may_lock l t ⟹ unlock_lock (lock_lock l t) = l"
by(cases l) auto


lemma may_lock_has_locks_0:
  "⟦ may_lock l t; t ≠ t' ⟧ ⟹ has_locks l t' = 0"
by(auto elim!: may_lockE)


fun upd_lock :: "'t lock ⇒ 't ⇒ lock_action ⇒ 't lock"
where
  "upd_lock l t Lock = lock_lock l t"
| "upd_lock l t Unlock = unlock_lock l"
| "upd_lock l t UnlockFail = l"
| "upd_lock l t ReleaseAquire = release_all l t"

fun upd_locks :: "'t lock ⇒ 't ⇒ lock_action list ⇒ 't lock"
where
  "upd_locks l t [] = l"
| "upd_locks l t (L # Ls) = upd_locks (upd_lock l t L) t Ls"

lemma upd_locks_append [simp]:
  "upd_locks l t (Ls @ Ls') = upd_locks (upd_locks l t Ls) t Ls'"
by(induct Ls arbitrary: l, auto)

lemma upd_lock_Some_thread_idD:
  assumes ul: "upd_lock l t L = ⌊(t', n)⌋"
  and tt': "t ≠ t'"
  shows "∃n. l = ⌊(t', n)⌋"
proof(cases L)
  case Lock
  with ul tt' show ?thesis
    by(cases l, auto)
next
  case Unlock
  with ul tt' show ?thesis
    by(auto dest: unlock_lock_SomeD)
next
  case UnlockFail
  with ul show ?thesis by(simp)
next
  case ReleaseAcquire
  with ul show ?thesis
    by(cases l, auto split: if_split_asm)
qed


lemma has_lock_upd_lock_implies_has_lock:
  "⟦ has_lock (upd_lock l t L) t'; t ≠ t' ⟧ ⟹ has_lock l t'"
by(cases l L rule: option.exhaust[case_product lock_action.exhaust])(auto split: if_split_asm nat.split_asm)

lemma has_lock_upd_locks_implies_has_lock:
  "⟦ has_lock (upd_locks l t Ls) t'; t ≠ t' ⟧ ⟹ has_lock l t'"
by(induct l t Ls rule: upd_locks.induct)(auto intro: has_lock_upd_lock_implies_has_lock)

(* Preconditions for lock actions *)

fun lock_action_ok :: "'t lock ⇒ 't ⇒ lock_action ⇒ bool" where
  "lock_action_ok l t Lock = may_lock l t"
| "lock_action_ok l t Unlock = has_lock l t"
| "lock_action_ok l t UnlockFail = (¬ has_lock l t)"
| "lock_action_ok l t ReleaseAcquire = True"

fun lock_actions_ok :: "'t lock ⇒ 't ⇒ lock_action list ⇒ bool" where
  "lock_actions_ok l t [] = True"
| "lock_actions_ok l t (L # Ls) = (lock_action_ok l t L ∧ lock_actions_ok (upd_lock l t L) t Ls)"

lemma lock_actions_ok_append [simp]:
  "lock_actions_ok l t (Ls @ Ls') ⟷ lock_actions_ok l t Ls ∧ lock_actions_ok (upd_locks l t Ls) t Ls'"
by(induct Ls arbitrary: l) auto

lemma not_lock_action_okE [consumes 1, case_names Lock Unlock UnlockFail]:
  "⟦ ¬ lock_action_ok l t L;
     ⟦ L = Lock; ¬ may_lock l t ⟧ ⟹ Q;
     ⟦ L = Unlock; ¬ has_lock l t ⟧ ⟹ Q;
     ⟦ L = UnlockFail; has_lock l t ⟧ ⟹ Q⟧
  ⟹ Q"
by(cases L) auto

lemma may_lock_upd_lock_conv [simp]:
  "lock_action_ok l t L ⟹ may_lock (upd_lock l t L) t = may_lock l t"
by(cases L) auto

lemma may_lock_upd_locks_conv [simp]:
  "lock_actions_ok l t Ls ⟹ may_lock (upd_locks l t Ls) t = may_lock l t"
by(induct l t Ls rule: upd_locks.induct) simp_all

lemma lock_actions_ok_Lock_may_lock:
  "⟦ lock_actions_ok l t Ls; Lock ∈ set Ls ⟧ ⟹ may_lock l t"
by(induct l t Ls rule: lock_actions_ok.induct) auto

lemma has_locks_lock_lock_conv' [simp]:
  "⟦ may_lock l t'; t ≠ t' ⟧ ⟹ has_locks (lock_lock l t') t = has_locks l t"
by(cases l)(auto elim: may_lock.cases)

lemma has_locks_unlock_lock_conv' [simp]:
  "⟦ has_lock l t'; t ≠ t' ⟧ ⟹ has_locks (unlock_lock l) t = has_locks l t"
by(cases l)(auto split: if_split_asm nat.split)

lemma has_locks_release_all_conv' [simp]:
  "t ≠ t' ⟹ has_locks (release_all l t') t = has_locks l t"
by(cases l) auto

lemma has_locks_acquire_locks_conv' [simp]:
  "⟦ may_lock l t; t ≠ t' ⟧ ⟹ has_locks (acquire_locks l t n) t' = has_locks l t'"
by(induct l t n rule: acquire_locks.induct) simp_all

lemma lock_action_ok_has_locks_upd_lock_eq_has_locks [simp]:
  "⟦ lock_action_ok l t' L; t ≠ t' ⟧ ⟹ has_locks (upd_lock l t' L) t = has_locks l t"
by(cases L) auto

lemma lock_actions_ok_has_locks_upd_locks_eq_has_locks [simp]:
  "⟦ lock_actions_ok l t' Ls; t ≠ t' ⟧ ⟹ has_locks (upd_locks l t' Ls) t = has_locks l t"
by(induct l t' Ls rule: upd_locks.induct) simp_all

lemma has_lock_acquire_locks_implies_has_lock:
  "⟦ has_lock (acquire_locks l t n) t'; t ≠ t' ⟧ ⟹ has_lock l t'"
 unfolding acquire_locks_conv
 by(cases n)(auto split: if_split_asm)

lemma has_lock_has_lock_acquire_locks:
  "has_lock l T ⟹ has_lock (acquire_locks l t n) T"
  unfolding acquire_locks_conv
  by(auto)


fun lock_actions_ok' :: "'t lock ⇒ 't ⇒ lock_action list ⇒ bool" where
  "lock_actions_ok' l t [] = True"
| "lock_actions_ok' l t (L#Ls) = ((L = Lock ∧ ¬ may_lock l t) ∨
                                  lock_action_ok l t L ∧ lock_actions_ok' (upd_lock l t L) t Ls)"

lemma lock_actions_ok'_iff:
  "lock_actions_ok' l t las ⟷ 
   lock_actions_ok l t las ∨ (∃xs ys. las = xs @ Lock # ys ∧ lock_actions_ok l t xs ∧ ¬ may_lock (upd_locks l t xs) t)"
proof(induct l t las rule: lock_actions_ok.induct)
  case (2 L t LA LAS)
  show ?case
  proof(cases "LA = Lock ∧ ¬ may_lock L t")
    case True
    hence "(∃ys. Lock # LAS = [] @ Lock # ys) ∧ lock_actions_ok L t [] ∧ ¬ may_lock (upd_locks L t []) t"
      by(simp)
    with True show ?thesis by(simp (no_asm))(blast)
  next
    case False
    with 2 show ?thesis
      by(fastforce simp add: Cons_eq_append_conv elim: allE[where x="LA # xs" for xs])
  qed
qed simp

lemma lock_actions_ok'E[consumes 1, case_names ok Lock]:
  "⟦ lock_actions_ok' l t las;
     lock_actions_ok l t las ⟹ P;
     ⋀xs ys. ⟦ las = xs @ Lock # ys; lock_actions_ok l t xs; ¬ may_lock (upd_locks l t xs) t ⟧ ⟹ P ⟧ 
  ⟹ P"
by(auto simp add: lock_actions_ok'_iff)

end