Library rt.implementation.apa.bertogna_edf_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_edf
               rt.analysis.apa.bertogna_edf_comp.
Require Import rt.implementation.apa.job
               rt.implementation.apa.task
               rt.implementation.apa.schedule
               rt.implementation.apa.arrival_sequence.

Module ResponseTimeAnalysisEDF.

  Import Job Schedule SporadicTaskset Priority Schedulability
         Affinity Platform InterferenceBoundEDF WorkloadBound
         Interference ResponseTimeIterationEDF.
  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.

    (* Next, recall the EDF 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 :=
      edf_schedulable (@task_cost _) (@task_period _)
                      (@task_deadline _) num_cpus task_affinity
                      task_affinity. (* For simplicity, we use subaffinity alpha' = alpha. *)

    (* Now, we guide Coq to compute the schedulability test function
       and show it returns true. *)

    Fact schedulability_test_succeeds :
      schedulability_test ts = true.
      Local Ltac f :=
        unfold edf_rta_iteration; simpl;
        unfold edf_response_time_bound, div_floor, total_interference_bound_edf, interference_bound_edf, interference_bound_generic, W, edf_specific_interference_bound, different_task_in, affinity_intersects; simpl;
        rewrite !addnE !set_card !big_cons ?big_nil /=.
      Local Ltac g := destruct master_key; f; simpl_exists_ord.

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

    (* Let sched be the weak APA EDF scheduler. *)
    Let sched := scheduler job_arrival job_cost job_task num_cpus arr_seq task_affinity
                           (JLFP_to_JLDP (EDF job_arrival job_deadline)).

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

    (* To show that the RTA works, we infer the schedulability of the task
       set from the result of the RTA procedure. *)

    Corollary ts_is_schedulable:
       tsk,
        tsk \in ts
        no_deadline_missed_by tsk.

  End ExampleRTA.

End ResponseTimeAnalysisEDF.