Library rt.analysis.global.basic.workload_bound

Require Import rt.util.all.
Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.task_arrival.
Require Import rt.model.schedule.global.workload rt.model.schedule.global.response_time
               rt.model.schedule.global.schedulability.
Require Import rt.model.schedule.global.basic.schedule.

Module WorkloadBound.

  Import Job SporadicTaskset Schedule ScheduleOfSporadicTask TaskArrival ResponseTime Schedulability Workload.

  Section WorkloadBoundDef.

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

    (* Consider any task tsk with response-time bound R_tsk,
       that is scheduled in an interval of length delta. *)

    Variable tsk: sporadic_task.
    Variable R_tsk: time.
    Variable delta: time.

    (* Based on the number of jobs that execute completely in the interval, ... *)
    Definition max_jobs :=
      div_floor (delta + R_tsk - task_cost tsk) (task_period tsk).

    (* ... Bertogna and Cirinei's workload bound is defined as follows. *)
    Definition W :=
      let e_k := (task_cost tsk) in
      let p_k := (task_period tsk) in
        minn e_k (delta + R_tsk - e_k - max_jobs × p_k) + max_jobs × e_k.

  End WorkloadBoundDef.

  Section BasicLemmas.

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

    (* Let tsk be any task...*)
    Variable tsk: sporadic_task.

    (* ... with period > 0. *)
    Hypothesis H_period_positive: task_period tsk > 0.

    (* Let R1 <= R2 be two response-time bounds that
       are larger than the cost of the tsk. *)

    Variable R1 R2: time.
    Hypothesis H_R_lower_bound: R1 task_cost tsk.
    Hypothesis H_R1_le_R2: R1 R2.

    Let workload_bound := W task_cost task_period tsk.

    (* Then, Bertogna and Cirinei's workload bound is monotonically increasing. *)
    Lemma W_monotonic :
       t1 t2,
        t1 t2
        workload_bound R1 t1 workload_bound R2 t2.

  End BasicLemmas.

  Section ProofWorkloadBound.

    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_task: Job sporadic_task.
    Variable job_deadline: Job time.

    Variable arr_seq: arrival_sequence Job.

    (* Assume that all jobs have valid parameters *)
    Hypothesis H_jobs_have_valid_parameters :
       j,
        arrives_in arr_seq j
        valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.

    (* Consider any schedule. *)
    Context {num_cpus: nat}.
    Variable sched: schedule Job num_cpus.
    Hypothesis H_jobs_come_from_arrival_sequence:
      jobs_come_from_arrival_sequence sched arr_seq.

    (* Assumption: jobs only execute if they arrived.
       This is used to eliminate jobs that arrive after end of the interval t1 + delta. *)

    Hypothesis H_jobs_must_arrive_to_execute:
      jobs_must_arrive_to_execute job_arrival sched.

    (* Assumption: jobs do not execute after they completed.
       This is used to eliminate jobs that complete before the start of the interval t1. *)

    Hypothesis H_completed_jobs_dont_execute:
      completed_jobs_dont_execute job_cost sched.

    (* Assumption: Jobs are sequential.
       This is required to use interval lengths as a measure of service. *)

    Hypothesis H_sequential_jobs: sequential_jobs sched.

    (* Assumption: sporadic task model.
       This is necessary to conclude that consecutive jobs ordered by arrival times
       are separated by at least 'period' times units. *)

    Hypothesis H_sporadic_tasks: sporadic_task_model task_period job_arrival job_task arr_seq.

    (* Before starting the proof, let's give simpler names to the definitions. *)
    Let job_has_completed_by := completed job_cost sched.

    Let workload_of (tsk: sporadic_task) (t1 t2: time) :=
      workload job_task sched tsk t1 t2.

    (* Now we define the theorem. Let tsk be any task in the taskset. *)
    Variable tsk: sporadic_task.

    (* Assumption: the task must have valid parameters:
         a) period > 0 (used in divisions)
         b) deadline of the jobs = deadline of the task
         c) cost <= period
            (used to prove that the distance between the first and last
             jobs is at least (cost + n*period), where n is the number
             of middle jobs. If cost >> period, the claim does not hold
             for every task set. *)

    Hypothesis H_valid_task_parameters:
      is_valid_sporadic_task task_cost task_period task_deadline tsk.

    (* Assumption: the task must have a constrained deadline.
       This is required to prove that n_k (max_jobs) from Bertogna
       and Cirinei's formula accounts for at least the number of
       middle jobs (i.e., number of jobs - 2 in the worst case). *)

    Hypothesis H_constrained_deadline: task_deadline tsk task_period tsk.

    (* Consider an interval [t1, t1 + delta). *)
    Variable t1 delta: time.

    (* Assume that a response-time bound R_tsk for that task in any
       schedule of this processor platform is also given, ... *)

    Variable R_tsk: time.

    Hypothesis H_response_time_bound :
       j,
        arrives_in arr_seq j
        job_task j = tsk
        job_arrival j + R_tsk < t1 + delta
        job_has_completed_by j (job_arrival j + R_tsk).

    (* ... such that R_tsk >= task_cost tsk and R_tsk <= task_deadline tsk. *)
    Hypothesis H_response_time_ge_cost: R_tsk task_cost tsk.
    Hypothesis H_no_deadline_miss: R_tsk task_deadline tsk.

    Section MainProof.

      (* In this section, we prove that the workload of a task in the
         interval [t1, t1 + delta) is bounded by W. *)


      (* Let's simplify the names a bit. *)
      Let t2 := t1 + delta.
      Let n_k := max_jobs task_cost task_period tsk R_tsk delta.
      Let workload_bound := W task_cost task_period tsk R_tsk delta.

      (* Since we only care about the workload of tsk, we restrict
         our view to the set of jobs of tsk scheduled in [t1, t2). *)

      Let scheduled_jobs :=
        jobs_of_task_scheduled_between job_task sched tsk t1 t2.

      (* Now, let's 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 scheduled_jobs.

      (* The first step consists in simplifying the sum corresponding
         to the workload. *)

      Section SimplifyJobSequence.

        (* After switching to the definition of workload based on a list
           of jobs, we show that sorting the list preserves the sum. *)

        Lemma workload_bound_simpl_by_sorting_scheduled_jobs :
          workload_joblist job_task sched tsk t1 t2 =
           \sum_(i <- sorted_jobs) service_during sched i t1 t2.

        (* Remember that both sequences have the same set of elements *)
        Lemma workload_bound_job_in_same_sequence :
           j,
            (j \in scheduled_jobs) = (j \in sorted_jobs).

        (* Remember that all jobs in the sorted sequence is an
           interfering job of task tsk. *)

        Lemma workload_bound_all_jobs_from_tsk :
           j_i,
            j_i \in sorted_jobs
            arrives_in arr_seq j_i
            job_task j_i = tsk
            service_during sched j_i t1 t2 != 0
            j_i \in jobs_scheduled_between sched t1 t2.

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

      End SimplifyJobSequence.

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

      Section WorkloadNotManyJobs.

        Lemma workload_bound_holds_for_at_most_n_k_jobs :
          size sorted_jobs n_k
          \sum_(i <- sorted_jobs) service_during sched i t1 t2
            workload_bound.

      End WorkloadNotManyJobs.

      (* Otherwise, assume that the number of jobs is larger than n_k >= 0.
         First, consider the simple case with only one job. *)

      Section WorkloadSingleJob.

        (* Assume that there's at least one job in the sorted list. *)
        Hypothesis H_at_least_one_job: size sorted_jobs > 0.

        Variable elem: Job.
        Let j_fst := nth elem sorted_jobs 0.

        (* The first job is an interfering job of task tsk. *)
        Lemma workload_bound_j_fst_is_job_of_tsk :
          arrives_in arr_seq j_fst
          job_task j_fst = tsk
          service_during sched j_fst t1 t2 != 0
          j_fst \in jobs_scheduled_between sched t1 t2.

        (* The workload bound holds for the single job. *)
        Lemma workload_bound_holds_for_a_single_job :
          \sum_(0 i < 1) service_during sched (nth elem sorted_jobs i) t1 t2
          workload_bound.

      End WorkloadSingleJob.

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

      Section WorkloadTwoOrMoreJobs.

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

        Variable elem: Job.
        Let j_fst := nth elem sorted_jobs 0.
        Let j_lst := nth elem sorted_jobs num_mid_jobs.+1.

        (* The last job is an interfering job of task tsk. *)
        Lemma workload_bound_j_lst_is_job_of_tsk :
          arrives_in arr_seq j_lst
          job_task j_lst = tsk
          service_during sched j_lst t1 t2 != 0
          j_lst \in jobs_scheduled_between sched t1 t2.

        (* The response time of the first job must fall inside the interval. *)
        Lemma workload_bound_response_time_of_first_job_inside_interval :
          t1 job_arrival j_fst + R_tsk.

        (* The arrival of the last job must also fall inside the interval. *)
        Lemma workload_bound_last_job_arrives_before_end_of_interval :
          job_arrival j_lst < t2.

        (* Next, we upper-bound the service of the first and last jobs using their arrival times. *)
        Lemma workload_bound_service_of_first_and_last_jobs :
          service_during sched j_fst t1 t2 +
          service_during sched j_lst t1 t2
            (job_arrival j_fst + R_tsk - t1) + (t2 - job_arrival j_lst).

        (* Simplify the expression from the previous lemma. *)
        Lemma workload_bound_simpl_expression_with_first_and_last :
          job_arrival j_fst + R_tsk - t1 + (t2 - job_arrival j_lst) =
                       delta + R_tsk - (job_arrival j_lst - job_arrival j_fst).

        (* Bound the service of the middle jobs. *)
        Lemma workload_bound_service_of_middle_jobs :
          \sum_(0 i < num_mid_jobs)
            service_during sched (nth elem sorted_jobs i.+1) t1 t2
            num_mid_jobs × task_cost tsk.

        (* Conclude that the distance between first and last is at least num_mid_jobs + 1 periods. *)
        Lemma workload_bound_many_periods_in_between :
          job_arrival j_lst - job_arrival j_fst num_mid_jobs.+1 × (task_period tsk).

        (* Prove that n_k is at least the number of the middle jobs *)
        Lemma workload_bound_n_k_covers_middle_jobs :
          n_k num_mid_jobs.

        (* If n_k = num_mid_jobs, then the workload bound holds. *)
        Lemma workload_bound_n_k_equals_num_mid_jobs :
          num_mid_jobs = n_k
          service_during sched j_lst t1 t2 +
            service_during sched j_fst t1 t2 +
            \sum_(0 i < num_mid_jobs)
             service_during sched (nth elem sorted_jobs i.+1) t1 t2
           workload_bound.

        (* If n_k = num_mid_jobs + 1, then the workload bound holds. *)
        Lemma workload_bound_n_k_equals_num_mid_jobs_plus_1 :
          num_mid_jobs.+1 = n_k
          service_during sched j_lst t1 t2 +
            service_during sched j_fst t1 t2 +
            \sum_(0 i < num_mid_jobs)
             service_during sched (nth elem sorted_jobs i.+1) t1 t2
           workload_bound.

      End WorkloadTwoOrMoreJobs.

      (* Using the lemmas above, we prove the main theorem about the workload bound. *)
      Theorem workload_bounded_by_W :
        workload_of tsk t1 (t1 + delta) workload_bound.

    End MainProof.

  End ProofWorkloadBound.

End WorkloadBound.