Library prosa.classic.model.schedule.global.jitter.interference_edf

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.arrival_sequence prosa.classic.model.priority prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.schedule.global.jitter.job
               prosa.classic.model.schedule.global.jitter.schedule
               prosa.classic.model.schedule.global.jitter.interference
               prosa.classic.model.schedule.global.jitter.platform.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.

Module InterferenceEDF.

  Import ScheduleWithJitter Priority Platform Interference Priority.

  Section Lemmas.

    Context {Job: eqType}.
    Variable job_arrival: Job → time.
    Variable job_cost: Job → time.
    Variable job_deadline: Job → time.
    Variable job_jitter: Job → time.

    Variable arr_seq: arrival_sequence Job.

    Variable num_cpus: nat.
    Variable sched: schedule Job num_cpus.

    Hypothesis H_scheduler_uses_EDF:
      respects_JLFP_policy job_arrival job_cost job_jitter arr_seq sched
                           (EDF job_arrival job_deadline).

    Lemma interference_under_edf_implies_shorter_deadlines :
      ∀ j j' t1 t2,
        arrives_in arr_seq j →
        arrives_in arr_seq j' →
        job_interference job_arrival job_cost job_jitter sched j' j t1 t2 != 0 →
        job_arrival j + job_deadline j ≤ job_arrival j' + job_deadline j'.
    Proof.
      rename H_scheduler_uses_EDF into PRIO.
      intros j j' t1 t2 ARR ARR' INTERF.
      unfold job_interference in INTERF.
      destruct ([∃ t': 'I_t2,
                   [∃ cpu: processor num_cpus,
                      (t' ≥ t1) &&
                      backlogged job_arrival job_cost job_jitter sched j' t' &&
                      scheduled_on sched j cpu t']]) eqn:EX.
      {
        move: EX ⇒ /existsP [t' /existsP [cpu /andP [/andP [LE BACK] SCHED]]].
        apply PRIO with (t := t'); try (by done).
        by apply/existsP; ∃ cpu.
      }
      {
        apply negbT in EX; rewrite negb_exists in EX; move: EX ⇒ /forallP ALL.
        rewrite big_nat_cond (eq_bigr (fun x ⇒ 0)) in INTERF;
          first by rewrite -big_nat_cond big_const_nat iter_addn mul0n addn0 eq_refl in INTERF.
        move ⇒ i /andP [/andP [GEi LTi] _].
        specialize (ALL (Ordinal LTi)).
        rewrite negb_exists in ALL.
        move: ALL ⇒ /forallP ALL.
        rewrite (eq_bigr (fun x ⇒ 0));
          first by rewrite big_const_ord iter_addn mul0n addn0.
        intros cpu _; specialize (ALL cpu); simpl in ALL.
        destruct (backlogged job_arrival job_cost job_jitter sched j' i); last by rewrite andFb.
        rewrite GEi 2!andTb in ALL; rewrite andTb.
        by apply negbTE in ALL; rewrite ALL.
      }
    Qed.

  End Lemmas.

End InterferenceEDF.