Library prosa.classic.model.schedule.global.response_time

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.schedule.global.basic.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

Module ResponseTime.

  Import Schedule SporadicTaskset TaskArrival.

  Section ResponseTimeBound.

    Context {sporadic_task: eqType}.
    Context {Job: eqType}.
    Variable job_arrival: Job → time.
    Variable job_cost: Job → time.
    Variable job_task: Job → sporadic_task.

    Variable arr_seq: arrival_sequence Job.

    Context {num_cpus : nat}.
    Variable sched: schedule Job num_cpus.

    Let job_has_completed_by := completed job_cost sched.

    Section Definitions.

      Variable tsk: sporadic_task.

      Variable R: time.

      Definition is_response_time_bound_of_task :=
        ∀ j,
          arrives_in arr_seq j →
          job_task j = tsk →
          job_has_completed_by j (job_arrival j + R).

    End Definitions.

    Section BasicLemmas.

      Hypothesis H_completed_jobs_dont_execute:
        completed_jobs_dont_execute job_cost sched.

      Section SpecificJob.

        Variable j: Job.
        Hypothesis H_j_arrives: arrives_in arr_seq j.

        Variable R: time.
        Hypothesis response_time_bound:
          job_has_completed_by j (job_arrival j + R).

        Lemma service_after_job_rt_zero :
          ∀ t',
            t' ≥ job_arrival j + R →
            service_at sched j t' = 0.
        Proof.
          rename response_time_bound into RT,
                 H_completed_jobs_dont_execute into EXEC; ins.
          unfold is_response_time_bound_of_task, completed,
                 completed_jobs_dont_execute in ×.
          apply/eqP; rewrite -leqn0.
          eapply completion_monotonic in RT; eauto 2.
          apply completed_implies_not_scheduled in RT; eauto 2.
            by move: RT; rewrite not_scheduled_no_service; move ⇒ /eqP RT; rewrite RT.
        Qed.

        Lemma cumulative_service_after_job_rt_zero :
          ∀ t' t'',
            t' ≥ job_arrival j + R →
            \sum_(t' ≤ t < t'') service_at sched j t = 0.
        Proof.
          ins; apply/eqP; rewrite -leqn0.
          rewrite big_nat_cond; rewrite → eq_bigr with (F2 := fun i ⇒ 0);
            first by rewrite big_const_seq iter_addn mul0n addn0 leqnn.
          intro i; rewrite andbT; move ⇒ /andP [LE _].
          by rewrite service_after_job_rt_zero;
            [by ins | by apply leq_trans with (n := t')].
        Qed.

      End SpecificJob.

      Section AllJobs.

        Variable tsk: sporadic_task.

        Variable R: time.
        Hypothesis response_time_bound:
          is_response_time_bound_of_task tsk R.

        Variable j: Job.
        Hypothesis H_j_arrives: arrives_in arr_seq j.
        Hypothesis H_job_of_task: job_task j = tsk.

        Lemma service_after_task_rt_zero :
          ∀ t',
            t' ≥ job_arrival j + R →
            service_at sched j t' = 0.
        Proof.
          by ins; apply service_after_job_rt_zero with (R := R); [apply response_time_bound |].
        Qed.

        Lemma cumulative_service_after_task_rt_zero :
          ∀ t' t'',
            t' ≥ job_arrival j + R →
            \sum_(t' ≤ t < t'') service_at sched j t = 0.
        Proof.
          by ins; apply cumulative_service_after_job_rt_zero with (R := R);
            first by apply response_time_bound.
        Qed.

      End AllJobs.

    End BasicLemmas.

  End ResponseTimeBound.

End ResponseTime.