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