Library rt.implementation.parallel.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.parallel.workload_bound
               rt.analysis.parallel.interference_bound_edf
               rt.analysis.parallel.bertogna_edf_comp.
Require Import rt.implementation.parallel.job
               rt.implementation.parallel.task
               rt.implementation.parallel.schedule
               rt.implementation.parallel.arrival_sequence.
From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.

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 := 6; task_deadline := 6|}.
    Let tsk2 := {| task_id := 2; task_cost := 3; task_period := 8; task_deadline := 6|}.
    Let tsk3 := {| task_id := 3; task_cost := 2; task_period := 12; task_deadline := 12|}.

    (* 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.
      Proof.
        intros tsk IN.
        repeat (move: IN ⇒ /orP [/eqP EQ | IN]; subst; compute); by done.
      Qed.

      Fact ts_has_constrained_deadlines:
        ∀ tsk,
          tsk ∈ ts →
          task_deadline tsk ≤ task_period tsk.
      Proof.
        intros tsk IN.
        repeat (move: IN ⇒ /orP [/eqP EQ | IN]; subst; compute); by done.
      Qed.

    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.
    Proof.
      unfold schedulability_test, edf_schedulable, edf_claimed_bounds; desf.
      apply negbT in Heq; move: Heq ⇒ /negP ALL.
      exfalso; apply ALL; clear ALL.
      assert (STEPS: \sum_(tsk <- ts) (task_deadline tsk - task_cost tsk) + 1 = 18).
      {
        by rewrite unlock; compute.
      } rewrite STEPS; clear STEPS.

      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; simpl;
        repeat rewrite addnE;
        repeat rewrite big_cons; repeat rewrite big_nil;
        repeat rewrite addnE; simpl;
        unfold num_cpus, divn; simpl.

      rewrite [edf_rta_iteration]lock; simpl.

      unfold locked at 18; destruct master_key; f.
      unfold locked at 17; destruct master_key; f.
      unfold locked at 16; destruct master_key; f.
      unfold locked at 15; destruct master_key; f.
      unfold locked at 14; destruct master_key; f.
      unfold locked at 13; destruct master_key; f.
      unfold locked at 12; destruct master_key; f.
      unfold locked at 11; destruct master_key; f.
      unfold locked at 10; destruct master_key; f.
      unfold locked at 9; destruct master_key; f.
      unfold locked at 8; destruct master_key; f.
      unfold locked at 7; destruct master_key; f.
      unfold locked at 6; destruct master_key; f.
      unfold locked at 5; destruct master_key; f.
      unfold locked at 4; destruct master_key; f.
      unfold locked at 3; destruct master_key; f.
      unfold locked at 2; destruct master_key; f.
      by unfold locked at 1; destruct master_key; f.
    Qed.

    (* 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 ∈ ts →
        no_deadline_missed_by tsk.
    Proof.
      intros tsk IN.
      have VALID := periodic_arrivals_valid_job_parameters ts ts_has_valid_parameters.
      have TSVALID := ts_has_valid_parameters.
      unfold valid_sporadic_job, valid_realtime_job in *; des.
      apply taskset_schedulable_by_edf_rta with (task_cost := task_cost) (task_period := task_period) (task_deadline := task_deadline) (ts0 := ts).
      - by apply ts_has_valid_parameters.
      - by apply ts_has_constrained_deadlines.
      - by apply periodic_arrivals_all_jobs_from_taskset.
      - by apply periodic_arrivals_valid_job_parameters, ts_has_valid_parameters.
      - by apply periodic_arrivals_are_sporadic.
      - by compute.
      - by apply scheduler_jobs_must_arrive_to_execute.
      - apply scheduler_completed_jobs_dont_execute; intro j'.
        -- by specialize (VALID j'); des.
        -- by apply periodic_arrivals_is_a_set.
      - by apply scheduler_work_conserving.
      - apply scheduler_enforces_policy.
        -- by apply EDF_is_transitive.
        -- by apply EDF_is_total.
      - by apply schedulability_test_succeeds.
      - by apply IN.
    Qed.

  End ExampleRTA.

End ResponseTimeAnalysisEDF.