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'.

  End Lemmas.

End InterferenceEDF.