ideal_schedule.v 3.93 KB
Newer Older
1
From mathcomp Require Import all_ssreflect.
2 3 4
Require Export rt.restructuring.model.processor.platform_properties.

(** Throughout this file, we assume ideal uniprocessor schedules. *)
5
Require Import rt.restructuring.model.processor.ideal.
6

7
(** Note: we do not re-export the basic definitions to avoid littering the global
8 9
   namespace with type class instances. *)

10
(** In this section we estlish the classes to which an ideal schedule belongs. *)
11
Section ScheduleClass.
12 13

  Local Transparent service_in scheduled_in scheduled_on.
14
  (** Consider any job type and the ideal processor model. *)
15
  Context {Job: JobType}.
16 17
  Context `{JobArrival Job}.
  Context `{JobCost Job}.  
18

19
  (** We note that the ideal processor model is indeed a uniprocessor
20 21
     model. *)
  Lemma ideal_proc_model_is_a_uniprocessor_model:
22
    uniprocessor_model (processor_state Job).
23
  Proof.
24 25
    move=> j1 j2 sched t /existsP[[]/eqP E1] /existsP[[]/eqP E2].
    by move: E1 E2=>->[].
26
  Qed.
27

28
  (** We observe that the ideal processor model falls into the category
29 30 31
     of ideal-progress models, i.e., a scheduled job always receives
     service. *)
  Lemma ideal_proc_model_ensures_ideal_progress:
32
    ideal_progress_proc_model (processor_state Job).
Maxime Lesourd's avatar
Maxime Lesourd committed
33
  Proof.
34 35
    move=> j s /existsP[[]/eqP->]/=.
    by rewrite eqxx.
Maxime Lesourd's avatar
Maxime Lesourd committed
36
  Qed.
37

38
  (** The ideal processor model is a unit-service model. *)
39
  Lemma ideal_proc_model_provides_unit_service:
40
    unit_service_proc_model (processor_state Job).
41 42
  Proof.
    move=> j s.
43 44
    rewrite /service_in/=/nat_of_bool.
    by case:ifP.
45 46
  Qed.

47 48 49 50 51 52 53 54 55 56 57 58 59 60
  Lemma scheduled_in_def (j : Job) s :
    scheduled_in j s = (s == Some j).
  Proof.
    rewrite /scheduled_in/scheduled_on/=.
    case: existsP=>[[_->]//|].
    case: (s == Some j)=>//=[[]].
      by exists.
  Qed.

  Lemma scheduled_at_def sched (j : Job) t :
    scheduled_at sched j t = (sched t == Some j).
  Proof.
      by rewrite /scheduled_at scheduled_in_def.
  Qed.
61

62 63 64 65 66 67 68 69 70 71 72
  Lemma service_in_is_scheduled_in (j : Job) s :
    service_in j s = scheduled_in j s.
  Proof.
    by rewrite /service_in scheduled_in_def/=.
  Qed.

  Lemma service_at_is_scheduled_at sched (j : Job) t :
    service_at sched j t = scheduled_at sched j t.
  Proof.
      by rewrite /service_at service_in_is_scheduled_in.
  Qed.
73 74 75 76 77 78 79 80 81 82 83 84 85
    
  (** 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:
    forall (sched : schedule (ideal.processor_state Job)) (t : instant),
      is_idle sched t \/ exists j, scheduled_at sched j t. 
  Proof.
    intros.
    unfold is_idle; simpl; destruct (sched t) eqn:EQ.
    - by right; exists s; auto; rewrite scheduled_at_def EQ.
    - by left; auto.
  Qed.
  
86
End ScheduleClass.
87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113

(** * 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 subgoals: 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].