Library prosa.analysis.facts.model.ideal_schedule

Require Export prosa.util.all.
Require Export prosa.model.processor.platform_properties.
Require Export prosa.analysis.facts.behavior.service.

Throughout this file, we assume ideal uni-processor schedules.
Require Import prosa.model.processor.ideal.

Note: we do not re-export the basic definitions to avoid littering the global namespace with type class instances.
In this section we establish the classes to which an ideal schedule belongs.
Section ScheduleClass.

  Local Transparent service_in scheduled_in scheduled_on.
Consider any job type and the ideal processor model.
  Context {Job: JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

We note that the ideal processor model is indeed a uni-processor model.
  Lemma ideal_proc_model_is_a_uniprocessor_model:
    uniprocessor_model (processor_state Job).

We observe that the ideal processor model falls into the category of ideal-progress models, i.e., a scheduled job always receives service.
  Lemma ideal_proc_model_ensures_ideal_progress:
    ideal_progress_proc_model (processor_state Job).

The ideal processor model is a unit-service model.
  Lemma ideal_proc_model_provides_unit_service:
    unit_service_proc_model (processor_state Job).

  Lemma scheduled_in_def (j : Job) s :
    scheduled_in j s = (s == Some j).

  Lemma scheduled_at_def sched (j : Job) t :
    scheduled_at sched j t = (sched t == Some j).

  Lemma service_in_is_scheduled_in (j : Job) s :
    service_in j s = scheduled_in j s.

  Lemma service_at_is_scheduled_at sched (j : Job) t :
    service_at sched j t = scheduled_at sched j t.

Next we prove a lemma which helps us to do a case analysis on the state of an ideal schedule.
  Lemma ideal_proc_model_sched_case_analysis:
    ∀ (sched : schedule (ideal.processor_state Job)) (t : instant),
      is_idle sched t ∨ ∃ j, scheduled_at sched j t.

End ScheduleClass.

Incremental Service in Ideal Schedule

In the following section we prove a few facts about service in ideal schedule.
(* Note that these lemmas can be generalized to an arbitrary scheduler. *)
Section IncrementalService.

Consider any job type, ...
  Context {Job : JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

... any arrival sequence, ...
  Variable arr_seq : arrival_sequence Job.

... and any ideal uni-processor schedule of this arrival sequence.
  Variable sched : schedule (ideal.processor_state Job).

As a base case, we prove that if a job j receives service in some time interval t1,t2), then there ∃ a time instant t ∈ [t1,t2) such that j is scheduled at time t and t is the first instant where j receives service.
  Lemma positive_service_during:
    ∀ j t1 t2,
      0 < service_during sched j t1 t2 →
      ∃ t : nat, t1 ≤ t < t2 ∧ scheduled_at sched j t ∧ service_during sched j t1 t = 0.

Next, we prove that if in some time interval t1,t2) a job j receives k units of service, then there ∃ a time instant t ∈ [t1,t2) such that j is scheduled at time t and service of job j within interval [t1,t) is equal to k.
  Lemma incremental_service_during:
    ∀ j t1 t2 k,
      service_during sched j t1 t2 > k →
      ∃ t, t1 ≤ t < t2 ∧ scheduled_at sched j t ∧ service_during sched j t1 t = k.

End IncrementalService.

Automation

We add the above lemmas into a "Hint Database" basic_facts, so Coq will be able to apply them automatically.
Hint Resolve ideal_proc_model_is_a_uniprocessor_model
     ideal_proc_model_ensures_ideal_progress
     ideal_proc_model_provides_unit_service : basic_facts.

We also provide tactics for case analysis on ideal processor state.
The first tactic generates two sub-goals: one with idle processor and the other with processor executing a job named JobName.
Ltac ideal_proc_model_sched_case_analysis sched t JobName :=
  let Idle := fresh "Idle" in
  let Sched := fresh "Sched_" JobName in
  destruct (ideal_proc_model_sched_case_analysis sched t) as [Idle | [JobName Sched]].

The second tactic is similar to the first, but it additionally generates two equalities: sched t = None and sched t = Some j.
Ltac ideal_proc_model_sched_case_analysis_eq sched t JobName :=
  let Idle := fresh "Idle" in
  let IdleEq := fresh "Eq" Idle in
  let Sched := fresh "Sched_" JobName in
  let SchedEq := fresh "Eq" Sched in
  destruct (ideal_proc_model_sched_case_analysis sched t) as [Idle | [JobName Sched]];
  [move: (Idle) ⇒ /eqP IdleEq; rewrite ?IdleEq
  | move: (Sched); simpl; move ⇒ /eqP SchedEq; rewrite ?SchedEq].