Newer
Older
[simpl | by apply AFTERt1 | by apply ltnW].
rewrite -[\sum_(_ <= _ < _) 1]addn0; apply leq_add.
{
simpl_sum_const; rewrite -{1}[_ + R_k](addKn t1) -addnBA //.
by apply job_interference_le_delta.
}
apply leq_trans with (n := service_during sched j_fst (a_fst + R_k) t2);
first by apply job_interference_le_service.
(try ( apply cumulative_service_after_job_rt_zero with (job_cost0 := job_cost) (R := R_k)
(job_arrival0 := job_arrival) ) ||
apply cumulative_service_after_job_rt_zero with (job_cost := job_cost) (R := R_k)
(job_arrival := job_arrival)); [ by done | | by apply leqnn].
by apply interference_bound_edf_j_fst_completed_on_time.
}
Qed.
(* ..., which leads to the following bounds based on interval lengths. *)
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
Lemma interference_bound_edf_bounding_interference_with_interval_lengths :
interference_caused_by j_fst t1 t2 + (D_k - R_k) + D_i %/ p_k * p_k <=
\sum_(t1 <= t < a_fst + R_k) 1
+ \sum_(a_fst + R_k <= t < a_fst + D_k) 1
+ \sum_(a_fst + D_k <= t < a_lst + D_k) 1.
Proof.
apply leq_trans with (n := \sum_(t1 <= t < a_fst + R_k) 1 + (D_k - R_k) +
D_i %/ p_k * p_k).
{
rewrite 2!leq_add2r.
apply interference_bound_edf_interference_of_j_fst_bounded_by_response_time.
}
apply leq_trans with (n := \sum_(t1 <= t < a_fst + R_k) 1 + (D_k - R_k) +
(a_lst - a_fst)).
{
rewrite leq_add2l; fold (div_floor D_i p_k) n_k.
rewrite interference_bound_edf_n_k_equals_num_mid_jobs_plus_one.
by apply interference_bound_edf_many_periods_in_between.
}
apply leq_trans with (n := \sum_(t1 <= t < a_fst + R_k) 1 +
\sum_(a_fst + R_k <= t < a_fst + D_k) 1 + \sum_(a_fst + D_k <= t < a_lst + D_k) 1).
{
by rewrite -2!addnA leq_add2l; apply leq_add;
rewrite big_const_nat iter_addn mul1n addn0;
rewrite ?subnDl ?subnDr leqnn.
}
by apply leqnn.
Qed.
(* To conclude, we show that the concatenation of these interval lengths equals
(a_lst + D_k) - 1, ... *)
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
Lemma interference_bound_edf_simpl_by_concatenation_of_intervals :
\sum_(t1 <= t < a_fst + R_k) 1
+ \sum_(a_fst + R_k <= t < a_fst + D_k) 1
+ \sum_(a_fst + D_k <= t < a_lst + D_k) 1 = (a_lst + D_k) - t1.
Proof.
assert (AFTERt1: t1 <= a_fst + R_k).
{
apply interference_bound_edf_j_fst_completion_implies_rt_bound_inside_interval.
by apply interference_bound_edf_j_fst_completed_on_time.
}
rewrite -big_cat_nat;
[simpl | by apply AFTERt1 | by rewrite leq_add2l; apply H_R_k_le_deadline].
rewrite -big_cat_nat; simpl; last 2 first.
{
apply leq_trans with (n := a_fst + R_k); first by apply AFTERt1.
by rewrite leq_add2l; apply H_R_k_le_deadline.
}
{
rewrite leq_add2r; unfold a_fst, a_lst, j_fst, j_lst.
rewrite -[num_mid_jobs.+1]add0n; apply prev_le_next;
last by rewrite add0n H_at_least_two_jobs ltnSn.
by ins; apply interference_bound_edf_jobs_ordered_by_arrival.
}
by rewrite big_const_nat iter_addn mul1n addn0.
Qed.
(* ... which results in proving that (a_lst + D_k) - t1 <= D_i.
This holds because high-priority jobs have earlier deadlines. Therefore,
the interference caused by the first job is bounded by D_i %% p_k - (D_k - R_k). *)
Lemma interference_bound_edf_interference_of_j_fst_limited_by_remainder_and_slack :
interference_caused_by j_fst t1 t2 <= D_i %% p_k - (D_k - R_k).
Proof.
apply interference_bound_edf_simpl_by_moving_to_left_side.
apply (leq_trans interference_bound_edf_bounding_interference_with_interval_lengths).
rewrite interference_bound_edf_simpl_by_concatenation_of_intervals leq_subLR.
have LST := interference_bound_edf_j_lst_is_job_of_tsk_k.
destruct LST as [LSTarr [_ [ LSTserv _]]].
unfold D_i, D_k, a_lst, t1; rewrite -interference_bound_edf_j_lst_deadline
-interference_bound_edf_j_i_deadline.
try ( by apply interference_under_edf_implies_shorter_deadlines
with (arr_seq0 := arr_seq) (job_deadline0 := job_deadline) in LSTserv ) ||
by apply interference_under_edf_implies_shorter_deadlines
with (arr_seq := arr_seq) (job_deadline := job_deadline) in LSTserv.
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
(* Using the lemmas above we show that the interference bound works in the
case of two or more jobs. *)
Lemma interference_bound_edf_holds_for_multiple_jobs :
\sum_(0 <= i < num_mid_jobs.+2)
interference_caused_by (nth elem sorted_jobs i) t1 t2 <= interference_bound.
Proof.
(* Knowing that we have at least two elements, we take first and last out of the sum *)
rewrite [nth]lock big_nat_recl // big_nat_recr // /= -lock.
rewrite addnA addnC addnA.
have NK := interference_bound_edf_n_k_equals_num_mid_jobs_plus_one.
(* We use the lemmas we proved to show that the interference bound holds. *)
unfold interference_bound, edf_specific_interference_bound.
fold D_i D_k p_k n_k.
rewrite addnC addnA; apply leq_add;
first by rewrite addnC interference_bound_edf_holds_for_middle_and_last_jobs.
rewrite leq_min; apply/andP; split.
{
apply interference_bound_edf_interference_le_task_cost.
rewrite interference_bound_edf_job_in_same_sequence.
by apply mem_nth; rewrite H_at_least_two_jobs.
}
by apply interference_bound_edf_interference_of_j_fst_limited_by_remainder_and_slack.
Qed.
End InterferenceTwoOrMoreJobs.
End InterferenceManyJobs.
Theorem interference_bound_edf_bounds_interference :
x <= interference_bound.
Proof.
(* Use the definition of workload based on list of jobs. *)
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.
(* Now we order the list by job arrival time. *)
rewrite interference_bound_edf_simpl_by_sorting_interfering_jobs.
(* Next, we show that the workload bound holds if n_k
is no larger than the number of interferings jobs. *)
destruct (size sorted_jobs <= n_k) eqn:NUM;
first by apply interference_bound_edf_holds_for_at_most_n_k_jobs.
apply negbT in NUM; rewrite -ltnNge in NUM.
(* Find some dummy element to use in the nth function *)
assert (EX: exists elem: Job, True).
destruct sorted_jobs as [| j]; [by rewrite ltn0 in NUM | by exists j].
destruct EX as [elem _].
(* Now we index the sum to access the first and last elements. *)
rewrite (big_nth elem).
(* First, we show that the bound holds for an empty list of jobs. *)
destruct (size sorted_jobs) as [| n] eqn:SIZE;
first by rewrite big_geq.
(* Then, we show the same for a single job, or for multiple jobs. *)
destruct n as [| num_mid_jobs].
rewrite big_nat_recr // big_geq //.
rewrite [nth]lock /= -lock add0n.
by apply interference_bound_edf_holds_for_a_single_job; rewrite SIZE.
by apply interference_bound_edf_holds_for_multiple_jobs; first by rewrite SIZE.
End ProofSpecificBound.
(* As required by the proof of convergence of EDF RTA, we show that the
EDF-specific bound is monotonically increasing with both the size
of the interval and the value of the previous response-time bounds. *)
Section MonotonicitySpecificBound.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task -> time.
Variable task_period: sporadic_task -> time.
Variable task_deadline: sporadic_task -> time.
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
Variable tsk tsk_other: sporadic_task.
Hypothesis H_period_positive: task_period tsk_other > 0.
Variable delta delta' R R': time.
Hypothesis H_delta_monotonic: delta <= delta'.
Hypothesis H_response_time_monotonic: R <= R'.
Hypothesis H_cost_le_rt_bound: task_cost tsk_other <= R.
Lemma interference_bound_edf_monotonic :
interference_bound_edf task_cost task_period task_deadline tsk delta (tsk_other, R) <=
interference_bound_edf task_cost task_period task_deadline tsk delta' (tsk_other, R').
Proof.
rename H_response_time_monotonic into LEr, H_delta_monotonic into LEx,
H_cost_le_rt_bound into LEcost, H_period_positive into GEperiod.
unfold interference_bound_edf, interference_bound_generic.
rewrite leq_min; apply/andP; split.
{
rewrite leq_min; apply/andP; split.
apply leq_trans with (n := (minn (W task_cost task_period (fst (tsk_other, R))
(snd (tsk_other, R)) delta) (delta - task_cost tsk + 1)));
first by apply geq_minl.
apply leq_trans with (n := W task_cost task_period (fst (tsk_other, R))
(snd (tsk_other, R)) delta);
[by apply geq_minl | by apply W_monotonic].
apply leq_trans with (n := minn (W task_cost task_period (fst (tsk_other, R)) (snd (tsk_other, R)) delta) (delta - task_cost tsk + 1));
first by apply geq_minl.
apply leq_trans with (n := delta - task_cost tsk + 1);
first by apply geq_minr.
by rewrite leq_add2r leq_sub2r.
}
{
apply leq_trans with (n := edf_specific_interference_bound task_cost task_period
task_deadline tsk tsk_other R);
first by apply geq_minr.
unfold edf_specific_interference_bound; simpl.
rewrite leq_add2l leq_min; apply/andP; split; first by apply geq_minl.
apply leq_trans with (n := task_deadline tsk %% task_period tsk_other -
(task_deadline tsk_other - R));
[by apply geq_minr | by rewrite 2?leq_sub2l 2?leq_sub2r // leq_sub2l].
}
Qed.
End MonotonicitySpecificBound.