arrivals.v 7.77 KB
Newer Older
Björn Brandenburg's avatar
Björn Brandenburg committed
1 2
Require Export prosa.behavior.all.
Require Export prosa.util.all.
3

4 5
(** * Arrival Sequence *)

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
(** First, we relate the stronger to the weaker arrival predicates. *)
Section ArrivalPredicates.

  (** Consider any kinds of jobs with arrival times. *)
  Context {Job : JobType} `{JobArrival Job}.

  (** A job that arrives in some interval [[t1, t2)] certainly arrives before
      time [t2]. *)
  Lemma arrived_between_before:
    forall j t1 t2,
      arrived_between j t1 t2 ->
      arrived_before j t2.
  Proof.
    move=> j t1 t2.
    now rewrite /arrived_before /arrived_between => /andP [_ CLAIM].
  Qed.

  (** A job that arrives before a time [t] certainly has arrived by time
      [t]. *)
  Lemma arrived_before_has_arrived:
    forall j t,
      arrived_before j t ->
      has_arrived j t.
  Proof.
    move=> j t.
    rewrite /arrived_before /has_arrived.
    now apply ltnW.
  Qed.

End ArrivalPredicates.

37
(** In this section, we relate job readiness to [has_arrived]. *)
38
Section Arrived.
Sergey Bozhko's avatar
Sergey Bozhko committed
39
  
40
  (** Consider any kinds of jobs and any kind of processor state. *)
41 42 43
  Context {Job : JobType} {PState : Type}.
  Context `{ProcessorState Job PState}.

44
  (** Consider any schedule... *)
45 46
  Variable sched : schedule PState.

47 48
  (** ...and suppose that jobs have a cost, an arrival time, and a
      notion of readiness. *)
49 50
  Context `{JobCost Job}.
  Context `{JobArrival Job}.
Sergey Bozhko's avatar
Sergey Bozhko committed
51
  Context `{JobReady Job PState}.
52 53 54 55 56 57 58

  (** First, we note that readiness models are by definition consistent
      w.r.t. [pending]. *)
  Lemma any_ready_job_is_pending:
    forall j t,
      job_ready sched j t -> pending sched j t.
  Proof.
Sergey Bozhko's avatar
Sergey Bozhko committed
59
    move: H5 => [is_ready CONSISTENT].
60 61 62 63
    move=> j t READY.
    apply CONSISTENT.
    by exact READY.
  Qed.
64

65
  (** Next, we observe that a given job must have arrived to be ready... *)
66 67 68 69
  Lemma ready_implies_arrived:
    forall j t, job_ready sched j t -> has_arrived j t.
  Proof.
    move=> j t READY.
70
    move: (any_ready_job_is_pending j t READY).
71 72 73
    by rewrite /pending => /andP [ARR _].
  Qed.

74
  (** ...and lift this observation also to the level of whole schedules. *)
75 76 77 78 79 80 81 82 83 84
  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.

85 86 87 88 89 90 91 92 93 94
  (** Since backlogged jobs are by definition ready, any backlogged job must have arrived. *)
  Corollary backlogged_implies_arrived:
    forall j t,
      backlogged sched j t -> has_arrived j t.
  Proof.
    rewrite /backlogged.
    move=> j t /andP [READY _].
    now apply ready_implies_arrived.
  Qed.

95 96
End Arrived.

97
(** In this section, we establish useful facts about arrival sequence prefixes. *)
98 99
Section ArrivalSequencePrefix.

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

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

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

110
    (** First, we show that the set of arriving jobs can be split
111
         into disjoint intervals. *)
112 113 114 115 116 117 118 119 120 121 122 123
    Lemma arrivals_between_cat:
      forall t1 t t2,
        t1 <= t ->
        t <= t2 ->
        arrivals_between arr_seq t1 t2 =
        arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2.
    Proof.
      unfold arrivals_between; intros t1 t t2 GE LE.
        by rewrite (@big_cat_nat _ _ _ t).
    Qed.

    (** Second, the same observation applies to membership in the set of
124
         arrived jobs. *)
125 126 127 128 129 130 131 132 133 134 135
    Lemma arrivals_between_mem_cat:
      forall j t1 t t2,
        t1 <= t ->
        t <= t2 ->
        j \in arrivals_between arr_seq t1 t2 =
        (j \in arrivals_between arr_seq t1 t ++ arrivals_between arr_seq t t2).
    Proof.
        by intros j t1 t t2 GE LE; rewrite (arrivals_between_cat _ t).
    Qed.

    (** Third, we observe that we can grow the considered interval without
136 137
         "losing" any arrived jobs, i.e., membership in the set of arrived jobs
         is monotonic. *)
138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164
    Lemma arrivals_between_sub:
      forall j t1 t1' t2 t2',
        t1' <= t1 ->
        t2 <= t2' ->
        j \in arrivals_between arr_seq t1 t2 ->
        j \in arrivals_between arr_seq t1' t2'.
    Proof.
      intros j t1 t1' t2 t2' GE1 LE2 IN.
      move: (leq_total t1 t2) => /orP [BEFORE | AFTER];
                                  last by rewrite /arrivals_between big_geq // in IN.
      rewrite /arrivals_between.
      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. *)
    Hypothesis H_consistent_arrival_times:
      consistent_arrival_times arr_seq.

    (** First, we prove that if a job belongs to the prefix
165
         (jobs_arrived_before t), then it arrives in the arrival sequence. *)
166 167 168 169 170 171 172 173 174 175 176 177 178
    Lemma in_arrivals_implies_arrived:
      forall j t1 t2,
        j \in arrivals_between arr_seq t1 t2 ->
        arrives_in arr_seq j.
    Proof.
      rename H_consistent_arrival_times into CONS.
      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
179 180
         (jobs_arrived_between t1 t2), then it indeed arrives between t1 and
         t2. *)
181 182 183 184 185 186 187 188 189 190 191 192 193
    Lemma in_arrivals_implies_arrived_between:
      forall j t1 t2,
        j \in arrivals_between arr_seq t1 t2 ->
        arrived_between j t1 t2.
    Proof.
      rename H_consistent_arrival_times into CONS.
      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),
194
           then it indeed arrives before time t. *)
195 196 197 198 199 200 201 202 203 204 205
    Lemma in_arrivals_implies_arrived_before:
      forall j t,
        j \in arrivals_before arr_seq t ->
        arrived_before j t.
    Proof.
      intros j t IN.
      have: arrived_between j 0 t by apply in_arrivals_implies_arrived_between.
        by rewrite /arrived_between /=.
    Qed.

    (** Similarly, we prove that if a job from the arrival sequence arrives
206
         before t, then it belongs to the sequence (jobs_arrived_before t). *)
207 208 209 210 211 212 213 214 215 216 217 218 219
    Lemma arrived_between_implies_in_arrivals:
      forall j t1 t2,
        arrives_in arr_seq j ->
        arrived_between j t1 t2 ->
        j \in arrivals_between arr_seq t1 t2.
    Proof.
      rename H_consistent_arrival_times into CONS.
      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
220
         jobs, the same applies for any of its prefixes. *)
221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241
    Lemma arrivals_uniq :
      arrival_sequence_uniq arr_seq ->
      forall t1 t2, uniq (arrivals_between arr_seq t1 t2).
    Proof.
      rename H_consistent_arrival_times into CONS.
      unfold arrivals_up_to; intros SET t1 t2.
      apply bigcat_nat_uniq; first by done.
      intros x t t' IN1 IN2.
        by apply CONS in IN1; apply CONS in IN2; subst.
    Qed.

    (** Also note there can't by any arrivals in an empty time interval. *)
    Lemma arrivals_between_geq:
      forall t1 t2,
        t1 >= t2 ->
        arrivals_between arr_seq t1 t2  = [::].
    Proof.
        by intros ? ? GE; rewrite /arrivals_between big_geq.
    Qed.
    
  End ArrivalTimes.
242

243
End ArrivalSequencePrefix.