arrivals.v 6.39 KB
Newer Older
1
From rt.restructuring.behavior Require Export arrival_sequence schedule.
2 3
From rt.util Require Import all.

4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40
(* In this section, we relate job readiness to [has_arrived]. *)
Section Arrived.
  (* Consider any kinds of jobs and any kind of processor state. *)
  Context {Job : JobType} {PState : Type}.
  Context `{ProcessorState Job PState}.

  (* Consider any schedule... *)
  Variable sched : schedule PState.

  (* ...and suppose that jobs have a cost, an arrival time, and a notion of
     readiness. *)
  Context `{JobCost Job}.
  Context `{JobArrival Job}.
  Context `{JobReady Job PState}.

  (* We observe that a given job must have arrived to be ready... *)
  Lemma ready_implies_arrived:
    forall j t, job_ready sched j t -> has_arrived j t.
  Proof.
    move=> j t READY.
    move: (any_ready_job_is_pending sched j t READY).
    by rewrite /pending => /andP [ARR _].
  Qed.

  (* ...and lift this observation also to the level of whole schedules. *)
  Lemma jobs_must_arrive_to_be_ready:
    jobs_must_be_ready_to_execute sched ->
    jobs_must_arrive_to_execute sched.
  Proof.
    rewrite /jobs_must_be_ready_to_execute /jobs_must_arrive_to_execute.
    move=> READY_IF_SCHED j t SCHED.
    move: (READY_IF_SCHED j t SCHED) => READY.
    by apply ready_implies_arrived.
  Qed.

End Arrived.

41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58
(* In this section, we establish useful facts about arrival sequence prefixes. *)
Section ArrivalSequencePrefix.

  (* Assume that job arrival times are known. *)
  Context {Job: JobType}.
  Context `{JobArrival Job}.

  (* Consider any job arrival sequence. *)
  Variable arr_seq: arrival_sequence Job.

  (* In this section, we prove some lemmas about arrival sequence prefixes. *)
  Section Lemmas.

    (* We begin with basic lemmas for manipulating the sequences. *)
    Section Composition.

      (* First, we show that the set of arriving jobs can be split
         into disjoint intervals. *)
59
      Lemma arrivals_between_cat:
60 61 62
        forall t1 t t2,
          t1 <= t ->
          t <= t2 ->
63
          arrivals_between arr_seq t1 t2 = arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2.
64
      Proof.
65
        unfold arrivals_between; intros t1 t t2 GE LE.
66 67 68 69 70
          by rewrite (@big_cat_nat _ _ _ t).
      Qed.

      (* Second, the same observation applies to membership in the set of
         arrived jobs. *)
71
      Lemma arrivals_between_mem_cat:
72 73 74
        forall j t1 t t2,
          t1 <= t ->
          t <= t2 ->
75 76
          j \in arrivals_between arr_seq t1 t2 =
                (j \in arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2).
77
      Proof.
78
          by intros j t1 t t2 GE LE; rewrite (arrivals_between_cat _ t).
79 80 81 82 83
      Qed.

      (* Third, we observe that we can grow the considered interval without
         "losing" any arrived jobs, i.e., membership in the set of arrived jobs
         is monotonic. *)
84
      Lemma arrivals_between_sub:
85 86 87
        forall j t1 t1' t2 t2',
          t1' <= t1 ->
          t2 <= t2' ->
88 89
          j \in arrivals_between arr_seq t1 t2 ->
          j \in arrivals_between arr_seq t1' t2'.
90 91 92
      Proof.
        intros j t1 t1' t2 t2' GE1 LE2 IN.
        move: (leq_total t1 t2) => /orP [BEFORE | AFTER];
93 94
                                   last by rewrite /arrivals_between big_geq // in IN.
        rewrite /arrivals_between.
95 96 97 98 99 100 101 102 103 104 105 106
        rewrite -> big_cat_nat with (n := t1); [simpl | by done | by apply: (leq_trans BEFORE)].
        rewrite mem_cat; apply/orP; right.
        rewrite -> big_cat_nat with (n := t2); [simpl | by done | by done].
          by rewrite mem_cat; apply/orP; left.
      Qed.

    End Composition.

    (* Next, we relate the arrival prefixes with job arrival times. *)
    Section ArrivalTimes.

      (* Assume that job arrival times are consistent. *)
107 108
      Hypothesis H_consistent_arrival_times:
        consistent_arrival_times arr_seq.
109 110 111 112 113

      (* First, we prove that if a job belongs to the prefix
         (jobs_arrived_before t), then it arrives in the arrival sequence. *)
      Lemma in_arrivals_implies_arrived:
        forall j t1 t2,
114 115
          j \in arrivals_between arr_seq t1 t2 ->
          arrives_in arr_seq j.
116
      Proof.
117
        rename H_consistent_arrival_times into CONS.
118 119 120 121 122 123 124 125 126 127 128
        intros j t1 t2 IN.
        apply mem_bigcat_nat_exists in IN.
        move: IN => [arr [IN _]].
          by exists arr.
      Qed.

      (* Next, we prove that if a job belongs to the prefix
         (jobs_arrived_between t1 t2), then it indeed arrives between t1 and
         t2. *)
      Lemma in_arrivals_implies_arrived_between:
        forall j t1 t2,
129
          j \in arrivals_between arr_seq t1 t2 ->
130 131
                arrived_between j t1 t2.
      Proof.
132
        rename H_consistent_arrival_times into CONS.
133 134 135 136 137 138 139 140 141 142
        intros j t1 t2 IN.
        apply mem_bigcat_nat_exists in IN.
        move: IN => [t0 [IN /= LT]].
          by apply CONS in IN; rewrite /arrived_between IN.
      Qed.

      (* Similarly, if a job belongs to the prefix (jobs_arrived_before t),
           then it indeed arrives before time t. *)
      Lemma in_arrivals_implies_arrived_before:
        forall j t,
143
          j \in arrivals_before arr_seq t ->
144 145 146 147
                arrived_before j t.
      Proof.
        intros j t IN.
        have: arrived_between j 0 t by apply in_arrivals_implies_arrived_between.
Maxime Lesourd's avatar
Maxime Lesourd committed
148
          by rewrite /arrived_between /=.
149 150 151 152 153 154 155 156
      Qed.

      (* Similarly, we prove that if a job from the arrival sequence arrives
         before t, then it belongs to the sequence (jobs_arrived_before t). *)
      Lemma arrived_between_implies_in_arrivals:
        forall j t1 t2,
          arrives_in arr_seq j ->
          arrived_between j t1 t2 ->
157
          j \in arrivals_between arr_seq t1 t2.
158
      Proof.
159
        rename H_consistent_arrival_times into CONS.
160 161 162 163 164 165 166 167
        move => j t1 t2 [a_j ARRj] BEFORE.
        have SAME := ARRj; apply CONS in SAME; subst a_j.
          by apply mem_bigcat_nat with (j := (job_arrival j)).
      Qed.

      (* Next, we prove that if the arrival sequence doesn't contain duplicate
         jobs, the same applies for any of its prefixes. *)
      Lemma arrivals_uniq :
168
        arrival_sequence_uniq arr_seq ->
169
        forall t1 t2, uniq (arrivals_between arr_seq t1 t2).
170
      Proof.
171
        rename H_consistent_arrival_times into CONS.
172
        unfold arrivals_up_to; intros SET t1 t2.
173 174 175 176 177 178 179 180 181 182
        apply bigcat_nat_uniq; first by done.
        intros x t t' IN1 IN2.
          by apply CONS in IN1; apply CONS in IN2; subst.
      Qed.

    End ArrivalTimes.

  End Lemmas.

End ArrivalSequencePrefix.