Skip to content
Snippets Groups Projects
Commit 7755715d authored by Felipe Cerqueira's avatar Felipe Cerqueira
Browse files

Remove rate from the definitions

parent 331a6359
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 201 additions and 327 deletions
bertogna_edf_comp.v
+ 7
− 11
View file @ 7755715d
......@@ -912,21 +912,17 @@ Module ResponseTimeIterationEDF.
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period arr_seq job_task.
(* Then, consider any platform with at least one CPU and unit
unit execution rate, where...*)
Variable rate: Job -> processor num_cpus -> nat.
(* 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_rate_equals_one :
forall j cpu, rate j cpu = 1.
(* ...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 rate sched.
completed_jobs_dont_execute job_cost sched.
(* ...and do not execute in parallel. *)
Hypothesis H_no_parallelism:
......@@ -949,12 +945,12 @@ Module ResponseTimeIterationEDF.
Let higher_eq_priority :=
@EDF Job arr_seq job_deadline. (* TODO: implicit params seems broken *)
Hypothesis H_global_scheduling_invariant:
JLFP_JLDP_scheduling_invariant_holds job_cost num_cpus rate sched higher_eq_priority.
JLFP_JLDP_scheduling_invariant_holds job_cost num_cpus sched higher_eq_priority.
Definition no_deadline_missed_by_task (tsk: sporadic_task) :=
task_misses_no_deadline job_cost job_deadline job_task rate sched tsk.
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 rate sched.
job_misses_no_deadline job_cost job_deadline 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
......@@ -964,7 +960,7 @@ Module ResponseTimeIterationEDF.
(tsk, R) \In edf_claimed_bounds ts ->
forall j : JobIn arr_seq,
job_task j = tsk ->
completed job_cost rate sched j (job_arrival j + R).
completed job_cost sched j (job_arrival j + R).
Proof.
intros tsk R IN j JOBj.
destruct (edf_claimed_bounds ts) as [rt_bounds |] eqn:SOME; last by done.
......@@ -1011,7 +1007,7 @@ Module ResponseTimeIterationEDF.
[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 rate sched j (job_arrival j + R)); last first.
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.
......
bertogna_edf_theory.v
+ 33
− 31
View file @ 7755715d
......@@ -88,7 +88,6 @@ Module ResponseTimeAnalysisEDF.
(* Consider any schedule such that...*)
Variable num_cpus: nat.
Variable rate: Job -> processor num_cpus -> nat.
Variable sched: schedule num_cpus arr_seq.
(* ...jobs do not execute before their arrival times nor longer
......@@ -96,14 +95,12 @@ Module ResponseTimeAnalysisEDF.
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 rate sched.
completed_jobs_dont_execute job_cost sched.
(* Also assume that jobs do not execute in parallel, processors have
unit speed, and that there exists at least one processor. *)
(* 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_rate_equals_one :
forall j cpu, rate j cpu = 1.
Hypothesis H_at_least_one_cpu :
num_cpus > 0.
......@@ -128,9 +125,9 @@ Module ResponseTimeAnalysisEDF.
forall tsk, tsk \in ts -> task_deadline tsk <= task_period tsk.
Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
task_misses_no_deadline job_cost job_deadline job_task rate sched tsk.
task_misses_no_deadline job_cost job_deadline job_task sched tsk.
Let response_time_bounded_by (tsk: sporadic_task) :=
is_response_time_bound_of_task job_cost job_task tsk rate sched.
is_response_time_bound_of_task job_cost job_task tsk sched.
(* Assume a known response-time bound R is known... *)
Let task_with_response_time := (sporadic_task * time)%type.
......@@ -152,13 +149,20 @@ Module ResponseTimeAnalysisEDF.
forall tsk_other R,
(tsk_other, R) \in rt_bounds -> R <= task_deadline tsk_other.
Let higher_eq_priority := @EDF Job arr_seq job_deadline. (* TODO: implicit params broken *)
(* Assume that the schedule satisfies the global scheduling invariant
for EDF, i.e., if any job of tsk is backlogged, every processor
must be busy with jobs with no larger absolute deadline. *)
Let higher_eq_priority := @EDF Job arr_seq job_deadline. (* TODO: implicit params broken *)
Hypothesis H_global_scheduling_invariant:
JLFP_JLDP_scheduling_invariant_holds job_cost num_cpus rate sched higher_eq_priority.
JLFP_JLDP_scheduling_invariant_holds job_cost num_cpus sched higher_eq_priority.
(* Assume that the task set has no duplicates. Otherwise, counting
the number of tasks that have some property does not make sense
(for example, for stating the global scheduling invariant as
using number of scheduled interfering tasks = number of cpus). *)
Hypothesis H_ts_is_a_set : uniq ts.
(* In order to prove that R is a response-time bound, we first present some lemmas. *)
Section Lemmas.
......@@ -173,7 +177,7 @@ Module ResponseTimeAnalysisEDF.
Hypothesis H_job_of_tsk: job_task j = tsk.
(* Assume that job j did not complete on time, ... *)
Hypothesis H_j_not_completed: ~~ completed job_cost rate sched j (job_arrival j + R).
Hypothesis H_j_not_completed: ~~ completed job_cost sched j (job_arrival j + R).
(* and that it is the first job not to satisfy its response-time bound. *)
Hypothesis H_all_previous_jobs_completed_on_time :
......@@ -181,15 +185,15 @@ Module ResponseTimeAnalysisEDF.
job_task j_other = tsk_other ->
(tsk_other, R_other) \in rt_bounds ->
job_arrival j_other + R_other < job_arrival j + R ->
completed job_cost rate sched j_other (job_arrival j_other + R_other).
completed job_cost sched j_other (job_arrival j_other + R_other).
(* Let's call x the interference incurred by job j due to tsk_other, ...*)
Let x (tsk_other: sporadic_task) :=
task_interference job_cost job_task rate sched j
task_interference job_cost job_task sched j
tsk_other (job_arrival j) (job_arrival j + R).
(* and X the total interference incurred by job j due to any task. *)
Let X := total_interference job_cost rate sched j (job_arrival j) (job_arrival j + R).
Let X := total_interference job_cost sched j (job_arrival j) (job_arrival j + R).
(* Recall Bertogna and Cirinei's workload bound ... *)
Let workload_bound (tsk_other: sporadic_task) (R_other: time) :=
......@@ -234,21 +238,19 @@ Module ResponseTimeAnalysisEDF.
x tsk_other <= workload_bound tsk_other R_other.
Proof.
unfold valid_sporadic_job in *.
rename H_rate_equals_one into RATE,
H_all_previous_jobs_completed_on_time into BEFOREok,
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_tasks_miss_no_deadlines into NOMISS.
unfold x, task_interference.
have INts := bertogna_edf_tsk_other_in_ts.
apply leq_trans with (n := workload job_task rate sched tsk_other
apply leq_trans with (n := workload job_task sched tsk_other
(job_arrival j) (job_arrival j + R));
first by apply task_interference_le_workload; ins; rewrite RATE.
first by apply task_interference_le_workload.
apply workload_bounded_by_W with (task_deadline0 := task_deadline) (job_cost0 := job_cost) (job_deadline0 := job_deadline); try (by ins); last 2 first;
[ by apply bertogna_edf_R_other_ge_cost
| by ins; apply BEFOREok with (tsk_other := tsk_other); ins; rewrite RATE
| by ins; rewrite RATE
| by ins; apply BEFOREok with (tsk_other := tsk_other)
| by ins; apply TASK_PARAMS
| by ins; apply RESTR |].
red; move => j' JOBtsk' LEdl; unfold job_misses_no_deadline.
......@@ -289,7 +291,7 @@ Module ResponseTimeAnalysisEDF.
(* Since j has not completed, recall the time when it is not
executing is the total interference. *)
exploit (complement_of_interf_equals_service job_cost rate sched j (job_arrival j)
exploit (complement_of_interf_equals_service job_cost sched j (job_arrival j)
(job_arrival j + R));
last intro EQinterf; ins; unfold has_arrived; first by apply leqnn.
rewrite {2}[_ + R]addnC -addnBA // subnn addn0 in EQinterf.
......@@ -300,7 +302,7 @@ Module ResponseTimeAnalysisEDF.
apply (leq_ltn_trans (COMP j (job_arrival j + R))) in NOTCOMP.
by rewrite ltnn in NOTCOMP.
}
apply leq_trans with (n := R - service rate sched j (job_arrival j + R)); last first.
apply leq_trans with (n := R - service sched j (job_arrival j + R)); last first.
{
unfold service; rewrite service_before_arrival_eq_service_during; ins.
rewrite EQinterf subKn; first by done.
......@@ -333,9 +335,9 @@ Module ResponseTimeAnalysisEDF.
rename H_global_scheduling_invariant into INV.
unfold x, X, total_interference, task_interference.
rewrite -big_mkcond -exchange_big big_distrl /=.
rewrite [\sum_(_ <= _ < _ | backlogged _ _ _ _ _) _]big_mkcond.
rewrite [\sum_(_ <= _ < _ | backlogged _ _ _ _) _]big_mkcond.
apply eq_big_nat; move => t LTt.
destruct (backlogged job_cost rate sched j t) eqn:BACK;
destruct (backlogged job_cost sched j t) eqn:BACK;
last by rewrite (eq_bigr (fun i => 0));
[by rewrite big_const_seq iter_addn mul0n addn0 | by done].
rewrite big_mkcond mul1n /=.
......@@ -363,11 +365,11 @@ Module ResponseTimeAnalysisEDF.
rename H_global_scheduling_invariant into INVARIANT.
intros delta HAS.
set some_interference_A := fun t =>
backlogged job_cost rate sched j t &&
backlogged job_cost sched j t &&
has (fun tsk_k => ((x tsk_k >= delta) &&
task_is_scheduled job_task sched tsk_k t)) ts_interf.
set total_interference_B := fun t =>
backlogged job_cost rate sched j t *
backlogged job_cost sched j t *
count (fun tsk_k => (x tsk_k < delta) &&
task_is_scheduled job_task sched tsk_k t) ts_interf.
......@@ -380,7 +382,7 @@ Module ResponseTimeAnalysisEDF.
apply leq_trans with (n := x tsk_a); first by apply LEa.
unfold x, task_interference, some_interference_A.
apply leq_sum; ins.
destruct (backlogged job_cost rate sched j i);
destruct (backlogged job_cost sched j i);
[rewrite 2!andTb | by ins].
destruct (task_is_scheduled job_task sched tsk_a i) eqn:SCHEDa;
[apply eq_leq; symmetry | by ins].
......@@ -393,7 +395,7 @@ Module ResponseTimeAnalysisEDF.
rewrite big_distrl /=.
apply leq_sum; intros t _.
unfold some_interference_A, total_interference_B.
destruct (backlogged job_cost rate sched j t) eqn:BACK;
destruct (backlogged job_cost sched j t) eqn:BACK;
[rewrite andTb mul1n | by done].
destruct (has (fun tsk_k : sporadic_task => (delta <= x tsk_k) &&
task_is_scheduled job_task sched tsk_k t) ts_interf) eqn:HAS';
......@@ -455,7 +457,7 @@ Module ResponseTimeAnalysisEDF.
unfold x at 2, task_interference.
rewrite exchange_big /=; apply leq_sum; intros t _.
unfold total_interference_B.
destruct (backlogged job_cost rate sched j t); last by ins.
destruct (backlogged job_cost sched j t); last by ins.
rewrite mul1n -sum1_count.
rewrite big_seq_cond big_mkcond [\sum_(i <- ts_interf | _ < _) _]big_mkcond.
by apply leq_sum; ins; clear -i; desf; des; rewrite ?Heq2.
......@@ -631,7 +633,7 @@ Module ResponseTimeAnalysisEDF.
job_task j0 = tsk ->
(tsk, R0) \in rt_bounds ->
job_arrival j0 + R0 < job_arrival j + R' ->
service rate sched j0 (job_arrival j0 + R0) == job_cost j0).
service sched j0 (job_arrival j0 + R0) == job_cost j0).
{
by ins; apply IH with (tsk := tsk0) (R := R0).
}
......@@ -640,7 +642,7 @@ Module ResponseTimeAnalysisEDF.
(* The proof follows by contradiction. Assume that job j does not complete by its
response-time bound. By the induction hypothesis, all jobs with absolute
response-time bound t < (job_arrival j + R) have correct response-time bounds. *)
destruct (completed job_cost rate sched j (job_arrival j + R')) eqn:NOTCOMP;
destruct (completed job_cost sched j (job_arrival j + R')) eqn:NOTCOMP;
first by done.
apply negbT in NOTCOMP; exfalso.
......
bertogna_fp_comp.v
+ 7
− 11
View file @ 7755715d
......@@ -604,21 +604,17 @@ Module ResponseTimeIterationFP.
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period arr_seq job_task.
(* Then, consider any platform with at least one CPU and unit
unit execution rate, where...*)
Variable rate: Job -> processor num_cpus -> nat.
(* 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_rate_equals_one :
forall j cpu, rate j cpu = 1.
(* ...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 rate sched.
completed_jobs_dont_execute job_cost sched.
(* ...and do not execute in parallel (required by the workload bound). *)
Hypothesis H_no_parallelism:
......@@ -626,14 +622,14 @@ Module ResponseTimeIterationFP.
(* Assume the platform satisfies the global scheduling invariant. *)
Hypothesis H_global_scheduling_invariant:
FP_scheduling_invariant_holds job_cost job_task num_cpus rate sched ts higher_priority.
FP_scheduling_invariant_holds job_cost job_task num_cpus sched ts higher_priority.
Let no_deadline_missed_by_task (tsk: sporadic_task) :=
task_misses_no_deadline job_cost job_deadline job_task rate sched tsk.
task_misses_no_deadline job_cost job_deadline job_task sched tsk.
Let no_deadline_missed_by_job :=
job_misses_no_deadline job_cost job_deadline rate sched.
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 rate sched.
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 fp_claimed_bounds is safe. The proof follows by induction on the task set:
......@@ -787,7 +783,7 @@ Module ResponseTimeIterationFP.
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 rate sched j (job_arrival j + R)); last first.
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.
......
bertogna_fp_jitter_comp.v
+ 8
− 12
View file @ 7755715d
......@@ -505,21 +505,17 @@ Module ResponseTimeIterationFPWithJitter.
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period arr_seq job_task.
(* Then, consider any platform with at least one CPU and unit
unit execution rate, where...*)
Variable rate: Job -> processor num_cpus -> nat.
(* 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_rate_equals_one :
forall j cpu, rate j cpu = 1.
(* ...jobs only execute after the 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 rate sched.
completed_jobs_dont_execute job_cost sched.
(* ...and do not execute in parallel. *)
Hypothesis H_no_parallelism:
......@@ -527,12 +523,12 @@ Module ResponseTimeIterationFPWithJitter.
(* Assume the platform satisfies the global scheduling invariant. *)
Hypothesis H_global_scheduling_invariant:
FP_scheduling_invariant_holds job_cost job_task num_cpus rate sched ts higher_eq_priority.
FP_scheduling_invariant_holds job_cost job_task num_cpus sched ts higher_eq_priority.
Definition no_deadline_missed_by_task (tsk: sporadic_task_with_jitter) :=
task_misses_no_deadline job_cost job_deadline job_task rate sched tsk.
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 rate sched.
job_misses_no_deadline job_cost job_deadline sched.
Section HelperLemma.
......@@ -544,7 +540,7 @@ Module ResponseTimeIterationFPWithJitter.
(tsk, R) \in rt_bounds ->
forall j : JobIn arr_seq,
job_task j = tsk ->
completed job_cost rate sched j (job_arrival j + R).
completed job_cost sched j (job_arrival j + R).
Proof.
unfold valid_fp_policy, fp_is_transitive, fp_is_reflexive,
fp_is_total in *.
......@@ -690,7 +686,7 @@ Module ResponseTimeIterationFPWithJitter.
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 rate sched j (job_arrival j + R)); last first.
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.
......@@ -710,7 +706,7 @@ Module ResponseTimeIterationFPWithJitter.
R <= task_deadline tsk /\
forall (j: JobIn arr_seq),
job_task j = tsk ->
completed job_cost rate sched j (job_arrival j + R).
completed job_cost sched j (job_arrival j + R).
Proof.
intros tsk IN.
unfold fp_schedulable in *.
......
bertogna_fp_jitter_theory.v
+ 23
− 28
View file @ 7755715d
......@@ -95,7 +95,6 @@ Module ResponseTimeAnalysisJitter.
(* Consider any schedule such that...*)
Variable num_cpus: nat.
Variable rate: Job -> processor num_cpus -> nat.
Variable sched: schedule num_cpus arr_seq.
(* ...jobs do not execute before their arrival times nor longer
......@@ -103,14 +102,12 @@ Module ResponseTimeAnalysisJitter.
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 rate sched.
completed_jobs_dont_execute job_cost sched.
(* Also assume that jobs do not execute in parallel, processors have
unit speed, and that there exists at least one processor. *)
(* 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_rate_equals_one :
forall j cpu, rate j cpu = 1.
Hypothesis H_at_least_one_cpu :
num_cpus > 0.
......@@ -127,9 +124,9 @@ Module ResponseTimeAnalysisJitter.
Hypothesis task_in_ts: tsk \in ts.
Let no_deadline_is_missed_by_tsk (tsk: sporadic_task_with_jitter) :=
task_misses_no_deadline job_cost job_deadline job_task rate sched tsk.
task_misses_no_deadline job_cost job_deadline job_task sched tsk.
Let is_response_time_bound (tsk: sporadic_task_with_jitter) :=
is_response_time_bound_of_task job_cost job_task tsk rate sched.
is_response_time_bound_of_task job_cost job_task tsk sched.
(* Assume a known response-time bound for any interfering task *)
Let task_with_response_time := (sporadic_task_with_jitter * time)%type.
......@@ -148,7 +145,7 @@ Module ResponseTimeAnalysisJitter.
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 rate sched R.
is_response_time_bound_of_task job_cost job_task hp_tsk sched R.
(* Assume that the response-time bounds are larger than task costs. *)
Hypothesis H_response_time_bounds_ge_cost:
......@@ -166,7 +163,7 @@ Module ResponseTimeAnalysisJitter.
the processors must be busy with jobs of equal or higher
priority. *)
Hypothesis H_global_scheduling_invariant:
FP_scheduling_invariant_holds job_cost job_task num_cpus rate sched ts higher_eq_priority.
FP_scheduling_invariant_holds job_cost job_task num_cpus sched ts higher_eq_priority.
(* Next, we define Bertogna and Cirinei's response-time bound recurrence *)
......@@ -202,7 +199,6 @@ Module ResponseTimeAnalysisJitter.
H_response_time_of_interfering_tasks_is_known into RESP,
H_hp_bounds_has_interfering_tasks into UNZIP,
H_interfering_tasks_miss_no_deadlines into NOMISS,
H_rate_equals_one into RATE,
H_global_scheduling_invariant into INVARIANT,
H_response_time_bounds_ge_cost into GE_COST.
intros j JOBtsk.
......@@ -211,10 +207,10 @@ Module ResponseTimeAnalysisJitter.
scheduling, and let X denote the total interference. *)
set x := fun hp_tsk =>
if (hp_tsk \in ts) && interferes_with_tsk hp_tsk then
task_interference job_cost job_task rate sched j
task_interference job_cost job_task sched j
hp_tsk (job_arrival j) (job_arrival j + R)
else 0.
set X := total_interference job_cost rate sched j (job_arrival j) (job_arrival j + R).
set X := total_interference job_cost sched j (job_arrival j) (job_arrival j + R).
(* Let's recall the workload bound under FP scheduling. *)
set workload_bound := fun (tup: task_with_response_time) =>
......@@ -225,12 +221,12 @@ Module ResponseTimeAnalysisJitter.
(* Now we start the proof. Assume by contradiction that job j
is not complete at time (job_arrival j + R). *)
destruct (completed job_cost rate sched j (job_arrival j + R')) eqn:COMPLETED;
destruct (completed job_cost sched j (job_arrival j + R')) eqn:COMPLETED;
first by move: COMPLETED => /eqP COMPLETED; rewrite COMPLETED eq_refl.
apply negbT in COMPLETED; exfalso.
(* Note that j cannot have completed by job_arrival j + R either. *)
assert (COMPLETED': ~~ completed job_cost rate sched j (job_arrival j + R)).
assert (COMPLETED': ~~ completed job_cost sched j (job_arrival j + R)).
{
apply/negP; unfold not; intro BUG.
apply completion_monotonic with (t' := job_arrival j + R') in BUG;
......@@ -241,7 +237,7 @@ Module ResponseTimeAnalysisJitter.
(* Since j has not completed, recall the time when it is not
executing is the total interference. *)
exploit (complement_of_interf_equals_service job_cost rate sched j (job_arrival j)
exploit (complement_of_interf_equals_service job_cost sched j (job_arrival j)
(job_arrival j + R));
last intro EQinterf; ins; unfold has_arrived;
first by apply leqnn.
......@@ -258,14 +254,13 @@ Module ResponseTimeAnalysisJitter.
{
move => tsk_k /andP [INk INTERk] R_k HPk.
unfold x, workload_bound; rewrite INk INTERk andbT.
apply leq_trans with (n := workload job_task rate sched tsk_k
apply leq_trans with (n := workload job_task sched tsk_k
(job_arrival j) (job_arrival j + R));
first by apply task_interference_le_workload; ins; rewrite RATE.
first by apply task_interference_le_workload.
apply workload_bounded_by_W_jitter with (task_deadline0 := task_deadline)
(job_cost0 := job_cost) (job_deadline0 := job_deadline)
(job_jitter0 := job_jitter); ins;
[ by rewrite RATE
| by apply TASK_PARAMS
[ by apply TASK_PARAMS
| by apply RESTR
| by red; red; ins; apply (RESP tsk_k)
| by apply GE_COST |].
......@@ -292,7 +287,7 @@ Module ResponseTimeAnalysisJitter.
apply (leq_ltn_trans (COMP j (job_arrival j + R))) in COMPLETED'.
by rewrite ltnn in COMPLETED'.
}
apply leq_trans with (n := R - service rate sched j (job_arrival j + R)); last first.
apply leq_trans with (n := R - service sched j (job_arrival j + R)); last first.
{
unfold service.
rewrite service_before_arrival_eq_service_during; ins;
......@@ -327,7 +322,7 @@ Module ResponseTimeAnalysisJitter.
unfold x, X, total_interference, task_interference.
rewrite -big_mkcond -exchange_big big_distrl /=.
apply eq_big_nat; move => t LTt.
destruct (backlogged job_cost rate sched j t) eqn:BACK;
destruct (backlogged job_cost sched j t) eqn:BACK;
last by rewrite (eq_bigr (fun i => 0));
[by rewrite big_const_seq iter_addn mul0n addn0 mul0n|by ins].
rewrite big_mkcond mul1n /=.
......@@ -390,12 +385,12 @@ Module ResponseTimeAnalysisJitter.
(R - task_cost tsk + 1) * (num_cpus - cardA)).
{
set some_interference_A := fun t =>
backlogged job_cost rate sched j t &&
backlogged job_cost sched j t &&
has (fun tsk_k => (interferes_with_tsk tsk_k &&
((x tsk_k) >= R - task_cost tsk + 1) &&
task_is_scheduled job_task sched tsk_k t)) ts.
set total_interference_B := fun t =>
backlogged job_cost rate sched j t *
backlogged job_cost sched j t *
count (fun tsk_k =>
interferes_with_tsk tsk_k &&
((x tsk_k) < R - task_cost tsk + 1) &&
......@@ -412,7 +407,7 @@ Module ResponseTimeAnalysisJitter.
last by ins.
move: INTERFa => /andP INTERFa; des.
apply leq_sum; ins.
destruct (backlogged job_cost rate sched j i);
destruct (backlogged job_cost sched j i);
[rewrite 2!andTb | by ins].
destruct (task_is_scheduled job_task sched tsk_a i) eqn:SCHEDa;
[apply eq_leq; symmetry | by ins].
......@@ -427,7 +422,7 @@ Module ResponseTimeAnalysisJitter.
rewrite big_distrl /=.
apply leq_sum; intros t _.
unfold some_interference_A, total_interference_B.
destruct (backlogged job_cost rate sched j t) eqn:BACK;
destruct (backlogged job_cost sched j t) eqn:BACK;
[rewrite andTb mul1n | by ins].
destruct (has (fun tsk_k : sporadic_task_with_jitter =>
interferes_with_tsk tsk_k &&
......@@ -491,7 +486,7 @@ Module ResponseTimeAnalysisJitter.
rewrite [\sum_(i <- ts | _) _](eq_bigr
(fun i => \sum_(job_arrival j <= t < job_arrival j + R)
(i \in ts) && interferes_with_tsk i &&
backlogged job_cost rate sched j t &&
backlogged job_cost sched j t &&
task_is_scheduled job_task sched i t));
last first.
{
......@@ -503,7 +498,7 @@ Module ResponseTimeAnalysisJitter.
{
rewrite exchange_big /=; apply leq_sum; intros t _.
unfold total_interference_B.
destruct (backlogged job_cost rate sched j t); last by ins.
destruct (backlogged job_cost sched j t); last by ins.
rewrite mul1n -sum1_count.
rewrite big_seq_cond big_mkcond [\sum_(i <- ts | _ < _) _]big_mkcond.
apply leq_sum; ins; destruct (x i<R - task_cost tsk + 1);
......
guan_fp_comp.v
+ 8
− 12
View file @ 7755715d
......@@ -544,21 +544,17 @@ Module ResponseTimeIterationFPGuan.
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period arr_seq job_task.
(* Then, consider any platform with at least one CPU and unit
unit execution rate, where...*)
Variable rate: Job -> processor num_cpus -> nat.
(* 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_rate_equals_one :
forall j cpu, rate j cpu = 1.
(* ...jobs only execute after the jitter and no longer
than their execution costs,... *)
Hypothesis H_jobs_execute_after_jitter:
jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost rate sched.
completed_jobs_dont_execute job_cost sched.
(* ...and do not execute in parallel. *)
Hypothesis H_no_parallelism:
......@@ -566,12 +562,12 @@ Module ResponseTimeIterationFPGuan.
(* Assume the platform satisfies the global scheduling invariant. *)
Hypothesis H_global_scheduling_invariant:
FP_scheduling_invariant_holds job_cost job_task num_cpus rate sched ts higher_eq_priority.
FP_scheduling_invariant_holds job_cost job_task num_cpus sched ts higher_eq_priority.
Definition no_deadline_missed_by_task (tsk: sporadic_task) :=
task_misses_no_deadline job_cost job_deadline job_task rate sched tsk.
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 rate sched.
job_misses_no_deadline job_cost job_deadline sched.
Section HelperLemma.
......@@ -583,7 +579,7 @@ Module ResponseTimeIterationFPGuan.
(tsk, R) \in rt_bounds ->
forall j : JobIn arr_seq,
job_task j = tsk ->
completed job_cost rate sched j (job_arrival j + R).
completed job_cost sched j (job_arrival j + R).
Proof.
unfold valid_fp_policy, fp_is_transitive, fp_is_reflexive,
fp_is_total in *.
......@@ -726,7 +722,7 @@ Module ResponseTimeIterationFPGuan.
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 rate sched j (job_arrival j + R)); last first.
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.
......@@ -746,7 +742,7 @@ Module ResponseTimeIterationFPGuan.
R <= task_deadline tsk /\
forall (j: JobIn arr_seq),
job_task j = tsk ->
completed job_cost rate sched j (job_arrival j + R).
completed job_cost sched j (job_arrival j + R).
Proof.
intros tsk IN.
unfold guan_fp_schedulable in *.
......
guan_fp_theory.v
+ 23
− 28
View file @ 7755715d
......@@ -98,7 +98,6 @@ Module ResponseTimeAnalysisGuan.
(* Consider any schedule such that...*)
Variable num_cpus: nat.
Variable rate: Job -> processor num_cpus -> nat.
Variable sched: schedule num_cpus arr_seq.
(* ...jobs do not execute before their arrival times nor longer
......@@ -106,14 +105,12 @@ Module ResponseTimeAnalysisGuan.
Hypothesis H_jobs_execute_after_jitter:
jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost rate sched.
completed_jobs_dont_execute job_cost sched.
(* Also assume that jobs do not execute in parallel, processors have
unit speed, and that there exists at least one processor. *)
(* 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_rate_equals_one :
forall j cpu, rate j cpu = 1.
Hypothesis H_at_least_one_cpu :
num_cpus > 0.
......@@ -130,9 +127,9 @@ Module ResponseTimeAnalysisGuan.
Hypothesis task_in_ts: tsk \in ts.
Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
task_misses_no_deadline job_cost job_deadline job_task rate sched tsk.
task_misses_no_deadline job_cost job_deadline job_task sched tsk.
Let is_response_time_bound (tsk: sporadic_task) :=
is_response_time_bound_of_task job_cost job_task tsk rate sched.
is_response_time_bound_of_task job_cost job_task tsk sched.
(* Assume a known response-time bound for any interfering task *)
Let task_with_response_time := (sporadic_task * time)%type.
......@@ -151,7 +148,7 @@ Module ResponseTimeAnalysisGuan.
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 rate sched R.
is_response_time_bound_of_task job_cost job_task hp_tsk sched R.
(* Assume that the response-time bounds are larger than task costs. *)
Hypothesis H_response_time_bounds_ge_cost:
......@@ -171,7 +168,7 @@ Module ResponseTimeAnalysisGuan.
Hypothesis H_global_scheduling_invariant:
forall (j: JobIn arr_seq) (t: time),
job_task j = tsk ->
backlogged job_cost rate sched j t ->
backlogged job_cost sched j t ->
count
(fun tsk_other : sporadic_task =>
is_interfering_task_fp higher_eq_priority tsk tsk_other &&
......@@ -208,7 +205,6 @@ Module ResponseTimeAnalysisGuan.
H_response_time_of_interfering_tasks_is_known into RESP,
H_hp_bounds_has_interfering_tasks into HAS,
H_interfering_tasks_miss_no_deadlines into NOMISS,
H_rate_equals_one into RATE,
H_global_scheduling_invariant into INVARIANT,
H_response_time_bounds_ge_cost into GE_COST.
intros j JOBtsk.
......@@ -217,10 +213,10 @@ Module ResponseTimeAnalysisGuan.
scheduling, and let X denote the total interference. *)
set x := fun hp_tsk =>
if (hp_tsk \in ts) && interferes_with_tsk hp_tsk then
task_interference job_cost job_task rate sched j
task_interference job_cost job_task sched j
hp_tsk (job_arrival j) (job_arrival j + R)
else 0.
set X := total_interference job_cost rate sched j (job_arrival j) (job_arrival j + R).
set X := total_interference job_cost sched j (job_arrival j) (job_arrival j + R).
admit.
......@@ -233,12 +229,12 @@ Module ResponseTimeAnalysisGuan.
(* Now we start the proof. Assume by contradiction that job j
is not complete at time (job_arrival j + R). *)
destruct (completed job_cost rate sched j (job_arrival j + R')) eqn:COMPLETED;
destruct (completed job_cost sched j (job_arrival j + R')) eqn:COMPLETED;
first by move: COMPLETED => /eqP COMPLETED; rewrite COMPLETED eq_refl.
apply negbT in COMPLETED; exfalso.
(* Note that j cannot have completed by job_arrival j + R either. *)
assert (COMPLETED': ~~ completed job_cost rate sched j (job_arrival j + R)).
assert (COMPLETED': ~~ completed job_cost sched j (job_arrival j + R)).
{
apply/negP; unfold not; intro BUG.
apply completion_monotonic with (t' := job_arrival j + R') in BUG;
......@@ -249,7 +245,7 @@ Module ResponseTimeAnalysisGuan.
(* Since j has not completed, recall the time when it is not
executing is the total interference. *)
exploit (complement_of_interf_equals_service job_cost rate sched j (job_arrival j)
exploit (complement_of_interf_equals_service job_cost sched j (job_arrival j)
(job_arrival j + R));
last intro EQinterf; ins; unfold has_arrived;
first by apply leqnn.
......@@ -279,7 +275,7 @@ Module ResponseTimeAnalysisGuan.
Qed.
exploit (exists_R tsk_k); [by ins | by ins | intro INhp; des].
apply leq_trans with (n := workload job_task rate sched tsk_k
apply leq_trans with (n := workload job_task sched tsk_k
(job_arrival j) (job_arrival j + R)).
{
unfold task_interference, workload.
......@@ -292,12 +288,11 @@ Module ResponseTimeAnalysisGuan.
destruct SCHED as [cpu _ HAScpu].
rewrite -> bigD1 with (j := cpu); simpl; last by ins.
apply ltn_addr; unfold service_of_task, schedules_job_of_tsk in *.
by destruct (sched cpu t);[by rewrite HAScpu mul1n RATE|by ins].
by destruct (sched cpu t);[by rewrite HAScpu mul1n|by ins].
}
{
apply workload_bounded_by_W_jitter with (task_deadline0 := task_deadline) (job_cost0 := job_cost) (job_deadline0 := job_deadline) (job_jitter0 := job_jitter); ins;
[ by rewrite RATE
| by apply TASK_PARAMS
[ by apply TASK_PARAMS
| by apply RESTR
| by red; red; ins; apply (RESP tsk_k)
| by apply GE_COST |].
......@@ -325,7 +320,7 @@ Module ResponseTimeAnalysisGuan.
apply (leq_ltn_trans (COMP j (job_arrival j + R))) in COMPLETED'.
by rewrite ltnn in COMPLETED'.
}
apply leq_trans with (n := R - service rate sched j (job_arrival j + R)); last first.
apply leq_trans with (n := R - service sched j (job_arrival j + R)); last first.
{
unfold service.
rewrite service_before_arrival_eq_service_during; ins;
......@@ -360,7 +355,7 @@ Module ResponseTimeAnalysisGuan.
unfold x, X, total_interference, task_interference.
rewrite -big_mkcond -exchange_big big_distrl /=.
apply eq_big_nat; move => t LTt.
destruct (backlogged job_cost rate sched j t) eqn:BACK;
destruct (backlogged job_cost sched j t) eqn:BACK;
last by rewrite (eq_bigr (fun i => 0));
[by rewrite big_const_seq iter_addn mul0n addn0 mul0n|by ins].
rewrite big_mkcond mul1n /=.
......@@ -422,12 +417,12 @@ Module ResponseTimeAnalysisGuan.
(R - task_cost tsk + 1) * (num_cpus - cardA)).
{
set some_interference_A := fun t =>
backlogged job_cost rate sched j t &&
backlogged job_cost sched j t &&
has (fun tsk_k => (interferes_with_tsk tsk_k &&
((x tsk_k) >= R - task_cost tsk + 1) &&
task_is_scheduled job_task sched tsk_k t)) ts.
set total_interference_B := fun t =>
backlogged job_cost rate sched j t *
backlogged job_cost sched j t *
count (fun tsk_k =>
interferes_with_tsk tsk_k &&
((x tsk_k) < R - task_cost tsk + 1) &&
......@@ -444,7 +439,7 @@ Module ResponseTimeAnalysisGuan.
last by ins.
move: INTERFa => /andP INTERFa; des.
apply leq_sum; ins.
destruct (backlogged job_cost rate sched j i);
destruct (backlogged job_cost sched j i);
[rewrite 2!andTb | by ins].
destruct (task_is_scheduled job_task sched tsk_a i) eqn:SCHEDa;
[apply eq_leq; symmetry | by ins].
......@@ -459,7 +454,7 @@ Module ResponseTimeAnalysisGuan.
rewrite big_distrl /=.
apply leq_sum; intros t _.
unfold some_interference_A, total_interference_B.
destruct (backlogged job_cost rate sched j t) eqn:BACK;
destruct (backlogged job_cost sched j t) eqn:BACK;
[rewrite andTb mul1n | by ins].
destruct (has (fun tsk_k : sporadic_task_with_jitter =>
interferes_with_tsk tsk_k &&
......@@ -525,7 +520,7 @@ Module ResponseTimeAnalysisGuan.
rewrite [\sum_(i <- ts | _) _](eq_bigr
(fun i => \sum_(job_arrival j <= t < job_arrival j + R)
(i \in ts) && interferes_with_tsk i &&
backlogged job_cost rate sched j t &&
backlogged job_cost sched j t &&
task_is_scheduled job_task sched i t));
last first.
{
......@@ -537,7 +532,7 @@ Module ResponseTimeAnalysisGuan.
{
rewrite exchange_big /=; apply leq_sum; intros t _.
unfold total_interference_B.
destruct (backlogged job_cost rate sched j t); last by ins.
destruct (backlogged job_cost sched j t); last by ins.
rewrite mul1n -sum1_count.
rewrite big_seq_cond big_mkcond [\sum_(i <- ts | _ < _) _]big_mkcond.
apply leq_sum; ins; destruct (x i<R - task_cost tsk + 1);
......
interference_bound_edf.v
+ 32
− 46
View file @ 7755715d
......@@ -81,16 +81,6 @@ Module EDFSpecificBound.
Hypothesis H_at_least_one_cpu :
num_cpus > 0.
(* In order not to overcount job interference, we assume that
jobs of the same task do not execute in parallel.
Note that under EDF, this is equivalent to task precedence
constraints.
This is required because our proof uses a definition of
interference based on the sum of the individual contributions
of each job: I_total = I_j1 + I_j2 + ... *)
Hypothesis H_no_intra_task_parallelism:
jobs_of_same_task_dont_execute_in_parallel job_task sched.
(* Assume that we have a task set where all tasks have valid
parameters and restricted deadlines. *)
Variable ts: taskset_of sporadic_task.
......@@ -185,8 +175,7 @@ Module EDFSpecificBound.
x <= \sum_(j <- jobs_scheduled_between sched t1 t2 | job_task j == tsk_k)
interference_caused_by j t1 t2.
Proof.
apply interference_eq_interference_joblist.
apply interference_le_interference_joblist.
Qed.
(* Remove the elements that we don't care about from the sum *)
......@@ -252,8 +241,8 @@ Module EDFSpecificBound.
rename H_valid_job_parameters into PARAMS.
intros j; rewrite mem_filter; move => /andP [/andP [/eqP JOBj _] _].
specialize (PARAMS j); des.
apply leq_trans with (n := service_during rate sched j t1 t2);
first by apply job_interference_le_service; ins; rewrite RATE.
apply leq_trans with (n := service_during sched j t1 t2);
first by apply job_interference_le_service.
by apply cumulative_service_le_task_cost with (job_task0 := job_task)
(task_deadline0 := task_deadline) (job_cost0 := job_cost)
(job_deadline0 := job_deadline).
......@@ -269,14 +258,14 @@ Module EDFSpecificBound.
TODO: Should this be in the interference.v file? *)
Lemma interference_under_edf_implies_shorter_deadlines :
forall (j j': JobIn arr_seq) t1 t2,
job_interference job_cost rate sched j' j t1 t2 != 0 ->
job_interference job_cost sched j' j t1 t2 != 0 ->
job_arrival j + job_deadline j <= job_arrival j' + job_deadline j'.
Proof.
rename H_global_scheduling_invariant into INV.
clear - t1 t2 INV; clear t1 t2.
intros j j' t1 t2 INTERF.
unfold job_interference in INTERF.
destruct ([exists t': 'I_t2, (t' >= t1) && backlogged job_cost rate sched j' t' &&
destruct ([exists t': 'I_t2, (t' >= t1) && backlogged job_cost sched j' t' &&
scheduled sched j t']) eqn:EX.
{
move: EX => /existsP EX; destruct EX as [t' EX];move: EX => /andP [/andP [LE BACK] SCHED].
......@@ -307,7 +296,6 @@ Module EDFSpecificBound.
\sum_(j <- sorted_jobs) interference_caused_by j t1 t2 <=
interference_bound.
Proof.
rename H_rate_equals_one into RATE.
rewrite -[\sum_(_ <- _ | _) _]addn0 leq_add //.
apply leq_trans with (n := \sum_(x <- sorted_jobs) task_cost tsk_k);
last by rewrite big_const_seq iter_addn addn0 mulnC leq_mul2r; apply/orP; right.
......@@ -375,17 +363,16 @@ Module EDFSpecificBound.
(* If j_fst completes by its response-time bound, then t1 <= a_fst + R_k,
where t1 is the beginning of the time window (arrival of j_i). *)
Lemma interference_bound_edf_j_fst_completion_implies_rt_bound_inside_interval :
completed job_cost rate sched j_fst (a_fst + R_k) ->
completed job_cost sched j_fst (a_fst + R_k) ->
t1 <= a_fst + R_k.
Proof.
rename H_rate_equals_one into RATE.
intros RBOUND.
rewrite leqNgt; apply/negP; unfold not; intro BUG.
have FST := interference_bound_edf_j_fst_is_job_of_tsk_k.
destruct FST as [_ [ FSTserv _]].
move: FSTserv => /negP FSTserv; apply FSTserv.
rewrite -leqn0; apply leq_trans with (n := service_during rate sched j_fst t1 t2);
first by apply job_interference_le_service; ins; rewrite RATE.
rewrite -leqn0; apply leq_trans with (n := service_during sched j_fst t1 t2);
first by apply job_interference_le_service.
rewrite leqn0; apply/eqP.
by apply cumulative_service_after_job_rt_zero with (job_cost0 := job_cost) (R := R_k);
try (by done); apply ltnW.
......@@ -424,10 +411,10 @@ Module EDFSpecificBound.
Section ResponseTimeOfSingleJobBounded.
Hypothesis H_j_fst_completed_by_rt_bound :
completed job_cost rate sched j_fst (a_fst + R_k).
completed job_cost sched j_fst (a_fst + R_k).
Lemma interference_bound_edf_holds_for_single_job_that_completes_on_time :
job_interference job_cost rate sched j_i j_fst t1 t2 <= D_i - (D_k - R_k).
job_interference job_cost sched j_i j_fst t1 t2 <= D_i - (D_k - R_k).
Proof.
rename H_j_fst_completed_by_rt_bound into RBOUND.
have AFTERt1 :=
......@@ -439,7 +426,7 @@ Module EDFSpecificBound.
{
apply negbT in LEdk; rewrite -ltnNge in LEdk.
apply leq_trans with (n := 0); last by done.
apply leq_trans with (n := job_interference job_cost rate sched j_i j_fst
apply leq_trans with (n := job_interference job_cost sched j_i j_fst
(a_fst + R_k) t2).
{
apply extend_sum; last by apply leqnn.
......@@ -450,8 +437,8 @@ Module EDFSpecificBound.
rewrite -addnA leq_add2l.
by apply ltnW; rewrite -ltn_subRL.
}
apply leq_trans with (n := service_during rate sched j_fst (a_fst + R_k) t2);
first by apply job_interference_le_service; ins; rewrite H_rate_equals_one.
apply leq_trans with (n := service_during sched j_fst (a_fst + R_k) t2);
first by apply job_interference_le_service.
unfold service_during; rewrite leqn0; apply/eqP.
by apply cumulative_service_after_job_rt_zero with (job_cost0 := job_cost) (R := R_k);
try (by done); apply leqnn.
......@@ -464,7 +451,7 @@ Module EDFSpecificBound.
rewrite addnC -subnBA; last by apply leq_addr.
by rewrite addnC -addnBA // subnn addn0.
}
apply leq_trans with (n := job_interference job_cost rate sched j_i j_fst t1
apply leq_trans with (n := job_interference job_cost sched j_i j_fst t1
(a_fst + D_k) + (D_k - R_k)).
{
rewrite leq_add2r.
......@@ -479,11 +466,11 @@ Module EDFSpecificBound.
apply negbT in LEt2; rewrite -ltnNge in LEt2.
rewrite -> big_cat_nat with (n := a_fst + R_k);
[simpl | by apply AFTERt1 | by apply ltnW].
apply leq_trans with (n := job_interference job_cost rate sched j_i j_fst t1
(a_fst + R_k) + service_during rate sched j_fst (a_fst + R_k) t2).
apply leq_trans with (n := job_interference job_cost sched j_i j_fst t1
(a_fst + R_k) + service_during sched j_fst (a_fst + R_k) t2).
{
rewrite leq_add2l.
by apply job_interference_le_service; ins; rewrite H_rate_equals_one.
by apply job_interference_le_service.
}
unfold service_during.
rewrite -> cumulative_service_after_job_rt_zero with (job_cost0 := job_cost)
......@@ -497,11 +484,11 @@ Module EDFSpecificBound.
unfold job_interference.
rewrite -> big_cat_nat with (n := a_fst + R_k);
[simpl| by apply AFTERt1 | by rewrite leq_add2l; apply H_R_k_le_deadline].
apply leq_trans with (n := job_interference job_cost rate sched j_i j_fst t1
(a_fst+R_k) + service_during rate sched j_fst (a_fst+R_k) (a_fst+D_k) + (D_k-R_k)).
apply leq_trans with (n := job_interference job_cost sched j_i j_fst t1
(a_fst+R_k) + service_during sched j_fst (a_fst+R_k) (a_fst+D_k) + (D_k-R_k)).
{
rewrite leq_add2r leq_add2l.
by apply job_interference_le_service; ins; rewrite H_rate_equals_one.
by apply job_interference_le_service.
}
unfold service_during.
rewrite -> cumulative_service_after_job_rt_zero with (job_cost0 := job_cost) (R:=R_k);
......@@ -528,7 +515,7 @@ Module EDFSpecificBound.
Section ResponseTimeOfSingleJobNotBounded.
Hypothesis H_j_fst_not_complete_by_rt_bound :
~~ completed job_cost rate sched j_fst (a_fst + R_k).
~~ completed job_cost sched j_fst (a_fst + R_k).
(* This trivially implies that a_fst + R_k lies after the end of the interval,
otherwise j_fst would have completed by its response-time bound. *)
......@@ -574,7 +561,7 @@ Module EDFSpecificBound.
destruct FST as [FSTtask [LEdl _]].
have LTr := interference_bound_edf_response_time_bound_of_j_fst_after_interval.
apply subh3; last by apply LEdk.
apply leq_trans with (n := job_interference job_cost rate sched j_i j_fst t1
apply leq_trans with (n := job_interference job_cost sched j_i j_fst t1
(job_arrival j_fst + R_k) + (D_k - R_k));
first by rewrite leq_add2r; apply extend_sum; [by apply leqnn|].
apply leq_trans with (n := \sum_(t1 <= t < a_fst + R_k) 1 +
......@@ -605,7 +592,7 @@ Module EDFSpecificBound.
Lemma interference_bound_edf_interference_of_j_fst_limited_by_slack :
interference_caused_by j_fst t1 t2 <= D_i - (D_k - R_k).
Proof.
destruct (completed job_cost rate sched j_fst (a_fst + R_k)) eqn:COMP;
destruct (completed job_cost sched j_fst (a_fst + R_k)) eqn:COMP;
first by apply interference_bound_edf_holds_for_single_job_that_completes_on_time.
apply negbT in COMP.
destruct (ltnP D_i (D_k - R_k)) as [LEdk | LTdk].
......@@ -684,7 +671,6 @@ Module EDFSpecificBound.
Lemma interference_bound_edf_last_job_arrives_before_end_of_interval :
job_arrival j_lst < t2.
Proof.
rename H_rate_equals_one into RATE.
rewrite leqNgt; apply/negP; unfold not; intro LT2.
exploit interference_bound_edf_all_jobs_from_tsk_k.
{
......@@ -693,8 +679,8 @@ Module EDFSpecificBound.
}
instantiate (1 := elem); move => [LSTtsk [/eqP LSTserv LSTin]].
apply LSTserv; apply/eqP; rewrite -leqn0.
apply leq_trans with (n := service_during rate sched j_lst t1 t2);
first by apply job_interference_le_service; ins; rewrite RATE.
apply leq_trans with (n := service_during sched j_lst t1 t2);
first by apply job_interference_le_service.
rewrite leqn0; apply/eqP; unfold service_during.
by apply cumulative_service_before_job_arrival_zero.
Qed.
......@@ -703,7 +689,7 @@ Module EDFSpecificBound.
the interval that its response-time bound is valid
(by the assumption H_all_previous_jobs_completed_on_time). *)
Lemma interference_bound_edf_j_fst_completed_on_time :
completed job_cost rate sched j_fst (a_fst + R_k).
completed job_cost sched j_fst (a_fst + R_k).
Proof.
have FST := interference_bound_edf_j_fst_is_job_of_tsk_k; des.
set j_snd := nth elem sorted_jobs 1.
......@@ -716,9 +702,9 @@ Module EDFSpecificBound.
apply leq_ltn_trans with (n := job_arrival j_snd); last first.
{
rewrite ltnNge; apply/negP; red; intro BUG; apply SNDserv.
apply/eqP; rewrite -leqn0; apply leq_trans with (n := service_during rate
apply/eqP; rewrite -leqn0; apply leq_trans with (n := service_during
sched j_snd t1 t2);
first by apply job_interference_le_service; ins; rewrite H_rate_equals_one.
first by apply job_interference_le_service.
rewrite leqn0; apply/eqP.
by apply cumulative_service_before_job_arrival_zero.
}
......@@ -928,7 +914,7 @@ Module EDFSpecificBound.
}
destruct (leqP t2 (a_fst + R_k)) as [LEt2 | GTt2].
{
apply leq_trans with (n := job_interference job_cost rate sched j_i j_fst t1
apply leq_trans with (n := job_interference job_cost sched j_i j_fst t1
(a_fst + R_k));
first by apply extend_sum; rewrite ?leqnn.
by apply leq_sum; ins; rewrite leq_b1.
......@@ -939,8 +925,8 @@ Module EDFSpecificBound.
[simpl | by apply AFTERt1 | by apply ltnW].
rewrite -[\sum_(_ <= _ < _) 1]addn0; apply leq_add;
first by apply leq_sum; ins; apply leq_b1.
apply leq_trans with (n := service_during rate sched j_fst (a_fst + R_k) t2);
first by apply job_interference_le_service; ins; rewrite H_rate_equals_one.
apply leq_trans with (n := service_during sched j_fst (a_fst + R_k) t2);
first by apply job_interference_le_service.
rewrite leqn0; apply/eqP.
apply cumulative_service_after_job_rt_zero with (job_cost0 := job_cost) (R := R_k);
[ by done | | by apply leqnn].
......@@ -1058,7 +1044,7 @@ Module EDFSpecificBound.
x <= interference_bound.
Proof.
(* Use the definition of workload based on list of jobs. *)
rewrite interference_bound_edf_use_another_definition.
apply (leq_trans interference_bound_edf_use_another_definition).
(* We only care about the jobs that cause interference. *)
rewrite interference_bound_edf_simpl_by_filtering_interfering_jobs.
......
workload_guan.v
+ 36
− 110
View file @ 7755715d
......@@ -183,7 +183,6 @@ Module WorkloadBoundGuan.
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
Variable num_cpus: nat.
Variable rate: Job -> processor num_cpus -> nat.
Variable schedule_of_platform: schedule num_cpus arr_seq -> Prop.
(* Assume any schedule of a given platform. *)
......@@ -198,16 +197,12 @@ Module WorkloadBoundGuan.
(* 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 rate sched.
completed_jobs_dont_execute job_cost sched.
(* Assumptions:
1) A job does not execute in parallel.
2) The service rate of the platform is at most 1.
(* Assumptiom: A job does not execute in parallel.
This is required to use interval lengths as a measure of service. *)
Hypothesis H_no_parallelism:
jobs_dont_execute_in_parallel sched.
Hypothesis H_rate_at_most_one :
forall j cpu, rate j cpu <= 1.
(* Assumption: sporadic task model.
This is necessary to conclude that consecutive jobs ordered by arrival times
......@@ -215,12 +210,12 @@ Module WorkloadBoundGuan.
Hypothesis H_sporadic_tasks: sporadic_task_model task_period arr_seq job_task.
(* Before starting the proof, let's give simpler names to the definitions. *)
Let job_has_completed_by := completed job_cost rate sched.
Let job_has_completed_by := completed job_cost sched.
Let no_deadline_misses_by (tsk: sporadic_task) (t: time) :=
task_misses_no_deadline_before job_cost job_deadline job_task
rate sched tsk t.
sched tsk t.
Let workload_of (tsk: sporadic_task) (t1 t2: time) :=
workload job_task rate sched tsk t1 t2.
workload job_task sched tsk t1 t2.
(* Now we define the theorem. Let tsk be any task in the taskset. *)
Variable tsk: sporadic_task.
......@@ -259,78 +254,10 @@ Module WorkloadBoundGuan.
job_arrival j + R_tsk < t1 + delta ->
job_has_completed_by j (job_arrival j + R_tsk).
(* If a job i scheduled in an time interval, it will get service in this interval. *)
(*Lemma scheduled_between_implies_service :
forall j t1 t2,
(forall j cpu, rate j cpu > 0) ->
(j \in jobs_scheduled_between sched t1 t2) =
(service_during rate sched j t1 t2 != 0).
Proof.
intros j t1 t2 RATE; unfold service_during; rewrite mem_undup.
induction t2;
first by rewrite 2?big_geq //.
destruct (leqP t1 t2) as [LE | GT]; last by rewrite 2?big_geq //.
unfold service_during; rewrite 2?big_nat_recr ?mem_cat /= //.
rewrite IHt2.
destruct (\sum_(t1 <= t < t2) service_at rate sched j t);
last by done.
rewrite eq_refl orFb add0n.
by apply scheduled_between_helper, RATE.
Qed.*)
(* ??? *)
(*Lemma scheduled_between_helper :
forall j t,
(forall cpu t, rate cpu t > 0) ->
(j \in \big[cat/[::]]_(cpu < num_cpus) make_sequence (sched cpu t))
= (service_at rate sched j t != 0).
Proof.
unfold service_at; intros j t RATE.
rewrite [\sum_(_ < _ | _) _]big_mkcond.
destruct num_cpus; first by rewrite 2!big_ord0 in_nil.
assert (LT0: 0 < n.+1); first by done.
rewrite 2!(big_nth (Ordinal LT0)).
set m := size (index_enum (ordinal_finType n.+1)).
induction m; first by rewrite big_geq // big_geq //.
{
rewrite big_nat_recr; last by done.
rewrite big_nat_recr; last by done.
rewrite mem_cat IHm.
destruct ( (j
\in make_sequence
(sched
(nth (Ordinal (n:=n.+1) (m:=0) LT0)
(index_enum (ordinal_finType n.+1)) m) t))) eqn: SUBST.
{
rewrite orbT.
unfold make_sequence in SUBST.
destruct (sched (nth (Ordinal LT0) (index_enum (ordinal_finType n.+1)) m) t); last by done.
rewrite mem_seq1 in SUBST.
move: SUBST => /eqP SUBST; subst.
rewrite eq_refl.
symmetry; rewrite -lt0n.
apply leq_trans with (0 + 1); first by done.
apply leq_add; first by done.
by rewrite RATE.
}
{
unfold make_sequence in SUBST.
destruct (sched (nth (Ordinal LT0) (index_enum (ordinal_finType n.+1)) m ) t);
last by desf; rewrite orbF /= addn0.
{
rewrite mem_seq1 in SUBST.
destruct (Some j0 == Some j) eqn:SOME;
last by rewrite SOME orbF /= addn0.
move: SOME SUBST => /eqP SOME /eqP SUBST; inversion SOME.
by rewrite H0 in SUBST.
}
}
}
Qed.*)
(*Section GuanNoCarry.
Let is_carry_in_job := carried_in job_cost rate sched.
Let is_carry_in_job := carried_in job_cost sched.
(* Assume that task tsk has no carry-in job in the interval delta. *)
Hypothesis H_no_carry_in:
......@@ -363,17 +290,17 @@ Module WorkloadBoundGuan.
(* Identify the subset of jobs that actually cause interference *)
set interfering_jobs :=
filter (fun (x: JobIn arr_seq) =>
(job_task x == tsk) && (service_during rate sched x t1 t2 != 0))
(job_task x == tsk) && (service_during sched x t1 t2 != 0))
(jobs_scheduled_between sched t1 t2).
(* Remove the elements that we don't care about from the sum *)
assert (SIMPL:
\sum_(i <- jobs_scheduled_between sched t1 t2 | job_task i == tsk)
service_during rate sched i t1 t2 =
\sum_(i <- interfering_jobs) service_during rate sched i t1 t2).
service_during sched i t1 t2 =
\sum_(i <- interfering_jobs) service_during sched i t1 t2).
{
unfold interfering_jobs.
rewrite (bigID (fun x => service_during rate sched x t1 t2 == 0)) /=.
rewrite (bigID (fun x => service_during sched x t1 t2 == 0)) /=.
rewrite (eq_bigr (fun x => 0)); last by move => j_i /andP JOBi; des; apply /eqP.
rewrite big_const_seq iter_addn mul0n add0n add0n.
by rewrite big_filter.
......@@ -381,7 +308,7 @@ Module WorkloadBoundGuan.
(* Remember that for any job of tsk, service <= task_cost tsk *)
assert (LTserv: forall j_i (INi: j_i \in interfering_jobs),
service_during rate sched j_i t1 t2 <= task_cost tsk).
service_during sched j_i t1 t2 <= task_cost tsk).
{
ins; move: INi; rewrite mem_filter; move => /andP xxx; des.
move: xxx; move => /andP JOBi; des; clear xxx0 JOBi0.
......@@ -462,7 +389,7 @@ Module WorkloadBoundGuan.
}
{
apply leq_trans with (n := \sum_(t1 <= t < t2) 1).
by apply leq_sum; ins; apply service_at_le_max_rate.
by apply leq_sum.
by unfold t2; rewrite big_const_nat iter_addn mul1n addn0 addnC -addnBA// subnn addn0.
}
}
......@@ -499,7 +426,7 @@ Module WorkloadBoundGuan.
unfold service; rewrite -> big_cat_nat with (n := t1);
[simpl | by done | by apply leq_addr].
move: COMPLETED => /eqP COMPLETED; rewrite -COMPLETED.
apply leq_trans with (n := service rate sched j_fst t1 + 1);
apply leq_trans with (n := service sched j_fst t1 + 1);
first by rewrite addn1.
by rewrite leq_add2l lt0n.
}
......@@ -516,7 +443,7 @@ Module WorkloadBoundGuan.
unfold service; rewrite -> big_cat_nat with (n := t1);
[simpl | by done | by apply leq_addr].
move: COMPLETED => /eqP COMPLETED; rewrite -COMPLETED.
apply leq_trans with (n := service rate sched j_lst t1 + 1);
apply leq_trans with (n := service sched j_lst t1 + 1);
first by rewrite addn1.
by rewrite leq_add2l lt0n.
}
......@@ -543,7 +470,7 @@ Module WorkloadBoundGuan.
(* Now we upper-bound the service of the middle jobs. *)
assert (BOUNDmid: \sum_(0 <= i < n)
service_during rate sched (nth elem sorted_jobs i.+1) t1 t2 <=
service_during sched (nth elem sorted_jobs i.+1) t1 t2 <=
n * task_cost tsk).
{
apply leq_trans with (n := n * task_cost tsk);
......@@ -663,7 +590,7 @@ Module WorkloadBoundGuan.
try (by ins); last by apply ltnW.
rewrite cumulative_service_before_job_arrival_zero ?leqnn // add0n.
apply leq_trans with (n := \sum_(job_arrival j_lst <= i < t2) 1).
apply leq_sum; first by ins; apply service_at_le_max_rate.
apply leq_sum.
rewrite big_const_nat iter_addn mul1n addn0.
rewrite -(leq_add2r (job_arrival j_lst)).
rewrite [t2 - _ + _]subh1; last by apply ltnW.
......@@ -687,7 +614,7 @@ Module WorkloadBoundGuan.
Section GuanCarry.
Let is_carry_in_job := carried_in job_cost rate sched.
Let is_carry_in_job := carried_in job_cost sched.
Let is_idle_at := is_idle sched.
(* Assume task precedence constraints. *)
......@@ -696,7 +623,7 @@ Module WorkloadBoundGuan.
job_task j = job_task j' ->
job_arrival j < job_arrival j' ->
scheduled sched j' t ->
completed job_cost rate sched j t.
completed job_cost sched j t.
(* Assume that task tsk has a carry-in job in the interval. *)
Hypothesis H_has_carry_in:
......@@ -741,11 +668,11 @@ Module WorkloadBoundGuan.
(* Remove the elements that we don't care about from the sum *)
(*assert (SIMPL:
\sum_(i <- jobs_scheduled_between sched t1 t2 | job_task i == tsk)
service_during rate sched i t1 t2 =
\sum_(i <- interfering_jobs) service_during rate sched i t1 t2).
service_during sched i t1 t2 =
\sum_(i <- interfering_jobs) service_during sched i t1 t2).
{
unfold interfering_jobs.
rewrite (bigID (fun x => service_during rate sched x t1 t2 == 0)) /=.
rewrite (bigID (fun x => service_during sched x t1 t2 == 0)) /=.
rewrite (eq_bigr (fun x => 0)); last by move => j_i /andP JOBi; des; apply /eqP.
rewrite big_const_seq iter_addn mul0n add0n add0n.
by rewrite big_filter.
......@@ -753,7 +680,7 @@ Module WorkloadBoundGuan.
(* Remember that for any job of tsk, service <= task_cost tsk *)
assert (LTserv: forall j_i (INi: j_i \in interfering_jobs),
service_during rate sched j_i t1 t2 <= task_cost tsk).
service_during sched j_i t1 t2 <= task_cost tsk).
{
intros j_i; rewrite mem_filter; move => /andP [JOBi _].
have PROP := job_properties j_i; des.
......@@ -815,7 +742,7 @@ Module WorkloadBoundGuan.
by instantiate (1:= sorted_jobs); instantiate (1 := 0); rewrite SIZE.
move: FST (FST) => FSTin; rewrite -INboth mem_filter (scheduled_between_implies_service rate);
move: FST (FST) => FSTin; rewrite -INboth mem_filter (scheduled_between_implies_service);
last by admit.
move => /andP [FSTtsk FSTserv].
......@@ -836,7 +763,7 @@ Module WorkloadBoundGuan.
}
{
apply leq_trans with (n := \sum_(t1 <= t < t2) 1).
by apply leq_sum; ins; apply service_at_le_max_rate.
by apply leq_sum.
by unfold t2; rewrite big_const_nat iter_addn mul1n addn0 addnC -addnBA// subnn addn0.
}
}
......@@ -854,8 +781,8 @@ Module WorkloadBoundGuan.
by unfold j_lst; rewrite INboth; apply mem_nth; rewrite SIZE.
}
move: LST (LST) => LSTin.
rewrite mem_filter (scheduled_between_implies_service rate);
last by admit. (* RATE bug *)
rewrite mem_filter (scheduled_between_implies_service);
last by admit. (* bug *)
move => /andP [LSTtsk LSTserv].
......@@ -881,7 +808,7 @@ Module WorkloadBoundGuan.
unfold service; rewrite -> big_cat_nat with (n := t1);
[simpl | by done | by apply leq_addr].
move: COMPLETED => /eqP COMPLETED; rewrite -COMPLETED.
apply leq_trans with (n := service rate sched j_fst t1 + 1);
apply leq_trans with (n := service sched j_fst t1 + 1);
first by rewrite addn1.
by rewrite leq_add2l lt0n.
}*)
......@@ -898,7 +825,7 @@ Module WorkloadBoundGuan.
unfold service; rewrite -> big_cat_nat with (n := t1);
[simpl | by done | by apply leq_addr].
move: COMPLETED => /eqP COMPLETED; rewrite -COMPLETED.
apply leq_trans with (n := service rate sched j_lst t1 + 1);
apply leq_trans with (n := service sched j_lst t1 + 1);
first by rewrite addn1.
by rewrite leq_add2l lt0n.
}*)
......@@ -919,7 +846,7 @@ Module WorkloadBoundGuan.
(* Now we upper-bound the service of the middle jobs. *)
assert (BOUNDmid: \sum_(0 <= i < n)
service_during rate sched (nth elem sorted_jobs i.+1) t1 t2 <=
service_during sched (nth elem sorted_jobs i.+1) t1 t2 <=
n * task_cost tsk).
{
apply leq_trans with (n := n * task_cost tsk);
......@@ -1032,7 +959,7 @@ Module WorkloadBoundGuan.
apply/andP; split; first by done.
unfold completed; apply/negP; move => /eqP EQcost.
move: FSTserv => /negP FSTserv; apply FSTserv.
rewrite -leqn0 -(leq_add2l (service rate sched j_fst t1)); rewrite addn0.
rewrite -leqn0 -(leq_add2l (service sched j_fst t1)); rewrite addn0.
rewrite {2}[service _ _ _ _]EQcost.
by unfold service, service_during; rewrite <- big_cat_nat with (n := t1);
[by apply COMP | by done | by apply leq_addr].
......@@ -1043,11 +970,11 @@ Module WorkloadBoundGuan.
apply negbT in LEQ; rewrite -ltnNge in LEQ.
assert (LISTin: j_in \in sorted_jobs).
{
destruct (service_during rate sched j_in t1 t2 != 0) eqn:SERV.
destruct (service_during sched j_in t1 t2 != 0) eqn:SERV.
{
(* If j_in executes in the interval, then it automatically belongs to sorted_jobs.*)
rewrite -INboth mem_filter JOBin eq_refl andTb.
by rewrite (scheduled_between_implies_service rate);
by rewrite (scheduled_between_implies_service);
last by admit.
}
{
......@@ -1060,23 +987,23 @@ Module WorkloadBoundGuan.
[by rewrite FSTtsk JOBin | by apply LEQ | | intro COMPin].
{
rewrite -[scheduled _ _ _]negbK; apply/negP; intro BUG.
apply not_scheduled_no_service with (rate0 := rate) in BUG. by rewrite BUG in FSTserv.
apply not_scheduled_no_service in BUG. by rewrite BUG in FSTserv.
}
clear PREC SPO EQ.
apply negbT in SERV; rewrite negbK in SERV.
unfold completed, service, service_during in NOTCOMPin, COMPin, SERV.
assert (BUG: \sum_(0 <= t0 < t) service_at rate sched j_in t0 < job_cost j_in).
assert (BUG: \sum_(0 <= t0 < t) service_at sched j_in t0 < job_cost j_in).
{
rewrite -> big_cat_nat with (n := t1);
[simpl | by done | by apply LEt].
assert (TMP: \sum_(0 <= t0 < t1) service_at rate sched j_in t0 < job_cost j_in).
assert (TMP: \sum_(0 <= t0 < t1) service_at sched j_in t0 < job_cost j_in).
{
rewrite ltn_neqAle; apply/andP; split; first by done.
by apply COMP.
}
rewrite addnC -addn1 -[job_cost _]addn0 -addnA addnC.
apply leq_add; first by rewrite addn1.
apply leq_trans with (n := \sum_(t1 <= i < t) service_at rate sched j_in i + \sum_(t <= i < t2) service_at rate sched j_in i);
apply leq_trans with (n := \sum_(t1 <= i < t) service_at sched j_in i + \sum_(t <= i < t2) service_at sched j_in i);
first by apply leq_addr.
by rewrite <- big_cat_nat;
[by rewrite leqn0 | by apply LEt | by apply ltnW, GTt].
......@@ -1105,5 +1032,4 @@ Module WorkloadBoundGuan.
End ProofWorkloadBound.
End WorkloadBoundGuan.
workload_jitter.v
+ 24
− 38
View file @ 7755715d
......@@ -19,7 +19,6 @@ Module WorkloadWithJitter.
Context {arr_seq: arrival_sequence Job}.
Context {num_cpus: nat}.
Variable rate: Job -> processor num_cpus -> nat.
Variable sched: schedule num_cpus arr_seq.
(* Consider some task *)
......@@ -136,7 +135,6 @@ Module WorkloadWithJitter.
valid_sporadic_job_with_jitter task_cost task_deadline task_jitter job_cost job_deadline job_task job_jitter j.
Variable num_cpus: nat.
Variable rate: Job -> processor num_cpus -> nat.
Variable schedule_of_platform: schedule num_cpus arr_seq -> Prop.
(* Assume any schedule of a given platform. *)
......@@ -151,16 +149,12 @@ Module WorkloadWithJitter.
(* 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 rate sched.
completed_jobs_dont_execute job_cost sched.
(* Assumptions:
1) A job does not execute in parallel.
2) The service rate of the platform is at most 1.
(* Assumptiom: A job does not execute in parallel.
This is required to use interval lengths as a measure of service. *)
Hypothesis no_parallelism:
jobs_dont_execute_in_parallel sched.
Hypothesis rate_at_most_one :
forall j cpu, rate j cpu <= 1.
(* Assumption: sporadic task model.
This is necessary to conclude that consecutive jobs ordered by arrival times
......@@ -172,12 +166,12 @@ Module WorkloadWithJitter.
Section CleanerDefinitions.
Variable tsk: sporadic_task_with_jitter.
Definition response_time_bound_of (R: time) :=
is_response_time_bound_of_task job_cost job_task tsk rate sched R.
is_response_time_bound_of_task job_cost job_task tsk sched R.
Definition no_deadline_misses_by (t: time) :=
task_misses_no_deadline_before job_cost job_deadline job_task
rate sched tsk t.
sched tsk t.
Definition workload_of (t1 t2: time) :=
workload job_task rate sched tsk t1 t2.
workload job_task sched tsk t1 t2.
End CleanerDefinitions.
(* Now we define the theorem. Let tsk be any task in the taskset. *)
......@@ -235,17 +229,17 @@ Module WorkloadWithJitter.
(* Identify the subset of jobs that actually cause interference *)
set interfering_jobs :=
filter (fun (x: JobIn arr_seq) =>
(job_task x == tsk) && (service_during rate sched x t1 t2 != 0))
(job_task x == tsk) && (service_during sched x t1 t2 != 0))
(jobs_scheduled_between sched t1 t2).
(* Remove the elements that we don't care about from the sum *)
assert (SIMPL:
\sum_(i <- jobs_scheduled_between sched t1 t2 | job_task i == tsk)
service_during rate sched i t1 t2 =
\sum_(i <- interfering_jobs) service_during rate sched i t1 t2).
service_during sched i t1 t2 =
\sum_(i <- interfering_jobs) service_during sched i t1 t2).
{
unfold interfering_jobs.
rewrite (bigID (fun x => service_during rate sched x t1 t2 == 0)) /=.
rewrite (bigID (fun x => service_during sched x t1 t2 == 0)) /=.
rewrite (eq_bigr (fun x => 0)); last by move => j_i /andP JOBi; des; apply /eqP.
rewrite big_const_seq iter_addn mul0n add0n add0n.
by rewrite big_filter.
......@@ -253,7 +247,7 @@ Module WorkloadWithJitter.
(* Remember that for any job of tsk, service <= task_cost tsk *)
assert (LTserv: forall j_i (INi: j_i \in interfering_jobs),
service_during rate sched j_i t1 t2 <= task_cost tsk).
service_during sched j_i t1 t2 <= task_cost tsk).
{
ins; apply cumulative_service_le_task_cost with (task_deadline0 := task_deadline) (job_cost0 := job_cost) (job_deadline0 := job_deadline) (job_task0 := job_task); try (by done);
last by apply job_properties.
......@@ -293,7 +287,7 @@ Module WorkloadWithJitter.
apply leq_trans with (n := \sum_(x <- sorted_jobs) task_cost tsk);
last by rewrite big_const_seq iter_addn addn0 mulnC leq_mul2r; apply/orP; right.
{
rewrite [\sum_(_ <- _) service_during _ _ _ _ _]big_seq_cond.
rewrite [\sum_(_ <- _) service_during _ _ _ _]big_seq_cond.
rewrite [\sum_(_ <- _) task_cost _]big_seq_cond.
by apply leq_sum; intros j_i; move/andP => xxx; des; apply LTserv; rewrite INboth.
}
......@@ -315,14 +309,6 @@ Module WorkloadWithJitter.
move: FST => /andP FST; des; move: FST => /eqP FST.
rename FST0 into FSTin, FST into FSTtask, FST1 into FSTserv.
(* Since there is at least one job of the task, we show that R_tsk >= cost tsk. *)
(*assert (GEcost: R_tsk >= task_cost tsk).
{
apply (response_time_ub_ge_task_cost job_task) with (sched0 := sched) (rate0 := rate); ins.
by exists (nth elem sorted_jobs 0); rewrite FSTtask.
}*)
(* Now we show that the bound holds for a singleton set of interfering jobs. *)
destruct n.
{
......@@ -337,11 +323,11 @@ Module WorkloadWithJitter.
}
{
rewrite -addnBA; last by ins.
rewrite -[service_during _ _ _ _ _]addn0.
rewrite -[service_during _ _ _ _]addn0.
apply leq_add; last by ins.
apply leq_trans with (n := \sum_(t1 <= t < t2) 1).
by apply leq_sum; ins; apply service_at_le_max_rate.
by unfold t2; rewrite big_const_nat iter_addn mul1n addn0 addnC -addnBA // subnn addn0 leq_addr.
apply leq_trans with (n := \sum_(t1 <= t < t2) 1);
first by apply leq_sum; intros i _; apply service_at_most_one.
by unfold t2; rewrite big_const_nat iter_addn mul1n addn0 addnC -addnBA // subnn addn0 leq_addr.
}
}
} rewrite [nth]lock /= -lock in ALL.
......@@ -378,16 +364,16 @@ Module WorkloadWithJitter.
}
(* Next, we upper-bound the service of the first and last jobs using their arrival times. *)
assert (BOUNDend: service_during rate sched j_fst t1 t2 +
service_during rate sched j_lst t1 t2 <=
assert (BOUNDend: service_during sched j_fst t1 t2 +
service_during sched j_lst t1 t2 <=
(job_arrival j_fst + R_tsk - t1) + (t2 - job_arrival j_lst)).
{
apply leq_add; unfold service_during.
{
rewrite -[_ + _ - _]mul1n -[1*_]addn0 -iter_addn -big_const_nat.
apply leq_trans with (n := \sum_(t1 <= t < job_arrival j_fst + R_tsk)
service_at rate sched j_fst t);
last by apply leq_sum; ins; apply service_at_le_max_rate.
service_at sched j_fst t);
last by apply leq_sum; ins; apply service_at_most_one.
destruct (job_arrival j_fst + R_tsk <= t2) eqn:LEt2; last first.
{
unfold t2; apply negbT in LEt2; rewrite -ltnNge in LEt2.
......@@ -408,10 +394,10 @@ Module WorkloadWithJitter.
destruct (job_arrival j_lst <= t1) eqn:LT.
{
apply leq_trans with (n := \sum_(job_arrival j_lst <= t < t2)
service_at rate sched j_lst t);
service_at sched j_lst t);
first by rewrite -> big_cat_nat with (m := job_arrival j_lst) (n := t1);
[by apply leq_addl | by ins | by apply leq_addr].
by apply leq_sum; ins; apply service_at_le_max_rate.
by apply leq_sum; ins; apply service_at_most_one.
}
{
apply negbT in LT; rewrite -ltnNge in LT.
......@@ -422,7 +408,7 @@ Module WorkloadWithJitter.
[by ins| |by apply leqnn].
by apply arrival_before_jitter with (job_jitter0 := job_jitter).
}
by apply leq_sum; ins; apply service_at_le_max_rate.
by apply leq_sum; ins; apply service_at_most_one.
}
}
}
......@@ -444,7 +430,7 @@ Module WorkloadWithJitter.
(* Now we upper-bound the service of the middle jobs. *)
assert (BOUNDmid: \sum_(0 <= i < n)
service_during rate sched (nth elem sorted_jobs i.+1) t1 t2 <=
service_during sched (nth elem sorted_jobs i.+1) t1 t2 <=
n * task_cost tsk).
{
apply leq_trans with (n := n * task_cost tsk);
......@@ -556,7 +542,7 @@ Module WorkloadWithJitter.
unfold service_during; apply/eqP; rewrite -leqn0.
rewrite <- leq_add2l with (p := job_cost j_fst); rewrite addn0.
move: COMP => /eqP COMP; unfold service in COMP; rewrite -{1}COMP.
apply leq_trans with (n := service rate sched j_fst t2); last by apply EXEC.
apply leq_trans with (n := service sched j_fst t2); last by apply EXEC.
unfold service; rewrite -> big_cat_nat with (m := 0) (p := t2) (n := t1);
[rewrite leq_add2r /= | by ins | by apply leq_addr].
rewrite -> big_cat_nat with (p := t1) (n := job_arrival j_fst + job_deadline j_fst);
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment