Library rt.model.basic.response_time

pan class="id" title="keyword">Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.task_arrival
               rt.model.basic.schedule.

(* Definition of response-time bound and some simple lemmas. *)
Module ResponseTime.

  Import Schedule SporadicTaskset SporadicTaskArrival.

  Section ResponseTimeBound.

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

    (* Given a task ...*)
    Variable tsk: sporadic_task.

    (* ... and a particular schedule, ...*)
    Context {num_cpus : nat}.
    Variable sched: schedule num_cpus arr_seq.

    (* ... R is a response-time bound of tsk in this schedule ... *)
    Variable R: time.

    Let job_has_completed_by := completed job_cost sched.

    (* ... 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: JobIn arr_seq),
        job_task j = tsk
        job_has_completed_by j (job_arrival j + R).

  End ResponseTimeBound.

  Section BasicLemmas.

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

    Context {arr_seq: arrival_sequence Job}.

    (* Consider any valid schedule... *)
    Context {num_cpus : nat}.
    Variable sched: schedule num_cpus arr_seq.

    Let job_has_completed_by := completed job_cost sched.

    (* ... where jobs dont execute after completion. *)
    Hypothesis H_completed_jobs_dont_execute:
      completed_jobs_dont_execute job_cost sched.

    Section SpecificJob.

      (* Then, for any job j ...*)
      Variable j: JobIn arr_seq.

      (* ...with response-time bound R in this schedule, ... *)
      Variable R: time.
      Hypothesis response_time_bound:
        job_has_completed_by j (job_arrival j + R).

      (* 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.

      (* 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.

    End SpecificJob.

    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_cost job_task tsk sched R.

      (* Then, for any job j of this task, ...*)
      Variable j: JobIn arr_seq.
      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.

      (* 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.

    End AllJobs.

  End BasicLemmas.

End ResponseTime.