Library rt.analysis.basic.bertogna_fp_comp

Require Import rt.util.all.
Require Import rt.analysis.basic.bertogna_fp_theory.

Module ResponseTimeIterationFP.

  Import ResponseTimeAnalysisFP.

  (* In this section, we define the algorithm of Bertogna and Cirinei's
     response-time analysis for FP scheduling. *)

  Section Analysis.

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

    (* As input for each iteration of the algorithm, we consider pairs
       of tasks and computed response-time bounds. *)

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

    Context {Job: eqType}.
    Variable job_cost: Job time.
    Variable job_deadline: Job time.
    Variable job_task: Job sporadic_task.

    (* Consider a platform with num_cpus processors, ... *)
    Variable num_cpus: nat.

    (* ..., and priorities based on an FP policy. *)
    Variable higher_priority: FP_policy sporadic_task.

    (* Next we define the fixed-point iteration for computing
       Bertogna's response-time bound of a task set. *)

    (* First, given a sequence of pairs R_prev = <..., (tsk_hp, R_hp)> of
       response-time bounds for the higher-priority tasks, we define an
       iteration that computes the response-time bound of the current task:

           R_tsk (0) = task_cost tsk
           R_tsk (step + 1) =  f (R step),

       where f is the response-time recurrence, step is the number of iterations,
       and R_tsk (0) is the initial state. *)

    Definition per_task_rta (tsk: sporadic_task)
                            (R_prev: seq task_with_response_time) (step: nat) :=
      iter step
        (fun ttask_cost tsk +
                    (total_interference_bound_fp task_cost task_period tsk
                                                R_prev t higher_priority)
        (task_cost tsk).

    (* To ensure that the iteration converges, we will apply per_task_rta
       a "sufficient" number of times: task_deadline tsk - task_cost tsk + 1.
       This corresponds to the time complexity of the iteration. *)

    Definition max_steps (tsk: sporadic_task) := task_deadline tsk - task_cost tsk + 1.

    (* Next we compute the response-time bounds for the entire task set.
       Since high-priority tasks may not be schedulable, we allow the
       computation to fail.
       Thus, given the response-time bound of previous tasks, we either
       (a) append the computed response-time bound (tsk, R) of the current task
           to the list of pairs, or,
       (b) return None if the response-time analysis failed. *)

    Definition fp_bound_of_task hp_pairs tsk :=
      if hp_pairs is Some rt_bounds then
        let R := per_task_rta tsk rt_bounds (max_steps tsk) in
          if R task_deadline tsk then
            Some (rcons rt_bounds (tsk, R))
          else None
      else None.

    (* The response-time analysis for a given task set is defined
       as a left-fold (reduce) based on the function above.
       This either returns a list of task and response-time bounds, or None. *)

    Definition fp_claimed_bounds (ts: taskset_of sporadic_task) :=
      foldl fp_bound_of_task (Some [::]) ts.

    (* The schedulability test simply checks if we got a list of
       response-time bounds (i.e., if the computation did not fail). *)

    Definition fp_schedulable (ts: taskset_of sporadic_task) :=
      fp_claimed_bounds ts != None.

    (* In the following section, we prove several helper lemmas about the
       list of response-time bounds. The results seem trivial, but must be proven
       nonetheless since the list of response-time bounds is computed with
       a specific algorithm and there are no lemmas in the library for that. *)

    Section SimpleLemmas.

      (* First, we show that the first component of the computed list is the set of tasks. *)
      Lemma fp_claimed_bounds_unzip :
         ts hp_bounds,
          fp_claimed_bounds ts = Some hp_bounds
          unzip1 hp_bounds = ts.

      (* Next, we show that some properties of the analysis are preserved for the
         prefixes of the list: (a) the tasks do not change, (b) R <= deadline,
         (c) R is computed using the response-time equation, ... *)

      Lemma fp_claimed_bounds_rcons :
         ts' hp_bounds tsk1 tsk2 R,
          (fp_claimed_bounds (rcons ts' tsk1) = Some (rcons hp_bounds (tsk2, R))
           (fp_claimed_bounds ts' = Some hp_bounds
            tsk1 = tsk2
            R = per_task_rta tsk1 hp_bounds (max_steps tsk1)
            R task_deadline tsk1)).

      (* ..., which implies that any prefix of the computation is the computation
         of the prefix. *)

      Lemma fp_claimed_bounds_take :
         ts hp_bounds i,
          fp_claimed_bounds ts = Some hp_bounds
          i size hp_bounds
          fp_claimed_bounds (take i ts) = Some (take i hp_bounds).

      (* If the analysis suceeds, the computed response-time bounds are no larger
         than the deadlines ... *)

      Lemma fp_claimed_bounds_le_deadline :
         ts' rt_bounds tsk R,
          fp_claimed_bounds ts' = Some rt_bounds
          (tsk, R) \in rt_bounds
          R task_deadline tsk.

      (* ... and no smaller than the task costs. *)
      Lemma fp_claimed_bounds_ge_cost :
         ts' rt_bounds tsk R,
          fp_claimed_bounds ts' = Some rt_bounds
          (tsk, R) \in rt_bounds
          R task_cost tsk.

      (* Short lemma about unfolding the iteration one step. *)
      Lemma per_task_rta_fold :
         tsk rt_bounds,
          task_cost tsk +
           div_floor (total_interference_bound_fp task_cost task_period tsk rt_bounds
                     (per_task_rta tsk rt_bounds (max_steps tsk)) higher_priority) num_cpus
          = per_task_rta tsk rt_bounds (max_steps tsk).+1.

    End SimpleLemmas.

    (* In this section, we prove that if the task set is sorted by priority,
       the tasks in fp_claimed_bounds are interfering tasks.  *)

    Section HighPriorityTasks.

      (* Consider a list of previous tasks and a task tsk to be analyzed. *)
      Variable ts: taskset_of sporadic_task.

      (* Assume that the task set doesn't contain duplicates and is sorted by priority, ... *)
      Hypothesis H_task_set_is_a_set: uniq ts.
      Hypothesis H_task_set_is_sorted: sorted higher_priority ts.

      (* ...the priority order is strict (<), ...*)
      Hypothesis H_priority_irreflexive: irreflexive higher_priority.
      Hypothesis H_priority_transitive: transitive higher_priority.
      Hypothesis H_priority_antissymetric: antisymmetric higher_priority.

      (* ... and that the response-time analysis succeeds. *)
      Variable hp_bounds: seq task_with_response_time.
      Variable R: time.
      Hypothesis H_analysis_succeeds: fp_claimed_bounds ts = Some hp_bounds.

      (* Let's refer to tasks by index. *)
      Variable elem: sporadic_task.
      Let TASK := nth elem ts.

      (* Then, the tasks in the prefix of fp_claimed_bounds are exactly interfering tasks
         under FP scheduling.*)

      Lemma fp_claimed_bounds_interf:
          idx < size ts
          [seq tsk_hp <- ts | fp_can_interfere_with higher_priority (TASK idx) tsk_hp] = take idx ts.

    End HighPriorityTasks.

    (* In this section, we show that the fixed-point iteration converges. *)
    Section Convergence.

      (* Consider any set of higher-priority tasks. *)
      Variable ts_hp: taskset_of sporadic_task.

      (* Assume that the response-time analysis succeeds for the higher-priority tasks. *)
      Variable rt_bounds: seq task_with_response_time.
      Hypothesis H_test_succeeds: fp_claimed_bounds ts_hp = Some rt_bounds.

      (* Consider any task tsk to be analyzed, ... *)
      Variable tsk: sporadic_task.

      (* ... and assume all tasks have valid parameters. *)
      Hypothesis H_valid_task_parameters:
        valid_sporadic_taskset task_cost task_period task_deadline (rcons ts_hp tsk).

      (* To simplify, let f denote the fixed-point iteration. *)
      Let f := per_task_rta tsk rt_bounds.

      (* Assume that f (max_steps tsk) is no larger than the deadline. *)
      Hypothesis H_no_larger_than_deadline: f (max_steps tsk) task_deadline tsk.

      (* First, we show that f is monotonically increasing. *)
      Lemma bertogna_fp_comp_f_monotonic :
         x1 x2, x1 x2 f x1 f x2.

      (* If the iteration converged at an earlier step, it remains as a fixed point. *)
      Lemma bertogna_fp_comp_f_converges_early :
        ( k, k max_steps tsk f k = f k.+1)
        f (max_steps tsk) = f (max_steps tsk).+1.

      (* Else, we derive a contradiction. *)
      Section DerivingContradiction.

        (* Assume instead that the iteration continued to diverge. *)
        Hypothesis H_keeps_diverging:
            k max_steps tsk f k != f k.+1.

        (* By monotonicity, it follows that the value always increases. *)
        Lemma bertogna_fp_comp_f_increases :
            k max_steps tsk
            f k < f k.+1.

        (* In the end, the response-time bound must exceed the deadline. Contradiction! *)
        Lemma bertogna_fp_comp_rt_grows_too_much :
            k max_steps tsk
            f k > k + task_cost tsk - 1.

      End DerivingContradiction.

      (* Using the lemmas above, we prove the convergence of the iteration after max_steps. *)
      Lemma per_task_rta_converges:
        f (max_steps tsk) = f (max_steps tsk).+1.

    End Convergence.

    Section MainProof.

      (* Consider a task set ts. *)
      Variable ts: taskset_of sporadic_task.

      (* Assume that higher_priority is a total strict order (<).
         TODO: it doesn't have to be total over the universe of tasks,
         but only within the task set. However, to weaken this hypothesis
         we need to re-prove some lemmas from ssreflect. *)

      Hypothesis H_irreflexive: irreflexive higher_priority.
      Hypothesis H_transitive: transitive higher_priority.
      Hypothesis H_unique_priorities: antisymmetric higher_priority.
      Hypothesis H_total: total higher_priority.

      (* Assume the task set has no duplicates, ... *)
      Hypothesis H_ts_is_a_set: uniq ts.

      (* ...all tasks have valid parameters, ... *)
      Hypothesis H_valid_task_parameters:
        valid_sporadic_taskset task_cost task_period task_deadline ts.

      (* ...constrained deadlines, ...*)
      Hypothesis H_constrained_deadlines:
         tsk, tsk \in ts task_deadline tsk task_period tsk.

      (* ...and tasks are ordered by increasing priorities. *)
      Hypothesis H_sorted_ts: sorted higher_priority ts.

      (* Next, consider any arrival sequence such that...*)
      Context {arr_seq: arrival_sequence Job}.

     (* ...all jobs come from task set ts, ...*)
      Hypothesis H_all_jobs_from_taskset:
         (j: JobIn arr_seq), job_task j \in ts.

      (* have valid parameters,...*)
      Hypothesis H_valid_job_parameters:
         (j: JobIn arr_seq),
          valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.

      (* ... and satisfy the sporadic task model.*)
      Hypothesis H_sporadic_tasks:
        sporadic_task_model task_period arr_seq job_task.

      (* Then, consider any platform with at least one CPU such that...*)
      Variable sched: schedule num_cpus arr_seq.
      Hypothesis H_at_least_one_cpu : num_cpus > 0.

      (* only execute after they arrived and no 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 (as required by the workload bound). *)
      Hypothesis H_sequential_jobs: sequential_jobs sched.

      (* Assume that the scheduler is work-conserving and enforces the FP policy. *)
      Hypothesis H_work_conserving: work_conserving job_cost sched.
      Hypothesis H_enforces_FP_policy:
        enforces_FP_policy job_cost job_task sched higher_priority.

      Let no_deadline_missed_by_task (tsk: sporadic_task) :=
        task_misses_no_deadline job_cost job_deadline job_task sched tsk.
      Let no_deadline_missed_by_job :=
        job_misses_no_deadline job_cost job_deadline sched.
      Let response_time_bounded_by (tsk: sporadic_task) :=
        is_response_time_bound_of_task job_cost job_task tsk sched.

      (* In the following theorem, we prove that any response-time bound contained
         in fp_claimed_bounds is safe. The proof follows by induction on the task set:

           Induction hypothesis: assume all higher-priority tasks have safe response-time bounds.
           Inductive step: we prove that the response-time bound of the current task is safe.

         Note that the inductive step is a direct application of the main Theorem from
         bertogna_fp_theory.v. *)

      Theorem fp_analysis_yields_response_time_bounds :
         tsk R,
          (tsk, R) \In fp_claimed_bounds ts
          response_time_bounded_by tsk R.

      (* Therefore, if the schedulability test suceeds, ...*)
      Hypothesis H_test_succeeds: fp_schedulable ts.

      (*..., no task misses its deadline. *)
      Theorem taskset_schedulable_by_fp_rta :
         tsk, tsk \in ts no_deadline_missed_by_task tsk.

      (* For completeness, since all jobs of the arrival sequence
         are spawned by the task set, we also conclude that no job in
         the schedule misses its deadline. *)

      Theorem jobs_schedulable_by_fp_rta :
         (j: JobIn arr_seq), no_deadline_missed_by_job j.

    End MainProof.

  End Analysis.

End ResponseTimeIterationFP.