interference_bound_edf.v

Require Import Vbase task job task_arrival schedule platform interference
        workload workload_bound schedulability priority response_time
        bertogna_fp_theory util_divround util_lemmas
        ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.

  (* In the following section, we define Bertogna and Cirinei's
     EDF-specific per-task interference bound. *)
Module EDFSpecificBound.

  Import Job SporadicTaskset ScheduleOfSporadicTask Schedulability ResponseTime
         Priority SporadicTaskArrival Interference.

  Section EDFBoundDef.
    
    Context {sporadic_task: eqType}.
    Variable task_cost: sporadic_task -> nat.
    Variable task_period: sporadic_task -> nat.
    Variable task_deadline: sporadic_task -> nat.
    
    (* 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 EDFBoundDef.

  Section ProofInterferenceBound.

    Import Schedule Interference Platform SporadicTaskset.
    
    Context {sporadic_task: eqType}.
    Variable task_cost: sporadic_task -> nat.
    Variable task_period: sporadic_task -> nat.
    Variable task_deadline: sporadic_task -> nat.
    
    Context {Job: eqType}.
    Variable job_cost: Job -> nat.
    Variable job_deadline: Job -> nat.
    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:
      forall (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 do not execute in parallel and that
       there exists at least one processor. *)
    Hypothesis H_no_parallelism:
      jobs_dont_execute_in_parallel sched.
    Hypothesis H_at_least_one_cpu :
      num_cpus > 0.

    (* In order not to overcount job interference, we assume that
       jobs of the same task do not execute in parallel.
       Note that under EDF, this is equivalent to task precedence
       constraints.
       This is required because our proof uses a definition of
       interference based on the sum of the individual contributions
       of each job: I_total = I_j1 + I_j2 + ... *)
    Hypothesis H_no_intra_task_parallelism:
      jobs_of_same_task_dont_execute_in_parallel job_task sched.

    (* Assume that we have a task set where all tasks have valid
       parameters and restricted deadlines. *)
    Variable ts: taskset_of sporadic_task.
    Hypothesis all_jobs_from_taskset:
      forall (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_restricted_deadlines:
      forall 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 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. *)
    Let higher_eq_priority := @EDF Job arr_seq job_deadline. (* TODO: implicit params broken *)    
    Hypothesis H_global_scheduling_invariant:
      JLFP_JLDP_scheduling_invariant_holds job_cost num_cpus sched higher_eq_priority.

    (* 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 :
      forall (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.
      
      (* Identify the subset of jobs that actually cause interference *)
      Let interfering_jobs :=
        filter (fun (x: JobIn arr_seq) =>
                 (job_task x == tsk_k) && (job_interference job_cost sched j_i x t1 t2 != 0))
               (jobs_scheduled_between sched t1 t2).

      (* Let's give a simpler name to job interference. *)
      Let interference_caused_by := job_interference job_cost sched j_i.
      
      (* Now, consider the list of interfering jobs sorted by arrival time. *)
      Let order := fun (x y: JobIn arr_seq) => job_arrival x <= job_arrival y.
      Let sorted_jobs := (sort order 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.
        Proof.
          apply interference_eq_interference_joblist.
          
        Qed.

        (* 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.
        Proof.
          unfold interfering_jobs; rewrite big_filter.
          rewrite big_mkcond; rewrite [\sum_(_ <- _ | _) _]big_mkcond /=.
          apply eq_bigr; intros i _; clear -i.