Library prosa.classic.model.schedule.apa.interference_edf

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

Module InterferenceEDF.

  Import Schedule Priority Platform Interference Priority Affinity.

  Section Lemmas.

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

    Variable arr_seq: arrival_sequence Job.

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

    Variable alpha: task_affinity sporadic_task num_cpus.

    Hypothesis H_scheduler_uses_EDF:
      respects_JLFP_policy_under_weak_APA job_arrival job_cost job_task arr_seq sched
                                          alpha (EDF job_arrival job_deadline).

    Lemma interference_under_edf_implies_shorter_deadlines :
      ∀ j j' t1 t2,
        arrives_in arr_seq j' →
        job_interference job_arrival job_cost job_task sched alpha 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.
      unfold respects_JLDP_policy_under_weak_APA in ×.
      intros j j' t1 t2 ARR' INTERF.
      unfold job_interference in INTERF.
      destruct ([∃ t': 'I_t2,
                   [∃ cpu: processor num_cpus,
                      (t' ≥ t1) &&
                      backlogged job_arrival job_cost sched j' t' &&
                      can_execute_on alpha (job_task j') cpu &&
                      scheduled_on sched j cpu t']]) eqn:EX.
      {
        move: EX ⇒ /existsP [t' /existsP [cpu /andP [/andP [/andP [LE BACK] CAN] SCHED]]].
        by specialize (PRIO j' j cpu t' ARR' BACK SCHED CAN).
      }
      {
        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 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.