Library rt.analysis.basic.interference_bound_edf

Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
               rt.model.basic.task_arrival rt.model.basic.platform rt.model.basic.response_time
               rt.model.basic.workload rt.model.basic.priority rt.model.basic.schedulability
               rt.model.basic.interference rt.model.basic.interference_edf.
Require Import rt.analysis.basic.workload_bound rt.analysis.basic.interference_bound.

Module InterferenceBoundEDF.

  Import Job SporadicTaskset Schedule ScheduleOfSporadicTask Schedulability
         WorkloadBound ResponseTime Priority
         SporadicTaskArrival Interference InterferenceEDF.
  Export InterferenceBoundGeneric.

  (* In this section, we define Bertogna and Cirinei's EDF-specific
     interference bound. *)

  Section SpecificBoundDef.

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

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

    (* Consider the interference incurred by tsk in a window of length delta... *)
    Variable delta: time.

    (* ... due to a different task tsk_other, with response-time bound R_other. *)
    Variable tsk_other: sporadic_task.
    Variable R_other: time.

    (* Bertogna and Cirinei define the following bound for task interference
       under EDF scheduling. *)

    Definition edf_specific_interference_bound :=
      let d_tsk := task_deadline tsk in
      let e_other := task_cost tsk_other in
      let p_other := task_period tsk_other in
      let d_other := task_deadline tsk_other in
        (div_floor d_tsk p_other) × e_other +
        minn e_other ((d_tsk %% p_other) - (d_other - R_other)).

  End SpecificBoundDef.

  (* Next, we define the total interference bound for EDF, which combines the generic
     and the EDF-specific bounds. *)

  Section TotalInterferenceBoundEDF.

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

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

    Let task_with_response_time := (sporadic_task × time)%type.

    (* Assume a known response-time bound for each interfering task ... *)
    Variable R_prev: seq task_with_response_time.

    (* ... and an interval length delta. *)
    Variable delta: time.

    Section PerTask.

      Variable tsk_R: task_with_response_time.
      Let tsk_other := fst tsk_R.
      Let R_other := snd tsk_R.

      (* By combining Bertogna's interference bound for a work-conserving
         scheduler ... *)

      Let basic_interference_bound := interference_bound_generic task_cost task_period tsk delta tsk_R.

      (* ... with and EDF-specific interference bound, ... *)
      Let edf_specific_bound := edf_specific_interference_bound task_cost task_period task_deadline tsk tsk_other R_other.

      (* ... Bertogna and Cirinei define the following interference bound
         under EDF scheduling. *)

      Definition interference_bound_edf :=
        minn basic_interference_bound edf_specific_bound.

    End PerTask.

    Section AllTasks.

      Let interferes_with_tsk := jldp_can_interfere_with tsk.

      (* The total interference incurred by tsk is bounded by the sum
         of individual task interferences. *)

      Definition total_interference_bound_edf :=
        \sum_((tsk_other, R_other) <- R_prev | interferes_with_tsk tsk_other)
           interference_bound_edf (tsk_other, R_other).

    End AllTasks.

  End TotalInterferenceBoundEDF.

  (* In this section, we show that the EDF-specific interference bound is safe. *)
  Section ProofSpecificBound.

    Import Schedule Interference Platform SporadicTaskset.

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

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

    (* ... in which jobs arrive sporadically and have valid parameters. *)
    Hypothesis H_sporadic_tasks:
      sporadic_task_model task_period arr_seq job_task.
    Hypothesis H_valid_job_parameters:
       (j: JobIn arr_seq),
        valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.

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

    (* ...jobs do not execute before their arrival times nor longer
       than their execution costs. *)

    Hypothesis H_jobs_must_arrive_to_execute:
      jobs_must_arrive_to_execute sched.
    Hypothesis H_completed_jobs_dont_execute:
      completed_jobs_dont_execute job_cost sched.

    (* Also assume that jobs are sequential and that there exists at
       least one processor. *)

    Hypothesis H_sequential_jobs: sequential_jobs sched.
    Hypothesis H_at_least_one_cpu: num_cpus > 0.

    (* Consider a task set ts where all jobs come from the task set
       and tasks have valid parameters and constrained deadlines. *)

    Variable ts: taskset_of sporadic_task.
    Hypothesis all_jobs_from_taskset:
       (j: JobIn arr_seq), job_task j \in ts.
    Hypothesis H_valid_task_parameters:
      valid_sporadic_taskset task_cost task_period task_deadline ts.
    Hypothesis H_constrained_deadlines:
       tsk, tsk \in ts task_deadline tsk task_period tsk.

    Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
      task_misses_no_deadline job_cost job_deadline job_task sched tsk.
    Let response_time_bounded_by (tsk: sporadic_task) :=
      is_response_time_bound_of_task job_cost job_task tsk sched.

    (* Assume that the scheduler is a work-conserving EDF scheduler. *)
    Hypothesis H_work_conserving: work_conserving job_cost sched.
    Hypothesis H_edf_scheduler:
      enforces_JLDP_policy job_cost sched (EDF job_deadline).

    (* Let tsk_i be the task to be analyzed, ...*)
    Variable tsk_i: sporadic_task.
    Hypothesis H_tsk_i_in_task_set: tsk_i \in ts.

    (* ... and j_i one of its jobs. *)
    Variable j_i: JobIn arr_seq.
    Hypothesis H_job_of_tsk_i: job_task j_i = tsk_i.

    (* Let tsk_k denote any interfering task, ... *)
    Variable tsk_k: sporadic_task.
    Hypothesis H_tsk_k_in_task_set: tsk_k \in ts.

    (* ...and R_k its response-time bound. *)
    Variable R_k: time.
    Hypothesis H_R_k_le_deadline: R_k task_deadline tsk_k.

    (* Consider a time window of length delta <= D_i, starting with j_i's arrival time. *)
    Variable delta: time.
    Hypothesis H_delta_le_deadline: delta task_deadline tsk_i.

    (* Assume that the jobs of tsk_k satisfy the response-time bound before the end of the interval *)
    Hypothesis H_all_previous_jobs_completed_on_time :
       (j_k: JobIn arr_seq),
        job_task j_k = tsk_k
        job_arrival j_k + R_k < job_arrival j_i + delta
        completed job_cost sched j_k (job_arrival j_k + R_k).

    (* In this section, we prove that Bertogna and Cirinei's EDF interference bound
       indeed bounds the interference caused by task tsk_k in the interval
[t1, t1 + delta). *)
    Section MainProof.

      (* Let's call x the task interference incurred by job j due to tsk_k. *)
      Let x :=
        task_interference job_cost job_task sched j_i tsk_k
                          (job_arrival j_i) (job_arrival j_i + delta).

      (* Also, recall the EDF-specific interference bound for EDF. *)
      Let interference_bound :=
        edf_specific_interference_bound task_cost task_period task_deadline tsk_i tsk_k R_k.

      (* Let's simplify the names a bit. *)
      Let t1 := job_arrival j_i.
      Let t2 := job_arrival j_i + delta.
      Let D_i := task_deadline tsk_i.
      Let D_k := task_deadline tsk_k.
      Let p_k := task_period tsk_k.

      Let n_k := div_floor D_i p_k.

      (* Let's give a simpler name to job interference. *)
      Let interference_caused_by := job_interference job_cost sched j_i.

      (* Identify the subset of jobs that actually cause interference *)
      Let interfering_jobs :=
        filter (fun (x: JobIn arr_seq) ⇒
                 (job_task x == tsk_k) && (interference_caused_by x t1 t2 != 0))
               (jobs_scheduled_between sched t1 t2).

      (* Now, consider the list of interfering jobs sorted by arrival time. *)
      Let earlier_arrival := fun (x y: JobIn arr_seq) ⇒ job_arrival x job_arrival y.
      Let sorted_jobs := (sort earlier_arrival interfering_jobs).

      (* Now we proceed with the proof. The first step consists in simplifying the sum corresponding to the workload. *)
      Section SimplifyJobSequence.

        (* Use the alternative definition of task interference, based on
           individual job interference. *)

        Lemma interference_bound_edf_use_another_definition :
          x \sum_(j <- jobs_scheduled_between sched t1 t2 | job_task j == tsk_k)
                interference_caused_by j t1 t2.

        (* Remove the elements that we don't care about from the sum *)
        Lemma interference_bound_edf_simpl_by_filtering_interfering_jobs :
          \sum_(j <- jobs_scheduled_between sched t1 t2 | job_task j == tsk_k)
             interference_caused_by j t1 t2 =
          \sum_(j <- interfering_jobs) interference_caused_by j t1 t2.

        (* Then, we consider the sum over the sorted sequence of jobs. *)
        Lemma interference_bound_edf_simpl_by_sorting_interfering_jobs :
          \sum_(j <- interfering_jobs) interference_caused_by j t1 t2 =
           \sum_(j <- sorted_jobs) interference_caused_by j t1 t2.

        (* Note that both sequences have the same set of elements. *)
        Lemma interference_bound_edf_job_in_same_sequence :
           j, (j \in interfering_jobs) = (j \in sorted_jobs).

        (* Also recall that all jobs in the sorted sequence is an interfering job of tsk_k, ... *)
        Lemma interference_bound_edf_all_jobs_from_tsk_k :
           j,
            j \in sorted_jobs
            job_task j = tsk_k
            interference_caused_by j t1 t2 != 0
            j \in jobs_scheduled_between sched t1 t2.

        (* ...and consecutive jobs are ordered by arrival. *)
        Lemma interference_bound_edf_jobs_ordered_by_arrival :
           i elem,
            i < (size sorted_jobs).-1
            earlier_arrival (nth elem sorted_jobs i) (nth elem sorted_jobs i.+1).

        (* Finally, for any job of task tsk_k, the interference is bounded by the task cost. *)
        Lemma interference_bound_edf_interference_le_task_cost :
           j,
            j \in interfering_jobs
            interference_caused_by j t1 t2 task_cost tsk_k.

      End SimplifyJobSequence.

      (* Next, we show that if the number of jobs is no larger than n_k,
         the workload bound trivially holds. *)

      Section InterferenceFewJobs.

        Hypothesis H_few_jobs: size sorted_jobs n_k.

        Lemma interference_bound_edf_holds_for_at_most_n_k_jobs :
           \sum_(j <- sorted_jobs) interference_caused_by j t1 t2
             interference_bound.
      End InterferenceFewJobs.

      (* Otherwise, assume that the number of jobs is larger than n_k >= 0. *)
      Section InterferenceManyJobs.

        Hypothesis H_many_jobs: n_k < size sorted_jobs.

        (* This trivially implies that there's at least one job. *)
        Lemma interference_bound_edf_at_least_one_job: size sorted_jobs > 0.

        (* Let j_fst be the first job, and a_fst its arrival time. *)
        Variable elem: JobIn arr_seq.
        Let j_fst := nth elem sorted_jobs 0.
        Let a_fst := job_arrival j_fst.

        (* In this section, we prove some basic lemmas about j_fst. *)
        Section FactsAboutFirstJob.

          (* The first job is an interfering job of task tsk_k. *)
          Lemma interference_bound_edf_j_fst_is_job_of_tsk_k :
            job_task j_fst = tsk_k
            interference_caused_by j_fst t1 t2 != 0
            j_fst \in jobs_scheduled_between sched t1 t2.

          (* The deadline of j_fst is the deadline of tsk_k. *)
          Lemma interference_bound_edf_j_fst_deadline :
            job_deadline j_fst = task_deadline tsk_k.

          (* The deadline of j_i is the deadline of tsk_i. *)
          Lemma interference_bound_edf_j_i_deadline :
            job_deadline j_i = task_deadline tsk_i.

          (* If j_fst completes by its response-time bound, then t1 <= a_fst + R_k,
             where t1 is the beginning of the time window (arrival of j_i). *)

          Lemma interference_bound_edf_j_fst_completion_implies_rt_bound_inside_interval :
            completed job_cost sched j_fst (a_fst + R_k)
            t1 a_fst + R_k.

        End FactsAboutFirstJob.

        (* Now, let's prove the interference bound for the particular case of a single job.
           This case must be solved separately because the single job can simultaneously
           be carry-in and carry-out job, so its response time is not necessarily
           bounded by R_k (from the hypothesis H_all_previous_jobs_completed_on_time). *)

        Section InterferenceSingleJob.

          (* Assume that there's at least one job in the sorted list. *)
          Hypothesis H_only_one_job: size sorted_jobs = 1.

          (* Since there's only one job, we simplify the terms in the interference bound. *)
          Lemma interference_bound_edf_simpl_when_there's_one_job :
            D_i %% p_k - (D_k - R_k) = D_i - (D_k - R_k).

          (* Next, we show that if j_fst completes by its response-time bound R_k,
             then then interference bound holds. *)

          Section ResponseTimeOfSingleJobBounded.

            Hypothesis H_j_fst_completed_by_rt_bound :
              completed job_cost sched j_fst (a_fst + R_k).

            Lemma interference_bound_edf_holds_for_single_job_that_completes_on_time :
              job_interference job_cost sched j_i j_fst t1 t2 D_i - (D_k - R_k).

          End ResponseTimeOfSingleJobBounded.

          (* Else, if j_fst did not complete by its response-time bound, then
             we need a separate proof. *)

          Section ResponseTimeOfSingleJobNotBounded.

            Hypothesis H_j_fst_not_complete_by_rt_bound :
              ~~ completed job_cost sched j_fst (a_fst + R_k).

            (* This trivially implies that a_fst + R_k lies after the end of the interval,
               otherwise j_fst would have completed by its response-time bound. *)

            Lemma interference_bound_edf_response_time_bound_of_j_fst_after_interval :
              job_arrival j_fst + R_k job_arrival j_i + delta.

            (* If the slack is too big (D_i < D_k - R_k), j_fst causes no interference. *)
            Lemma interference_bound_edf_holds_for_single_job_with_big_slack :
              D_i < D_k - R_k
              interference_caused_by j_fst t1 t2 = 0.

            (* Else, if the slack is small, j_fst causes interference for no longer than
               D_i - (D_k - R_k). *)

            Lemma interference_bound_edf_holds_for_single_job_with_small_slack :
              D_i D_k - R_k
              interference_caused_by j_fst t1 t2 D_i - (D_k - R_k).

          End ResponseTimeOfSingleJobNotBounded.

          (* By combining the results above, we prove that the interference caused by the single job
             is bounded by D_i - (D_k - R_k), ... *)

          Lemma interference_bound_edf_interference_of_j_fst_limited_by_slack :
            interference_caused_by j_fst t1 t2 D_i - (D_k - R_k).

          (* ... and thus the interference bound holds. *)
          Lemma interference_bound_edf_holds_for_a_single_job :
            interference_caused_by j_fst t1 t2 interference_bound.

        End InterferenceSingleJob.

        (* Next, consider the other case where there are at least two jobs:
           the first job j_fst, and the last job j_lst. *)

        Section InterferenceTwoOrMoreJobs.

          (* Assume there are at least two jobs. *)
          Variable num_mid_jobs: nat.
          Hypothesis H_at_least_two_jobs : size sorted_jobs = num_mid_jobs.+2.

          (* Let j_lst be the last job of the sequence and a_lst its arrival time. *)
          Let j_lst := nth elem sorted_jobs num_mid_jobs.+1.
          Let a_lst := job_arrival j_lst.

          (* In this section, we prove some basic lemmas about the first and last jobs. *)
          Section FactsAboutFirstAndLastJobs.

            (* The last job is an interfering job of task tsk_k. *)
            Lemma interference_bound_edf_j_lst_is_job_of_tsk_k :
              job_task j_lst = tsk_k
              interference_caused_by j_lst t1 t2 != 0
              j_lst \in jobs_scheduled_between sched t1 t2.

            (* The deadline of j_lst is the deadline of tsk_k. *)
            Lemma interference_bound_edf_j_lst_deadline :
              job_deadline j_lst = task_deadline tsk_k.

            (* The first job arrives before the last job. *)
            Lemma interference_bound_edf_j_fst_before_j_lst :
              job_arrival j_fst job_arrival j_lst.

            (* The last job arrives before the end of the interval. *)
            Lemma interference_bound_edf_last_job_arrives_before_end_of_interval :
              job_arrival j_lst < t2.

            (* Since there are multiple jobs, j_fst is far enough from the end of
               the interval that its response-time bound is valid
               (by the assumption H_all_previous_jobs_completed_on_time). *)

            Lemma interference_bound_edf_j_fst_completed_on_time :
              completed job_cost sched j_fst (a_fst + R_k).

          End FactsAboutFirstAndLastJobs.

          (* Next, we prove that the distance between the first and last jobs is at least
             num_mid_jobs + 1 periods. *)

          Lemma interference_bound_edf_many_periods_in_between :
            a_lst - a_fst num_mid_jobs.+1 × p_k.

          (* Using the lemma above, we prove that the ratio n_k is at least the number of
             middle jobs + 1, ... *)

          Lemma interference_bound_edf_n_k_covers_middle_jobs_plus_one :
            n_k num_mid_jobs.+1.

          (* ... which allows bounding the interference of the middle and last jobs
             using n_k multiplied by the cost. *)

          Lemma interference_bound_edf_holds_for_middle_and_last_jobs :
            interference_caused_by j_lst t1 t2 +
              \sum_(0 i < num_mid_jobs)
                interference_caused_by (nth elem sorted_jobs i.+1) t1 t2
             n_k × task_cost tsk_k.

          (* Now, since n_k < sorted_jobs = num_mid_jobs + 2, it follows that
             n_k = num_mid_jobs + 1. *)

          Lemma interference_bound_edf_n_k_equals_num_mid_jobs_plus_one :
            n_k = num_mid_jobs.+1.

          (* After proving the bounds of the middle and last jobs, we do the same for
             the first job. This requires a different proof in order to exploit the slack. *)

          Section InterferenceOfFirstJob.

            (* As required by the next lemma, in order to move (D_i % p_k) to the left of
               the inequality (<=), we must show that it is no smaller than the slack. *)

            Lemma interference_bound_edf_remainder_ge_slack :
              D_k - R_k D_i %% p_k.

            (* To conclude that the interference bound holds, it suffices to show that
               this reordered inequality holds. *)

            Lemma interference_bound_edf_simpl_by_moving_to_left_side :
              interference_caused_by j_fst t1 t2 + (D_k - R_k) + D_i %/ p_k × p_k D_i
              interference_caused_by j_fst t1 t2 D_i %% p_k - (D_k - R_k).

            (* Next, we prove that interference caused by j_fst is bounded by the length
               of the interval 
[t1, a_fst + R_k), ... *)
            Lemma interference_bound_edf_interference_of_j_fst_bounded_by_response_time :
               interference_caused_by j_fst t1 t2 \sum_(t1 t < a_fst + R_k) 1.

            (* ..., which leads to the following bounds based on interval lengths. *)
            Lemma interference_bound_edf_bounding_interference_with_interval_lengths :
              interference_caused_by j_fst t1 t2 + (D_k - R_k) + D_i %/ p_k × p_k
              \sum_(t1 t < a_fst + R_k) 1
              + \sum_(a_fst + R_k t < a_fst + D_k) 1
              + \sum_(a_fst + D_k t < a_lst + D_k) 1.

            (* To conclude, we show that the concatenation of these interval lengths equals
               (a_lst + D_k) - 1, ... *)

            Lemma interference_bound_edf_simpl_by_concatenation_of_intervals :
              \sum_(t1 t < a_fst + R_k) 1
              + \sum_(a_fst + R_k t < a_fst + D_k) 1
              + \sum_(a_fst + D_k t < a_lst + D_k) 1 = (a_lst + D_k) - t1.

            (* ... which results in proving that (a_lst + D_k) - t1 <= D_i.
               This holds because high-priority jobs have earlier deadlines. Therefore,
               the interference caused by the first job is bounded by D_i % p_k - (D_k - R_k). *)

            Lemma interference_bound_edf_interference_of_j_fst_limited_by_remainder_and_slack :
              interference_caused_by j_fst t1 t2 D_i %% p_k - (D_k - R_k).

          End InterferenceOfFirstJob.

          (* Using the lemmas above we show that the interference bound works in the
             case of two or more jobs. *)

          Lemma interference_bound_edf_holds_for_multiple_jobs :
            \sum_(0 i < num_mid_jobs.+2)
              interference_caused_by (nth elem sorted_jobs i) t1 t2 interference_bound.

        End InterferenceTwoOrMoreJobs.

      End InterferenceManyJobs.

      Theorem interference_bound_edf_bounds_interference :
        x interference_bound.

    End MainProof.

  End ProofSpecificBound.

  (* As required by the proof of convergence of EDF RTA, we show that the
     EDF-specific bound is monotonically increasing with both the size
     of the interval and the value of the previous response-time bounds. *)

  Section MonotonicitySpecificBound.

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

    Variable tsk tsk_other: sporadic_task.
    Hypothesis H_period_positive: task_period tsk_other > 0.

    Variable delta delta' R R': time.
    Hypothesis H_delta_monotonic: delta delta'.
    Hypothesis H_response_time_monotonic: R R'.
    Hypothesis H_cost_le_rt_bound: task_cost tsk_other R.

    Lemma interference_bound_edf_monotonic :
      interference_bound_edf task_cost task_period task_deadline tsk delta (tsk_other, R)
      interference_bound_edf task_cost task_period task_deadline tsk delta' (tsk_other, R').

  End MonotonicitySpecificBound.

End InterferenceBoundEDF.