Library rt.implementation.apa.bertogna_fp_example

Require Import rt.util.all.
Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task rt.model.priority.
Require Import rt.model.schedule.global.schedulability.
Require Import rt.model.schedule.global.basic.schedule.
Require Import rt.model.schedule.apa.affinity rt.model.schedule.apa.interference rt.model.schedule.apa.platform.
Require Import rt.analysis.apa.workload_bound
               rt.analysis.apa.interference_bound_fp
               rt.analysis.apa.bertogna_fp_comp.
Require Import rt.implementation.apa.job
               rt.implementation.apa.task
               rt.implementation.apa.schedule
               rt.implementation.apa.arrival_sequence.

Module ResponseTimeAnalysisFP.

  Import Job Schedule SporadicTaskset Priority Schedulability Platform
         Interference InterferenceBoundFP WorkloadBound
         ResponseTimeIterationFP Affinity.
  Import ConcreteJob ConcreteTask ConcreteArrivalSequence ConcreteScheduler.

  (* In this section, we instantiate a simple example to show that the theorems
     contain no contradictory assumptions. *)

  Section ExampleRTA.

    (* Assume there are two processors. *)
    Let num_cpus := 2.

    (* Let (cpu j) denote the j-th processor *)
    Let cpu j := @Ordinal num_cpus j.

    (* Define alpha1 := {cpu 0, cpu 1} with the two processors. *)
    Program Let alpha1 : affinity num_cpus :=
      (Build_set [:: cpu 0 _; cpu 1 _] _).

    (* Define the singleton affinity alpha2 := {cpu 0}. *)
    Program Let alpha2 : affinity num_cpus :=
      (Build_set [:: cpu 0 _] _).

    (* Define the singleton affinity alpha3 := {cpu 1}. *)
    Program Let alpha3 : affinity num_cpus :=
      (Build_set [:: cpu 1 _] _).

    (* Now we create three tasks using the affinities above ... *)
    Let tsk1 := {| task_id := 1; task_cost := 3; task_period := 5;
                   task_deadline := 3; task_affinity := alpha1|}.
    Let tsk2 := {| task_id := 2; task_cost := 2; task_period := 6;
                   task_deadline := 5; task_affinity := alpha2|}.
    Let tsk3 := {| task_id := 3; task_cost := 2; task_period := 12;
                   task_deadline := 11; task_affinity := alpha3|}.

    (* ... and group these tasks into task set ts. *)
    Program Let ts := Build_set [:: tsk1; tsk2; tsk3] _.

    (* In this section, we let Coq compute a few properties about ts. *)
    Section FactsAboutTaskset.

      (* There are no empty affinities. *)
      Fact ts_non_empty_affinities:
         tsk,
          tsk \in ts #|task_affinity tsk| > 0.

      (* The tasks have valid parameters (e.g., cost > 0). *)
      Fact ts_has_valid_parameters:
        valid_sporadic_taskset task_cost task_period task_deadline ts.

      (* The task set has constrained deadlines. *)
      Fact ts_has_constrained_deadlines:
         tsk,
          tsk \in ts
          task_deadline tsk task_period tsk.

    End FactsAboutTaskset.

    (* Then, let arr_seq be the periodic arrival sequence from ts. *)
    Let arr_seq := periodic_arrival_sequence ts.

    (* Assume rate-monotonic priorities. *)
    Let higher_priority : JLDP_policy (@concrete_job_eqType num_cpus) :=
      FP_to_JLDP job_task (RM task_period).

    Section FactsAboutPriorityOrder.

      Lemma ts_has_unique_priorities :
        FP_is_antisymmetric_over_task_set (RM task_period) ts.

      Lemma priority_is_total :
        FP_is_total_over_task_set (RM task_period) ts.

    End FactsAboutPriorityOrder.

    (* Next, recall the FP RTA schedulability test for APA scheduling.
       Note that the task functions (from implementation/apa/task.v)
       require num_cpus as a parameter, so we leave a blank space so that
       can be inferred automatically. *)

    Let schedulability_test :=
      fp_schedulable (@task_cost _) (@task_period _) (@task_deadline _)
                     num_cpus (RM task_period) task_affinity
                     task_affinity. (* For simplicity, we use subaffinity alpha' = alpha. *)

    (* Now we show that the schedulability test returns true. *)
    Fact schedulability_test_succeeds :
      schedulability_test ts = true.
      Ltac f := unfold div_floor;
                rewrite !big_cons big_nil /= /higher_priority_task_in /=
                        /affinity_intersects !addn0 /= ?set_card ?divn1 ?addn0;
                unfold interference_bound_generic, W, max_jobs, div_floor;
                rewrite addn1 ?addn0.
        Ltac g :=
            rewrite /total_interference_bound_fp /interference_bound_generic
                    /W /max_jobs /div_floor !big_cons big_nil /= /higher_priority_task_in /=
                    /affinity_intersects.

    (* Let sched be the work-conserving RM APA scheduler. *)
    Let sched :=
      scheduler job_arrival job_cost job_task num_cpus arr_seq task_affinity higher_priority.

    (* Recall the definition of deadline miss. *)
    Let no_deadline_missed_by :=
      task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched.

    (* Next, we prove that ts is schedulable with the result of the test. *)
    Corollary ts_is_schedulable:
       tsk,
        tsk \in ts
        no_deadline_missed_by tsk.

  End ExampleRTA.

End ResponseTimeAnalysisFP.