Theory J1Heap

(*  Title:      JinjaThreads/Compiler/J1Heap.hty
    Author:     Andreas Lochbihler
*)

section ‹Abstract heap locales for J1 programs›

theory J1Heap imports
  J1State
  "../Common/Conform"
begin

locale J1_heap_base = heap_base +
  constrains addr2thread_id :: "('addr :: addr) ⇒ 'thread_id"
  and thread_id2addr :: "'thread_id ⇒ 'addr"
  and sc_spurious_wakeups :: bool
  and empty_heap :: "'heap"
  and allocate :: "'heap ⇒ htype ⇒ ('heap × 'addr) set"
  and typeof_addr :: "'heap ⇒ 'addr ⇀ htype"
  and heap_read :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ bool"
  and heap_write :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ 'heap ⇒ bool"

locale J1_heap = heap + 
  constrains addr2thread_id :: "('addr :: addr) ⇒ 'thread_id"
  and thread_id2addr :: "'thread_id ⇒ 'addr"
  and sc_spurious_wakeups :: bool
  and empty_heap :: "'heap"
  and allocate :: "'heap ⇒ htype ⇒ ('heap × 'addr) set"
  and typeof_addr :: "'heap ⇒ 'addr ⇀ htype"
  and heap_read :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ bool"
  and heap_write :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ 'heap ⇒ bool"
  and P :: "'addr J1_prog"

sublocale J1_heap < J1_heap_base .

locale J1_heap_conf_base = heap_conf_base +
  constrains addr2thread_id :: "('addr :: addr) ⇒ 'thread_id"
  and thread_id2addr :: "'thread_id ⇒ 'addr"
  and sc_spurious_wakeups :: bool
  and empty_heap :: "'heap"
  and allocate :: "'heap ⇒ htype ⇒ ('heap × 'addr) set"
  and typeof_addr :: "'heap ⇒ 'addr ⇀ htype"
  and heap_read :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ bool"
  and heap_write :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ 'heap ⇒ bool"
  and hconf :: "'heap ⇒ bool"
  and P :: "'addr J1_prog"

sublocale J1_heap_conf_base < J1_heap_base .

locale J1_heap_conf = 
  J1_heap_conf_base +
  heap_conf +
  constrains addr2thread_id :: "('addr :: addr) ⇒ 'thread_id"
  and thread_id2addr :: "'thread_id ⇒ 'addr"
  and sc_spurious_wakeups :: bool
  and empty_heap :: "'heap"
  and allocate :: "'heap ⇒ htype ⇒ ('heap × 'addr) set"
  and typeof_addr :: "'heap ⇒ 'addr ⇀ htype"
  and heap_read :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ bool"
  and heap_write :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ 'heap ⇒ bool"
  and hconf :: "'heap ⇒ bool"
  and P :: "'addr J1_prog"

sublocale J1_heap_conf < J1_heap by(unfold_locales)

locale J1_conf_read =
  J1_heap_conf +
  heap_conf_read +
  constrains addr2thread_id :: "('addr :: addr) ⇒ 'thread_id"
  and thread_id2addr :: "'thread_id ⇒ 'addr"
  and sc_spurious_wakeups :: bool
  and empty_heap :: "'heap"
  and allocate :: "'heap ⇒ htype ⇒ ('heap × 'addr) set"
  and typeof_addr :: "'heap ⇒ 'addr ⇀ htype"
  and heap_read :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ bool"
  and heap_write :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ 'heap ⇒ bool"
  and hconf :: "'heap ⇒ bool"
  and P :: "'addr J1_prog"

end