Newer
Older
Require Import Vbase task job task_arrival schedule platform interference
workload workload_bound schedulability priority response_time
bertogna_fp_theory bertogna_edf_theory interference_bound_edf util_divround util_lemmas
ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Import Job SporadicTaskset ScheduleOfSporadicTask Workload Schedulability ResponseTime
Priority SporadicTaskArrival WorkloadBound EDFSpecificBound ResponseTimeAnalysisFP
ResponseTimeAnalysisEDF.
(* In this section, we define the algorithm of Bertogna and Cirinei's
response-time analysis for EDF scheduling. *)
Section Analysis.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task -> nat.
Variable task_period: sporadic_task -> nat.
Variable task_deadline: sporadic_task -> nat.
(* During the iterations of the algorithm, we pass around pairs
of tasks and computed response-time bounds. *)
Let task_with_response_time := (sporadic_task * nat)%type.
Context {Job: eqType}.
Variable job_cost: Job -> nat.
Variable job_deadline: Job -> nat.
Variable job_task: Job -> sporadic_task.
(* Consider a platform with num_cpus processors. *)
(* First, recall the interference bound under EDF, ... *)
Let I (rt_bounds: seq task_with_response_time)
(tsk: sporadic_task) (delta: time) :=
total_interference_bound_edf task_cost task_period task_deadline tsk rt_bounds delta.
(* ..., which yields the following response-time bound. *)
Definition edf_response_time_bound (rt_bounds: seq task_with_response_time)
(tsk: sporadic_task) (delta: time) :=
task_cost tsk + div_floor (I rt_bounds tsk delta) num_cpus.
(* Also note that a response-time is only valid if it is no larger
than the deadline. *)
Definition R_le_deadline (pair: task_with_response_time) :=
let (tsk, R) := pair in
R <= task_deadline tsk.
(* Next we define the fixed-point iteration for computing
Bertogna's response-time bound of a task set. *)
(* Given a sequence 'rt_bounds' of task and response-time bounds
from the previous iteration, we compute the response-time
bound of a single task using the RTA for EDF. *)
Definition update_bound (rt_bounds: seq task_with_response_time)
(pair : task_with_response_time) :=
let (tsk, R) := pair in
(tsk, edf_response_time_bound rt_bounds tsk R).
(* To compute the response-time bounds of the entire task set,
We start the iteration with a sequence of tasks and costs:
<(task1, cost1), (task2, cost2), ...>. *)
Let initial_state (ts: taskset_of sporadic_task) :=
map (fun t => (t, task_cost t)) ts.
(* Then, we successively update the the response-time bounds based
on the slack computed in the previous iteration. *)
Definition edf_rta_iteration (rt_bounds: seq task_with_response_time) :=
(* To ensure that the procedure converges, we run the iteration a
"sufficient" number of times: task_deadline tsk - task_cost tsk + 1.
This corresponds to the time complexity of the procedure. *)
Let max_steps (ts: taskset_of sporadic_task) :=
\sum_(tsk <- ts) (task_deadline tsk - task_cost tsk) + 1.
(* This yields the following definition for the RTA. At the end of
the iteration, we check if all computed response-time bounds
are less than or equal to the deadline, in which case they are
valid. *)
Definition edf_claimed_bounds (ts: taskset_of sporadic_task) :=
let R_values := iter (max_steps ts) edf_rta_iteration (initial_state ts) in
if (all R_le_deadline R_values) then
Some R_values
else None.
(* The schedulability test simply checks if we got a list of
response-time bounds (i.e., if the computation did not fail). *)
Definition edf_schedulable (ts: taskset_of sporadic_task) :=
(* In the following section, we prove several helper lemmas about the
list of tasks/response-time bounds. *)
Section SimpleLemmas.
(* Updating a single response-time bound does not modify the task. *)
Lemma edf_claimed_bounds_unzip1_update_bound :
forall l rt_bounds,
unzip1 (map (update_bound rt_bounds) l) = unzip1 l.
Proof.
induction l; first by done.
intros rt_bounds.
simpl; f_equal; last by done.
by unfold update_bound; desf.
Qed.
(* At any point of the iteration, the tasks are the same. *)
Lemma edf_claimed_bounds_unzip1_iteration :
forall l k,
unzip1 (iter k edf_rta_iteration (initial_state l)) = l.
Proof.
intros l k; clear -k.
induction k; simpl.
{
unfold initial_state.
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
by simpl; rewrite IHl.
}
{
unfold edf_rta_iteration.
by rewrite edf_claimed_bounds_unzip1_update_bound.
}
Qed.
(* The iteration preserves the size of the list. *)
Lemma edf_claimed_bounds_size :
forall l k,
size (iter k edf_rta_iteration (initial_state l)) = size l.
Proof.
intros l k; clear -k.
induction k; simpl; first by rewrite size_map.
by rewrite size_map.
Qed.
(* If the analysis succeeds, the computed response-time bounds are no smaller
than the task cost. *)
Lemma edf_claimed_bounds_ge_cost :
forall l k tsk R,
(tsk, R) \in (iter k edf_rta_iteration (initial_state l)) ->
R >= task_cost tsk.
Proof.
intros l k tsk R IN.
destruct k.
{
move: IN => /mapP IN; destruct IN as [x IN EQ]; inversion EQ.
by apply leqnn.
}
{
rewrite iterS in IN.
move: IN => /mapP IN; destruct IN as [x IN EQ].
unfold update_bound in EQ; destruct x; inversion EQ.
by unfold edf_response_time_bound; apply leq_addr.
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
}
Qed.
(* If the analysis suceeds, the computed response-time bounds are no larger
than the deadline. *)
Lemma edf_claimed_bounds_le_deadline :
forall ts rt_bounds tsk R,
edf_claimed_bounds ts = Some rt_bounds ->
(tsk, R) \in rt_bounds ->
R <= task_deadline tsk.
Proof.
intros ts rt_bounds tsk R SOME PAIR; unfold edf_claimed_bounds in SOME.
destruct (all R_le_deadline (iter (max_steps ts)
edf_rta_iteration (initial_state ts))) eqn:DEADLINE;
last by done.
move: DEADLINE => /allP DEADLINE.
inversion SOME as [EQ]; rewrite -EQ in PAIR.
by specialize (DEADLINE (tsk, R) PAIR).
Qed.
(* The list contains a response-time bound for every task in the task set. *)
Lemma edf_claimed_bounds_has_R_for_every_task :
forall ts rt_bounds tsk,
edf_claimed_bounds ts = Some rt_bounds ->
tsk \in ts ->
exists R,
(tsk, R) \in rt_bounds.
Proof.
intros ts rt_bounds tsk SOME IN.
unfold edf_claimed_bounds in SOME.
destruct (all R_le_deadline (iter (max_steps ts) edf_rta_iteration (initial_state ts)));
last by done.
inversion SOME as [EQ]; clear SOME EQ.
generalize dependent tsk.
induction (max_steps ts) as [| step]; simpl in *.
{
intros tsk IN; unfold initial_state.
exists (task_cost tsk).
by apply/mapP; exists tsk.
}
{
intros tsk IN.
set prev_state := iter step edf_rta_iteration (initial_state ts).
fold prev_state in IN, IHstep.
specialize (IHstep tsk IN); des.
exists (edf_response_time_bound prev_state tsk R).
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
by apply/mapP; exists (tsk, R); [by done | by f_equal].
}
Qed.
End SimpleLemmas.
(* As required by the proof of convergence, we show that the
interference bound is monotonically increasing with both
the size of the interval and the value of the previous
response-time bounds.
TODO: move to bertogna_edf_theory.v? *)
Section MonotonicityOfInterferenceBound.
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_fp.
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].
}
Qed.
End MonotonicityOfInterferenceBound.
(* In this section, we prove the convergence of the RTA procedure.
Since we define the RTA procedure as the application of a function
a fixed number of times, this translates into proving that the value
of the iteration at (max_steps ts) is equal to the value at (max_steps ts) + 1. *)
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
Section Convergence.
(* Consider any valid task set. *)
Variable ts: taskset_of sporadic_task.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
(* To simplify, let f denote the RTA procedure. *)
Let f (k: nat) := iter k edf_rta_iteration (initial_state ts).
(* Since the iteration is applied directly to a list of tasks and response-times,
we define a corresponding relation "<=" over those lists. *)
(* Let 'all_le' be a binary relation over lists of tasks/response-time bounds.
It states that every element of list l1 has a response-time bound R that is less
than or equal to the corresponding response-time bound R' in list l2 (point-wise).
In addition, the relation states that the tasks of both lists are unchanged. *)
Let all_le := fun (l1 l2: list task_with_response_time) =>
(unzip1 l1 == unzip1 l2) &&
all (fun p => (snd (fst p)) <= (snd (snd p))) (zip l1 l2).
(* Similarly, we define a strict version of 'all_le' called 'one_lt', which states that
there exists at least one element whose response-time bound increases. *)
Let one_lt := fun (l1 l2: list task_with_response_time) =>
(unzip1 l1 == unzip1 l2) &&
has (fun p => (snd (fst p)) < (snd (snd p))) (zip l1 l2).
(* Next, we prove some basic properties about the relation all_le. *)
Section RelationProperties.
(* The relation is reflexive, ... *)
Lemma all_le_reflexive : reflexive all_le.
Proof.
intros l; unfold all_le; rewrite eq_refl andTb.
destruct l; first by done.
apply/(zipP (fun x y => snd x <= snd y)); try (by ins).
by ins; apply leqnn.
(* ... and transitive. *)
Lemma all_le_transitive: transitive all_le.
unfold transitive, all_le.
move => y x z /andP [/eqP ZIPxy LExy] /andP [/eqP ZIPyz LEyz].
apply/andP; split; first by rewrite ZIPxy -ZIPyz.
move: LExy => /(zipP (fun x y => snd x <= snd y)) LExy.
move: LEyz => /(zipP (fun x y => snd x <= snd y)) LEyz.
assert (SIZExy: size (unzip1 x) = size (unzip1 y)).
by rewrite ZIPxy.
assert (SIZEyz: size (unzip1 y) = size (unzip1 z)).
by rewrite ZIPyz.
rewrite 2!size_map in SIZExy; rewrite 2!size_map in SIZEyz.
destruct y.
apply size0nil in SIZExy; symmetry in SIZEyz.
by apply size0nil in SIZEyz; subst.
apply/(zipP (fun x y => snd x <= snd y));
[by apply (t, 0) | by rewrite SIZExy -SIZEyz|].
intros i LTi.
exploit LExy; first by rewrite SIZExy.
rewrite size_zip -SIZEyz -SIZExy minnn in LTi.
by rewrite size_zip -SIZExy minnn; apply LTi.
instantiate (1 := t); intro LE.
exploit LEyz; first by apply SIZEyz.
{
rewrite size_zip SIZExy SIZEyz minnn in LTi.
by rewrite size_zip SIZEyz minnn; apply LTi.
}
by instantiate (1 := t); intro LE'; apply (leq_trans LE).
(* At any step of the iteration, the corresponding list
is larger than or equal to the initial state. *)
Lemma bertogna_edf_comp_iteration_preserves_minimum :
forall step, all_le (initial_state ts) (f step).
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
unfold f.
intros step; destruct step; first by apply all_le_reflexive.
apply/andP; split.
{
assert (UNZIP0 := edf_claimed_bounds_unzip1_iteration ts 0).
by simpl in UNZIP0; rewrite UNZIP0 edf_claimed_bounds_unzip1_iteration.
}
destruct ts as [| tsk0 ts'].
{
clear -step; induction step; first by done.
by rewrite iterSr IHstep.
}
apply/(zipP (fun x y => snd x <= snd y));
[by apply (tsk0,0)|by rewrite edf_claimed_bounds_size size_map |].
intros i LTi; rewrite iterS; unfold edf_rta_iteration at 1.
have MAP := @nth_map _ (tsk0,0) _ (tsk0,0).
rewrite size_zip edf_claimed_bounds_size size_map minnn in LTi.
rewrite MAP; clear MAP; last by rewrite edf_claimed_bounds_size.
destruct (nth (tsk0, 0) (initial_state (tsk0 :: ts')) i) as [tsk_i R_i] eqn:SUBST.
rewrite SUBST; unfold update_bound.
unfold initial_state in SUBST.
have MAP := @nth_map _ tsk0 _ (tsk0, 0).
rewrite ?MAP // in SUBST; inversion SUBST; clear MAP.
assert (EQtsk: tsk_i = fst (nth (tsk0, 0) (iter step edf_rta_iteration
(initial_state (tsk0 :: ts'))) i)).
{
have MAP := @nth_map _ (tsk0,0) _ tsk0 (fun x => fst x).
rewrite -MAP; clear MAP; last by rewrite edf_claimed_bounds_size.
have UNZIP := edf_claimed_bounds_unzip1_iteration; unfold unzip1 in UNZIP.
by rewrite UNZIP; symmetry.
}
destruct (nth (tsk0, 0) (iter step edf_rta_iteration (initial_state (tsk0 :: ts')))) as [tsk_i' R_i'].
by simpl in EQtsk; rewrite -EQtsk; subst; apply leq_addr.
(* As a last step, we show that edf_rta_iteration preserves order, i.e., for any
list l1 no smaller than the initial state, and list l2 such that
l1 <= l2, we have (edf_rta_iteration l1) <= (edf_rta_iteration l2). *)
Lemma bertogna_edf_comp_iteration_preserves_order :
forall l1 l2,
all_le (initial_state ts) l1 ->
all_le l1 l2 ->
all_le (edf_rta_iteration l1) (edf_rta_iteration l2).
rename H_valid_task_parameters into VALID.
intros x1 x2 LEinit LE.
move: LE => /andP [/eqP ZIP LE]; unfold all_le.
assert (UNZIP': unzip1 (edf_rta_iteration x1) = unzip1 (edf_rta_iteration x2)).
by rewrite 2!edf_claimed_bounds_unzip1_update_bound.
}
apply/andP; split; first by rewrite UNZIP'.
apply f_equal with (B := nat) (f := fun x => size x) in UNZIP'.
rename UNZIP' into SIZE.
rewrite size_map [size (unzip1 _)]size_map in SIZE.
move: LE => /(zipP (fun x y => snd x <= snd y)) LE.
destruct x1 as [| p0 x1'], x2 as [| p0' x2']; try (by ins).
apply/(zipP (fun x y => snd x <= snd y));
[by apply (p0,0) | by done |].
intros i LTi.
exploit LE; first by rewrite 2!size_map in SIZE.
{
by rewrite size_zip 2!size_map -size_zip in LTi; apply LTi.
}
rewrite 2!size_map in SIZE.
instantiate (1 := p0); intro LEi.
rewrite (nth_map p0);
last by rewrite size_zip 2!size_map -SIZE minnn in LTi.
rewrite (nth_map p0);
last by rewrite size_zip 2!size_map SIZE minnn in LTi.
unfold update_bound, edf_response_time_bound; desf; simpl.
rename s into tsk_i, s0 into tsk_i', n into R_i, n0 into R_i', Heq into EQ, Heq0 into EQ'.
assert (EQtsk: tsk_i = tsk_i').
{
destruct p0 as [tsk0 R0], p0' as [tsk0' R0']; simpl in H2; subst.
have MAP := @nth_map _ (tsk0',R0) _ tsk0' (fun x => fst x) i ((tsk0', R0) :: x1').
have MAP' := @nth_map _ (tsk0',R0) _ tsk0' (fun x => fst x) i ((tsk0', R0') :: x2').
assert (FSTeq: fst (nth (tsk0', R0)((tsk0', R0) :: x1') i) =
fst (nth (tsk0',R0) ((tsk0', R0') :: x2') i)).
rewrite -MAP;
last by simpl; rewrite size_zip 2!size_map /= -H0 minnn in LTi.
rewrite -MAP';
last by simpl; rewrite size_zip 2!size_map /= H0 minnn in LTi.
by f_equal; simpl; f_equal.
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
apply f_equal with (B := sporadic_task) (f := fun x => fst x) in EQ.
apply f_equal with (B := sporadic_task) (f := fun x => fst x) in EQ'.
by rewrite FSTeq EQ' /= in EQ; rewrite EQ.
}
subst tsk_i'; rewrite leq_add2l.
unfold I, total_interference_bound_edf; apply leq_div2r.
rewrite 2!big_cons.
destruct p0 as [tsk0 R0], p0' as [tsk0' R0'].
simpl in H2; subst tsk0'.
rename R_i into delta, R_i' into delta'.
rewrite EQ EQ' in LEi; simpl in LEi.
rename H0 into SIZE, H1 into UNZIP; clear EQ EQ'.
assert (SUBST: forall l delta,
\sum_(j <- l | let '(tsk_other, _) := j in
is_interfering_task_jlfp tsk_i tsk_other)
(let '(tsk_other, R_other) := j in
interference_bound_edf task_cost task_period task_deadline tsk_i delta
(tsk_other, R_other)) =
\sum_(j <- l | is_interfering_task_jlfp tsk_i (fst j))
interference_bound_edf task_cost task_period task_deadline tsk_i delta j).
{
intros l x; clear -l.
induction l; first by rewrite 2!big_nil.
by rewrite 2!big_cons; rewrite IHl; desf; rewrite /= Heq in Heq0.
} rewrite 2!SUBST; clear SUBST.
assert (VALID': valid_sporadic_taskset task_cost task_period task_deadline
(unzip1 ((tsk0, R0) :: x1'))).
{
move: LEinit => /andP [/eqP EQinit _].
rewrite -EQinit; unfold valid_sporadic_taskset.
move => tsk /mapP IN. destruct IN as [p INinit EQ]; subst.
by move: INinit => /mapP INinit; destruct INinit as [tsk INtsk]; subst; apply VALID.
}
assert (GE_COST: all (fun p => task_cost (fst p) <= snd p) ((tsk0, R0) :: x1')).
{
clear LE; move: LEinit => /andP [/eqP UNZIP' LE].
move: LE => /(zipP (fun x y => snd x <= snd y)) LE.
specialize (LE (tsk0, R0)).
apply/(all_nthP (tsk0,R0)).
intros j LTj; generalize UNZIP'; simpl; intro SIZE'.
have F := @f_equal _ _ size (unzip1 (initial_state ts)).
apply F in SIZE'; clear F; rewrite /= 3!size_map in SIZE'.
exploit LE; [by rewrite size_map /= | |].
rewrite size_zip size_map /= SIZE' minnn.
by simpl in LTj; apply LTj.
clear LE; intro LE.
unfold initial_state in LE.
have MAP := @nth_map _ tsk0 _ (tsk0,R0).
rewrite MAP /= in LE;
[clear MAP | by rewrite SIZE'; simpl in LTj].
apply leq_trans with (n := task_cost (nth tsk0 ts j));
[apply eq_leq; f_equal | by done].
have MAP := @nth_map _ (tsk0, R0) _ tsk0 (fun x => fst x).
rewrite -MAP; [clear MAP | by done].
unfold unzip1 in UNZIP'; rewrite -UNZIP'; f_equal.
clear -ts; induction ts; [by done | by simpl; f_equal].
move: GE_COST => /allP GE_COST.
assert (LESUM: \sum_(j <- x1' | is_interfering_task_jlfp tsk_i (fst j))
interference_bound_edf task_cost task_period task_deadline tsk_i delta j <= \sum_(j <- x2' | is_interfering_task_jlfp tsk_i (fst j))
interference_bound_edf task_cost task_period task_deadline tsk_i delta' j).
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
set elem := (tsk0, R0); rewrite 2!(big_nth elem).
rewrite -SIZE.
rewrite big_mkcond [\sum_(_ <- _ | is_interfering_task_jlfp _ _)_]big_mkcond.
rewrite big_seq_cond [\sum_(_ <- _ | true) _]big_seq_cond.
apply leq_sum; intros j; rewrite andbT; intros INj.
rewrite mem_iota add0n subn0 in INj; move: INj => /andP [_ INj].
assert (FSTeq: fst (nth elem x1' j) = fst (nth elem x2' j)).
{
have MAP := @nth_map _ elem _ tsk0 (fun x => fst x).
by rewrite -2?MAP -?SIZE //; f_equal.
} rewrite -FSTeq.
destruct (is_interfering_task_jlfp tsk_i (fst (nth elem x1' j))) eqn:INTERF;
last by done.
{
exploit (LE elem); [by rewrite /= SIZE | | intro LEj].
{
rewrite size_zip 2!size_map /= -SIZE minnn in LTi.
by rewrite size_zip /= -SIZE minnn; apply (leq_ltn_trans INj).
}
simpl in LEj.
exploit (VALID' (fst (nth elem x1' j))); last intro VALIDj.
{
apply/mapP; exists (nth elem x1' j); last by done.
by rewrite in_cons; apply/orP; right; rewrite mem_nth.
}
exploit (GE_COST (nth elem x1' j)); last intro GE_COSTj.
{
by rewrite in_cons; apply/orP; right; rewrite mem_nth.
}
unfold is_valid_sporadic_task in *.
destruct (nth elem x1' j) as [tsk_j R_j], (nth elem x2' j) as [tsk_j' R_j'].
simpl in FSTeq; rewrite -FSTeq; simpl in LEj; simpl in VALIDj; des.
by apply interference_bound_edf_monotonic.
}
}
destruct (is_interfering_task_jlfp tsk_i tsk0) eqn:INTERFtsk0; last by done.
apply leq_add; last by done.
{
exploit (LE (tsk0, R0)); [by rewrite /= SIZE | | intro LEj];
first by instantiate (1 := 0); rewrite size_zip /= -SIZE minnn.
exploit (VALID' tsk0); first by rewrite in_cons; apply/orP; left.
exploit (GE_COST (tsk0, R0)); first by rewrite in_cons eq_refl orTb.
unfold is_valid_sporadic_task; intros GE_COST0 VALID0; des; simpl in LEj.
by apply interference_bound_edf_monotonic.
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
(* It follows from the properties above that the iteration is monotonically increasing. *)
Lemma bertogna_edf_comp_iteration_monotonic: forall k, all_le (f k) (f k.+1).
Proof.
unfold f; intros k.
apply fun_mon_iter_mon_generic with (x1 := k) (x2 := k.+1);
try (by done);
[ by apply all_le_reflexive
| by apply all_le_transitive
| by apply leqnSn
| by apply bertogna_edf_comp_iteration_preserves_order
| by apply bertogna_edf_comp_iteration_preserves_minimum].
Qed.
End RelationProperties.
(* Knowing that the iteration is monotonically increasing (with respect to all_le),
we show that the RTA procedure converges to a fixed point. *)
(* First, note that when there are no tasks, the iteration trivially converges. *)
Lemma bertogna_edf_comp_f_converges_with_no_tasks :
size ts = 0 ->
f (max_steps ts) = f (max_steps ts).+1.
Proof.
intro SIZE; destruct ts; last by inversion SIZE.
unfold max_steps; rewrite big_nil /=.
by unfold edf_rta_iteration.
Qed.
(* Otherwise, if the iteration reached a fixed point before (max_steps ts), then
the value at (max_steps ts) is still at a fixed point. *)
Lemma bertogna_edf_comp_f_converges_early :
(exists k, k <= max_steps ts /\ f k = f k.+1) ->
f (max_steps ts) = f (max_steps ts).+1.
Proof.
by intros EX; des; apply iter_fix with (k := k).
Qed.
(* Else, we derive a contradiction. *)
Section DerivingContradiction.
(* Assume that there are tasks. *)
Hypothesis H_at_least_one_task: size ts > 0.
(* Assume that the iteration continued to diverge. *)
Hypothesis H_keeps_diverging:
forall k,
k <= max_steps ts -> f k != f k.+1.
(* Since the iteration is monotonically increasing, it must be
strictly increasing. *)
Lemma bertogna_edf_comp_f_increases :
forall k,
k <= max_steps ts -> one_lt (f k) (f k.+1).
rename H_at_least_one_task into NONEMPTY.
intros step LEstep; unfold one_lt; apply/andP; split;
first by rewrite 2!edf_claimed_bounds_unzip1_iteration.
rewrite -[has _ _]negbK; apply/negP; unfold not; intro ALL.
rewrite -all_predC in ALL.
move: ALL => /allP ALL.
exploit (H_keeps_diverging step); [by done | intro DIFF].
assert (DUMMY: exists tsk: sporadic_task, True).
destruct ts as [|tsk0]; first by rewrite ltnn in NONEMPTY.
by exists tsk0.
des; clear DUMMY.
move: DIFF => /eqP DIFF; apply DIFF.
apply eq_from_nth with (x0 := (tsk, 0));
first by simpl; rewrite size_map.
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
intros i LTi.
remember (nth (tsk, 0)(f step) i) as p_i;rewrite -Heqp_i.
remember (nth (tsk, 0)(f step.+1) i) as p_i';rewrite -Heqp_i'.
rename Heqp_i into EQ, Heqp_i' into EQ'.
exploit (ALL (p_i, p_i')).
{
rewrite EQ EQ'.
rewrite -nth_zip; last by unfold f; rewrite iterS size_map.
apply mem_nth; rewrite size_zip.
unfold f; rewrite iterS size_map.
by rewrite minnn.
}
unfold predC; simpl; rewrite -ltnNge; intro LTp.
have GROWS := bertogna_edf_comp_iteration_monotonic step.
move: GROWS => /andP [_ /allP GROWS].
exploit (GROWS (p_i, p_i')).
{
rewrite EQ EQ'.
rewrite -nth_zip; last by unfold f; rewrite iterS size_map.
apply mem_nth; rewrite size_zip.
unfold f; rewrite iterS size_map.
by rewrite minnn.
}
simpl; intros LE.
destruct p_i as [tsk_i R_i], p_i' as [tsk_i' R_i'].
simpl in *.
assert (EQtsk: tsk_i = tsk_i').
{
unfold edf_rta_iteration in EQ'.
rewrite (nth_map (tsk, 0)) in EQ'; last by done.
by unfold update_bound in EQ'; desf.
}
rewrite EQtsk; f_equal.
by apply/eqP; rewrite eqn_leq; apply/andP; split.
}
(* In the end, each response-time bound is so high that the sum
of all response-time bounds exceeds the sum of all deadlines.
Contradiction! *)
Lemma bertogna_edf_comp_rt_grows_too_much :
forall k,
k <= max_steps ts ->
\sum_((tsk, R) <- f k) (R - task_cost tsk) + 1 > k.
rename H_at_least_one_task into NONEMPTY.
unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
rename H_valid_task_parameters into VALID.
intros step LE.
assert (DUMMY: exists tsk: sporadic_task, True).
destruct ts as [|tsk0]; first by rewrite ltnn in NONEMPTY.
by exists tsk0.
} destruct DUMMY as [elem _].
induction step.
{
by rewrite addn1.
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
rewrite -addn1 ltn_add2r.
apply leq_ltn_trans with (n := \sum_(i <- f step) (let '(tsk, R) := i in R - task_cost tsk)).
{
rewrite -ltnS; rewrite addn1 in IHstep.
by apply IHstep, ltnW.
}
rewrite (eq_bigr (fun x => snd x - task_cost (fst x)));
last by ins; destruct i.
rewrite [\sum_(_ <- f step.+1)_](eq_bigr (fun x => snd x - task_cost (fst x)));
last by ins; destruct i.
unfold f at 2; rewrite iterS.
rewrite big_map; fold (f step).
rewrite -(ltn_add2r (\sum_(i <- f step) task_cost (fst i))).
rewrite -2!big_split /=.
rewrite big_seq_cond [\sum_(_ <- _ | true)_]big_seq_cond.
rewrite (eq_bigr (fun i => snd i)); last first.
{
intro i; rewrite andbT; intro IN;
rewrite subh1; first by rewrite -addnBA // subnn addn0.
have GE_COST := edf_claimed_bounds_ge_cost ts step.
by destruct i; apply GE_COST.
}
rewrite [\sum_(_ <- _ | _)(_ - _ + _)](eq_bigr (fun i => snd (update_bound (f step) i))); last first.
{
intro i; rewrite andbT; intro IN.
unfold update_bound; destruct i; simpl.
rewrite subh1; first by rewrite -addnBA // subnn addn0.
apply (edf_claimed_bounds_ge_cost ts step.+1).
by rewrite iterS; apply/mapP; exists (s, n).
}
rewrite -2!big_seq_cond.
have LT := bertogna_edf_comp_f_increases step (ltnW LE).
have MONO := bertogna_edf_comp_iteration_monotonic step.
move: LT => /andP [_ LT]; move: LT => /hasP LT.
destruct LT as [[x1 x2] INzip LT]; simpl in *.
move: MONO => /andP [_ /(zipP (fun x y => snd x <= snd y)) MONO].
rewrite 2!(big_nth (elem, 0)).
apply mem_zip_exists with (elem := (elem, 0)) (elem' := (elem, 0)) in INzip; des;
last by rewrite size_map.
rewrite -> big_cat_nat with (m := 0) (n := idx) (p := size (f step));
[simpl | by done | by apply ltnW].
rewrite -> big_cat_nat with (m := idx) (n := idx.+1) (p := size (f step));
[simpl | by done | by done].
rewrite big_nat_recr /=; last by done.
rewrite -> big_cat_nat with (m := 0) (n := idx) (p := size (f step));
[simpl | by done | by apply ltnW].
rewrite -> big_cat_nat with (m := idx) (n := idx.+1) (p := size (f step));
[simpl | by done | by done].
rewrite big_nat_recr /=; last by done.
rewrite [\sum_(idx <= i < idx) _]big_geq // add0n.
rewrite [\sum_(idx <= i < idx) _]big_geq // add0n.
rewrite -addn1 -addnA; apply leq_add.
{
rewrite big_nat_cond [\sum_(_ <= _ < _ | true) _]big_nat_cond.
apply leq_sum; move => i /andP [/andP [LT1 LT2] _].
exploit (MONO (elem,0)); [by rewrite size_map | | intro LEi].
{
rewrite size_zip; apply (ltn_trans LT2).
by apply leq_trans with (n := size (f step));
[by done | by rewrite size_map minnn].
}
unfold edf_rta_iteration in LEi.
by rewrite -> nth_map with (x1 := (elem, 0)) in LEi;
last by apply (ltn_trans LT2).
}
rewrite -addnA [_ + 1]addnC addnA; apply leq_add.
{
unfold edf_rta_iteration in INzip2; rewrite addn1.
rewrite -> nth_map with (x1 := (elem, 0)) in INzip2; last by done.
by rewrite -INzip2 -INzip1.
}
{
rewrite big_nat_cond [\sum_(_ <= _ < _ | true) _]big_nat_cond.
apply leq_sum; move => i /andP [/andP [LT1 LT2] _].
exploit (MONO (elem,0));
[ by rewrite size_map
| by rewrite size_zip; apply (leq_trans LT2); rewrite size_map minnn | intro LEi ].
unfold edf_rta_iteration in LEi.
by rewrite -> nth_map with (x1 := (elem, 0)) in LEi; last by done.
}
(* Using the lemmas above, we prove that edf_rta_iteration reaches a fixed point
after (max_steps ts) iterations, ... *)
Lemma edf_claimed_bounds_converges_helper :
forall rt_bounds,
edf_claimed_bounds ts = Some rt_bounds ->
valid_sporadic_taskset task_cost task_period task_deadline ts ->
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
Proof.
intros rt_bounds SOME VALID.
unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
unfold edf_claimed_bounds in SOME; desf.
rename Heq into LE.
fold (f (max_steps ts)) in *; fold (f (max_steps ts).+1).
(* Either the task set is empty or not. *)
destruct (size ts == 0) eqn:EMPTY;
first by apply bertogna_edf_comp_f_converges_with_no_tasks; apply/eqP.
apply negbT in EMPTY; rewrite -lt0n in EMPTY.
(* Either f converges by the deadline or not. *)
destruct ([exists k in 'I_((max_steps ts).+1), f k == f k.+1]) eqn:EX.
{
move: EX => /exists_inP EX; destruct EX as [k _ ITERk].
destruct k as [k LTk]; simpl in ITERk.
apply bertogna_edf_comp_f_converges_early.
exists k; split; [by apply LTk | by apply/eqP].
}
(* If not, then we reach a contradiction *)
apply negbT in EX; rewrite negb_exists_in in EX.
move: EX => /forall_inP EX.
assert (SAMESUM: \sum_(tsk <- ts) task_cost tsk = \sum_(p <- f (max_steps ts)) task_cost (fst p)).
{
have MAP := @big_map _ 0 addn _ _ (fun x => fst x) (f (max_steps ts))
(fun x => true) (fun x => task_cost x).
have UNZIP := edf_claimed_bounds_unzip1_iteration ts (max_steps ts).
fold (f (max_steps ts)) in UNZIP; unfold unzip1 in UNZIP.
by rewrite UNZIP in MAP; rewrite MAP.
}
(* Show that the sum is less than the sum of all deadlines. *)
assert (SUM: \sum_(p <- f (max_steps ts)) (snd p - task_cost (fst p)) + 1 <= max_steps ts).
{
unfold max_steps at 2; rewrite leq_add2r.
rewrite -(leq_add2r (\sum_(tsk <- ts) task_cost tsk)).
rewrite {1}SAMESUM -2!big_split /=.
rewrite big_seq_cond [\sum_(_ <- _ | true)_]big_seq_cond.
rewrite (eq_bigr (fun x => snd x)); last first.
{
intro i; rewrite andbT; intro IN.
rewrite subh1; first by rewrite -addnBA // subnn addn0.
have GE_COST := edf_claimed_bounds_ge_cost ts (max_steps ts).
fold (f (max_steps ts)) in GE_COST.
by destruct i; apply GE_COST.
}
rewrite (eq_bigr (fun x => task_deadline x)); last first.
{
intro i; rewrite andbT; intro IN.
rewrite subh1; first by rewrite -addnBA // subnn addn0.
by specialize (VALID i IN); des.
}
rewrite -2!big_seq_cond.
have MAP := @big_map _ 0 addn _ _ (fun x => fst x) (f (max_steps ts))
(fun x => true) (fun x => task_deadline x).
have UNZIP := edf_claimed_bounds_unzip1_iteration ts (max_steps ts).
fold (f (max_steps ts)) in UNZIP; unfold unzip1 in UNZIP.
rewrite UNZIP in MAP; rewrite MAP.
rewrite big_seq_cond [\sum_(_ <- _|true)_]big_seq_cond.
apply leq_sum; intro i; rewrite andbT; intro IN.
move: LE => /allP LE; unfold R_le_deadline in LE.
by specialize (LE i IN); destruct i.
}
have TOOMUCH :=
bertogna_edf_comp_rt_grows_too_much EMPTY _ (max_steps ts) (leqnn (max_steps ts)).
exploit TOOMUCH; [| intro BUG].
{
intros k LEk; rewrite -ltnS in LEk.
by exploit (EX (Ordinal LEk)); [by done | by ins].
}
rewrite (eq_bigr (fun i => snd i - task_cost (fst i))) in BUG;
last by ins; destruct i.
by apply (leq_ltn_trans SUM) in BUG; rewrite ltnn in BUG.
Qed.
(* ..., which in turn implies that the response-time bound is the fixed
point from Bertogna and Cirinei's equation. *)
Lemma edf_claimed_bounds_converges :
forall tsk R rt_bounds,
edf_claimed_bounds ts = Some rt_bounds ->
(tsk, R) \in rt_bounds ->
R = task_cost tsk + div_floor (I rt_bounds tsk R) num_cpus.
Proof.
intros tsk R rt_bounds SOME IN.
have CONV := edf_claimed_bounds_converges_helper rt_bounds.
unfold edf_claimed_bounds in *; desf.
exploit (CONV); [by done | by done | intro ITER; clear CONV].
cut (update_bound (iter (max_steps ts)
edf_rta_iteration (initial_state ts)) (tsk,R) = (tsk, R)).
{
intros EQ.
have F := @f_equal _ _ (fun x => snd x) _ (tsk, R).
by apply F in EQ; simpl in EQ.
}
set s := iter (max_steps ts) edf_rta_iteration (initial_state ts).
fold s in ITER, IN.
move: IN => /(nthP (tsk,0)) IN; destruct IN as [i LT EQ].
generalize EQ; rewrite ITER iterS in EQ; intro EQ'.
fold s in EQ.
unfold edf_rta_iteration in EQ.
have MAP := @nth_map _ (tsk,0) _ _ (update_bound s).
by rewrite MAP // EQ' in EQ; rewrite EQ.
Qed.
End Convergence.
Section MainProof.
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
(* Consider a task set ts. *)
Variable ts: taskset_of sporadic_task.
(* Assume the task set has no duplicates, ... *)
Hypothesis H_ts_is_a_set: uniq ts.
(* ...all tasks have valid parameters, ... *)
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
(* ...restricted deadlines, ...*)
Hypothesis H_restricted_deadlines:
forall tsk, tsk \in ts -> task_deadline tsk <= task_period tsk.
(* Next, consider any arrival sequence such that...*)
Context {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.
(* ...they have valid parameters,...*)
Hypothesis H_valid_job_parameters:
forall (j: JobIn arr_seq),
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.
(* Then, consider any platform with at least one CPU and unit
unit execution rate, where...*)
Variable rate: Job -> processor num_cpus -> nat.
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.
(* ...and do not execute in parallel. *)
Hypothesis H_no_parallelism:
jobs_dont_execute_in_parallel sched.
(* In order not to overcount job interference, we assume that
jobs of the same task do not execute in parallel.
Our proof requires a definition of interference based on
the sum of the individual contributions of each job:
I_total = I_j1 + I_j2 + ...
Note that under EDF, this is equivalent to task precedence
constraints. *)
Hypothesis H_no_intra_task_parallelism:
jobs_of_same_task_dont_execute_in_parallel job_task sched.
(* Assume that the schedule satisfies the global scheduling
invariant with EDF priority, i.e., if any job of tsk is
backlogged, every processor must be busy with jobs with
no greater absolute deadline. *)
Let higher_eq_priority :=
@EDF Job arr_seq job_deadline. (* TODO: implicit params seems broken *)
JLFP_JLDP_scheduling_invariant_holds job_cost num_cpus rate 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.
Definition no_deadline_missed_by_job :=
job_misses_no_deadline job_cost job_deadline rate 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
the main Theorem from bertogna_edf_theory.v. *)
Theorem edf_analysis_yields_response_time_bounds :
forall tsk R,
(tsk, R) \In edf_claimed_bounds ts ->
forall j : JobIn arr_seq,
job_task j = tsk ->
completed job_cost rate 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.
unfold edf_rta_iteration in *.
have BOUND := bertogna_cirinei_response_time_bound_edf.
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)
(job_task := job_task) (ts := ts) (tsk := tsk) (rt_bounds := rt_bounds); try (by ins).
by unfold edf_claimed_bounds in SOME; desf; rewrite edf_claimed_bounds_unzip1_iteration.
by ins; apply edf_claimed_bounds_converges with (ts := ts).
by ins; rewrite (edf_claimed_bounds_le_deadline ts rt_bounds).
Qed.
(* Therefore, if the schedulability test suceeds, ...*)
forall tsk, tsk \in ts -> no_deadline_missed_by_task tsk.
Proof.
unfold no_deadline_missed_by_task, task_misses_no_deadline,
job_misses_no_deadline, completed,
edf_schedulable,
valid_sporadic_job in *.
rename H_valid_job_parameters into JOBPARAMS,
H_valid_task_parameters into TASKPARAMS,
H_restricted_deadlines into RESTR,
H_completed_jobs_dont_execute into COMP,
H_jobs_must_arrive_to_execute into MUSTARRIVE,
H_global_scheduling_invariant into INVARIANT,
H_all_jobs_from_taskset into ALLJOBS,
H_test_succeeds into TEST.