Commit eb877428 authored by Felipe Cerqueira's avatar Felipe Cerqueira

Use the definition names from the paper

parent 8d6b42b6
......@@ -867,8 +867,8 @@ Module ResponseTimeIterationEDF.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
(* ...restricted deadlines, ...*)
Hypothesis H_restricted_deadlines:
(* ...constrained deadlines, ...*)
Hypothesis H_constrained_deadlines:
forall tsk, tsk \in ts -> task_deadline tsk <= task_period tsk.
(* Next, consider any arrival sequence such that...*)
......@@ -889,19 +889,17 @@ Module ResponseTimeIterationEDF.
(* Then, consider any platform with at least one CPU such that...*)
Variable sched: schedule num_cpus arr_seq.
Hypothesis H_at_least_one_cpu :
num_cpus > 0.
Hypothesis H_at_least_one_cpu: num_cpus > 0.
(* ...jobs only execute after they arrived and no longer
than their execution costs,... *)
than their execution costs. *)
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* ...and do not execute in parallel. *)
Hypothesis H_no_parallelism:
jobs_dont_execute_in_parallel sched.
(* Also assume that jobs are sequential. *)
Hypothesis H_sequential_jobs: sequential_jobs sched.
(* Assume a work-conserving scheduler with EDF policy. *)
Hypothesis H_work_conserving: work_conserving job_cost sched.
......@@ -911,6 +909,8 @@ Module ResponseTimeIterationEDF.
task_misses_no_deadline job_cost job_deadline job_task sched tsk.
Definition no_deadline_missed_by_job :=
job_misses_no_deadline job_cost job_deadline sched.
Let response_time_bounded_by (tsk: sporadic_task) :=
is_response_time_bound_of_task job_cost job_task tsk sched.
(* In the following theorem, we prove that any response-time bound contained
in edf_claimed_bounds is safe. The proof follows by direct application of
......@@ -918,9 +918,7 @@ Module ResponseTimeIterationEDF.
Theorem edf_analysis_yields_response_time_bounds :
forall tsk R,
(tsk, R) \In edf_claimed_bounds ts ->
forall j : JobIn arr_seq,
job_task j = tsk ->
completed job_cost sched j (job_arrival j + R).
response_time_bounded_by tsk R.
Proof.
intros tsk R IN j JOBj.
destruct (edf_claimed_bounds ts) as [rt_bounds |] eqn:SOME; last by done.
......@@ -948,7 +946,7 @@ Module ResponseTimeIterationEDF.
valid_sporadic_job in *.
rename H_valid_job_parameters into JOBPARAMS,
H_valid_task_parameters into TASKPARAMS,
H_restricted_deadlines into RESTR,
H_constrained_deadlines into RESTR,
H_completed_jobs_dont_execute into COMP,
H_jobs_must_arrive_to_execute into MUSTARRIVE,
H_all_jobs_from_taskset into ALLJOBS,
......
......@@ -48,19 +48,18 @@ Module ResponseTimeAnalysisEDF.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Also assume that jobs do not execute in parallel and that
(* Also assume that jobs are sequential and that
there exists at least one processor. *)
Hypothesis H_no_parallelism:
jobs_dont_execute_in_parallel sched.
Hypothesis H_sequential_jobs: sequential_jobs sched.
Hypothesis H_at_least_one_cpu :
num_cpus > 0.
(* Assume that we have a task set where all tasks have valid
parameters and restricted deadlines, ... *)
parameters and constrained deadlines, ... *)
Variable ts: taskset_of sporadic_task.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Hypothesis H_restricted_deadlines:
Hypothesis H_constrained_deadlines:
forall tsk, tsk \in ts -> task_deadline tsk <= task_period tsk.
(* ... and that all jobs in the arrival sequence come from the task set. *)
......@@ -178,7 +177,7 @@ Module ResponseTimeAnalysisEDF.
rename H_all_previous_jobs_completed_on_time into BEFOREok,
H_valid_job_parameters into PARAMS,
H_valid_task_parameters into TASK_PARAMS,
H_restricted_deadlines into RESTR,
H_constrained_deadlines into RESTR,
H_tasks_miss_no_deadlines into NOMISS.
unfold x, task_interference.
have INts := bertogna_edf_tsk_other_in_ts.
......@@ -277,7 +276,7 @@ Module ResponseTimeAnalysisEDF.
H_all_previous_jobs_completed_on_time into BEFOREok,
H_tasks_miss_no_deadlines into NOMISS,
H_rt_bounds_contains_all_tasks into UNZIP,
H_restricted_deadlines into RESTR,
H_constrained_deadlines into RESTR,
H_work_conserving into WORK.
unfold x, X, total_interference, task_interference.
move => t /andP [LEt LTt] BACK.
......@@ -320,7 +319,7 @@ Module ResponseTimeAnalysisEDF.
H_all_previous_jobs_completed_on_time into BEFOREok,
H_tasks_miss_no_deadlines into NOMISS,
H_rt_bounds_contains_all_tasks into UNZIP,
H_restricted_deadlines into RESTR.
H_constrained_deadlines into RESTR.
unfold sporadic_task_model in *.
unfold x, X, total_interference, task_interference.
rewrite -big_mkcond -exchange_big big_distrl /=.
......@@ -360,7 +359,7 @@ Module ResponseTimeAnalysisEDF.
H_tsk_R_in_rt_bounds into INbounds,
H_all_previous_jobs_completed_on_time into BEFOREok,
H_tasks_miss_no_deadlines into NOMISS,
H_restricted_deadlines into RESTR.
H_constrained_deadlines into RESTR.
unfold sporadic_task_model in *.
intros delta HAS.
set some_interference_A := fun t =>
......
......@@ -530,8 +530,8 @@ Module ResponseTimeIterationFP.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
(* ...restricted deadlines, ...*)
Hypothesis H_restricted_deadlines:
(* ...constrained deadlines, ...*)
Hypothesis H_constrained_deadlines:
forall tsk, tsk \in ts -> task_deadline tsk <= task_period tsk.
(* ...and tasks are ordered by increasing priorities. *)
......@@ -559,15 +559,14 @@ Module ResponseTimeIterationFP.
num_cpus > 0.
(* ...jobs only execute after they arrived and no longer
than their execution costs,... *)
than their execution costs. *)
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* ...and do not execute in parallel (required by the workload bound). *)
Hypothesis H_no_parallelism:
jobs_dont_execute_in_parallel sched.
(* Also assume that jobs are sequential (as required by the workload bound). *)
Hypothesis H_sequential_jobs: sequential_jobs sched.
(* Assume that the scheduler is work-conserving and enforces the FP policy. *)
Hypothesis H_work_conserving: work_conserving job_cost sched.
......
......@@ -45,23 +45,21 @@ Module ResponseTimeAnalysisFP.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Also assume that jobs do not execute in parallel and that
there exists at least one processor. *)
Hypothesis H_no_parallelism:
jobs_dont_execute_in_parallel sched.
Hypothesis H_at_least_one_cpu :
num_cpus > 0.
(* Also assume that jobs are sequential and that there exists
at least one processor. *)
Hypothesis H_sequential_jobs: sequential_jobs sched.
Hypothesis H_at_least_one_cpu: num_cpus > 0.
(* Consider a task set ts with no duplicates where all jobs
come from the task set and all tasks have valid parameters
and restricted deadlines. *)
and constrained deadlines. *)
Variable ts: taskset_of sporadic_task.
Hypothesis H_ts_is_a_set: uniq ts.
Hypothesis H_all_jobs_from_taskset:
forall (j: JobIn arr_seq), job_task j \in ts.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Hypothesis H_restricted_deadlines:
Hypothesis H_constrained_deadlines:
forall tsk, tsk \in ts -> task_deadline tsk <= task_period tsk.
(* Next, consider a task tsk that is to be analyzed. *)
......@@ -70,7 +68,7 @@ Module ResponseTimeAnalysisFP.
Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
task_misses_no_deadline job_cost job_deadline job_task sched tsk.
Let is_response_time_bound (tsk: sporadic_task) :=
Let response_time_bounded_by (tsk: sporadic_task) :=
is_response_time_bound_of_task job_cost job_task tsk sched.
(* Assume a given FP policy. *)
......@@ -83,7 +81,7 @@ Module ResponseTimeAnalysisFP.
Hypothesis H_response_time_of_interfering_tasks_is_known:
forall hp_tsk R,
(hp_tsk, R) \in hp_bounds ->
is_response_time_bound_of_task job_cost job_task hp_tsk sched R.
response_time_bounded_by hp_tsk R.
(* ... for any task in ts that interferes with tsk. *)
Hypothesis H_hp_bounds_has_interfering_tasks:
......@@ -184,11 +182,11 @@ Module ResponseTimeAnalysisFP.
Lemma bertogna_fp_workload_bounds_interference :
x tsk_other <= workload_bound tsk_other R_other.
Proof.
unfold is_response_time_bound, is_response_time_bound_of_task,
unfold response_time_bounded_by, is_response_time_bound_of_task,
completed, completed_jobs_dont_execute, valid_sporadic_job in *.
rename H_valid_job_parameters into PARAMS,
H_valid_task_parameters into TASK_PARAMS,
H_restricted_deadlines into RESTR,
H_constrained_deadlines into RESTR,
H_response_time_of_interfering_tasks_is_known into RESP,
H_interfering_tasks_miss_no_deadlines into NOMISS,
H_response_time_bounds_ge_cost into GE_COST.
......@@ -275,7 +273,7 @@ Module ResponseTimeAnalysisFP.
H_job_of_tsk into JOBtsk,
H_sporadic_tasks into SPO,
H_valid_job_parameters into JOBPARAMS,
H_restricted_deadlines into RESTR,
H_constrained_deadlines into RESTR,
H_hp_bounds_has_interfering_tasks into UNZIP,
H_interfering_tasks_miss_no_deadlines into NOMISS,
H_response_time_of_interfering_tasks_is_known into PREV.
......@@ -579,7 +577,7 @@ Module ResponseTimeAnalysisFP.
(* Using the lemmas above, we prove that R bounds the response time of task tsk. *)
Theorem bertogna_cirinei_response_time_bound_fp :
is_response_time_bound tsk R.
response_time_bounded_by tsk R.
Proof.
rename H_response_time_bounds_ge_cost into GE_COST,
H_interfering_tasks_miss_no_deadlines into NOMISS,
......@@ -607,7 +605,7 @@ Module ResponseTimeAnalysisFP.
by ins; apply IH; try (by done); rewrite ltn_add2r.
} clear IH.
unfold is_response_time_bound, is_response_time_bound_of_task,
unfold response_time_bounded_by, is_response_time_bound_of_task,
completed, completed_jobs_dont_execute, valid_sporadic_job in *.
(* Now we start the proof. Assume by contradiction that job j
......
......@@ -135,21 +135,19 @@ Module InterferenceBoundEDF.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Also assume that jobs do not execute in parallel and that
there exists at least one processor. *)
Hypothesis H_no_parallelism:
jobs_dont_execute_in_parallel sched.
Hypothesis H_at_least_one_cpu :
num_cpus > 0.
(* Also assume that jobs are sequential and that there exists at
least one processor. *)
Hypothesis H_sequential_jobs: sequential_jobs sched.
Hypothesis H_at_least_one_cpu: num_cpus > 0.
(* Consider a task set ts where all jobs come from the task set
and tasks have valid parameters and restricted deadlines. *)
and tasks have valid parameters and constrained deadlines. *)
Variable ts: taskset_of sporadic_task.
Hypothesis all_jobs_from_taskset:
forall (j: JobIn arr_seq), job_task j \in ts.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Hypothesis H_restricted_deadlines:
Hypothesis H_constrained_deadlines:
forall tsk, tsk \in ts -> task_deadline tsk <= task_period tsk.
Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
......@@ -736,7 +734,7 @@ Module InterferenceBoundEDF.
apply leq_trans with (n := a_fst + p_k).
{
by rewrite leq_add2l; apply leq_trans with (n := D_k);
[by apply H_R_k_le_deadline | by apply H_restricted_deadlines].
[by apply H_R_k_le_deadline | by apply H_constrained_deadlines].
}
(* Since jobs are sporadic, we know that the first job arrives
......
......@@ -147,10 +147,9 @@ Module WorkloadBound.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Assumptiom: Jobs do not execute in parallel.
(* Assumption: Jobs are sequential.
This is required to use interval lengths as a measure of service. *)
Hypothesis H_no_parallelism:
jobs_dont_execute_in_parallel sched.
Hypothesis H_sequential_jobs: sequential_jobs sched.
(* Assumption: sporadic task model.
This is necessary to conclude that consecutive jobs ordered by arrival times
......@@ -177,11 +176,11 @@ Module WorkloadBound.
Hypothesis H_valid_task_parameters:
is_valid_sporadic_task task_cost task_period task_deadline tsk.
(* Assumption: the task must have a restricted deadline.
(* Assumption: the task must have a constrained deadline.
This is required to prove that n_k (max_jobs) from Bertogna
and Cirinei's formula accounts for at least the number of
middle jobs (i.e., number of jobs - 2 in the worst case). *)
Hypothesis H_restricted_deadline: task_deadline tsk <= task_period tsk.
Hypothesis H_constrained_deadline: task_deadline tsk <= task_period tsk.
(* Consider an interval [t1, t1 + delta). *)
Variable t1 delta: time.
......@@ -582,7 +581,7 @@ Module WorkloadBound.
intros BEFOREt2; apply BEFOREt2'; clear BEFOREt2'.
apply leq_trans with (n := job_arrival j_fst + task_deadline tsk + delta);
last by apply leq_trans with (n := job_arrival j_fst + task_period tsk + delta);
[rewrite leq_add2r leq_add2l; apply H_restricted_deadline | apply DISTmax].
[rewrite leq_add2r leq_add2l; apply H_constrained_deadline | apply DISTmax].
unfold t2; rewrite leq_add2r.
apply leq_trans with (n := job_arrival j_fst + R_tsk);
last by rewrite leq_add2l.
......
......@@ -955,8 +955,8 @@ Module ResponseTimeIterationEDF.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
(* ...restricted deadlines, ...*)
Hypothesis H_restricted_deadlines:
(* ...constrained deadlines, ...*)
Hypothesis H_constrained_deadlines:
forall tsk, tsk \in ts -> task_deadline tsk <= task_period tsk.
(* Next, consider any arrival sequence such that...*)
......@@ -981,15 +981,14 @@ Module ResponseTimeIterationEDF.
Hypothesis H_at_least_one_cpu :
num_cpus > 0.
(* ...jobs only execute after jitter and no longer than their execution costs,... *)
(* ...jobs only execute after jitter and no longer than their execution costs. *)
Hypothesis H_jobs_execute_after_jitter:
jobs_execute_after_jitter job_jitter sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* ...and do not execute in parallel. *)
Hypothesis H_no_parallelism:
jobs_dont_execute_in_parallel sched.
(* Also assume that jobs are sequential. *)
Hypothesis H_sequential_jobs: sequential_jobs sched.
(* Assume that we have a work-conserving EDF scheduler. *)
Hypothesis H_work_conserving: work_conserving job_cost job_jitter sched.
......@@ -1041,7 +1040,7 @@ Module ResponseTimeIterationEDF.
valid_sporadic_job_with_jitter, valid_sporadic_job in *.
rename H_valid_job_parameters into JOBPARAMS,
H_valid_task_parameters into TASKPARAMS,
H_restricted_deadlines into RESTR,
H_constrained_deadlines into RESTR,
H_completed_jobs_dont_execute into COMP,
H_jobs_execute_after_jitter into AFTER,
H_all_jobs_from_taskset into ALLJOBS,
......
......@@ -52,22 +52,20 @@ Module ResponseTimeAnalysisEDFJitter.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Also assume that jobs do not execute in parallel and that
there exists at least one processor. *)
Hypothesis H_no_parallelism:
jobs_dont_execute_in_parallel sched.
Hypothesis H_at_least_one_cpu :
num_cpus > 0.
(* Also assume that jobs are sequential and that there exists
at least one processor. *)
Hypothesis H_sequential_jobs: sequential_jobs sched.
Hypothesis H_at_least_one_cpu: num_cpus > 0.
(* Assume that we have a task set ts, such that all jobs come
from the task set, and all tasks have valid parameters and
restricted deadlines. *)
constrained deadlines. *)
Variable ts: taskset_of sporadic_task.
Hypothesis H_all_jobs_from_taskset:
forall (j: JobIn arr_seq), job_task j \in ts.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Hypothesis H_restricted_deadlines:
Hypothesis H_constrained_deadlines:
forall tsk, tsk \in ts -> task_deadline tsk <= task_period tsk.
Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
......@@ -184,7 +182,7 @@ Module ResponseTimeAnalysisEDFJitter.
rename H_all_previous_jobs_completed_on_time into BEFOREok,
H_valid_job_parameters into PARAMS,
H_valid_task_parameters into TASK_PARAMS,
H_restricted_deadlines into RESTR,
H_constrained_deadlines into RESTR,
H_tasks_miss_no_deadlines into NOMISS.
unfold x, task_interference, valid_sporadic_job_with_jitter, valid_sporadic_job in *.
have INts := bertogna_edf_tsk_other_in_ts.
......@@ -296,7 +294,7 @@ Module ResponseTimeAnalysisEDFJitter.
H_all_previous_jobs_completed_on_time into BEFOREok,
H_tasks_miss_no_deadlines into NOMISS,
H_rt_bounds_contains_all_tasks into UNZIP,
H_restricted_deadlines into RESTR,
H_constrained_deadlines into RESTR,
H_work_conserving into WORK.
unfold valid_sporadic_job_with_jitter, valid_sporadic_job in *.
move => t /andP [LEt LTt] BACK.
......@@ -348,7 +346,7 @@ Module ResponseTimeAnalysisEDFJitter.
H_tsk_R_in_rt_bounds into INbounds,
H_all_previous_jobs_completed_on_time into BEFOREok,
H_tasks_miss_no_deadlines into NOMISS,
H_restricted_deadlines into RESTR.
H_constrained_deadlines into RESTR.
unfold sporadic_task_model, valid_sporadic_job_with_jitter, valid_sporadic_job in *.
unfold x, X, total_interference, task_interference.
rewrite -big_mkcond -exchange_big big_distrl /=.
......@@ -388,7 +386,7 @@ Module ResponseTimeAnalysisEDFJitter.
H_tsk_R_in_rt_bounds into INbounds,
H_all_previous_jobs_completed_on_time into BEFOREok,
H_tasks_miss_no_deadlines into NOMISS,
H_restricted_deadlines into RESTR.
H_constrained_deadlines into RESTR.
unfold sporadic_task_model in *.
intros delta HAS.
set some_interference_A := fun t =>
......
......@@ -536,8 +536,8 @@ Module ResponseTimeIterationFP.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
(* ...restricted deadlines, ...*)
Hypothesis H_restricted_deadlines:
(* ...constrained deadlines, ...*)
Hypothesis H_constrained_deadlines:
forall tsk, tsk \in ts -> task_deadline tsk <= task_period tsk.
(* ...and tasks are ordered by increasing priorities. *)
......@@ -565,15 +565,14 @@ Module ResponseTimeIterationFP.
Hypothesis H_at_least_one_cpu :
num_cpus > 0.
(* ...jobs only execute after jitter and no longer than their execution costs,... *)
(* ...jobs only execute after jitter and no longer than their execution costs. *)
Hypothesis H_jobs_must_arrive_to_execute:
jobs_execute_after_jitter job_jitter sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* ...and do not execute in parallel (required by the workload bound). *)
Hypothesis H_no_parallelism:
jobs_dont_execute_in_parallel sched.
(* Also assume that jobs are sequential (as required by the workload bound). *)
Hypothesis H_sequential_jobs: sequential_jobs sched.
(* Assume that the scheduler is work-conserving and enforces the FP policy. *)
Hypothesis H_work_conserving: work_conserving job_cost job_jitter sched.
......@@ -601,7 +600,7 @@ Module ResponseTimeIterationFP.
response_time_bounded_by tsk (task_jitter tsk + R).
Proof.
rename H_valid_job_parameters into JOBPARAMS, H_valid_task_parameters into TASKPARAMS,
H_restricted_deadlines into RESTR, H_completed_jobs_dont_execute into COMP,
H_constrained_deadlines into RESTR, H_completed_jobs_dont_execute into COMP,
H_jobs_must_arrive_to_execute into MUSTARRIVE, H_sorted_ts into SORT,
H_unique_priorities into UNIQ,
H_all_jobs_from_taskset into ALLJOBS.
......
......@@ -49,22 +49,20 @@ Module ResponseTimeAnalysisFP.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Also assume that jobs do not execute in parallel and that
there exists at least one processor. *)
Hypothesis H_no_parallelism:
jobs_dont_execute_in_parallel sched.
Hypothesis H_at_least_one_cpu :
num_cpus > 0.
(* Also assume that jobs are sequential and that there exists
at least one processor. *)
Hypothesis H_sequential_jobs: sequential_jobs sched.
Hypothesis H_at_least_one_cpu: num_cpus > 0.
(* Assume that we have a task set (with no duplicates) where all jobs
come from the task set and all tasks have valid parameters and restricted deadlines. *)
come from the task set and all tasks have valid parameters and constrained deadlines. *)
Variable ts: taskset_of sporadic_task.
Hypothesis H_ts_is_a_set: uniq ts.
Hypothesis H_all_jobs_from_taskset:
forall (j: JobIn arr_seq), job_task j \in ts.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Hypothesis H_restricted_deadlines:
Hypothesis H_constrained_deadlines:
forall tsk, tsk \in ts -> task_deadline tsk <= task_period tsk.
(* Next, consider a task tsk that is to be analyzed. *)
......@@ -73,7 +71,7 @@ Module ResponseTimeAnalysisFP.
Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
task_misses_no_deadline job_cost job_deadline job_task sched tsk.
Let is_response_time_bound (tsk: sporadic_task) :=
Let response_time_bounded_by (tsk: sporadic_task) :=
is_response_time_bound_of_task job_cost job_task tsk sched.
(* Assume a known response-time bound for any interfering task *)
......@@ -93,7 +91,7 @@ Module ResponseTimeAnalysisFP.
Hypothesis H_response_time_of_interfering_tasks_is_known:
forall hp_tsk R,
(hp_tsk, R) \in hp_bounds ->
is_response_time_bound_of_task job_cost job_task hp_tsk sched (task_jitter hp_tsk + R).
response_time_bounded_by hp_tsk (task_jitter hp_tsk + R).
(* Assume that the response-time bounds are larger than task costs. *)
Hypothesis H_response_time_bounds_ge_cost:
......@@ -193,11 +191,11 @@ Module ResponseTimeAnalysisFP.
Lemma bertogna_fp_workload_bounds_interference :
x tsk_other <= workload_bound tsk_other R_other.
Proof.
unfold is_response_time_bound, is_response_time_bound_of_task,
unfold response_time_bounded_by, is_response_time_bound_of_task,
completed, completed_jobs_dont_execute, valid_sporadic_job in *.
rename H_valid_job_parameters into PARAMS,
H_valid_task_parameters into TASK_PARAMS,
H_restricted_deadlines into RESTR,
H_constrained_deadlines into RESTR,
H_response_time_of_interfering_tasks_is_known into RESP,
H_interfering_tasks_miss_no_deadlines into NOMISS,
H_response_time_bounds_ge_cost into GE_COST.
......@@ -286,7 +284,7 @@ Module ResponseTimeAnalysisFP.
H_all_jobs_from_taskset into FROMTS,
H_sporadic_tasks into SPO,
H_valid_job_parameters into JOBPARAMS,
H_restricted_deadlines into RESTR,
H_constrained_deadlines into RESTR,
H_hp_bounds_has_interfering_tasks into UNZIP,
H_interfering_tasks_miss_no_deadlines into NOMISS,
H_response_time_of_interfering_tasks_is_known into PREV,
......@@ -590,7 +588,7 @@ Module ResponseTimeAnalysisFP.
(* Using the lemmas above, we prove that R' bounds the response time of task tsk. *)
Theorem bertogna_cirinei_response_time_bound_fp :
is_response_time_bound tsk (task_jitter tsk + R).
response_time_bounded_by tsk (task_jitter tsk + R).
Proof.
rename H_valid_job_parameters into PARAMS.
unfold valid_sporadic_job_with_jitter, valid_sporadic_job in *.
......
......@@ -138,21 +138,19 @@ Module InterferenceBoundEDFJitter.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Also assume that jobs do not execute in parallel and that
there exists at least one processor. *)
Hypothesis H_no_parallelism:
jobs_dont_execute_in_parallel sched.
Hypothesis H_at_least_one_cpu :
num_cpus > 0.
(* Also assume that jobs are sequential and that there exists
at least one processor. *)
Hypothesis H_sequential_jobs: sequential_jobs sched.
Hypothesis H_at_least_one_cpu: num_cpus > 0.
(* Assume that we have a task set where all tasks have valid
parameters and restricted deadlines. *)
parameters and constrained deadlines. *)
Variable ts: taskset_of sporadic_task.
Hypothesis all_jobs_from_taskset:
forall (j: JobIn arr_seq), job_task j \in ts.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Hypothesis H_restricted_deadlines:
Hypothesis H_constrained_deadlines:
forall tsk, tsk \in ts -> task_deadline tsk <= task_period tsk.
Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
......@@ -821,7 +819,7 @@ Module InterferenceBoundEDFJitter.
{
apply leq_trans with (n := job_arrival j_fst + D_k);
first by rewrite -addnA leq_add2l.
by rewrite leq_add2l; apply H_restricted_deadlines.
by rewrite leq_add2l; apply H_constrained_deadlines.
}
(* Since jobs are sporadic, we know that the first job arrives
......
......@@ -151,10 +151,9 @@ Module WorkloadBoundJitter.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Assumptiom: Jobs do not execute in parallel.
(* Assumption: Jobs are sequential.
This is required to use interval lengths as a measure of service. *)
Hypothesis H_no_parallelism:
jobs_dont_execute_in_parallel sched.
Hypothesis H_sequential_jobs: sequential_jobs sched.
(* Assumption: sporadic task model.
This is necessary to conclude that consecutive jobs ordered by arrival times
......@@ -181,11 +180,11 @@ Module WorkloadBoundJitter.
Hypothesis H_valid_task_parameters:
is_valid_sporadic_task task_cost task_period task_deadline tsk.
(* Assumption: the task must have a restricted deadline.
(* Assumption: the task must have a constrained deadline.
This is required to prove that n_k (max_jobs) from Bertogna
and Cirinei's formula accounts for at least the number of
middle jobs (i.e., number of jobs - 2 in the worst case). *)
Hypothesis H_restricted_deadline: task_deadline tsk <= task_period tsk.
Hypothesis H_constrained_deadline: task_deadline tsk <= task_period tsk.
(* Consider an interval [t1, t1 + delta). *)
Variable t1 delta: time.
......@@ -603,7 +602,7 @@ Module WorkloadBoundJitter.
last first.
{
apply leq_trans with (n := job_arrival j_fst + task_period tsk + delta); last by done.
by rewrite leq_add2r leq_add2l; apply H_restricted_deadline.
by rewrite leq_add2r leq_add2l; apply H_constrained_deadline.
}
{
unfold t2; rewrite leq_add2r.
......
......@@ -868,8 +868,8 @@ Module ResponseTimeIterationEDF.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
(* ...restricted deadlines, ...*)
Hypothesis H_restricted_deadlines:
(* ...constrained deadlines, ...*)
Hypothesis H_constrained_deadlines:
forall tsk, tsk \in ts -> task_deadline tsk <= task_period tsk.
(* Next, consider any arrival sequence such that...*)
......@@ -908,6 +908,8 @@ Module ResponseTimeIterationEDF.
task_misses_no_deadline job_cost job_deadline job_task sched tsk.
Definition no_deadline_missed_by_job :=
job_misses_no_deadline job_cost job_deadline sched.
Let response_time_bounded_by (tsk: sporadic_task) :=
is_response_time_bound_of_task job_cost job_task tsk sched.
(* In the following theorem, we prove that any response-time bound contained
in edf_claimed_bounds is safe. The proof follows by direct application of
......@@ -915,9 +917,7 @@ Module ResponseTimeIterationEDF.
Theorem edf_analysis_yields_response_time_bounds :
forall tsk R,
(tsk, R) \In edf_claimed_bounds ts ->
forall j : JobIn arr_seq,
job_task j = tsk ->
completed job_cost sched j (job_arrival j + R).
response_time_bounded_by tsk R.
Proof.
intros tsk R IN j JOBj.
destruct (edf_claimed_bounds ts) as [rt_bounds |] eqn:SOME; last by done.
......@@ -945,7 +945,7 @@ Module ResponseTimeIterationEDF.
valid_sporadic_job in *.
rename H_valid_job_parameters into JOBPARAMS,
H_valid_task_parameters into TASKPARAMS,
H_restricted_deadlines into RESTR,
H_constrained_deadlines into RESTR,
H_completed_jobs_dont_execute into COMP,
H_jobs_must_arrive_to_execute into MUSTARRIVE,
H_all_jobs_from_taskset into ALLJOBS,
......
......@@ -54,13 +54,13 @@ Module ResponseTimeAnalysisEDF.
(* Assume that we have a task set ts such that all jobs come from
the task set, and all tasks have valid parameters and
restricted deadlines. *)
constrained deadlines. *)
Variable ts: taskset_of sporadic_task.
Hypothesis H_all_jobs_from_taskset:
forall (j: JobIn arr_seq), job_task j \in ts.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Hypothesis H_restricted_deadlines:
Hypothesis H_constrained_deadlines:
forall tsk, tsk \in ts -> task_deadline tsk <= task_period tsk.
Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
......@@ -174,7 +174,7 @@ Module ResponseTimeAnalysisEDF.
rename H_all_previous_jobs_completed_on_time into BEFOREok,
H_valid_job_parameters into PARAMS,
H_valid_task_parameters into TASK_PARAMS,
H_restricted_deadlines into RESTR,
H_constrained_deadlines into RESTR,
H_tasks_miss_no_deadlines into NOMISS.
unfold x, task_interference.
have INts := bertogna_edf_tsk_other_in_ts.
......@@ -267,7 +267,7 @@ Module ResponseTimeAnalysisEDF.
H_all_previous_jobs_completed_on_time into BEFOREok,
H_tasks_miss_no_deadlines into NOMISS,
H_rt_bounds_contains_all_tasks into UNZIP,
H_restricted_deadlines into RESTR.
H_constrained_deadlines into RESTR.
unfold sporadic_task_model in *.
unfold x, X, total_interference, task_interference.
rewrite -big_mkcond -exchange_big big_distrl /=.
......
......@@ -524,8 +524,8 @@ Module ResponseTimeIterationFP.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
(* ...restricted deadlines, ...*)
Hypothesis H_restricted_deadli