Theory JHeap

(*  Title:      JinjaThreads/J/JHeap.thy
    Author:     Andreas Lochbihler
*)

section ‹Abstract heap locales for source code programs›

theory JHeap
imports
  "../Common/Conform"
  Expr
begin

locale J_heap_base = heap_base +
  constrains addr2thread_id :: "('addr :: addr) ⇒ 'thread_id"
  and thread_id2addr :: "'thread_id ⇒ 'addr"
  and 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 J_heap = heap + 
  constrains addr2thread_id :: "('addr :: addr) ⇒ 'thread_id"
  and thread_id2addr :: "'thread_id ⇒ 'addr"
  and 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 J_prog"

sublocale J_heap < J_heap_base .

locale J_heap_conf_base = heap_conf_base +
  constrains addr2thread_id :: "('addr :: addr) ⇒ 'thread_id"
  and thread_id2addr :: "'thread_id ⇒ 'addr"
  and 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 J_prog"

sublocale J_heap_conf_base < J_heap_base .

locale J_heap_conf = 
  J_heap_conf_base +
  heap_conf +
  constrains addr2thread_id :: "('addr :: addr) ⇒ 'thread_id"
  and thread_id2addr :: "'thread_id ⇒ 'addr"
  and 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 J_prog"

sublocale J_heap_conf < J_heap
by(unfold_locales)

locale J_progress =
  heap_progress +
  J_heap_conf_base +
  constrains addr2thread_id :: "('addr :: addr) ⇒ 'thread_id"
  and thread_id2addr :: "'thread_id ⇒ 'addr"
  and 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 J_prog"

sublocale J_progress < J_heap by(unfold_locales) 

locale J_conf_read =
  heap_conf_read +
  J_heap_conf +
  constrains addr2thread_id :: "('addr :: addr) ⇒ 'thread_id"
  and thread_id2addr :: "'thread_id ⇒ 'addr"
  and 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 J_prog"

sublocale J_conf_read < J_heap by(unfold_locales)

locale J_typesafe =
  heap_typesafe +
  J_conf_read +
  J_progress +
  constrains addr2thread_id :: "('addr :: addr) ⇒ 'thread_id"
  and thread_id2addr :: "'thread_id ⇒ 'addr"
  and 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 J_prog"

end