Library prosa.classic.model.schedule.global.basic.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 prosa.classic.model.schedule.global.basic.interference
               prosa.classic.model.schedule.global.basic.platform.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.

Module InterferenceEDF.

  Import Schedule Priority Platform Interference Priority.

  Section Lemmas.

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

    Context {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 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 sched j' j t1 t2 != 0 →
        job_arrival j + job_deadline j ≤ job_arrival j' + job_deadline j'.

  End Lemmas.

End InterferenceEDF.