Theory SC_Schedulers

theory SC_Schedulers
imports
  Random_Scheduler
  Round_Robin
  "../MM/SC_Collections"
  (*
  "../../Collections/impl/RBTMapImpl"
  "../../Collections/impl/RBTSetImpl"
  "../../Collections/impl/Fifo"
  "../../Collections/impl/ListSetImpl_Invar"
  *)
  "../Basic/JT_ICF"
  
begin

abbreviation sc_start_state_refine ::
  "'m_t ⇒ (thread_id ⇒ ('x × addr released_locks) ⇒ 'm_t ⇒ 'm_t) ⇒ 'm_w ⇒ 's_i
  ⇒ (cname ⇒ mname ⇒ ty list ⇒ ty ⇒ 'md ⇒ addr val list ⇒ 'x) ⇒ 'md prog ⇒ cname ⇒ mname ⇒ addr val list
  ⇒ (addr, thread_id, heap, 'm_t, 'm_w, 's_i) state_refine"
where
  "⋀is_empty.
   sc_start_state_refine thr_empty thr_update ws_empty is_empty f P ≡
   heap_base.start_state_refine addr2thread_id sc_empty (sc_allocate P) thr_empty thr_update ws_empty is_empty f P"

abbreviation sc_state_α ::
  "('l, 't :: linorder, 'm, ('t, 'x × 'l ⇒f nat) rm, ('t, 'w wait_set_status) rm, 't rs) state_refine
  ⇒ ('l,'t,'x,'m,'w) state"
where "sc_state_α ≡ state_refine_base.state_α rm_α rm_α rs_α"

lemma sc_state_α_sc_start_state_refine [simp]:
  "sc_state_α (sc_start_state_refine (rm_empty ()) rm_update (rm_empty ()) (rs_empty ()) f P C M vs) = sc_start_state f P C M vs"
by(simp add: heap_base.start_state_refine_def state_refine_base.state_α.simps split_beta sc.start_state_def rm_correct rs_correct)

locale sc_scheduler =
  scheduler
    final r convert_RA 
    schedule "output" pick_wakeup σ_invar
    rm_α rm_invar rm_lookup rm_update
    rm_α rm_invar rm_lookup rm_update rm_delete rm_iteratei
    rs_α rs_invar rs_memb rs_ins rs_delete
    invariant
  for final :: "'x ⇒ bool"
  and r :: "'t ⇒ ('x × 'm) ⇒ (('l,'t :: linorder,'x,'m,'w,'o) thread_action × 'x × 'm) Predicate.pred"
  and convert_RA :: "'l released_locks ⇒ 'o list"
  and schedule :: "('l,'t,'x,'m,'w,'o,('t, 'x × 'l ⇒f nat) rm,('t, 'w wait_set_status) rm, 't rs, 's) scheduler"
  and "output" :: "'s ⇒ 't ⇒ ('l,'t,'x,'m,'w,'o) thread_action ⇒ 'q option"
  and pick_wakeup :: "'s ⇒ 't ⇒ 'w ⇒ ('t, 'w wait_set_status) RBT.rbt ⇒ 't option"
  and σ_invar :: "'s ⇒ 't set ⇒ bool"
  and invariant :: "('l,'t,'x,'m,'w) state set"

locale sc_round_robin_base =
  round_robin_base
    final r convert_RA "output"
    rm_α rm_invar rm_lookup rm_update 
    rm_α rm_invar rm_lookup rm_update rm_delete rm_iteratei rm_sel
    rs_α rs_invar rs_memb rs_ins rs_delete
    fifo_α fifo_invar fifo_empty fifo_isEmpty fifo_enqueue fifo_dequeue fifo_push
  for final :: "'x ⇒ bool"
  and r :: "'t ⇒ ('x × 'm) ⇒ (('l,'t :: linorder,'x,'m,'w,'o) thread_action × 'x × 'm) Predicate.pred"
  and convert_RA :: "'l released_locks ⇒ 'o list"
  and "output" :: "'t fifo round_robin ⇒ 't ⇒ ('l,'t,'x,'m,'w,'o) thread_action ⇒ 'q option"

locale sc_round_robin =
  round_robin 
    final r convert_RA "output"
    rm_α rm_invar rm_lookup rm_update 
    rm_α rm_invar rm_lookup rm_update rm_delete rm_iteratei rm_sel
    rs_α rs_invar rs_memb rs_ins rs_delete
    fifo_α fifo_invar fifo_empty fifo_isEmpty fifo_enqueue fifo_dequeue fifo_push
  for final :: "'x ⇒ bool"
  and r :: "'t ⇒ ('x × 'm) ⇒ (('l,'t :: linorder,'x,'m,'w,'o) thread_action × 'x × 'm) Predicate.pred"
  and convert_RA :: "'l released_locks ⇒ 'o list"
  and "output" :: "'t fifo round_robin ⇒ 't ⇒ ('l,'t,'x,'m,'w,'o) thread_action ⇒ 'q option"

sublocale sc_round_robin < sc_round_robin_base .

locale sc_random_scheduler_base =
  random_scheduler_base
    final r convert_RA "output"
    rm_α rm_invar rm_lookup rm_update rm_iteratei 
    rm_α rm_invar rm_lookup rm_update rm_delete rm_iteratei rm_sel
    rs_α rs_invar rs_memb rs_ins rs_delete
    lsi_α lsi_invar lsi_empty lsi_ins_dj lsi_to_list
  for final :: "'x ⇒ bool"
  and r :: "'t ⇒ ('x × 'm) ⇒ (('l,'t :: linorder,'x,'m,'w,'o) thread_action × 'x × 'm) Predicate.pred"
  and convert_RA :: "'l released_locks ⇒ 'o list"
  and "output" :: "random_scheduler ⇒ 't ⇒ ('l,'t,'x,'m,'w,'o) thread_action ⇒ 'q option"

locale sc_random_scheduler =
  random_scheduler
    final r convert_RA "output"
    rm_α rm_invar rm_lookup rm_update rm_iteratei 
    rm_α rm_invar rm_lookup rm_update rm_delete rm_iteratei rm_sel
    rs_α rs_invar rs_memb rs_ins rs_delete
    lsi_α lsi_invar lsi_empty lsi_ins_dj lsi_to_list
  for final :: "'x ⇒ bool"
  and r :: "'t ⇒ ('x × 'm) ⇒ (('l,'t :: linorder,'x,'m,'w,'o) thread_action × 'x × 'm) Predicate.pred"
  and convert_RA :: "'l released_locks ⇒ 'o list"
  and "output" :: "random_scheduler ⇒ 't ⇒ ('l,'t,'x,'m,'w,'o) thread_action ⇒ 'q option"

sublocale sc_random_scheduler < sc_random_scheduler_base .

text ‹No spurious wake-ups in generated code›
overloading sc_spurious_wakeups ≡ sc_spurious_wakeups
begin
  definition sc_spurious_wakeups [code]: "sc_spurious_wakeups ≡ False"
end

end