Library rt.model.schedule.apa.interference

Require Import rt.util.all.
Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task rt.model.priority.
Require Import rt.model.schedule.global.workload.
Require Import rt.model.schedule.global.basic.schedule.
Require Import rt.model.schedule.apa.affinity.

Module Interference.

  Import Schedule ScheduleOfSporadicTask Priority Workload Affinity.

  (* In this section, we define the notion of a possible interfering task. *)
  Section PossibleInterferingTasks.

    Context {sporadic_task: eqType}.
    Variable task_cost: sporadic_task time.
    Variable task_period: sporadic_task time.
    Variable task_deadline: sporadic_task time.

    (* Consider an APA platform with affinity alpha. *)
    Context {num_cpus: nat}.
    Variable alpha: task_affinity sporadic_task num_cpus.

    Section FP.

      (* Assume an FP policy. *)
      Variable higher_eq_priority: FP_policy sporadic_task.

      (* Let tsk be the task to be analyzed ... *)
      Variable tsk: sporadic_task.

      (* ...assuming a subaffinity alpha'. *)
      Variable alpha': affinity num_cpus.

      (* Let tsk_other be another task. *)
      Variable tsk_other: sporadic_task.

      (* Under FP scheduling with constrained deadlines, tsk_other can only interfere
         with tsk if it is a different task with higher or equal priority and
         intersecting affinity. *)

      Definition higher_priority_task_in :=
        higher_eq_priority tsk_other tsk &&
        (tsk_other != tsk) &&
        affinity_intersects alpha' (alpha tsk_other).

    End FP.

    Section JLFP.

      (* Let tsk be the task to be analyzed ... *)
      Variable tsk: sporadic_task.

      (* ...assuming a subaffinity alpha'. *)
      Variable alpha': affinity num_cpus.

      (* Let tsk_other be another task. *)
      Variable tsk_other: sporadic_task.

      (* Under JLFP/JLDP scheduling with constrained deadlines, tsk_other can only interfere
         with tsk if it is a different task with intersecting affinity. *)

      Definition different_task_in :=
        (tsk_other != tsk) &&
        affinity_intersects alpha' (alpha tsk_other).

    End JLFP.

  End PossibleInterferingTasks.

  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.

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

    (* ... and any schedule. *)
    Context {num_cpus: nat}.
    Variable sched: schedule Job num_cpus.

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

    (* Consider any job j that incurs interference. *)
    Variable j: Job.

    (* Recall the definition of backlogged (pending and not scheduled). *)
    Let job_is_backlogged (t: time) := backlogged job_arrival job_cost sched j t.

    (* First, we define total interference. *)
    Section TotalInterference.

      (* The total interference incurred by job j during [t1, t2) is the
         cumulative time in which j is backlogged in this interval. *)

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

    End TotalInterference.

    (* Next, we define job interference. *)
    Section JobInterference.

      (* Let job_other be a job that interferes with j. *)
      Variable job_other: Job.

      (* The interference caused by job_other during [t1, t2) is the cumulative
         time in which j is backlogged while job_other is scheduled. *)

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

    End JobInterference.

    (* Next, we define task interference. *)
    Section TaskInterference.

      (* Consider any interfering task tsk_other. *)
      Variable tsk_other: sporadic_task.

      (* The interference caused by tsk during [t1, t2) is the cumulative time
         in which j is backlogged while tsk is scheduled. *)

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

    End TaskInterference.

    (* Next, we define an approximation of the total interference based on
       each per-task interference. *)

    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.

    (* Now we prove some basic lemmas about interference. *)
    Section BasicLemmas.

      (* Total interference cannot be larger than the considered time window. *)
      Lemma total_interference_le_delta :
         t1 t2,
          total_interference t1 t2 t2 - t1.

      (* Job interference is bounded by the service of the interfering job. *)
      Lemma job_interference_le_service :
         j_other t1 t2,
          job_interference j_other t1 t2 service_during sched j_other t1 t2.

      (* Task interference is bounded by the workload of the interfering task. *)
      Lemma task_interference_le_workload :
         tsk t1 t2,
          task_interference tsk t1 t2 workload job_task sched tsk t1 t2.

    End BasicLemmas.

    (* Now we prove some bounds on interference for sequential jobs. *)
    Section InterferenceNoParallelism.

      (* If jobs are sequential, ... *)
      Hypothesis H_sequential_jobs: sequential_jobs sched.

      (* ... then the interference incurred by a job in an interval
         of length delta is at most delta. *)

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

    End InterferenceNoParallelism.

    (* Next, we show that the cumulative per-task interference bounds the total
       interference. *)

    Section BoundUsingPerTaskInterference.

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

    End BoundUsingPerTaskInterference.

  End InterferenceDefs.

End Interference.