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

Module ResponseTimeAnalysisEDF.

  Import Job Schedule SporadicTaskset Priority Schedulability Platform InterferenceBoundEDF WorkloadBound ResponseTimeIterationEDF.
  Import ConcreteJob ConcreteTask ConcreteArrivalSequence ConcreteScheduler.

  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. *)
    Let ts := [:: tsk1; tsk2; tsk3].

    Section FactsAboutTaskset.

      Fact ts_is_a_set: uniq ts.

      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.

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

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

    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.

    (* Let sched be the work-conserving EDF scheduler. *)
    Let sched := scheduler job_cost num_cpus arr_seq (EDF job_deadline).

    (* 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 \in ts →
        no_deadline_missed_by tsk.

  End ExampleRTA.

End ResponseTimeAnalysisEDF.