Library rt.analysis.basic.bertogna_edf_comp

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

Module ResponseTimeIterationEDF.

  Import ResponseTimeAnalysisEDF.

  (* In this section, we define the algorithm for Bertogna and Cirinei's
     response-time analysis for EDF 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.

    (* First, recall the interference bound under EDF, ... *)
    Let I (rt_bounds: seq task_with_response_time)
          (tsk: sporadic_task) (delta: time) :=
      total_interference_bound_edf task_cost task_period task_deadline tsk rt_bounds delta.

    (* ..., which yields the following response-time bound. *)
    Definition edf_response_time_bound (rt_bounds: seq task_with_response_time)
                                           (tsk: sporadic_task) (delta: time) :=
      task_cost tsk + div_floor (I rt_bounds tsk delta) num_cpus.

    (* Also note that a response-time is only valid if it is no larger
       than the deadline. *)

    Definition R_le_deadline (pair: task_with_response_time) :=
      let (tsk, R) := pair in
        R task_deadline tsk.

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


    (* Given a sequence 'rt_bounds' of task and response-time bounds
       from the previous iteration, we compute the response-time
       bound of a single task using the RTA for EDF. *)

    Definition update_bound (rt_bounds: seq task_with_response_time)
                        (pair : task_with_response_time) :=
      let (tsk, R) := pair in
        (tsk, edf_response_time_bound rt_bounds tsk R).

    (* To compute the response-time bounds of the entire task set,
       We start the iteration with a sequence of tasks and costs:
       <(task1, cost1), (task2, cost2), ...>. *)

    Let initial_state (ts: taskset_of sporadic_task) :=
      map (fun t(t, task_cost t)) ts.

    (* Then, we successively update the the response-time bounds based
       on the slack computed in the previous iteration. *)

    Definition edf_rta_iteration (rt_bounds: seq task_with_response_time) :=
      map (update_bound rt_bounds) rt_bounds.

    (* To ensure that the procedure converges, we stop the iteration
       after a "sufficient" number of times, which corresponds to
       the time complexity of the procedure. *)

    Let max_steps (ts: taskset_of sporadic_task) :=
      \sum_(tsk <- ts) (task_deadline tsk - task_cost tsk) + 1.

    (* This yields the following definition for the RTA. At the end
       we check if all computed response-time bounds are less than
       or equal to the deadline, in which case they are valid. *)

    Definition edf_claimed_bounds (ts: taskset_of sporadic_task) :=
      let R_values := iter (max_steps ts) edf_rta_iteration (initial_state ts) in
        if (all R_le_deadline R_values) then
          Some R_values
        else None.

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

    Definition edf_schedulable (ts: taskset_of sporadic_task) :=
      edf_claimed_bounds ts != None.

    (* In the following section, we prove several helper lemmas about the
       list of tasks/response-time bounds. *)

    Section SimpleLemmas.

      (* Updating a single response-time bound does not modify the task. *)
      Lemma edf_claimed_bounds_unzip1_update_bound :
         l rt_bounds,
          unzip1 (map (update_bound rt_bounds) l) = unzip1 l.

      (* At any point of the iteration, the tasks are the same. *)
      Lemma edf_claimed_bounds_unzip1_iteration :
         l k,
          unzip1 (iter k edf_rta_iteration (initial_state l)) = l.

      (* The iteration preserves the size of the list. *)
      Lemma edf_claimed_bounds_size :
         l k,
          size (iter k edf_rta_iteration (initial_state l)) = size l.

      (* If the analysis succeeds, the computed response-time bounds are no smaller
         than the task cost. *)

      Lemma edf_claimed_bounds_ge_cost :
         l k tsk R,
          (tsk, R) \in (iter k edf_rta_iteration (initial_state l))
          R task_cost tsk.

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

      Lemma edf_claimed_bounds_le_deadline :
         ts rt_bounds tsk R,
          edf_claimed_bounds ts = Some rt_bounds
          (tsk, R) \in rt_bounds
          R task_deadline tsk.

      (* The list contains a response-time bound for every task in the task set. *)
      Lemma edf_claimed_bounds_has_R_for_every_task :
         ts rt_bounds tsk,
          edf_claimed_bounds ts = Some rt_bounds
          tsk \in ts
           R, (tsk, R) \in rt_bounds.

    End SimpleLemmas.

    (* In this section, we prove the convergence of the RTA procedure.
       Since we define the RTA procedure as the application of a function
       a fixed number of times, this translates into proving that the value
       of the iteration at (max_steps ts) is equal to the value at (max_steps ts) + 1. *)

    Section Convergence.

      (* Consider any valid task set. *)
      Variable ts: taskset_of sporadic_task.
      Hypothesis H_valid_task_parameters:
        valid_sporadic_taskset task_cost task_period task_deadline ts.

      (* To simplify, let f denote the RTA procedure. *)
      Let f (k: nat) := iter k edf_rta_iteration (initial_state ts).

      (* Since the iteration is applied directly to a list of tasks and response-times,
         we define a corresponding relation "<=" over those lists. *)


      (* Let 'all_le' be a binary relation over lists of tasks/response-time bounds.
         It states that every element of list l1 has a response-time bound R that is less
         than or equal to the corresponding response-time bound R' in list l2 (point-wise).
         In addition, the relation states that the tasks of both lists are unchanged. *)

      Let all_le := fun (l1 l2: list task_with_response_time) ⇒
        (unzip1 l1 == unzip1 l2) &&
        all (fun p(snd (fst p)) (snd (snd p))) (zip l1 l2).

      (* Similarly, we define a strict version of 'all_le' called 'one_lt', which states that
         there exists at least one element whose response-time bound increases. *)

      Let one_lt := fun (l1 l2: list task_with_response_time) ⇒
        (unzip1 l1 == unzip1 l2) &&
        has (fun p(snd (fst p)) < (snd (snd p))) (zip l1 l2).

      (* Next, we prove some basic properties about the relation all_le. *)
      Section RelationProperties.

        (* The relation is reflexive, ... *)
        Lemma all_le_reflexive : reflexive all_le.

        (* ... and transitive. *)
        Lemma all_le_transitive: transitive all_le.

        (* At any step of the iteration, the corresponding list
           is larger than or equal to the initial state. *)

        Lemma bertogna_edf_comp_iteration_preserves_minimum :
           step, all_le (initial_state ts) (f step).

        (* The application of the function is inductive. *)
        Lemma bertogna_edf_comp_iteration_inductive (P : seq task_with_response_time Type) :
          P (initial_state ts)
          ( k, P (f k) P (f (k.+1)))
          P (f (max_steps ts)).

        (* As a last step, we show that edf_rta_iteration preserves order, i.e., for any
           list l1 no smaller than the initial state, and list l2 such that
           l1 <= l2, we have (edf_rta_iteration l1) <= (edf_rta_iteration l2). *)

        Lemma bertogna_edf_comp_iteration_preserves_order :
           l1 l2,
            all_le (initial_state ts) l1
            all_le l1 l2
            all_le (edf_rta_iteration l1) (edf_rta_iteration l2).

        (* It follows from the properties above that the iteration is monotonically increasing. *)
        Lemma bertogna_edf_comp_iteration_monotonic: k, all_le (f k) (f k.+1).

      End RelationProperties.

      (* Knowing that the iteration is monotonically increasing (with respect to all_le),
         we show that the RTA procedure converges to a fixed point. *)


      (* First, note that when there are no tasks, the iteration trivially converges. *)
      Lemma bertogna_edf_comp_f_converges_with_no_tasks :
        size ts = 0
        f (max_steps ts) = f (max_steps ts).+1.

      (* Otherwise, if the iteration reached a fixed point before (max_steps ts), then
         the value at (max_steps ts) is still at a fixed point. *)

      Lemma bertogna_edf_comp_f_converges_early :
        ( k, k max_steps ts f k = f k.+1)
        f (max_steps ts) = f (max_steps ts).+1.

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

        (* Assume that there are tasks. *)
        Hypothesis H_at_least_one_task: size ts > 0.

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

        (* Since the iteration is monotonically increasing, it must be
           strictly increasing. *)

        Lemma bertogna_edf_comp_f_increases :
           k,
            k max_steps ts one_lt (f k) (f k.+1).

        (* In the end, each response-time bound is so high that the sum
           of all response-time bounds exceeds the sum of all deadlines.
           Contradiction! *)

        Lemma bertogna_edf_comp_rt_grows_too_much :
           k,
            k max_steps ts
            \sum_((tsk, R) <- f k) (R - task_cost tsk) + 1 > k.

      End DerivingContradiction.

      (* Using the lemmas above, we prove that edf_rta_iteration reaches
         a fixed point after (max_steps ts) step, ... *)

      Lemma edf_claimed_bounds_finds_fixed_point_of_list :
         rt_bounds,
          edf_claimed_bounds ts = Some rt_bounds
          valid_sporadic_taskset task_cost task_period task_deadline ts
          f (max_steps ts) = edf_rta_iteration (f (max_steps ts)).

      (* ...and since there cannot be a vector of response-time bounds with values less than
         the task costs, this solution is also the least fixed point. *)

      Lemma edf_claimed_bounds_finds_least_fixed_point :
         v,
          all_le (initial_state ts) v
          v = edf_rta_iteration v
          all_le (f (max_steps ts)) v.

      (* Therefore, with regard to the response-time bound recurrence, ...*)
      Let rt_recurrence (tsk: sporadic_task) (rt_bounds: seq task_with_response_time) (R: time) :=
        task_cost tsk + div_floor (I rt_bounds tsk R) num_cpus.

      (* ..., the individual response-time bounds (elements of the list) are also fixed points. *)
      Theorem edf_claimed_bounds_finds_fixed_point_for_each_bound :
         tsk R rt_bounds,
          edf_claimed_bounds ts = Some rt_bounds
          (tsk, R) \in rt_bounds
          R = rt_recurrence tsk rt_bounds R.

    End Convergence.

    Section MainProof.

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

      (* 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.

      (* 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.

      (* ...they 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.

      (* ...jobs 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. *)
      Hypothesis H_sequential_jobs: sequential_jobs sched.

      (* Assume a work-conserving scheduler with EDF policy. *)
      Hypothesis H_work_conserving: work_conserving job_cost sched.
      Hypothesis H_edf_policy: enforces_JLDP_policy job_cost sched (EDF job_deadline).

      Definition no_deadline_missed_by_task (tsk: sporadic_task) :=
        task_misses_no_deadline job_cost job_deadline job_task sched tsk.
      Definition 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 edf_claimed_bounds is safe. The proof follows by direct application of
         the main Theorem from bertogna_edf_theory.v. *)

      Theorem edf_analysis_yields_response_time_bounds :
         tsk R,
          (tsk, R) \In edf_claimed_bounds ts
          response_time_bounded_by tsk R.

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

      (*... no task misses its deadline. *)
      Theorem taskset_schedulable_by_edf_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 conclude that no job misses
         its deadline. *)

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

    End MainProof.

  End Analysis.

End ResponseTimeIterationEDF.