Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.task_arrival prosa.classic.model.priority.
Require Import
Require Import
Require Import
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.

Module InterferenceBoundEDF.

  Import Job SporadicTaskset Schedule ScheduleOfSporadicTask Schedulability
         WorkloadBound ResponseTime Priority
         TaskArrival 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 RecallInterferenceBounds.

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

    (* Next we define the computation of the total interference for APA scheduling. *)
    Section TotalInterference.

      (* Let other_task denote tasks different from tsk. *)
      Let other_task := different_task tsk.

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

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

    End TotalInterference.

  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_arrival: Job time.
    Variable job_cost: Job time.
    Variable job_deadline: Job time.
    Variable job_task: Job sporadic_task.

    (* Assume any job arrival sequence... *)
    Variable arr_seq: arrival_sequence Job.

    (* ... in which jobs arrive sporadically and have valid parameters. *)
    Hypothesis H_sporadic_tasks:
      sporadic_task_model task_period job_arrival job_task arr_seq.
    Hypothesis H_valid_job_parameters:
        arrives_in arr_seq j
        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 Job num_cpus.
    Hypothesis H_jobs_come_from_arrival_sequence:
      jobs_come_from_arrival_sequence sched arr_seq.

    (* 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 job_arrival 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, arrives_in arr_seq j 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_arrival job_cost job_deadline job_task arr_seq sched tsk.
    Let response_time_bounded_by (tsk: sporadic_task) :=
      is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched tsk.

    (* Assume that the scheduler is a work-conserving EDF scheduler. *)
    Hypothesis H_work_conserving: work_conserving job_arrival job_cost arr_seq sched.
    Hypothesis H_edf_scheduler:
      respects_JLFP_policy job_arrival job_cost arr_seq sched (EDF job_arrival 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: Job.
    Hypothesis H_j_i_arrives: arrives_in arr_seq j_i.
    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 :
        arrives_in arr_seq j_k
        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_arrival 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_arrival job_cost sched j_i.

      (* Identify the subset of jobs that actually cause interference *)
      Let interfering_jobs :=
        filter (fun j'
                 (job_task j' == tsk_k) && (interference_caused_by j' 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 yjob_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 \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 \in sorted_jobs
            arrives_in arr_seq j
            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 \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

      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: Job.
        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 :
            arrives_in arr_seq j_fst
            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_arrival 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 :
              arrives_in arr_seq j_lst
              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.