Theory JMM_J

theory JMM_J
imports
  JMM_Framework
  "../J/Threaded"
begin

sublocale J_heap_base < red_mthr: 
  heap_multithreaded_base 
    addr2thread_id thread_id2addr
    spurious_wakeups
    empty_heap allocate typeof_addr heap_read heap_write
    "final_expr" "mred P" convert_RA
  for P
.

context J_heap_base begin

abbreviation J_ℰ ::
  "'addr J_prog ⇒ cname ⇒ mname ⇒ 'addr val list ⇒ status 
  ⇒ ('thread_id × ('addr, 'thread_id) obs_event action) llist set"
where
  "J_ℰ P ≡ red_mthr.ℰ_start P J_local_start P"

end

end