Library rt.analysis.apa.bertogna_edf_comp

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

Module ResponseTimeIterationEDF.

  Import ResponseTimeAnalysisEDF.

  (* In this section, we define the algorithm corresponding to the APA-reduction
     of Bertogna and Cirinei's RTA 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.

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

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

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

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

    (* Assume that every task has a processor affinity alpha. *)
    Variable alpha: task_affinity sporadic_task num_cpus.

    (* For the reduction to subproblems, consider a subaffinity alpha' for each task. *)
    Variable alpha': task_affinity sporadic_task num_cpus.

    (* First, recall the interference bound under EDF. Note that we use
       subaffinity (alpha' tsk) when computing the set of interfering tasks. *)

    Let I (rt_bounds: seq task_with_response_time)
          (tsk: sporadic_task) (delta: time) :=
      total_interference_bound_edf task_cost task_period task_deadline alpha tsk
                                   (alpha' tsk) (* Subproblem alpha' *)
                                   rt_bounds delta.

    (* Then, we define the response-time recurrence. Note that we divide the
       interference by the cardinality of (alpha' tsk). *)

    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)
                                #|alpha' tsk|.

    (* 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 the
       response-time bound of each task. *)


    (* 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 :=
      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: seq sporadic_task) :=
      map (fun tsk(tsk, task_cost tsk)) 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: seq 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: seq 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: seq 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 sequence of tasks with valid parameters. *)
      Variable ts: seq 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,  
         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 = edf_response_time_bound rt_bounds tsk R.

    End Convergence.

    (* Now we prove the correctness of the response-time bounds. *)
    Section MainProof.

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

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

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

      (* Assume that alpha' is a non-empty subaffinity of alpha. *)
      Hypothesis H_non_empty_affinity:
         tsk, tsk \in ts #|alpha' tsk| > 0.
      Hypothesis H_subaffinity:
         tsk, tsk \in ts is_subaffinity (alpha' tsk) (alpha tsk).

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

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

      (* ...they have valid parameters,...*)
      Hypothesis H_valid_job_parameters:
         j,
          arrives_in arr_seq j
          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 job_arrival job_task arr_seq.

      (* Then, consider any schedule with at least one CPU such that...*)
      Variable sched: schedule Job num_cpus.
      Hypothesis H_jobs_come_from_arrival_sequence:
        jobs_come_from_arrival_sequence sched arr_seq.

      (* ...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 job_arrival sched.
      Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.

      (* ...and jobs are sequential. *)
      Hypothesis H_sequential_jobs: sequential_jobs sched.

      (* Assume a work-conserving APA scheduler that respects EDF policy. *)
      Hypothesis H_respects_affinity: respects_affinity job_task sched alpha.
      Hypothesis H_work_conserving: apa_work_conserving job_arrival job_cost job_task arr_seq
                                                        sched alpha.
      Hypothesis H_edf_policy:
        respects_JLFP_policy_under_weak_APA job_arrival job_cost job_task
                                            arr_seq sched alpha (EDF job_arrival job_deadline).

      (* To avoid a long list of parameters, we provide some local definitions. *)
      Definition no_deadline_missed_by_task (tsk: sporadic_task) :=
        task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched tsk.
      Definition no_deadline_missed_by_job :=
        job_misses_no_deadline job_arrival job_cost job_deadline sched.
      Let response_time_bounded_by (tsk: sporadic_task) :=
        is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched tsk.

      (* 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, arrives_in arr_seq j no_deadline_missed_by_job j.

    End MainProof.

  End Analysis.

End ResponseTimeIterationEDF.