Library prosa.classic.analysis.global.jitter.bertogna_fp_theory

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.priority prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.schedule.global.workload prosa.classic.model.schedule.global.response_time
               prosa.classic.model.schedule.global.schedulability.
Require Import prosa.classic.model.schedule.global.jitter.job prosa.classic.model.schedule.global.jitter.interference
               prosa.classic.model.schedule.global.jitter.schedule prosa.classic.model.schedule.global.jitter.platform
               prosa.classic.model.schedule.global.jitter.constrained_deadlines.
Require Import prosa.classic.analysis.global.jitter.workload_bound
               prosa.classic.analysis.global.jitter.interference_bound_fp.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.

Module ResponseTimeAnalysisFP.

  Export JobWithJitter SporadicTaskset ScheduleOfSporadicTaskWithJitter
         Workload Interference Platform ConstrainedDeadlines Schedulability
         ResponseTime Priority TaskArrival WorkloadBoundJitter
         Interference InterferenceBoundFP.

  (* In this section, we prove that any fixed point in Bertogna and
     Cirinei's RTA for FP scheduling modified to account for jitter
     yields a safe response-time bound. This is an extension of the
     analysis found in Chapter 18.2 of Baruah et al.'s book
     Multiprocessor Scheduling for Real-time Systems. *)

  Section ResponseTimeBound.

    Context {sporadic_task: eqType}.
    Variable task_cost: sporadic_task time.
    Variable task_period: sporadic_task time.
    Variable task_deadline: sporadic_task time.
    Variable task_jitter: 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.
    Variable job_jitter: Job time.

    (* 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 job_arrival job_task arr_seq.
    Hypothesis H_valid_job_parameters:
       j,
        arrives_in arr_seq j
        valid_sporadic_job_with_jitter task_cost task_deadline task_jitter job_cost
                                       job_deadline job_task job_jitter j.

    (* Assume that we have a task set where all tasks have valid
       parameters and constrained deadlines, ... *)

    Variable ts: taskset_of sporadic_task.
    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.

    (* ... and that all jobs in the arrival sequence come from the task set. *)
    Hypothesis H_all_jobs_from_taskset:
       j,
        arrives_in arr_seq j job_task j \in ts.

    (* Next, consider any schedule of this arrival sequence 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.

    (* ...jobs are sequential, do not execute before the jitter
       has passed and nor longer than their execution costs. *)

    Hypothesis H_sequential_jobs: sequential_jobs sched.
    Hypothesis H_jobs_execute_after_jitter:
      jobs_execute_after_jitter job_arrival job_jitter sched.
    Hypothesis H_completed_jobs_dont_execute:
      completed_jobs_dont_execute job_cost sched.

    (* Assume that there exists at least one processor. *)
    Hypothesis H_at_least_one_cpu: num_cpus > 0.

    (* Consider a given FP policy, ... *)
    Variable higher_eq_priority: FP_policy sporadic_task.

    (* ...and assume that the schedule is work-conserving and respects this policy. *)
    Hypothesis H_work_conserving: work_conserving job_arrival job_cost job_jitter arr_seq sched.
    Hypothesis H_respects_priority:
      respects_FP_policy job_arrival job_cost job_task job_jitter arr_seq sched higher_eq_priority.

    (* Let's define some local names to avoid passing many parameters. *)
    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.

    (* Next, we consider the response-time recurrence.
       Let tsk be a task in ts that is to be analyzed. *)

    Variable tsk: sporadic_task.
    Hypothesis task_in_ts: tsk \in ts.

    (* Let is_hp_task denote whether a task is a higher-priority task
       (with respect to tsk). *)

    Let is_hp_task := higher_priority_task higher_eq_priority tsk.

    (* Assume a response-time bound is known... *)
    Let task_with_response_time := (sporadic_task × time)%type.
    Variable hp_bounds: seq task_with_response_time.
    Hypothesis H_response_time_of_interfering_tasks_is_known:
       hp_tsk R,
        (hp_tsk, R) \in hp_bounds
        response_time_bounded_by hp_tsk (task_jitter hp_tsk + R).

    (* ... for every higher-priority task. *)
    Hypothesis H_hp_bounds_has_interfering_tasks:
       hp_tsk,
        hp_tsk \in ts
        is_hp_task hp_tsk
         R,
          (hp_tsk, R) \in hp_bounds.

    (* Assume that the response-time bounds are larger than task costs. *)
    Hypothesis H_response_time_bounds_ge_cost:
       hp_tsk R,
        (hp_tsk, R) \in hp_bounds R task_cost hp_tsk.

    (* Assume that no deadline is missed by any higher-priority task. *)
    Hypothesis H_interfering_tasks_miss_no_deadlines:
       hp_tsk R,
        (hp_tsk, R) \in hp_bounds
        task_jitter hp_tsk + R task_deadline hp_tsk.

    (* Let R be the fixed point of Bertogna and Cirinei's recurrence, ...*)
    Variable R: time.
    Hypothesis H_response_time_recurrence_holds :
      R = task_cost tsk +
          div_floor
            (total_interference_bound_fp task_cost task_period task_jitter
                                         tsk hp_bounds R)
            num_cpus.

    (* ... and assume that jitter + R is no larger than the deadline of tsk.*)
    Hypothesis H_response_time_no_larger_than_deadline:
      task_jitter tsk + R task_deadline tsk.

    (* In order to prove that R is a response-time bound, we first provide some lemmas. *)
    Section Lemmas.

      (* Consider any job j of tsk. *)
      Variable j: Job.
      Hypothesis H_job_arrives: arrives_in arr_seq j.
      Hypothesis H_job_of_tsk: job_task j = tsk.

      (* Let t1 be the first point in time where j can actually be scheduled. *)
      Let t1 := job_arrival j + job_jitter j.

      (* Assume that job j is the first job of tsk not to complete by the response time bound. *)
      Hypothesis H_j_not_completed: ~~ completed job_cost sched j (t1 + R).
      Hypothesis H_previous_jobs_of_tsk_completed :
         j0,
          arrives_in arr_seq j0
          job_task j0 = tsk
          job_arrival j0 < job_arrival j
          completed job_cost sched j0 (job_arrival j0 + task_jitter tsk + R).

      (* Let's call x the interference incurred by job j due to tsk_other, ...*)
      Let x (tsk_other: sporadic_task) :=
        task_interference job_arrival job_cost job_task job_jitter sched j tsk_other t1 (t1 + R).

      (* ...and X the total interference incurred by job j due to any task. *)
      Let X := total_interference job_arrival job_cost job_jitter sched j t1 (t1 + R).

      (* Recall Bertogna and Cirinei's workload bound. *)
      Let workload_bound (tsk_other: sporadic_task) (R_other: time) :=
        W_jitter task_cost task_period task_jitter tsk_other R_other R.

      (* Let hp_tasks denote the set of higher-priority tasks. *)
      Let hp_tasks := [seq tsk_other <- ts | is_hp_task tsk_other].

      (* Now we establish results the higher-priority tasks. *)
      Section LemmasAboutHPTasks.

        (* Let (tsk_other, R_other) be any pair of higher-priority task and
           response-time bound computed in previous iterations. *)

        Variable tsk_other: sporadic_task.
        Variable R_other: time.
        Hypothesis H_response_time_of_tsk_other: (tsk_other, R_other) \in hp_bounds.

        (* Since tsk_other cannot interfere more than it executes, we show that
           the interference caused by tsk_other is no larger than workload bound W. *)

        Lemma bertogna_fp_workload_bounds_interference :
          x tsk_other workload_bound tsk_other R_other.

      End LemmasAboutHPTasks.

      (* Next we prove some lemmas that help to derive a contradiction.*)
      Section DerivingContradiction.

        (* 0) Since job j did not complete by its response time bound, it follows that
              the total interference X >= R - e_k + 1. *)

        Lemma bertogna_fp_too_much_interference : X R - task_cost tsk + 1.

        (* 1) Next, we prove that during the scheduling window of j, any job that is
              scheduled while j is backlogged comes from a different task.
              This follows from the fact that j is the first job not to complete
              by its response-time bound, so previous jobs of j's task must have
              completed by their periods and cannot be pending. *)

        Lemma bertogna_fp_interference_by_different_tasks :
           t j_other,
            t1 t < t1 + R
            arrives_in arr_seq j_other
            backlogged job_arrival job_cost job_jitter sched j t
            scheduled sched j_other t
            job_task j_other != tsk.

        (* Let's define a predicate to identify the other tasks that are scheduled. *)
        Let other_scheduled_task (t: time) (tsk_other: sporadic_task) :=
          task_is_scheduled job_task sched tsk_other t &&
          is_hp_task tsk_other.

        (* 2) Now we prove that, at all times that j is backlogged, the number
              of tasks other than tsk that are scheduled is exactly the number
              of processors in the system. This is required to prove lemma (3). *)

        Lemma bertogna_fp_all_cpus_are_busy:
           t,
            t1 t < t1 + R
            backlogged job_arrival job_cost job_jitter sched j t
            count (other_scheduled_task t) ts = num_cpus.

        (* 3) Now we prove that, at all times that j is backlogged, the number
              of tasks other than tsk that are scheduled is exactly the number
              of processors in the system. This is required to prove lemma (4). *)

        Lemma bertogna_fp_interference_on_all_cpus:
          \sum_(tsk_k <- hp_tasks) x tsk_k = X × num_cpus.

        (* Before stating the next lemma, let (num_tasks_exceeding delta) be the
           number of interfering tasks whose interference x is larger than delta. *)

        Let num_tasks_exceeding delta := count (fun ix i delta) (hp_tasks).

        (* 4) Now we prove that, for any delta, if (num_task_exceeding delta > 0), then the
              cumulative interference caused by the complementary set of interfering tasks fills
              the remaining, not-completely-full (num_cpus - num_tasks_exceeding delta)
              processors. *)

        Lemma bertogna_fp_interference_in_non_full_processors :
           delta,
            0 < num_tasks_exceeding delta < num_cpus
            \sum_(i <- hp_tasks | x i < delta) x i delta × (num_cpus - num_tasks_exceeding delta).

        (* 5) Based on lemma (4), we prove that, for any interval delta, if the sum of per-task
              interference exceeds (delta * num_cpus), the same applies for the
              sum of the minimum of the interference and delta. *)

        Lemma bertogna_fp_minimum_exceeds_interference :
           delta,
            \sum_(tsk_k <- hp_tasks) x tsk_k delta × num_cpus
               \sum_(tsk_k <- hp_tasks) minn (x tsk_k) delta
               delta × num_cpus.

        (* 6) Next, using lemmas (0), (3) and (5) we prove that the reduction-based
              interference bound is not enough to cover the sum of the minima over all tasks
              (artifact of the proof by contradiction). *)

        Lemma bertogna_fp_sum_exceeds_total_interference:
          \sum_((tsk_k, R_k) <- hp_bounds)
            minn (x tsk_k) (R - task_cost tsk + 1) >
          total_interference_bound_fp task_cost task_period task_jitter tsk hp_bounds R.

        (* 7) After concluding that the sum of the minima exceeds (R - e_i + 1),
              we prove that there exists a tuple (tsk_k, R_k) that satisfies
              min (x_k, R - e_i + 1) > min (W_k', R - e_i + 1).
              This implies that x_k > W_k', which is of course a contradiction,
              since W_k is a valid task interference bound. *)

        Lemma bertogna_fp_exists_task_that_exceeds_bound :
           tsk_k R_k,
            (tsk_k, R_k) \in hp_bounds
            (minn (x tsk_k) (R - task_cost tsk + 1) >
              minn (workload_bound tsk_k R_k) (R - task_cost tsk + 1)).

      End DerivingContradiction.

    End Lemmas.

    (* Using the lemmas above, we prove that R' bounds the response time of task tsk. *)
    Theorem bertogna_cirinei_response_time_bound_fp :
      response_time_bounded_by tsk (task_jitter tsk + R).

  End ResponseTimeBound.

End ResponseTimeAnalysisFP.