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_E ::
  "'addr J_prog → cname → mname → 'addr val list → status
  → ('thread_id × ('addr, 'thread_id) obs_event action) llist set"
where
  "J_E P ≡ red_mthr.E_start P J_local_start P"

end

end