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.
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.
Variable sched: schedule Job.
Let job_has_completed_by := completed_by job_cost sched.
Section Job.
Variable j: Job.
Variable R: time.
Definition is_response_time_bound_of_job := job_has_completed_by j (job_arrival j + R).
End Job.
Section Task.
Variable tsk: sporadic_task.
Variable R: time.
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.
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.
Variable arr_seq: arrival_sequence Job.
Variable sched: schedule Job.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Let response_time_bounded_by := is_response_time_bound_of_job job_arrival job_cost sched.
Section SpecificJob.
Variable j: Job.
Variable R: time.
Hypothesis response_time_bound: response_time_bounded_by j R.
Lemma service_after_job_rt_zero :
∀ t',
t' ≥ job_arrival j + R →
service_at sched j t' = 0.
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.
Variable tsk: sporadic_task.
Variable R: time.
Hypothesis response_time_bound:
is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched tsk R.
Variable j: Job.
Hypothesis H_from_arrival_sequence: 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.
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 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.
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.
Variable sched: schedule Job.
Let job_has_completed_by := completed_by job_cost sched.
Section Job.
Variable j: Job.
Variable R: time.
Definition is_response_time_bound_of_job := job_has_completed_by j (job_arrival j + R).
End Job.
Section Task.
Variable tsk: sporadic_task.
Variable R: time.
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.
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.
Variable arr_seq: arrival_sequence Job.
Variable sched: schedule Job.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Let response_time_bounded_by := is_response_time_bound_of_job job_arrival job_cost sched.
Section SpecificJob.
Variable j: Job.
Variable R: time.
Hypothesis response_time_bound: response_time_bounded_by j R.
Lemma service_after_job_rt_zero :
∀ t',
t' ≥ job_arrival j + R →
service_at sched j t' = 0.
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.
Variable tsk: sporadic_task.
Variable R: time.
Hypothesis response_time_bound:
is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched tsk R.
Variable j: Job.
Hypothesis H_from_arrival_sequence: 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.
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.