Library prosa.classic.model.schedule.global.basic.interference

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job prosa.classic.model.priority.
Require Import prosa.classic.model.schedule.global.workload.
Require Import prosa.classic.model.schedule.global.basic.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

Module Interference.

  Import Schedule ScheduleOfSporadicTask Priority Workload.

  Section InterferenceDefs.

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

    Variable arr_seq: arrival_sequence Job.

    Context {num_cpus: nat}.
    Variable sched: schedule Job num_cpus.

    Variable j: Job.

    Let job_is_backlogged (t: time) :=
      backlogged job_arrival job_cost sched j t.

    Section TotalInterference.

      Definition total_interference (t1 t2: time) :=
        \sum_(t1 ≤ t < t2) job_is_backlogged t.

    End TotalInterference.

    Section JobInterference.

      Variable job_other: Job.

      Definition job_interference (t1 t2: time) :=
        \sum_(t1 ≤ t < t2)
          \sum_(cpu < num_cpus)
            (job_is_backlogged t && scheduled_on sched job_other cpu t).

    End JobInterference.

    Section TaskInterference.

      Variable tsk_other: sporadic_task.

      Definition task_interference (t1 t2: time) :=
        \sum_(t1 ≤ t < t2)
          \sum_(cpu < num_cpus)
            (job_is_backlogged t &&
            task_scheduled_on job_task sched tsk_other cpu t).

    End TaskInterference.

    Section TaskInterferenceJobList.

      Variable tsk_other: sporadic_task.

      Definition task_interference_joblist (t1 t2: time) :=
        \sum_(j <- jobs_scheduled_between sched t1 t2 | job_task j == tsk_other)
         job_interference j t1 t2.

    End TaskInterferenceJobList.

    Section BasicLemmas.

      Lemma total_interference_le_delta :
        ∀ t1 t2,
          total_interference t1 t2 ≤ t2 - t1.

      Lemma job_interference_le_service :
        ∀ j_other t1 t2,
          job_interference j_other t1 t2 ≤ service_during sched j_other t1 t2.

      Lemma task_interference_le_workload :
        ∀ tsk t1 t2,
          task_interference tsk t1 t2 ≤ workload job_task sched tsk t1 t2.

    End BasicLemmas.

    Section InterferenceSequentialJobs.

      Hypothesis H_sequential_jobs: sequential_jobs sched.

      Lemma job_interference_le_delta :
        ∀ j_other t1 delta,
          job_interference j_other t1 (t1 + delta) ≤ delta.

    End InterferenceSequentialJobs.

    Section BoundUsingPerJobInterference.

      Lemma interference_le_interference_joblist :
        ∀ tsk t1 t2,
          task_interference tsk t1 t2 ≤ task_interference_joblist tsk t1 t2.

    End BoundUsingPerJobInterference.

  End InterferenceDefs.

End Interference.