Library rt.implementation.basic.bertogna_fp_example

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

Module ResponseTimeAnalysisFP.

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

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

    Let tsk1 := {| task_id := 1; task_cost := 2; task_period := 5; task_deadline := 3|}.
    Let tsk2 := {| task_id := 2; task_cost := 4; task_period := 6; task_deadline := 5|}.
    Let tsk3 := {| task_id := 3; task_cost := 3; task_period := 12; task_deadline := 11|}.

    (* Let ts be a task set containing these three tasks (sorted by rate-monotonic priority). *)
    Program Let ts := Build_set [:: tsk1; tsk2; tsk3] _.

    Section FactsAboutTaskset.

      Fact ts_has_valid_parameters:
        valid_sporadic_taskset task_cost task_period task_deadline ts.

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

    End FactsAboutTaskset.

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

    (* Recall the FP RTA schedulability test. *)
    Let schedulability_test :=
      fp_schedulable task_cost task_period task_deadline num_cpus.

    (* Now we show that the schedulability test returns true. *)
    Fact schedulability_test_succeeds :
      schedulability_test ts = true.

    (* 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 arr_seq :=
      (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 sched be the work-conserving RM scheduler. *)
    Let sched := scheduler job_cost num_cpus arr_seq higher_priority.

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

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

  End ExampleRTA.

End ResponseTimeAnalysisFP.