Library prosa.classic.model.schedule.uni.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.uni.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

Module ResponseTime.

  Import UniprocessorSchedule SporadicTaskset TaskArrival.

  (* In this section, we define the notion of response-time bound. *)
  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.

    (* Consider any job arrival sequence... *)
    Variable arr_seq: arrival_sequence Job.

    (* ...and any uniprocessor schedule of these jobs. *)
    Variable sched: schedule Job.

    (* For simplicity, let's define some local names. *)
    Let job_has_completed_by := completed_by job_cost sched.

    Section Job.

      (* Given any job j, ... *)
      Variable j: Job.

      (* ...we say that R is a response-time bound of j in this schedule ... *)
      Variable R: time.

      (* ... iff j completes by (job_arrival j + R). *)
      Definition is_response_time_bound_of_job := job_has_completed_by j (job_arrival j + R).

    End Job.

    Section Task.

      (* Let tsk be any task that is to be analyzed. *)
      Variable tsk: sporadic_task.

      (* Then, we say that R is a response-time bound of tsk in this schedule ... *)
      Variable R: time.

      (* ... iff any job j of tsk in this arrival sequence has
         completed by (job_arrival j + R). *)

      Definition is_response_time_bound_of_task :=
         j,
          arrives_in arr_seq j
          job_task j = tsk
          is_response_time_bound_of_job j R.

      End Task.

  End ResponseTimeBound.

  (* In this section, we prove some basic lemmas about response-time bounds. *)
  Section BasicLemmas.

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

    (* Consider any job arrival sequence... *)
    Variable arr_seq: arrival_sequence Job.

    (* ...and any uniprocessor schedule of these jobs. *)
    Variable sched: schedule Job.

    (* Assume that jobs don't execute after completion. *)
    Hypothesis H_completed_jobs_dont_execute:
      completed_jobs_dont_execute job_cost sched.

    (* For simplicity, let's define some local names. *)
    Let response_time_bounded_by := is_response_time_bound_of_job job_arrival job_cost sched.

    (* We begin by proving lemmas about job response-time bounds. *)
    Section SpecificJob.

      (* Let j be any job... *)
      Variable j: Job.

      (* ...with response-time bound R. *)
      Variable R: time.
      Hypothesis response_time_bound: response_time_bounded_by j R.

      (* Then, the service received by j at any time t' after its response time is 0. *)
      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_by,
               completed_jobs_dont_execute in ×.
        apply/eqP; rewrite eqb0; apply/negP; intros CONTR.
        unfold response_time_bounded_by,is_response_time_bound_of_job in ×.
        eapply completion_monotonic in RT; eauto 2.
        apply completed_implies_not_scheduled in RT; eauto 2.
          by move: RT ⇒ /negP RT; apply:RT.
      Qed.

      (* The same applies for the cumulative service of job j. *)
      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; rewriteeq_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.

    (* Next, we prove properties about task response-time bounds. *)
    Section AllJobs.

      (* Consider any task tsk ...*)
      Variable tsk: sporadic_task.

      (* ... for which a response-time bound R is known. *)
      Variable R: time.
      Hypothesis response_time_bound:
        is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched tsk R.

      (* Then, for any job j of this task, ...*)
      Variable j: Job.
      Hypothesis H_from_arrival_sequence: arrives_in arr_seq j.
      Hypothesis H_job_of_task: job_task j = tsk.

      (* ...the service received by job j at any time t' after the response time is 0. *)
      Lemma service_after_task_rt_zero :
         t',
          t' job_arrival j + R
          service_at sched j t' = 0.
      Proof.
        intros t' LE.
        apply service_after_job_rt_zero with (R := R); last by done.
        by apply response_time_bound.
      Qed.

      (* The same applies for the cumulative service of job j. *)
      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 ResponseTime.