Theory ExternalCall (Isabelle2009-1: December 2009)

(*  Title:      JinjaThreads/Common/ExternalCall.thy
    Author:     Andreas Lochbihler
*)

header {* \isaheader{Semantics of method calls that cannot be defined inside JinjaThreads} *}


theory ExternalCall imports
  Exceptions
  "../Framework/FWState"
  Observable_Events
begin

types
  external_thread_action = "(addr,thread_id,cname × mname × addr,heap,addr, obs_event option) thread_action"

translations
  "external_thread_action" <= (type) "(nat,nat,char list × char list × nat,heap,nat, obs_event option) thread_action"

inductive is_external_call :: "'m prog => ty => mname => bool"
for P :: "'m prog"
where
  ecThreadStart: "P \<turnstile> C \<preceq>^* Thread ==> is_external_call P (Class C) start"
| ecThreadJoin: "P \<turnstile> C \<preceq>^* Thread ==> is_external_call P (Class C) join"
| ecObjectWait: "is_refT T ==> is_external_call P T wait"
| ecObjectNotify: "is_refT T ==> is_external_call P T notify"
| ecObjectNotifyAll: "is_refT T ==> is_external_call P T notifyAll"

lemma is_external_call_is_refT: "is_external_call P T M ==> is_refT T"
by(auto elim: is_external_call.cases)

lemma is_external_call_widen_mono:
  "[| is_external_call P T M; P \<turnstile> T' ≤ T; T' ≠ NT |] ==> is_external_call P T' M"
by(fastsimp elim!: is_external_call.cases intro: is_external_call.intros rtranclp_trans widen_refT simp add: widen_Class)


subsection {* Semantics of external calls *}

inductive red_external :: "'m prog => heap => addr => mname => val list => external_thread_action => (val + addr) => heap => bool"
  and red_external_syntax :: "'m prog => addr => mname => val list => heap => external_thread_action => (val + addr) => heap => bool"
  ("_ \<turnstile> (⟨(_•_'(_')),/_⟩) -_->ext (⟨(_),/(_)⟩)" [50, 0, 0, 0, 0, 0, 0, 0] 51)
for P :: "'m prog" and h :: heap and a :: addr
where
  "P \<turnstile> ⟨a•M(vs), h⟩ -ta->ext ⟨va, h'⟩ ≡ red_external P h a M vs ta va h'"

| RedNewThread:
  "[| h a = ⌊Obj C fs⌋; P \<turnstile> C \<preceq>^* Thread |]
  ==> P \<turnstile> ⟨a•start([]), h⟩ -ε\<lbrace>_t NewThread a (C, run, a) h\<rbrace>\<lbrace>_o ThreadStart a \<rbrace>->ext ⟨Inl Unit, h⟩"

| RedNewThreadFail:
  "[| h a = ⌊Obj C fs⌋; P \<turnstile> C \<preceq>^* Thread |]
  ==> P \<turnstile> ⟨a•start([]), h⟩ -ε\<lbrace>_t ThreadExists a\<rbrace>->ext ⟨Inr (addr_of_sys_xcpt IllegalThreadState), h⟩"

| RedJoin:
  "[| h a = ⌊Obj C fs⌋; P \<turnstile> C \<preceq>^* Thread |]
  ==> P \<turnstile> ⟨a•join([]), h⟩ -ε\<lbrace>_c Join a\<rbrace>\<lbrace>_o ThreadJoin a\<rbrace>->ext ⟨Inl Unit, h⟩"

| RedWait:
  "P \<turnstile> ⟨a•wait([]), h⟩ -ε\<lbrace>_w Suspend a \<rbrace>\<lbrace>_l Unlock->a, Lock->a, ReleaseAcquire->a \<rbrace>\<lbrace>_o Synchronization a\<rbrace>->ext ⟨Inl Unit, h⟩"

| RedWaitFail:
  "P \<turnstile> ⟨a•wait([]), h⟩ -ε\<lbrace>_l UnlockFail->a \<rbrace>->ext ⟨Inr (addr_of_sys_xcpt IllegalMonitorState), h⟩"

| RedNotify:
  "P \<turnstile> ⟨a•notify([]), h⟩ -ε\<lbrace>_w Notify a \<rbrace>\<lbrace>_l Unlock->a, Lock->a \<rbrace>\<lbrace>_o Synchronization a\<rbrace>->ext ⟨Inl Unit, h⟩"

| RedNotifyFail:
  "P \<turnstile> ⟨a•notify([]), h⟩ -ε\<lbrace>_l UnlockFail->a \<rbrace>->ext ⟨Inr (addr_of_sys_xcpt IllegalMonitorState), h⟩"

| RedNotifyAll:
  "P \<turnstile> ⟨a•notifyAll([]), h⟩ -ε\<lbrace>_w NotifyAll a \<rbrace>\<lbrace>_l Unlock->a, Lock->a \<rbrace>\<lbrace>_o Synchronization a\<rbrace>->ext ⟨Inl Unit, h⟩"

| RedNotifyAllFail:
  "P \<turnstile> ⟨a•notifyAll([]), h⟩ -ε\<lbrace>_l UnlockFail->a \<rbrace>->ext ⟨Inr (addr_of_sys_xcpt IllegalMonitorState), h⟩"

subsection {* Aggressive formulation for external calls *}

definition red_external_list :: "'m prog => addr => mname => val list => heap => (external_thread_action × (val + addr) × heap) list"
where
  "red_external_list P a M vs h =
     (if M = wait then [(ε\<lbrace>_w Suspend a \<rbrace>\<lbrace>_l Unlock->a, Lock->a, ReleaseAcquire->a \<rbrace>\<lbrace>_o Synchronization a\<rbrace>, Inl Unit, h),
                        (ε\<lbrace>_l UnlockFail->a \<rbrace>, Inr (addr_of_sys_xcpt IllegalMonitorState), h)]
      else if M = notify then [(ε\<lbrace>_w Notify a \<rbrace>\<lbrace>_l Unlock->a, Lock->a \<rbrace>\<lbrace>_o Synchronization a\<rbrace>, Inl Unit, h),
                               (ε\<lbrace>_l UnlockFail->a \<rbrace>, Inr (addr_of_sys_xcpt IllegalMonitorState), h)]
      else if M = notifyAll then [(ε\<lbrace>_w NotifyAll a \<rbrace>\<lbrace>_l Unlock->a, Lock->a \<rbrace>\<lbrace>_o Synchronization a\<rbrace>, Inl Unit, h),
                                  (ε\<lbrace>_l UnlockFail->a \<rbrace>, Inr (addr_of_sys_xcpt IllegalMonitorState), h)]
      else if P \<turnstile> the (typeof_h (Addr a)) ≤ Class Thread then
           if M = start then [(ε\<lbrace>_t NewThread a (fst (the_obj (the (h a))), run, a) h\<rbrace>\<lbrace>_o ThreadStart a\<rbrace>, Inl Unit, h), 
                              (ε\<lbrace>_t ThreadExists a\<rbrace>, Inr (addr_of_sys_xcpt IllegalThreadState), h)]
           else if M = join then [(ε\<lbrace>_c Join a\<rbrace>\<lbrace>_o ThreadJoin a\<rbrace>, Inl Unit, h)] else []
      else undefined)"

lemma red_external_imp_red_external_list:
  "P \<turnstile> ⟨a•M(vs), h⟩ -ta->ext ⟨va, h'⟩ ==> (ta, va, h') ∈ set (red_external_list P a M vs h)"
unfolding red_external_list_def by(auto elim!: red_external.cases split: heapobj.splits)

lemma red_external_list_not_Nil:
  "is_external_call P (the (typeof_h (Addr a))) M ==> red_external_list P a M vs h ≠ []"
by(auto simp add: red_external_list_def elim: is_external_call.cases)

lemma red_external_hext: "P \<turnstile> ⟨a•M(vs), h⟩ -ta->ext ⟨va, h'⟩ ==> hext h h'"
by(auto elim: red_external.cases)

lemma red_external_xcp_heap_unchanged:
  "P \<turnstile> ⟨a•M(vs), h⟩ -ta->ext ⟨Inr xcp, h'⟩ ==> h' = h"
by(auto elim: red_external.cases)

lemma red_external_list_xcp_heap_unchanged:
  "[| (ta, Inr xcp, h') ∈ set (red_external_list P a M vs h); is_external_call P (the (typeof_h (Addr a))) M |] ==> h' = h"
unfolding red_external_list_def by(auto elim!: is_external_call.cases)

lemma red_ext_new_thread_heap:
  "[| P \<turnstile> ⟨a•M(vs), h⟩ -ta->ext ⟨va, h'⟩; NewThread t ex h'' ∈ set \<lbrace>ta\<rbrace>_t |] ==> h'' = h'"
by(auto elim: red_external.cases)

lemma red_ext_list_new_thread_heap:
  "[| (ta, va, h') ∈ set (red_external_list P a M vs h); is_external_call P (the (typeof_h (Addr a))) M; 
    NewThread t ex h'' ∈ set \<lbrace>ta\<rbrace>_t |] ==> h'' = h'"
by(auto simp add: red_external_list_def elim!: is_external_call.cases)

lemma red_external_new_thread_exists_thread_object:
  "[| P \<turnstile> ⟨a•M(vs), h⟩ -ta->ext ⟨va, h'⟩; NewThread t x h'' ∈ set \<lbrace>ta\<rbrace>_t; h a ≠ None |]
  ==> ∃C fs. h' t = ⌊Obj C fs⌋ ∧ P \<turnstile> C \<preceq>^* Thread"
by(auto elim!: red_external.cases split: heapobj.split_asm dest!: Array_widen)

lemma red_external_list_new_thread_exists_thread_object:
  "[| (ta, va, h') ∈ set (red_external_list P a M vs h); is_external_call P (the (typeof_h (Addr a))) M;
     NewThread t x h'' ∈ set \<lbrace>ta\<rbrace>_t; h a ≠ None |]
  ==> ∃C fs. h' t = ⌊Obj C fs⌋ ∧ P \<turnstile> C \<preceq>^* Thread"
by(auto simp add: red_external_list_def elim!: is_external_call.cases split: heapobj.split_asm dest!: Array_widen)


subsection {* Typing of external calls *}

inductive external_WT :: "'m prog => ty => mname => ty list => ty => bool" ("_ \<turnstile> (_•_'(_')) :: _" [50, 0, 0, 50] 60)
for P :: "'m prog"
where
  WTNewThread:
  "P \<turnstile> C \<preceq>^* Thread ==> P \<turnstile> Class C•start([]) :: Void"

| WTWait:
  "[| is_refT T; T ≠ NT |] ==> P \<turnstile> T•wait([]) :: Void"

| WTNotify:
  "[| is_refT T; T ≠ NT |] ==> P \<turnstile> T•notify([]) :: Void"

| WTNotifyAll:
  "[| is_refT T; T ≠ NT |] ==> P \<turnstile> T•notifyAll([]) :: Void"

| WTJoin:
  "P \<turnstile> C \<preceq>^* Thread ==> P \<turnstile> Class C•join([]) :: Void"

lemma external_WT_determ:
  "[| P \<turnstile> T•M(Ts) :: U; P \<turnstile> T•M(Ts) :: U' |] ==> U = U'"
by(auto elim: external_WT.cases)

lemma external_WT_The_conv:
  "P \<turnstile> T•M(TS) :: U ==> (THE U. P \<turnstile> T•M(TS) :: U) = U"
by(auto intro: external_WT_determ)

lemma external_WTrt_widen_mono:
  "[| P \<turnstile> T•M(Ts) :: U; P \<turnstile> T' ≤ T; P \<turnstile> Ts' [≤] Ts; T' ≠ NT |] ==> ∃U'. P \<turnstile> T'•M(Ts') :: U' ∧ P \<turnstile> U' ≤ U"
by(fastsimp elim!: external_WT.cases intro: external_WT.intros simp add: widen_Class intro: rtranclp_trans widen_refT)

lemma external_WT_is_external_call:
  "P \<turnstile> T•M(Ts) :: U ==> is_external_call P T M"
by(auto elim!: external_WT.cases intro: is_external_call.intros)

lemma external_WT_not_NT:
  "P \<turnstile> T•M(Ts) :: U ==> T ≠ NT"
by(auto elim: external_WT.cases)

lemma WT_external_is_type:
  "[| P \<turnstile> T•M(TS) :: U; is_type P T; set TS ⊆ is_type P |] ==> is_type P U"
by(auto elim: external_WT.cases)

inductive external_WT' :: "'m prog => heap => addr => mname => val list => ty => bool" ("_,_ \<turnstile> (_•_'(_')) : _" [50,0,0,0,50] 60)
for P :: "'m prog" and h :: heap and a :: addr and M :: mname and vs :: "val list" and U :: ty
where "[| typeof_h (Addr a) = ⌊T⌋; map typeof_h vs = map Some Ts; P \<turnstile> T•M(Ts) :: U |] ==> P,h \<turnstile> a•M(vs) : U"

lemma external_WT'_iff:
  "P,h \<turnstile> a•M(vs) : U <-> (∃T Ts. typeof_h (Addr a) = ⌊T⌋ ∧ map typeof_h vs = map Some Ts ∧ P \<turnstile> T•M(Ts) :: U)"
by(auto simp add: external_WT'_def lfp_const)

lemma red_external_list_hext: "[| (ta, va, h') ∈ set (red_external_list P a M vs h); P,h \<turnstile> a•M(vs) : U |] ==> hext h h'"
by(auto simp add: red_external_list_def elim!: external_WT'.cases external_WT.cases)

lemma external_call_progress:
  "P,h \<turnstile> a•M(vs) : U ==> ∃ta va h'. P \<turnstile> ⟨a•M(vs), h⟩ -ta->ext ⟨va, h'⟩"
unfolding external_WT'_iff
by(fastsimp intro: red_external.intros simp del: split_paired_Ex split: heapobj.split_asm elim!: external_WT.cases)

lemma red_external_UnlockFail_UnlockFail: (* Used only in Compiler/Correctness1Threaded *)
  "[| P \<turnstile> ⟨a•M(vs), h⟩ -ta->ext ⟨va, h'⟩; UnlockFail ∈ set (\<lbrace>ta\<rbrace>_l_f l) |] ==> \<lbrace>ta\<rbrace>_l_f l = [UnlockFail]"
by(auto elim: red_external.cases simp add: finfun_upd_apply split: split_if_asm)

subsection {* Lemmas for preservation of deadlocks *}

lemma red_external_Lock_hext:
  "[| P \<turnstile> ⟨a•M(vs), h⟩ -ta->ext ⟨va, h'⟩; Lock ∈ set (\<lbrace>ta\<rbrace>_l_f l); hext h h'' |]
  ==> P \<turnstile> ⟨a•M(vs), h''⟩ -ta->ext ⟨va, h''⟩"
by(fastsimp elim!: red_external.cases intro: red_external.intros[simplified] simp add: finfun_upd_apply split: split_if_asm)

lemma red_external_Join_hext:
  "[| P \<turnstile> ⟨a•M(vs), h⟩ -ta->ext ⟨va, h'⟩; Join t ∈ set \<lbrace>ta\<rbrace>_c; hext h h''; h a ≠ None |]
  ==> P \<turnstile> ⟨a•M(vs), h''⟩ -ta->ext ⟨va, h''⟩"
by(fastsimp elim!: red_external.cases intro: red_external.intros[simplified] dest: hext_objD Array_widen split: split_if_asm heapobj.split_asm)

lemma red_external_Lock_wth:
  "[| P \<turnstile> ⟨a•M(vs),h⟩ -ta->ext ⟨va,h'⟩; Lock ∈ set (\<lbrace>ta\<rbrace>_l_f l); hext h'' h; P,h'' \<turnstile> a•M(vs) : U |]
  ==> P \<turnstile> ⟨a•M(vs),h''⟩ -ta->ext ⟨va, h''⟩"
by(auto elim!: red_external.cases intro: red_external.intros[simplified])

lemma red_external_Join_wth:
  "[| P \<turnstile> ⟨a•M(vs),h⟩ -ta->ext ⟨va,h'⟩; Join t ∈ set \<lbrace>ta\<rbrace>_c; hext h'' h; P,h'' \<turnstile> a•M(vs) : U |]
  ==> P \<turnstile> ⟨a•M(vs),h''⟩ -ta->ext ⟨va, h''⟩"
by(fastsimp elim!: red_external.cases external_WT'.cases intro!: red_external.intros[simplified] dest: hext_objD hext_arrD split: heapobj.split_asm)

lemma red_external_wt_hconf_hext:
  "[| P \<turnstile> ⟨a•M(vs), h⟩ -ta->ext ⟨va, h'⟩; P,H \<turnstile> a•M(vs) : U; hext H h |]
  ==> ∃ta' va' h'. P \<turnstile> ⟨a•M(vs), H⟩ -ta'->ext ⟨va', h'⟩ ∧ locks_a ta' = locks_a ta ∧ wset_a ta' = wset_a ta ∧ cond_a ta' = cond_a ta"
by(fastsimp elim!: red_external.cases external_WT'.cases split: heapobj.splits dest: hext_objD hext_arrD intro: red_external.intros[simplified])

end