Library prosa.classic.implementation.apa.bertogna_fp_example

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.task prosa.classic.model.priority.
Require Import prosa.classic.model.schedule.global.schedulability.
Require Import prosa.classic.model.schedule.global.basic.schedule.
Require Import prosa.classic.model.schedule.apa.affinity prosa.classic.model.schedule.apa.interference prosa.classic.model.schedule.apa.platform.
Require Import prosa.classic.analysis.apa.workload_bound
               prosa.classic.analysis.apa.interference_bound_fp
               prosa.classic.analysis.apa.bertogna_fp_comp.
Require Import prosa.classic.implementation.apa.job
               prosa.classic.implementation.apa.task
               prosa.classic.implementation.apa.schedule
               prosa.classic.implementation.apa.arrival_sequence.
From mathcomp Require Import ssreflect ssrbool ssrnat eqtype fintype seq bigop div.

Module ResponseTimeAnalysisFP.

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

  Section ExampleRTA.

    Let num_cpus := 2.

    Let cpu j := @Ordinal num_cpus j.

    Program Let alpha1 : affinity num_cpus :=
      (Build_set [:: cpu 0 _; cpu 1 _] _).

    Program Let alpha2 : affinity num_cpus :=
      (Build_set [:: cpu 0 _] _).

    Program Let alpha3 : affinity num_cpus :=
      (Build_set [:: cpu 1 _] _).

    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|}.

    Program Let ts := Build_set [:: tsk1; tsk2; tsk3] _.

    Section FactsAboutTaskset.

      Fact ts_non_empty_affinities:
        ∀ tsk,
          tsk \in ts → #|task_affinity tsk| > 0.

      Fact ts_has_valid_parameters:
        valid_sporadic_taskset task_cost task_period task_deadline ts.

      Fact ts_has_constrained_deadlines:
        ∀ tsk,
          tsk \in ts →
          task_deadline tsk ≤ task_period tsk.

    End FactsAboutTaskset.

    Let arr_seq := periodic_arrival_sequence ts.

    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.

    Let schedulability_test :=
      fp_schedulable (@task_cost _) (@task_period _) (@task_deadline _)
                     num_cpus (RM task_period) task_affinity
                     task_affinity.
    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 :=
      scheduler job_arrival job_cost job_task num_cpus arr_seq task_affinity higher_priority.

    Let no_deadline_missed_by :=
      task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched.

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

  End ExampleRTA.

End ResponseTimeAnalysisFP.