Skip to content

GitLab

R
rt-proofs
Commit a58b283a authored by Felipe Cerqueira's avatar Felipe Cerqueira
Browse files
Options

Remove JobIn to simplify specification

parent 9295617e
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 4947 additions and 4519 deletions
Makefile
View file @ a58b283a
......@@ -14,7 +14,7 @@
#
# This Makefile was generated by the command line :
# coq_makefile -f _CoqProject ./util/ssromega.v ./util/seqset.v ./util/sorting.v ./util/step_function.v ./util/minmax.v ./util/powerset.v ./util/all.v ./util/ord_quantifier.v ./util/nat.v ./util/sum.v ./util/bigord.v ./util/counting.v ./util/tactics.v ./util/induction.v ./util/list.v ./util/divround.v ./util/bigcat.v ./util/fixedpoint.v ./util/notation.v ./analysis/global/jitter/bertogna_fp_comp.v ./analysis/global/jitter/interference_bound_edf.v ./analysis/global/jitter/workload_bound.v ./analysis/global/jitter/bertogna_edf_comp.v ./analysis/global/jitter/bertogna_fp_theory.v ./analysis/global/jitter/interference_bound.v ./analysis/global/jitter/interference_bound_fp.v ./analysis/global/jitter/bertogna_edf_theory.v ./analysis/global/parallel/bertogna_fp_comp.v ./analysis/global/parallel/interference_bound_edf.v ./analysis/global/parallel/workload_bound.v ./analysis/global/parallel/bertogna_edf_comp.v ./analysis/global/parallel/bertogna_fp_theory.v ./analysis/global/parallel/interference_bound.v ./analysis/global/parallel/interference_bound_fp.v ./analysis/global/parallel/bertogna_edf_theory.v ./analysis/global/basic/bertogna_fp_comp.v ./analysis/global/basic/interference_bound_edf.v ./analysis/global/basic/workload_bound.v ./analysis/global/basic/bertogna_edf_comp.v ./analysis/global/basic/bertogna_fp_theory.v ./analysis/global/basic/interference_bound.v ./analysis/global/basic/interference_bound_fp.v ./analysis/global/basic/bertogna_edf_theory.v ./analysis/apa/bertogna_fp_comp.v ./analysis/apa/interference_bound_edf.v ./analysis/apa/workload_bound.v ./analysis/apa/bertogna_edf_comp.v ./analysis/apa/bertogna_fp_theory.v ./analysis/apa/interference_bound.v ./analysis/apa/interference_bound_fp.v ./analysis/apa/bertogna_edf_theory.v ./analysis/uni/susp/dynamic/oblivious/fp_rta.v ./analysis/uni/susp/dynamic/oblivious/reduction.v ./analysis/uni/jitter/workload_bound_fp.v ./analysis/uni/jitter/fp_rta_comp.v ./analysis/uni/jitter/fp_rta_theory.v ./analysis/uni/basic/workload_bound_fp.v ./analysis/uni/basic/fp_rta_comp.v ./analysis/uni/basic/fp_rta_theory.v ./model/suspension.v ./model/schedule/partitioned/schedulability.v ./model/schedule/partitioned/schedule.v ./model/schedule/global/workload.v ./model/schedule/global/schedulability.v ./model/schedule/global/jitter/interference_edf.v ./model/schedule/global/jitter/interference.v ./model/schedule/global/jitter/job.v ./model/schedule/global/jitter/constrained_deadlines.v ./model/schedule/global/jitter/schedule.v ./model/schedule/global/jitter/platform.v ./model/schedule/global/response_time.v ./model/schedule/global/basic/interference_edf.v ./model/schedule/global/basic/interference.v ./model/schedule/global/basic/constrained_deadlines.v ./model/schedule/global/basic/schedule.v ./model/schedule/global/basic/platform.v ./model/schedule/apa/interference_edf.v ./model/schedule/apa/interference.v ./model/schedule/apa/affinity.v ./model/schedule/apa/constrained_deadlines.v ./model/schedule/apa/platform.v ./model/schedule/uni/workload.v ./model/schedule/uni/transformation/construction.v ./model/schedule/uni/susp/suspension_intervals.v ./model/schedule/uni/susp/last_execution.v ./model/schedule/uni/susp/schedule.v ./model/schedule/uni/susp/platform.v ./model/schedule/uni/schedulability.v ./model/schedule/uni/jitter/workload.v ./model/schedule/uni/jitter/busy_interval.v ./model/schedule/uni/jitter/schedule.v ./model/schedule/uni/jitter/platform.v ./model/schedule/uni/jitter/service.v ./model/schedule/uni/schedule_of_task.v ./model/schedule/uni/response_time.v ./model/schedule/uni/schedule.v ./model/schedule/uni/basic/busy_interval.v ./model/schedule/uni/basic/platform.v ./model/schedule/uni/service.v ./model/arrival/jitter/arrival_sequence.v ./model/arrival/jitter/task_arrival.v ./model/arrival/jitter/job.v ./model/arrival/jitter/arrival_bounds.v ./model/arrival/basic/arrival_sequence.v ./model/arrival/basic/task.v ./model/arrival/basic/task_arrival.v ./model/arrival/basic/job.v ./model/arrival/basic/arrival_bounds.v ./model/priority.v ./model/time.v ./implementation/arrival_sequence.v ./implementation/task.v ./implementation/global/jitter/arrival_sequence.v ./implementation/global/jitter/task.v ./implementation/global/jitter/bertogna_edf_example.v ./implementation/global/jitter/job.v ./implementation/global/jitter/bertogna_fp_example.v ./implementation/global/jitter/schedule.v ./implementation/global/parallel/bertogna_edf_example.v ./implementation/global/parallel/bertogna_fp_example.v ./implementation/global/basic/bertogna_edf_example.v ./implementation/global/basic/bertogna_fp_example.v ./implementation/global/basic/schedule.v ./implementation/job.v ./implementation/apa/arrival_sequence.v ./implementation/apa/task.v ./implementation/apa/bertogna_edf_example.v ./implementation/apa/job.v ./implementation/apa/bertogna_fp_example.v ./implementation/apa/schedule.v ./implementation/uni/susp/dynamic/arrival_sequence.v ./implementation/uni/susp/dynamic/task.v ./implementation/uni/susp/dynamic/job.v ./implementation/uni/susp/dynamic/oblivious/fp_rta_example.v ./implementation/uni/susp/schedule.v ./implementation/uni/jitter/arrival_sequence.v ./implementation/uni/jitter/task.v ./implementation/uni/jitter/job.v ./implementation/uni/jitter/fp_rta_example.v ./implementation/uni/jitter/schedule.v ./implementation/uni/basic/fp_rta_example.v ./implementation/uni/basic/schedule.v -o Makefile
# coq_makefile -f _CoqProject ./util/ssromega.v ./util/seqset.v ./util/sorting.v ./util/step_function.v ./util/minmax.v ./util/powerset.v ./util/all.v ./util/ord_quantifier.v ./util/nat.v ./util/sum.v ./util/bigord.v ./util/counting.v ./util/tactics.v ./util/induction.v ./util/list.v ./util/divround.v ./util/bigcat.v ./util/fixedpoint.v ./util/notation.v ./analysis/global/jitter/bertogna_fp_comp.v ./analysis/global/jitter/interference_bound_edf.v ./analysis/global/jitter/workload_bound.v ./analysis/global/jitter/bertogna_edf_comp.v ./analysis/global/jitter/bertogna_fp_theory.v ./analysis/global/jitter/interference_bound.v ./analysis/global/jitter/interference_bound_fp.v ./analysis/global/jitter/bertogna_edf_theory.v ./analysis/global/parallel/bertogna_fp_comp.v ./analysis/global/parallel/interference_bound_edf.v ./analysis/global/parallel/workload_bound.v ./analysis/global/parallel/bertogna_edf_comp.v ./analysis/global/parallel/bertogna_fp_theory.v ./analysis/global/parallel/interference_bound.v ./analysis/global/parallel/interference_bound_fp.v ./analysis/global/parallel/bertogna_edf_theory.v ./analysis/global/basic/bertogna_fp_comp.v ./analysis/global/basic/interference_bound_edf.v ./analysis/global/basic/workload_bound.v ./analysis/global/basic/bertogna_edf_comp.v ./analysis/global/basic/bertogna_fp_theory.v ./analysis/global/basic/interference_bound.v ./analysis/global/basic/interference_bound_fp.v ./analysis/global/basic/bertogna_edf_theory.v ./analysis/apa/bertogna_fp_comp.v ./analysis/apa/interference_bound_edf.v ./analysis/apa/workload_bound.v ./analysis/apa/bertogna_edf_comp.v ./analysis/apa/bertogna_fp_theory.v ./analysis/apa/interference_bound.v ./analysis/apa/interference_bound_fp.v ./analysis/apa/bertogna_edf_theory.v ./analysis/uni/susp/dynamic/oblivious/fp_rta.v ./analysis/uni/susp/dynamic/oblivious/reduction.v ./analysis/uni/jitter/workload_bound_fp.v ./analysis/uni/jitter/fp_rta_comp.v ./analysis/uni/jitter/fp_rta_theory.v ./analysis/uni/basic/workload_bound_fp.v ./analysis/uni/basic/fp_rta_comp.v ./analysis/uni/basic/fp_rta_theory.v ./model/suspension.v ./model/schedule/partitioned/schedulability.v ./model/schedule/partitioned/schedule.v ./model/schedule/global/workload.v ./model/schedule/global/transformation/construction.v ./model/schedule/global/schedulability.v ./model/schedule/global/jitter/interference_edf.v ./model/schedule/global/jitter/interference.v ./model/schedule/global/jitter/job.v ./model/schedule/global/jitter/constrained_deadlines.v ./model/schedule/global/jitter/schedule.v ./model/schedule/global/jitter/platform.v ./model/schedule/global/response_time.v ./model/schedule/global/basic/interference_edf.v ./model/schedule/global/basic/interference.v ./model/schedule/global/basic/constrained_deadlines.v ./model/schedule/global/basic/schedule.v ./model/schedule/global/basic/platform.v ./model/schedule/apa/interference_edf.v ./model/schedule/apa/interference.v ./model/schedule/apa/affinity.v ./model/schedule/apa/constrained_deadlines.v ./model/schedule/apa/platform.v ./model/schedule/uni/workload.v ./model/schedule/uni/transformation/construction.v ./model/schedule/uni/susp/suspension_intervals.v ./model/schedule/uni/susp/last_execution.v ./model/schedule/uni/susp/schedule.v ./model/schedule/uni/susp/platform.v ./model/schedule/uni/schedulability.v ./model/schedule/uni/jitter/busy_interval.v ./model/schedule/uni/jitter/schedule.v ./model/schedule/uni/jitter/platform.v ./model/schedule/uni/schedule_of_task.v ./model/schedule/uni/response_time.v ./model/schedule/uni/schedule.v ./model/schedule/uni/basic/busy_interval.v ./model/schedule/uni/basic/platform.v ./model/schedule/uni/service.v ./model/arrival/jitter/arrival_sequence.v ./model/arrival/jitter/task_arrival.v ./model/arrival/jitter/job.v ./model/arrival/jitter/arrival_bounds.v ./model/arrival/basic/arrival_sequence.v ./model/arrival/basic/task.v ./model/arrival/basic/task_arrival.v ./model/arrival/basic/job.v ./model/arrival/basic/arrival_bounds.v ./model/priority.v ./model/time.v ./implementation/arrival_sequence.v ./implementation/task.v ./implementation/global/jitter/arrival_sequence.v ./implementation/global/jitter/task.v ./implementation/global/jitter/bertogna_edf_example.v ./implementation/global/jitter/job.v ./implementation/global/jitter/bertogna_fp_example.v ./implementation/global/jitter/schedule.v ./implementation/global/parallel/bertogna_edf_example.v ./implementation/global/parallel/bertogna_fp_example.v ./implementation/global/basic/bertogna_edf_example.v ./implementation/global/basic/bertogna_fp_example.v ./implementation/global/basic/schedule.v ./implementation/job.v ./implementation/apa/arrival_sequence.v ./implementation/apa/task.v ./implementation/apa/bertogna_edf_example.v ./implementation/apa/job.v ./implementation/apa/bertogna_fp_example.v ./implementation/apa/schedule.v ./implementation/uni/susp/dynamic/arrival_sequence.v ./implementation/uni/susp/dynamic/task.v ./implementation/uni/susp/dynamic/job.v ./implementation/uni/susp/dynamic/oblivious/fp_rta_example.v ./implementation/uni/susp/schedule.v ./implementation/uni/jitter/arrival_sequence.v ./implementation/uni/jitter/task.v ./implementation/uni/jitter/job.v ./implementation/uni/jitter/fp_rta_example.v ./implementation/uni/jitter/schedule.v ./implementation/uni/basic/fp_rta_example.v ./implementation/uni/basic/schedule.v -o Makefile
#
.DEFAULT_GOAL := all
......@@ -157,6 +157,7 @@ VFILES:=util/ssromega.v\
model/schedule/partitioned/schedulability.v\
model/schedule/partitioned/schedule.v\
model/schedule/global/workload.v\
model/schedule/global/transformation/construction.v\
model/schedule/global/schedulability.v\
model/schedule/global/jitter/interference_edf.v\
model/schedule/global/jitter/interference.v\
......@@ -182,11 +183,9 @@ VFILES:=util/ssromega.v\
model/schedule/uni/susp/schedule.v\
model/schedule/uni/susp/platform.v\
model/schedule/uni/schedulability.v\
model/schedule/uni/jitter/workload.v\
model/schedule/uni/jitter/busy_interval.v\
model/schedule/uni/jitter/schedule.v\
model/schedule/uni/jitter/platform.v\
model/schedule/uni/jitter/service.v\
model/schedule/uni/schedule_of_task.v\
model/schedule/uni/response_time.v\
model/schedule/uni/schedule.v\
......
analysis/apa/bertogna_edf_comp.v
View file @ a58b283a
......@@ -16,6 +16,7 @@ Module ResponseTimeIterationEDF.
Variable task_deadline: sporadic_task -> time.
Context {Job: eqType}.
Variable job_arrival: Job -> time.
Variable job_cost: Job -> time.
Variable job_deadline: Job -> time.
Variable job_task: Job -> sporadic_task.
......@@ -883,46 +884,51 @@ Module ResponseTimeIterationEDF.
forall tsk, tsk \in ts -> is_subaffinity (alpha' tsk) (alpha tsk).
(* Next, consider any arrival sequence such that...*)
Context {arr_seq: arrival_sequence Job}.
Variable arr_seq: arrival_sequence Job.
(* ...all jobs come from task set ts, ...*)
Hypothesis H_all_jobs_from_taskset:
forall (j: JobIn arr_seq), job_task j \in ts.
forall j,
arrives_in arr_seq j -> job_task j \in ts.
(* ...they have valid parameters,...*)
Hypothesis H_valid_job_parameters:
forall (j: JobIn arr_seq),
forall j,
arrives_in arr_seq j ->
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
(* ... and satisfy the sporadic task model.*)
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period arr_seq job_task.
sporadic_task_model task_period job_arrival job_task arr_seq.
(* Then, consider any schedule with at least one CPU such that...*)
Variable sched: schedule num_cpus arr_seq.
Variable sched: schedule Job num_cpus.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
(* ...jobs only execute after they arrived and no longer
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.
Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
(* ...and jobs are sequential. *)
Hypothesis H_sequential_jobs: sequential_jobs sched.
(* Assume a work-conserving APA scheduler that respects EDF policy. *)
Hypothesis H_respects_affinity: respects_affinity job_task sched alpha.
Hypothesis H_work_conserving: apa_work_conserving job_cost job_task sched alpha.
Hypothesis H_edf_policy: respects_JLFP_policy_under_weak_APA job_cost job_task sched alpha (EDF job_deadline).
Hypothesis H_work_conserving: apa_work_conserving job_arrival job_cost job_task arr_seq
sched alpha.
Hypothesis H_edf_policy:
respects_JLFP_policy_under_weak_APA job_arrival job_cost job_task
arr_seq sched alpha (EDF job_arrival job_deadline).
(* To avoid a long list of parameters, we provide some local definitions. *)
Definition no_deadline_missed_by_task (tsk: sporadic_task) :=
task_misses_no_deadline job_cost job_deadline job_task sched tsk.
task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched tsk.
Definition no_deadline_missed_by_job :=
job_misses_no_deadline job_cost job_deadline sched.
job_misses_no_deadline job_arrival 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.
is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched tsk.
(* 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
......@@ -933,12 +939,12 @@ Module ResponseTimeIterationEDF.
response_time_bounded_by tsk R.
Proof.
have BOUND := bertogna_cirinei_response_time_bound_edf.
intros tsk R IN j JOBj.
intros tsk R IN j ARRj JOBj.
destruct (edf_claimed_bounds ts) as [rt_bounds |] eqn:SOME; last by done.
unfold edf_rta_iteration in *.
unfold is_response_time_bound_of_task in *.
apply BOUND with (task_cost := task_cost) (task_period := task_period)
(task_deadline := task_deadline) (job_deadline := job_deadline)
(arr_seq := arr_seq) (task_deadline := task_deadline) (job_deadline := job_deadline)
(job_task := job_task) (ts := ts) (tsk := tsk) (rt_bounds := rt_bounds) (alpha := alpha) (alpha' := alpha'); try (by ins).
by unfold edf_claimed_bounds in SOME; desf; rewrite edf_claimed_bounds_unzip1_iteration.
by ins; apply edf_claimed_bounds_finds_fixed_point_for_each_bound with (ts := ts).
......@@ -960,10 +966,10 @@ Module ResponseTimeIterationEDF.
edf_schedulable,
valid_sporadic_job in *.
rename H_valid_job_parameters into JOBPARAMS.
intros tsk INtsk j JOBtsk.
intros tsk INtsk j ARRj JOBtsk.
destruct (edf_claimed_bounds ts) as [rt_bounds |] eqn:SOME; last by ins.
exploit (HAS rt_bounds tsk); [by ins | by ins | clear HAS; intro HAS; des].
have COMPLETED := RLIST tsk R HAS j JOBtsk.
have COMPLETED := RLIST tsk R HAS j ARRj JOBtsk.
exploit (DL rt_bounds tsk R);
[by ins | by ins | clear DL; intro DL].
......@@ -972,7 +978,7 @@ Module ResponseTimeIterationEDF.
{
unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
apply extend_sum; rewrite // leq_add2l.
specialize (JOBPARAMS j); des; rewrite JOBPARAMS1.
specialize (JOBPARAMS j ARRj); des; rewrite JOBPARAMS1.
by rewrite JOBtsk.
}
rewrite leq_eqVlt; apply/orP; left; rewrite eq_sym.
......@@ -983,12 +989,12 @@ Module ResponseTimeIterationEDF.
are spawned by the task set, we conclude that no job misses
its deadline. *)
Theorem jobs_schedulable_by_edf_rta :
forall (j: JobIn arr_seq), no_deadline_missed_by_job j.
forall j, arrives_in arr_seq j -> no_deadline_missed_by_job j.
Proof.
intros j.
intros j ARRj.
have SCHED := taskset_schedulable_by_edf_rta.
unfold no_deadline_missed_by_task, task_misses_no_deadline in *.
apply SCHED with (tsk := job_task j); last by done.
apply SCHED with (tsk := job_task j); try (by done).
by apply H_all_jobs_from_taskset.
Qed.
......
analysis/apa/bertogna_edf_theory.v
View file @ a58b283a
This diff is collapsed.
analysis/apa/bertogna_fp_comp.v
View file @ a58b283a
......@@ -16,6 +16,7 @@ Module ResponseTimeIterationFP.
Variable task_deadline: sporadic_task -> time.
Context {Job: eqType}.
Variable job_arrival: Job -> time.
Variable job_cost: Job -> time.
Variable job_deadline: Job -> time.
Variable job_task: Job -> sporadic_task.
......@@ -503,47 +504,50 @@ Module ResponseTimeIterationFP.
Hypothesis H_priority_transitive: FP_is_transitive higher_priority.
(* Next, consider any arrival sequence such that...*)
Context {arr_seq: arrival_sequence Job}.
Variable arr_seq: arrival_sequence Job.
(* ...all jobs come from task set ts, ...*)
Hypothesis H_all_jobs_from_taskset:
forall (j: JobIn arr_seq), job_task j \in ts.
forall j, arrives_in arr_seq j -> job_task j \in ts.
(* ...jobs have valid parameters,...*)
Hypothesis H_valid_job_parameters:
forall (j: JobIn arr_seq),
forall j,
arrives_in arr_seq j ->
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
(* ... and satisfy the sporadic task model.*)
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period arr_seq job_task.
sporadic_task_model task_period job_arrival job_task arr_seq.
(* Then, consider any schedule such that...*)
Variable sched: schedule num_cpus arr_seq.
Variable sched: schedule Job num_cpus.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
(* ...jobs only execute after they arrived and no longer
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.
Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
(* ...and jobs are sequential. *)
Hypothesis H_sequential_jobs: sequential_jobs sched.
(* Assume a work-conserving APA scheduler that respects the FP policy. *)
Hypothesis H_respects_affinity: respects_affinity job_task sched alpha.
Hypothesis H_work_conserving: apa_work_conserving job_cost job_task sched alpha.
Hypothesis H_work_conserving: apa_work_conserving job_arrival job_cost job_task arr_seq
sched alpha.
Hypothesis H_respects_FP_policy:
respects_FP_policy_under_weak_APA job_cost job_task sched alpha higher_priority.
respects_FP_policy_under_weak_APA job_arrival job_cost job_task arr_seq sched
alpha higher_priority.
(* To avoid a long list of parameters, we provide some local definitions. *)
Let no_deadline_missed_by_task (tsk: sporadic_task) :=
task_misses_no_deadline job_cost job_deadline job_task sched tsk.
task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched tsk.
Let no_deadline_missed_by_job :=
job_misses_no_deadline job_cost job_deadline sched.
job_misses_no_deadline job_arrival 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.
is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched tsk.
(* In the following theorem, we prove that any response-time bound contained
in fp_claimed_bounds is safe. The proof follows by induction on the task set:
......@@ -580,20 +584,13 @@ Module ResponseTimeIterationFP.
clear EQ.
assert (PAIR: forall idx, (TASK idx, RESP idx) = NTH idx).
{
by intros i; unfold TASK, RESP; destruct (NTH i).
}
assert (SUBST: forall i, i < size hp_bounds -> TASK i = nth tsk ts i).
{
by intros i LTi; rewrite /TASK /NTH -UNZIP (nth_map elem) //.
}
assert (SIZE: size hp_bounds = size ts).
{
by rewrite -UNZIP size_map.
}
induction idx as [idx IH'] using strong_ind.
......@@ -688,7 +685,7 @@ Module ResponseTimeIterationFP.
job_misses_no_deadline, completed,
fp_schedulable, valid_sporadic_job in *.
rename H_valid_job_parameters into JOBPARAMS.
move => tsk INtsk j JOBtsk.
move => tsk INtsk j ARRj JOBtsk.
destruct (fp_claimed_bounds ts) as [rt_bounds |]; last by ins.
feed (UNZIP rt_bounds); first by done.
......@@ -697,14 +694,14 @@ Module ResponseTimeIterationFP.
rewrite set_mem -UNZIP in INtsk; move: INtsk => /mapP EX.
by destruct EX as [p]; destruct p as [tsk' R]; simpl in *; subst tsk'; exists R.
} des.
exploit (RLIST tsk R); [by ins | by apply JOBtsk | intro COMPLETED].
exploit (RLIST tsk R EX j ARRj); [by apply JOBtsk | intro COMPLETED].
exploit (DL rt_bounds tsk R); [by ins | by ins | clear DL; intro DL].
rewrite eqn_leq; apply/andP; split; first by apply cumulative_service_le_job_cost.
apply leq_trans with (n := service sched j (job_arrival j + R)); last first.
{
unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
apply extend_sum; rewrite // leq_add2l.
specialize (JOBPARAMS j); des; rewrite JOBPARAMS1.
specialize (JOBPARAMS j ARRj); des; rewrite JOBPARAMS1.
by rewrite JOBtsk.
}
rewrite leq_eqVlt; apply/orP; left; rewrite eq_sym.
......@@ -715,12 +712,12 @@ Module ResponseTimeIterationFP.
are spawned by the task set, we also conclude that no job in
the schedule misses its deadline. *)
Theorem jobs_schedulable_by_fp_rta :
forall (j: JobIn arr_seq), no_deadline_missed_by_job j.
forall j, arrives_in arr_seq j -> no_deadline_missed_by_job j.
Proof.
intros j.
intros j ARRj.
have SCHED := taskset_schedulable_by_fp_rta.
unfold no_deadline_missed_by_task, task_misses_no_deadline in *.
apply SCHED with (tsk := job_task j); last by done.
apply SCHED with (tsk := job_task j); try (by done).
by apply H_all_jobs_from_taskset.
Qed.
......
analysis/apa/bertogna_fp_theory.v
View file @ a58b283a
This diff is collapsed.
analysis/apa/interference_bound_edf.v
View file @ a58b283a
This diff is collapsed.
analysis/apa/workload_bound.v
View file @ a58b283a
......@@ -122,6 +122,7 @@ Module WorkloadBound.
Variable task_deadline: sporadic_task -> time.
Context {Job: eqType}.
Variable job_arrival: Job -> time.
Variable job_cost: Job -> time.
Variable job_task: Job -> sporadic_task.
Variable job_deadline: Job -> time.
......@@ -130,22 +131,23 @@ Module WorkloadBound.
(* Assume that all jobs have valid parameters *)
Hypothesis H_jobs_have_valid_parameters :
forall (j: JobIn arr_seq),
forall j,
arrives_in arr_seq j ->
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
(* Consider any schedule. *)
Context {num_cpus: nat}.
Variable sched: schedule num_cpus arr_seq.
Variable sched: schedule Job num_cpus.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
(* Assumption: jobs only execute if they arrived.
This is used to eliminate jobs that arrive after end of the interval t1 + delta. *)
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute sched.
Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute job_arrival sched.
(* Assumption: jobs do not execute after they completed.
This is used to eliminate jobs that complete before the start of the interval t1. *)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
(* Assumption: Jobs are sequential.
This is required to use interval lengths as a measure of service. *)
......@@ -154,13 +156,12 @@ Module WorkloadBound.
(* Assumption: sporadic task model.
This is necessary to conclude that consecutive jobs ordered by arrival times
are separated by at least 'period' times units. *)
Hypothesis H_sporadic_tasks: sporadic_task_model task_period arr_seq job_task.
Hypothesis H_sporadic_tasks: sporadic_task_model task_period job_arrival job_task arr_seq.
(* Before starting the proof, let's give simpler names to the definitions. *)
Let job_has_completed_by := completed job_cost sched.
Let workload_of (tsk: sporadic_task) (t1 t2: time) :=
workload job_task sched tsk t1 t2.
Let workload_of (tsk: sporadic_task) (t1 t2: time) := workload job_task sched tsk t1 t2.
(* Now we define the theorem. Let tsk be any task in the taskset. *)
Variable tsk: sporadic_task.
......@@ -190,10 +191,11 @@ Module WorkloadBound.
Variable R_tsk: time.
Hypothesis H_response_time_bound :
forall (j: JobIn arr_seq),
job_task j = tsk ->
job_arrival j + R_tsk < t1 + delta ->
job_has_completed_by j (job_arrival j + R_tsk).
forall j,
arrives_in arr_seq j ->
job_task j = tsk ->
job_arrival j + R_tsk < t1 + delta ->
job_has_completed_by j (job_arrival j + R_tsk).
(* ... such that R_tsk >= task_cost tsk and R_tsk <= task_deadline tsk. *)
Hypothesis H_response_time_ge_cost: R_tsk >= task_cost tsk.
......@@ -215,8 +217,8 @@ Module WorkloadBound.
jobs_of_task_scheduled_between job_task sched tsk t1 t2.
(* Now, let's consider the list of interfering jobs sorted by arrival time. *)
Let earlier_arrival := fun (x y: JobIn arr_seq) => job_arrival x <= job_arrival y.
Let sorted_jobs := (sort earlier_arrival scheduled_jobs).
Let earlier_arrival := fun x y => job_arrival x <= job_arrival y.
Let sorted_jobs := sort earlier_arrival scheduled_jobs.
(* The first step consists in simplifying the sum corresponding
to the workload. *)
......@@ -246,13 +248,19 @@ Module WorkloadBound.
Lemma workload_bound_all_jobs_from_tsk :
forall j_i,
j_i \in sorted_jobs ->
arrives_in arr_seq j_i /\
job_task j_i = tsk /\
service_during sched j_i t1 t2 != 0 /\
j_i \in jobs_scheduled_between sched t1 t2.
Proof.
rename H_jobs_come_from_arrival_sequence into FROMarr.
intros j_i LTi.
rewrite -workload_bound_job_in_same_sequence mem_filter in LTi; des.
repeat split; [by done | | by done].
have IN := LTi0.
unfold jobs_scheduled_between in *; rewrite mem_undup in IN.
apply mem_bigcat_nat_exists in IN; des.
rewrite mem_scheduled_jobs_eq_scheduled in IN.
repeat split; try (by done); first by apply (FROMarr j_i i).
unfold jobs_scheduled_between in *; rewrite mem_undup in LTi0.
apply mem_bigcat_nat_exists in LTi0; des.
rewrite mem_scheduled_jobs_eq_scheduled in LTi0.
......@@ -294,7 +302,7 @@ Module WorkloadBound.
apply leq_sum; intros j_i; move/andP => [INi _].
apply workload_bound_all_jobs_from_tsk in INi; des.
eapply cumulative_service_le_task_cost;
[by apply H_completed_jobs_dont_execute | by apply INi |].
[by apply H_completed_jobs_dont_execute | by apply INi0 |].
by apply H_jobs_have_valid_parameters.
}
Qed.
......@@ -308,11 +316,12 @@ Module WorkloadBound.
(* Assume that there's at least one job in the sorted list. *)
Hypothesis H_at_least_one_job: size sorted_jobs > 0.
Variable elem: JobIn arr_seq.
Variable elem: Job.
Let j_fst := nth elem sorted_jobs 0.
(* The first job is an interfering job of task tsk. *)
Lemma workload_bound_j_fst_is_job_of_tsk :
arrives_in arr_seq j_fst /\
job_task j_fst = tsk /\
service_during sched j_fst t1 t2 != 0 /\
j_fst \in jobs_scheduled_between sched t1 t2.
......@@ -334,14 +343,14 @@ Module WorkloadBound.
rewrite -[service_during _ _ _ _]add0n [_* task_cost tsk]mulSnr.
apply leq_add; first by done.
by eapply cumulative_service_le_task_cost;
[| by apply INfst
[| by apply INfst0
| by apply H_jobs_have_valid_parameters].
}
{
rewrite 2!mul0n addn0 subn0 leq_min; apply/andP; split.
{
by eapply cumulative_service_le_task_cost;
[| by apply INfst
[| by apply INfst0
| by apply H_jobs_have_valid_parameters].
}
{
......@@ -362,12 +371,13 @@ Module WorkloadBound.
Variable num_mid_jobs: nat.
Hypothesis H_at_least_two_jobs : size sorted_jobs = num_mid_jobs.+2.
Variable elem: JobIn arr_seq.
Variable elem: Job.
Let j_fst := nth elem sorted_jobs 0.
Let j_lst := nth elem sorted_jobs num_mid_jobs.+1.
(* The last job is an interfering job of task tsk. *)
Lemma workload_bound_j_lst_is_job_of_tsk :
arrives_in arr_seq j_lst /\
job_task j_lst = tsk /\
service_during sched j_lst t1 t2 != 0 /\
j_lst \in jobs_scheduled_between sched t1 t2.
......@@ -386,11 +396,11 @@ Module WorkloadBound.
apply mem_nth; instantiate (1 := 0).
apply ltn_trans with (n := 1); [by done | by rewrite H_at_least_two_jobs].
}
instantiate (1 := elem); move => [FSTtsk [/eqP FSTserv FSTin]].
instantiate (1 := elem); move => [FSTarr [FSTtsk [/eqP FSTserv FSTin]]].
apply FSTserv.
apply (cumulative_service_after_job_rt_zero job_cost) with (R := R_tsk);
apply (cumulative_service_after_job_rt_zero job_arrival job_cost) with (R := R_tsk);
try (by done); last by apply ltnW.
apply H_response_time_bound; first by done.
apply H_response_time_bound; try (by done).
by apply leq_trans with (n := t1); last by apply leq_addr.
Qed.
......@@ -404,8 +414,9 @@ Module WorkloadBound.
apply mem_nth; instantiate (1 := num_mid_jobs.+1).
by rewrite -(ltn_add2r 1) addn1 H_at_least_two_jobs addn1.
}
instantiate (1 := elem); move => [LSTtsk [/eqP LSTserv LSTin]].
by unfold service_during; apply LSTserv, cumulative_service_before_job_arrival_zero.
instantiate (1 := elem); move => [LSTarr [LSTtsk [/eqP LSTserv LSTin]]].
unfold service_during; apply LSTserv.
by apply cumulative_service_before_job_arrival_zero with (job_arrival0 := job_arrival).
Qed.
(* Next, we upper-bound the service of the first and last jobs using their arrival times. *)
......@@ -431,11 +442,11 @@ Module WorkloadBound.
[| by apply workload_bound_response_time_of_first_job_inside_interval
| by apply ltnW].
rewrite -{2}[\sum_(_ <= _ < _) _]addn0 /= leq_add2l leqn0; apply/eqP.
apply (cumulative_service_after_job_rt_zero job_cost) with (R := R_tsk); try (by done).
apply H_response_time_bound; last by done.
apply (cumulative_service_after_job_rt_zero job_arrival job_cost) with (R := R_tsk); try (by done).
exploit workload_bound_all_jobs_from_tsk.
by apply mem_nth; instantiate (1 := 0); rewrite H_at_least_two_jobs.
by instantiate (1 := elem); move => [FSTtsk _].
instantiate (1 := elem); move => [FSTarr [FSTtsk _]].
by apply H_response_time_bound.
}
}
{
......@@ -454,7 +465,7 @@ Module WorkloadBound.
[| by apply ltnW
| by apply ltnW, workload_bound_last_job_arrives_before_end_of_interval].
rewrite /= -[\sum_(_ <= _ < _) 1]add0n; apply leq_add.
rewrite cumulative_service_before_job_arrival_zero;
rewrite (cumulative_service_before_job_arrival_zero job_arrival);
[by apply leqnn | by ins | by apply leqnn].
by apply leq_sum; ins; apply service_at_most_one.
}
......@@ -490,15 +501,14 @@ Module WorkloadBound.
last by rewrite big_const_nat iter_addn addn0 mulnC subn0.
rewrite big_nat_cond [\sum_(0 <= i < num_mid_jobs) task_cost _]big_nat_cond.
apply leq_sum; intros i; rewrite andbT; move => /andP LT; des.
eapply cumulative_service_le_task_cost;
[by apply H_completed_jobs_dont_execute | | by apply H_jobs_have_valid_parameters].
exploit workload_bound_all_jobs_from_tsk.
{
instantiate (1 := nth elem sorted_jobs i.+1).
apply mem_nth; rewrite H_at_least_two_jobs.
by rewrite ltnS; apply leq_trans with (n := num_mid_jobs).
}
by ins; des.
move => [ARR [TSK _]].
by eapply cumulative_service_le_task_cost; eauto 2.
Qed.
(* Conclude that the distance between first and last is at least num_mid_jobs + 1 periods. *)
......@@ -521,14 +531,13 @@ Module WorkloadBound.
assert (ARRle: job_arrival cur <= job_arrival next).
by unfold cur, next; apply workload_bound_jobs_ordered_by_arrival.
(* Show that both cur and next are in the arrival sequence *)
assert (INnth: cur \in scheduled_jobs /\ next \in scheduled_jobs).
{
rewrite 2!workload_bound_job_in_same_sequence; split.
by apply mem_nth, (ltn_trans LT0); destruct sorted_jobs; ins.
by apply mem_nth; destruct sorted_jobs; ins.
}
rewrite 2?mem_filter in INnth; des.
feed (workload_bound_all_jobs_from_tsk cur).
by apply mem_nth, (ltn_trans LT0); destruct sorted_jobs.
intros [CURarr [CURtsk [_ CURin]]].
feed (workload_bound_all_jobs_from_tsk next).
by apply mem_nth; destruct sorted_jobs.
intros [NEXTarr [NEXTtsk [_ NEXTin]]].
(* Use the sporadic task model to conclude that cur and next are separated
by at least (task_period tsk) units. Of course this only holds if cur != next.
......@@ -536,15 +545,15 @@ Module WorkloadBound.
also prove that it doesn't contain duplicates. *)
assert (CUR_LE_NEXT: job_arrival cur + task_period (job_task cur) <= job_arrival next).
{
apply H_sporadic_tasks; last by ins.
apply H_sporadic_tasks; try (by done).
unfold cur, next, not; intro EQ; move: EQ => /eqP EQ.
rewrite nth_uniq in EQ; first by move: EQ => /eqP EQ; intuition.
by apply ltn_trans with (n := (size sorted_jobs).-1); destruct sorted_jobs; ins.
by destruct sorted_jobs; ins.