Library prosa.analysis.facts.model.ideal.service_of_jobs

Throughout this file, we assume ideal uni-processor schedules.

Service Received by Sets of Jobs in Ideal Uni-Processor Schedules

In this file, we establish a fact about the service received by sets of jobs under ideal uni-processor schedule and the presence of idle times. The lemma is currently specific to ideal uniprocessors only because of the lack of a general notion of idle time, which should be added in the near future. Conceptually, the fact holds for any ideal_progress_proc_model. Once a general notion of idle time has been defined, this file should be generalized.
Section IdealModelLemmas.

Consider any type of tasks ...
  Context {Task : TaskType}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

Consider any arrival sequence with consistent arrivals.
Next, consider any ideal uni-processor schedule of this arrival sequence ...
... where jobs do not execute before their arrival or after completion.
Let P be any predicate over jobs.
  Variable P : pred Job.

We prove that if the total service within some time interval [t1,t2) is smaller than t2 - t1, then there is an idle time instant t [t1,t2)].
  Lemma low_service_implies_existence_of_idle_time :
     t1 t2,
      service_of_jobs sched predT (arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1
       t, t1 t < t2 is_idle sched t.
    intros ? ? SERV.
    destruct (t1 t2) eqn:LE; last first.
    { move: LE ⇒ /negP/negP; rewrite -ltnNge.
      moveLT; apply ltnW in LT; rewrite -subn_eq0 in LT.
      by move: LT ⇒ /eqPin SERV; rewrite ltn0 in SERV.
    have EX: δ, t2 = t1 + δ.
    { by (t2 - t1); rewrite subnKC // ltnW. }
    move: EX ⇒ [δ EQ]; subst t2; clear LE.
    rewrite {3}[t1 + δ]addnC -addnBA // subnn addn0 in SERV.
    rewrite /service_of_jobs exchange_big //= in SERV.
    apply sum_le_summation_range in SERV.
    move: SERV ⇒ [x [/andP [GEx LEx] L]].
     x; split; first by apply/andP; split.
    apply/negPn; apply/negP; intros NIDLE.
    unfold is_idle in NIDLE.
    destruct(sched x) eqn:SCHED; last by done.
    move: SCHED ⇒ /eqP SCHED; clear NIDLE; rewrite -scheduled_at_def/= in SCHED.
    move: L ⇒ /eqP; rewrite sum_nat_eq0_nat filter_predT; move ⇒ /allP L.
    specialize (L s); feed L.
    { unfold arrivals_between.
      eapply arrived_between_implies_in_arrivals; eauto 2.
      by apply H_jobs_must_arrive_to_execute in SCHED; apply leq_ltn_trans with x.
    move: SCHED L ⇒ /=.
    rewrite scheduled_at_def service_at_def ⇒ /eqP→ /eqP.
    by rewrite eqxx.

End IdealModelLemmas.