Theory JMM_JVM

theory JMM_JVM
imports
  JMM_Framework
  "../JVM/JVMThreaded"
begin

sublocale JVM_heap_base < execd_mthr: 
  heap_multithreaded_base 
    addr2thread_id thread_id2addr
    spurious_wakeups
    empty_heap allocate typeof_addr heap_read heap_write
    JVM_final "mexecd P" convert_RA
  for P
.

context JVM_heap_base begin

abbreviation JVMd_ℰ ::
  "'addr jvm_prog ⇒ cname ⇒ mname ⇒ 'addr val list ⇒ status
  ⇒ ('thread_id × ('addr, 'thread_id) obs_event action) llist set"
where "JVMd_ℰ P ≡ execd_mthr.ℰ_start P JVM_local_start P"

end

end