Library rt.model.basic.response_time
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.
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.