Library rt.model.apa.interference_edf

Require Import rt.util.all.
Require Import rt.model.apa.task rt.model.apa.job rt.model.apa.schedule
               rt.model.apa.priority rt.model.apa.task_arrival rt.model.apa.interference
               rt.model.apa.arrival_sequence rt.model.apa.platform
               rt.model.apa.affinity.

Module InterferenceEDF.

  Import Schedule Priority Platform Interference Priority Affinity.

  Section Lemmas.

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

    (* Assume any job arrival sequence... *)
    Context {arr_seq: arrival_sequence Job}.

    (* Consider any schedule. *)
    Variable num_cpus: nat.
    Variable sched: schedule num_cpus arr_seq.

    (* Assume that every job at any time has a processor affinity alpha. *)
    Variable alpha: task_affinity sporadic_task num_cpus.

    (* Assume that the schedule satisfies the global scheduling invariant
       for EDF, i.e., if any job of tsk is backlogged, every processor
       must be busy with jobs with no larger absolute deadline. *)
    Hypothesis H_scheduler_uses_EDF:
      enforces_JLDP_policy_under_weak_APA job_cost job_task sched alpha (EDF job_deadline).

    (* Under EDF scheduling, a job only causes interference if its deadline
       is not larger than the deadline of the analyzed job. *)
    Lemma interference_under_edf_implies_shorter_deadlines :
      ∀ (j j': JobIn arr_seq) t1 t2,
        job_interference 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.