Library rt.implementation.jitter.bertogna_edf_example

Require Import rt.util.all.
Require Import rt.model.jitter.job rt.model.jitter.task
               rt.model.jitter.schedule rt.model.jitter.schedulability
               rt.model.jitter.priority rt.model.jitter.platform.
Require Import rt.analysis.jitter.workload_bound
               rt.analysis.jitter.interference_bound_edf
               rt.analysis.jitter.bertogna_edf_comp.
Require Import rt.implementation.jitter.job
               rt.implementation.jitter.task
               rt.implementation.jitter.schedule
               rt.implementation.jitter.arrival_sequence.

Module ResponseTimeAnalysisEDF.

  Import JobWithJitter ScheduleWithJitter SporadicTaskset Priority Schedulability Platform InterferenceBoundEDFJitter WorkloadBoundJitter ResponseTimeIterationEDF.
  Import ConcreteJob ConcreteTask ConcreteArrivalSequence ConcreteScheduler.

  Section ExampleRTA.

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

    (* Let ts be a task set containing these three tasks. *)
    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 EDF RTA schedulability test. *)
    Let schedulability_test :=
      edf_schedulable task_cost task_period task_deadline task_jitter 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 job_jitter 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 ∈ ts →
        no_deadline_missed_by tsk.

  End ExampleRTA.

End ResponseTimeAnalysisEDF.