bertogna_edf_theory.v 37.2 KB
Newer Older
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1
Require Import rt.util.all.
2
3
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.task_arrival
               rt.model.basic.schedule rt.model.basic.platform rt.model.basic.interference
4
5
6
               rt.model.basic.workload rt.model.basic.schedulability rt.model.basic.priority
               rt.model.basic.platform rt.model.basic.response_time.
Require Import rt.analysis.basic.workload_bound rt.analysis.basic.interference_bound_edf.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
7
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
8
9
10

Module ResponseTimeAnalysisEDF.

11
12
13
  Export Job SporadicTaskset Schedule ScheduleOfSporadicTask Workload Schedulability ResponseTime
         Priority SporadicTaskArrival WorkloadBound InterferenceBoundEDF
         Interference Platform.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
14

15
16
  (* In this section, we prove that Bertogna and Cirinei's RTA yields
     safe response-time bounds. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
17
18
19
  Section ResponseTimeBound.

    Context {sporadic_task: eqType}.
20
21
22
    Variable task_cost: sporadic_task -> time.
    Variable task_period: sporadic_task -> time.
    Variable task_deadline: sporadic_task -> time.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
23
24
    
    Context {Job: eqType}.
25
26
    Variable job_cost: Job -> time.
    Variable job_deadline: Job -> time.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
    Variable job_task: Job -> sporadic_task.
    
    (* Assume any job arrival sequence... *)
    Context {arr_seq: arrival_sequence Job}.

    (* ... in which jobs arrive sporadically and have valid parameters. *)
    Hypothesis H_sporadic_tasks:
      sporadic_task_model task_period arr_seq job_task.
    Hypothesis H_valid_job_parameters:
      forall (j: JobIn arr_seq),
        valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.

    (* Consider any schedule such that...*)
    Variable num_cpus: nat.
    Variable sched: schedule num_cpus arr_seq.

    (* ...jobs do not execute before their arrival times nor longer
       than their execution costs. *)
    Hypothesis H_jobs_must_arrive_to_execute:
      jobs_must_arrive_to_execute sched.
    Hypothesis H_completed_jobs_dont_execute:
48
      completed_jobs_dont_execute job_cost sched.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
49

50
    (* Also assume that jobs are sequential and that
51
       there exists at least one processor. *)
52
    Hypothesis H_sequential_jobs: sequential_jobs sched.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
53
54
55
56
    Hypothesis H_at_least_one_cpu :
      num_cpus > 0.

    (* Assume that we have a task set where all tasks have valid
57
       parameters and constrained deadlines, ... *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
58
59
60
    Variable ts: taskset_of sporadic_task.
    Hypothesis H_valid_task_parameters:
      valid_sporadic_taskset task_cost task_period task_deadline ts.
61
    Hypothesis H_constrained_deadlines:
Felipe Cerqueira's avatar
Felipe Cerqueira committed
62
63
      forall tsk, tsk \in ts -> task_deadline tsk <= task_period tsk.

64
65
66
67
    (* ... and that all jobs in the arrival sequence come from the task set. *)
    Hypothesis H_all_jobs_from_taskset:
      forall (j: JobIn arr_seq), job_task j \in ts.
    
Felipe Cerqueira's avatar
Felipe Cerqueira committed
68
    Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
69
      task_misses_no_deadline job_cost job_deadline job_task sched tsk.
70
    Let response_time_bounded_by (tsk: sporadic_task) :=
71
      is_response_time_bound_of_task job_cost job_task tsk sched.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
72

73
    (* Assume that a response-time bound R is known...  *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
74
    Let task_with_response_time := (sporadic_task * time)%type.
Felix Stutz's avatar
Felix Stutz committed
75
    Variable rt_bounds: seq task_with_response_time.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
76

77
    (* ...for any task in the task set, ... *)
78
    Hypothesis H_rt_bounds_contains_all_tasks: unzip1 rt_bounds = ts.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
79

80
    (* ... such that R is a fixed-point of the response-time recurrence, ... *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
81
82
    Let I (tsk: sporadic_task) (delta: time) :=
      total_interference_bound_edf task_cost task_period task_deadline tsk rt_bounds delta.
Felix Stutz's avatar
Felix Stutz committed
83
84
85
    Hypothesis H_response_time_is_fixed_point :
      forall tsk R,
        (tsk, R) \in rt_bounds ->
Felipe Cerqueira's avatar
Felipe Cerqueira committed
86
        R = task_cost tsk + div_floor (I tsk R) num_cpus.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
87
    
Felipe Cerqueira's avatar
Felipe Cerqueira committed
88
    (* ..., and R is no larger than the deadline. *)
89
    Hypothesis H_tasks_miss_no_deadlines:
Felix Stutz's avatar
Felix Stutz committed
90
91
      forall tsk_other R,
        (tsk_other, R) \in rt_bounds -> R <= task_deadline tsk_other.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
92

93
94
95
    (* Assume that we have a work-conserving EDF scheduler. *)
    Hypothesis H_work_conserving: work_conserving job_cost sched.
    Hypothesis H_edf_policy: enforces_JLDP_policy job_cost sched (EDF job_deadline).
96
    
97
98
99
    (* Assume that the task set has no duplicates. This is required to
       avoid problems when counting tasks (for example, when stating
       that the number of interfering tasks is at most num_cpus). *)
100
    Hypothesis H_ts_is_a_set : uniq ts.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
101

102
103
    (* In order to prove that R is a response-time bound, we first present some lemmas. *)
    Section Lemmas.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
104

105
106
107
108
      (* Let (tsk, R) be any task to be analyzed, with its response-time bound R. *)
      Variable tsk: sporadic_task.
      Variable R: time.
      Hypothesis H_tsk_R_in_rt_bounds: (tsk, R) \in rt_bounds.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
109

110
      (* Consider any job j of tsk ... *)
111
112
      Variable j: JobIn arr_seq.
      Hypothesis H_job_of_tsk: job_task j = tsk.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
113

114
      (* ... that did not complete on time, ... *)
115
      Hypothesis H_j_not_completed: ~~ completed job_cost sched j (job_arrival j + R).
116

117
      (* ... and that is the first job not to satisfy its response-time bound. *)
118
119
120
121
122
      Hypothesis H_all_previous_jobs_completed_on_time :
        forall (j_other: JobIn arr_seq) tsk_other R_other,
          job_task j_other = tsk_other ->
          (tsk_other, R_other) \in rt_bounds ->
          job_arrival j_other + R_other < job_arrival j + R ->
123
          completed job_cost sched j_other (job_arrival j_other + R_other).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
124

125
126
      (* Let's call x the interference incurred by job j due to tsk_other, ...*)
      Let x (tsk_other: sporadic_task) :=
127
128
        task_interference job_cost job_task sched j tsk_other
                          (job_arrival j) (job_arrival j + R).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
129

130
      (* and X the total interference incurred by job j due to any task. *)
131
      Let X := total_interference job_cost sched j (job_arrival j) (job_arrival j + R).
132
133
134
135
136
137
138
139
140
141
142
143
144
145

      (* Recall Bertogna and Cirinei's workload bound ... *)
      Let workload_bound (tsk_other: sporadic_task) (R_other: time) :=
        W task_cost task_period tsk_other R_other R.

      (*... and the EDF-specific bound, ... *)
      Let edf_specific_bound (tsk_other: sporadic_task) (R_other: time) :=
        edf_specific_interference_bound task_cost task_period task_deadline tsk tsk_other R_other.

      (* ... which combined form the interference bound. *)
      Let interference_bound (tsk_other: sporadic_task) (R_other: time) :=
        interference_bound_edf task_cost task_period task_deadline tsk R (tsk_other, R_other). 
      
      (* Also, let ts_interf be the subset of tasks that interfere with tsk. *)
146
      Let ts_interf := [seq tsk_other <- ts | jldp_can_interfere_with tsk tsk_other].
147
148

      Section LemmasAboutInterferingTasks.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
149
        
150
151
152
153
154
155
        (* Let (tsk_other, R_other) be any pair of higher-priority task and
           response-time bound computed in previous iterations. *)
        Variable tsk_other: sporadic_task.
        Variable R_other: time.
        Hypothesis H_response_time_of_tsk_other: (tsk_other, R_other) \in rt_bounds.

156
        (* Note that tsk_other is in the task set, ...*)
157
158
159
160
161
        Lemma bertogna_edf_tsk_other_in_ts: tsk_other \in ts.
        Proof.
          by rewrite -H_rt_bounds_contains_all_tasks; apply/mapP; exists (tsk_other, R_other).
        Qed.

162
        (* ... and R_other is larger than the cost of tsk_other. *)
163
164
165
166
167
168
169
170
171
172
173
174
175
        Lemma bertogna_edf_R_other_ge_cost :
          R_other >= task_cost tsk_other.
        Proof.
          by rewrite [R_other](H_response_time_is_fixed_point tsk_other);
            first by apply leq_addr.
        Qed.

        (* Since tsk_other cannot interfere more than it executes, we show that
           the interference caused by tsk_other is no larger than workload bound W. *)
        Lemma bertogna_edf_workload_bounds_interference :
          x tsk_other <= workload_bound tsk_other R_other.
        Proof.
          unfold valid_sporadic_job in *.
176
          rename H_all_previous_jobs_completed_on_time into BEFOREok,
177
178
                 H_valid_job_parameters into PARAMS,
                 H_valid_task_parameters into TASK_PARAMS,
179
                 H_constrained_deadlines into RESTR,
180
181
182
                 H_tasks_miss_no_deadlines into NOMISS.
          unfold x, task_interference.
          have INts := bertogna_edf_tsk_other_in_ts.
183
          apply leq_trans with (n := workload job_task sched tsk_other
184
                                         (job_arrival j) (job_arrival j + R));
185
            first by apply task_interference_le_workload.
186
187
          by apply workload_bounded_by_W with (task_deadline0 := task_deadline)
               (job_cost0 := job_cost) (job_deadline0 := job_deadline); try (by ins); last 2 first;
188
            [ by apply bertogna_edf_R_other_ge_cost
189
            | by ins; apply NOMISS
190
            | by ins; apply TASK_PARAMS
191
192
            | by ins; apply RESTR
            | by ins; apply BEFOREok with (tsk_other := tsk_other)].
193
194
        Qed.

195
        (* Recall that the edf-specific interference bound also holds for tsk_other. *)
196
197
198
        Lemma bertogna_edf_specific_bound_holds :
          x tsk_other <= edf_specific_bound tsk_other R_other.
        Proof.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
199
200
201
202
203
204
          apply interference_bound_edf_bounds_interference with (job_deadline0 := job_deadline)
                                                                  (ts0 := ts); try (by done);
            [ by apply bertogna_edf_tsk_other_in_ts
            | by apply H_tasks_miss_no_deadlines
            | by apply H_tasks_miss_no_deadlines | ].
          by ins; apply H_all_previous_jobs_completed_on_time with (tsk_other := tsk_other). 
205
        Qed.
206
        
207
      End LemmasAboutInterferingTasks.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
208

209
210
      (* Next we prove some lemmas that help to derive a contradiction.*)
      Section DerivingContradiction.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
211

212
      (* 0) Since job j did not complete by its response time bound, it follows that
213
214
215
216
            the total interference X >= R - e_k + 1. *)
      Lemma bertogna_edf_too_much_interference : X >= R - task_cost tsk + 1.
      Proof.
        rename H_completed_jobs_dont_execute into COMP,
217
218
               H_valid_job_parameters into PARAMS, H_response_time_is_fixed_point into REC,
               H_job_of_tsk into JOBtsk, H_j_not_completed into NOTCOMP.
219
        unfold completed, valid_sporadic_job in *.
220
221
222
223
224
225
226
        unfold X, total_interference; rewrite addn1.
        rewrite -(ltn_add2r (task_cost tsk)).
        rewrite subh1; last by rewrite [R](REC tsk) // leq_addr.
        rewrite -addnBA // subnn addn0.
        move: (NOTCOMP) => /negP NOTCOMP'.
        rewrite neq_ltn in NOTCOMP.
        move: NOTCOMP => /orP [LT | BUG]; last first.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
227
        {
228
229
          exfalso; rewrite ltnNge in BUG; move: BUG => /negP BUG; apply BUG.
          by apply cumulative_service_le_job_cost.
230
        }
231
232
233
        apply leq_ltn_trans with (n := (\sum_(job_arrival j <= t < job_arrival j + R)
                                     backlogged job_cost sched j t) +
                                   service sched j (job_arrival j + R)); last first.
234
        {
235
236
237
          rewrite -addn1 -addnA leq_add2l addn1.
          apply leq_trans with (n := job_cost j); first by done.
          by specialize (PARAMS j); des; rewrite -JOBtsk.
238
        }
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
        unfold service; rewrite service_before_arrival_eq_service_during //.
        rewrite -big_split /=.
        apply leq_trans with (n := \sum_(job_arrival j <= i < job_arrival j + R) 1);
          first by rewrite big_const_nat iter_addn mul1n addn0 addKn.
        rewrite big_nat_cond [\sum_(_ <= _ < _ | true) _]big_nat_cond.
        apply leq_sum; move => i /andP [/andP [GEi LTi] _].
        destruct (backlogged job_cost sched j i) eqn:BACK;
          first by rewrite -addn1 addnC; apply leq_add.
        apply negbT in BACK.
        rewrite add0n lt0n -not_scheduled_no_service negbK.
        rewrite /backlogged negb_and negbK in BACK.
        move: BACK => /orP [/negP NOTPENDING | SCHED]; last by done.
        exfalso; apply NOTPENDING; unfold pending; apply/andP; split; first by done.
        apply/negP; red; intro BUG; apply NOTCOMP'.
        by apply completion_monotonic with (t := i); try (by done); apply ltnW.
254
255
      Qed.

256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
      Let scheduled_task_other_than_tsk (t: time) (tsk_other: sporadic_task) :=
        task_is_scheduled job_task sched tsk_other t &&
        jldp_can_interfere_with tsk tsk_other.
      
      (* 1) At all times that j is backlogged, all processors are busy with other tasks. *)
      Lemma bertogna_edf_scheduling_invariant:
        forall t,
          job_arrival j <= t < job_arrival j + R ->
          backlogged job_cost sched j t ->
          count (scheduled_task_other_than_tsk t) ts = num_cpus.
      Proof.
        rename H_all_jobs_from_taskset into FROMTS,
               H_valid_task_parameters into PARAMS,
               H_job_of_tsk into JOBtsk,
               H_sporadic_tasks into SPO,
               H_tsk_R_in_rt_bounds into INbounds,
               H_all_previous_jobs_completed_on_time into BEFOREok,
               H_tasks_miss_no_deadlines into NOMISS,
               H_rt_bounds_contains_all_tasks into UNZIP,
275
               H_constrained_deadlines into RESTR,
276
277
278
279
280
281
282
283
284
285
               H_work_conserving into WORK.
        unfold x, X, total_interference, task_interference.
        move => t /andP [LEt LTt] BACK.
        unfold scheduled_task_other_than_tsk in *.
        eapply platform_cpus_busy_with_interfering_tasks; try (by done);
          [ by apply WORK | by apply SPO 
          | apply PARAMS; rewrite -JOBtsk; apply FROMTS
          | by apply JOBtsk | by apply BACK | ].
        {
          intros j0 tsk0 TSK0 LE.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
286
287
          cut (tsk0 \in unzip1 rt_bounds = true); last by rewrite UNZIP -TSK0 FROMTS.
          move => /mapP [p IN EQ]; destruct p as [tsk' R0]; simpl in *; subst tsk'.
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
          apply completion_monotonic with (t0 := job_arrival j0 + R0); try (by done).
          {
            rewrite leq_add2l TSK0.
            apply leq_trans with (n := task_deadline tsk0); first by apply NOMISS.
            by apply RESTR; rewrite -TSK0 FROMTS.
          }
          {
            apply BEFOREok with (tsk_other := tsk0); try (by done).
            apply leq_ltn_trans with (n := t); last by done.
            apply leq_trans with (n := job_arrival j0 + task_period tsk0); last by done.
            rewrite leq_add2l; apply leq_trans with (n := task_deadline tsk0); first by apply NOMISS.
            by apply RESTR; rewrite -TSK0 FROMTS.
          }
        }
      Qed.
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356

      (* 2) Prove that during the scheduling window of j, any job that is scheduled while j is
         backlogged comes from a different task. *)
      Lemma bertogna_edf_interference_by_different_tasks :
        forall t j_other,
          job_arrival j <= t < job_arrival j + R ->
          backlogged job_cost sched j t ->
          scheduled sched j_other t ->
          job_task j_other != tsk.
      Proof.
        rename H_all_jobs_from_taskset into FROMTS,
               H_valid_task_parameters into PARAMS,
               H_job_of_tsk into JOBtsk, H_sporadic_tasks into SPO,
               H_work_conserving into WORK,
               H_tsk_R_in_rt_bounds into INbounds,
               H_all_previous_jobs_completed_on_time into BEFOREok,
               H_tasks_miss_no_deadlines into NOMISS,
               H_constrained_deadlines into CONSTR.
        move => t j_other /andP [LEt GEt] BACK SCHED.
        apply/eqP; red; intro SAMEtsk.
        move: SCHED => /existsP [cpu SCHED].
        assert (SCHED': scheduled sched j_other t).
          by apply/existsP; exists cpu.
        clear SCHED; rename SCHED' into SCHED.
        move: (SCHED) => PENDING.
        apply scheduled_implies_pending with (job_cost0 := job_cost) in PENDING; try (by done).
        destruct (ltnP (job_arrival j_other) (job_arrival j)) as [BEFOREother | BEFOREj].
         {
          move: (BEFOREother) => LT; rewrite -(ltn_add2r R) in LT.
          specialize (BEFOREok j_other tsk R SAMEtsk INbounds LT).
          move: PENDING => /andP [_ /negP NOTCOMP]; apply NOTCOMP.
          apply completion_monotonic with (t0 := job_arrival j_other + R); try (by done).
          apply leq_trans with (n := job_arrival j); last by done.
          apply leq_trans with (n := job_arrival j_other + task_deadline tsk);
            first by rewrite leq_add2l; apply NOMISS.
          apply leq_trans with (n := job_arrival j_other + task_period tsk);
            first by rewrite leq_add2l; apply CONSTR; rewrite -JOBtsk FROMTS.
          rewrite -SAMEtsk; apply SPO; [ | by rewrite JOBtsk | by apply ltnW].
          by red; intro EQ; subst; rewrite ltnn in BEFOREother.
        }
        {
          move: PENDING => /andP [ARRIVED _].
          exploit (SPO j j_other); [ | by rewrite SAMEtsk | by done | ]; last first.
          {
            apply/negP; rewrite -ltnNge.
            apply leq_ltn_trans with (n := t); first by done.
            apply leq_trans with (n := job_arrival j + R); first by done.
            by rewrite leq_add2l; apply leq_trans with (n := task_deadline tsk);
              [by apply NOMISS | by rewrite JOBtsk CONSTR // -JOBtsk FROMTS].
          }
          by red; intros EQtsk; subst; rewrite /backlogged SCHED andbF in BACK.
        }
      Qed.

357
      
358
      (* 3) Next, we prove that the sum of the interference of each task is equal
359
360
361
362
363
            to the total interference multiplied by the number of processors. This
            holds because interference only occurs when all processors are busy. *)
      Lemma bertogna_edf_all_cpus_busy :
        \sum_(tsk_k <- ts_interf) x tsk_k = X * num_cpus.
      Proof.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
364
        have DIFFTASK := bertogna_edf_interference_by_different_tasks.
365
        rename H_all_jobs_from_taskset into FROMTS,
366
               H_valid_task_parameters into PARAMS,
367
368
               H_job_of_tsk into JOBtsk, H_sporadic_tasks into SPO,
               H_work_conserving into WORK,
369
370
371
               H_tsk_R_in_rt_bounds into INbounds,
               H_all_previous_jobs_completed_on_time into BEFOREok,
               H_tasks_miss_no_deadlines into NOMISS,
372
               H_rt_bounds_contains_all_tasks into UNZIP,
373
               H_constrained_deadlines into CONSTR.
374
        unfold sporadic_task_model in *.
375
        unfold x, X, total_interference, task_interference.
376
        rewrite -big_mkcond -exchange_big big_distrl /= mul1n.
377
        rewrite [\sum_(_ <= _ < _ | backlogged _ _ _ _) _]big_mkcond.
378
379
        apply eq_big_nat; move => t /andP [GEt LTt].
        destruct (backlogged job_cost sched j t) eqn:BACK; last first.
380
        {
381
382
383
384
          rewrite (eq_bigr (fun i => 0));
            first by rewrite big_const_seq iter_addn mul0n addn0.
          by intros i _; rewrite (eq_bigr (fun i => 0));
            first by rewrite big_const_seq iter_addn mul0n addn0.
385
        }
386
387
388
389
390
391
392
393
394
395
396
397
398
399
        rewrite big_mkcond /=.
        rewrite exchange_big /=.
        apply eq_trans with (y := \sum_(cpu < num_cpus) 1); last by simpl_sum_const.
        apply eq_bigr; intros cpu _.
        move: (WORK j t BACK cpu) => [j_other /eqP SCHED]; unfold scheduled_on in *.
        rewrite (bigD1_seq (job_task j_other)) /=; last by rewrite filter_uniq.
        {
          rewrite (eq_bigr (fun i => 0));
            last by intros i DIFF; rewrite /task_scheduled_on SCHED;apply/eqP;rewrite eqb0 eq_sym.
          rewrite big_const_seq iter_addn mul0n 2!addn0; apply/eqP; rewrite eqb1.
          by unfold task_scheduled_on; rewrite SCHED.
        }
        rewrite mem_filter; apply/andP; split; last by apply FROMTS.
        unfold jldp_can_interfere_with.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
400
        apply DIFFTASK with (t := t); [by auto | by done |].
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
        by apply/existsP; exists cpu; apply/eqP.
      Qed.

      (* 4) Show that by the induction hypothesis, all jobs released
         before the end of the interval complete by their periods. *)
      Lemma bertogna_edf_all_previous_jobs_complete_by_their_period:
        forall t (j0: JobIn arr_seq),
          t < job_arrival j + R ->
          job_arrival j0 + task_period (job_task j0) <= t ->
          completed job_cost sched j0
             (job_arrival j0 + task_period (job_task j0)).
      Proof.
        rename H_rt_bounds_contains_all_tasks into UNZIP,
               H_constrained_deadlines into CONSTR,
               H_tasks_miss_no_deadlines into NOMISS,
               H_all_jobs_from_taskset into FROMTS,
               H_all_previous_jobs_completed_on_time into BEFOREok.
        intros t j0 LEt LE.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
419
420
        cut ((job_task j0) \in unzip1 rt_bounds = true); last by rewrite UNZIP FROMTS.
        move => /mapP [p IN EQ]; destruct p as [tsk' R0]; simpl in *; subst tsk'.
421
422
423
424
425
426
427
428
429
430
        apply completion_monotonic with (t0 := job_arrival j0 + R0); first by done.
        {
          rewrite leq_add2l; apply leq_trans with (n := task_deadline (job_task j0));
            [by apply NOMISS | by apply CONSTR; rewrite FROMTS].
        }
        apply BEFOREok with (tsk_other := (job_task j0)); try by done.
        apply leq_ltn_trans with (n := t); last by done.
        apply leq_trans with (n := job_arrival j0 + task_period (job_task j0)); last by done.
        by rewrite leq_add2l; apply leq_trans with (n := task_deadline (job_task j0));
          [by apply NOMISS | apply CONSTR; rewrite FROMTS].
431
432
433
434
435
436
      Qed.

      (* Let (cardGE delta) be the number of interfering tasks whose interference
         is larger than delta. *)
      Let cardGE (delta: time) := count (fun i => x i >= delta) ts_interf.

437
      (* 5) If there is at least one of such tasks (e.g., cardGE > 0), then the
438
439
440
441
         cumulative interference caused by the complementary set of interfering
         tasks fills at least (num_cpus - cardGE) processors. *)
      Lemma bertogna_edf_helper_lemma :
        forall delta,
442
          0 < cardGE delta < num_cpus ->
443
444
          \sum_(i <- ts_interf | x i < delta) x i >= delta * (num_cpus - cardGE delta).
      Proof.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
445
446
        have COMP := bertogna_edf_all_previous_jobs_complete_by_their_period.
        have INV := bertogna_edf_scheduling_invariant.
447
        rename H_all_jobs_from_taskset into FROMTS,
448
449
450
451
452
453
               H_valid_task_parameters into PARAMS,
               H_job_of_tsk into JOBtsk,
               H_sporadic_tasks into SPO,
               H_tsk_R_in_rt_bounds into INbounds,
               H_all_previous_jobs_completed_on_time into BEFOREok,
               H_tasks_miss_no_deadlines into NOMISS,
454
455
               H_constrained_deadlines into CONSTR,
               H_sequential_jobs into SEQ.
456
        unfold sporadic_task_model in *.
457
458
459
        move => delta /andP [HAS LT]. 
        rewrite -has_count in HAS.

460
        set some_interference_A := fun t =>
461
462
463
          has (fun tsk_k => backlogged job_cost sched j t &&
                            (x tsk_k >= delta) &&
                            task_is_scheduled job_task sched tsk_k t) ts_interf.
464
        set total_interference_B := fun t =>
465
            backlogged job_cost sched j t *
466
            count (fun tsk_k => (x tsk_k < delta) &&
467
                  task_is_scheduled job_task sched tsk_k t) ts_interf.
468
469
470

        apply leq_trans with ((\sum_(job_arrival j <= t < job_arrival j + R)
                              some_interference_A t) * (num_cpus - cardGE delta)).
471
        {
472
473
474
475
          rewrite leq_mul2r; apply/orP; right.
          move: HAS => /hasP HAS; destruct HAS as [tsk_a INa LEa].
          apply leq_trans with (n := x tsk_a); first by apply LEa.
          unfold x, task_interference, some_interference_A.
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
          apply leq_sum_nat; move => t /andP [GEt LTt] _.
          destruct (backlogged job_cost sched j t) eqn:BACK;
            last by rewrite (eq_bigr (fun x => 0)); [by simpl_sum_const | by ins].
          destruct ([exists cpu, task_scheduled_on job_task sched tsk_a cpu t]) eqn:SCHED;
            last first.
          {
            apply negbT in SCHED; rewrite negb_exists in SCHED; move: SCHED => /forallP ALL.
            rewrite (eq_bigr (fun x => 0)); first by simpl_sum_const.
            by intros cpu _; specialize (ALL cpu); apply negbTE in ALL; rewrite ALL.
          }
          move: SCHED => /existsP [cpu SCHED].
          apply leq_trans with (n := 1); last first.
          {
            rewrite lt0b; apply/hasP; exists tsk_a; first by done.
            by rewrite LEa 2!andTb; apply/existsP; exists cpu.
          }
          rewrite (bigD1 cpu) /= // SCHED.
          rewrite (eq_bigr (fun x => 0)); first by simpl_sum_const; rewrite leq_b1.
          intros cpu' DIFF.
          apply/eqP; rewrite eqb0; apply/negP.
          intros SCHED'. 
          move: DIFF => /negP DIFF; apply DIFF; apply/eqP.
          unfold task_scheduled_on in *.
          destruct (sched cpu t) as [j1|] eqn:SCHED1; last by done.
          destruct (sched cpu' t) as [j2|] eqn:SCHED2; last by done.
          move: SCHED SCHED' => /eqP JOB /eqP JOB'.
          subst tsk_a; symmetry in JOB'.
          assert (PENDING1: pending job_cost sched j1 t).
          {
            apply scheduled_implies_pending; try by done.
            by apply/existsP; exists cpu; apply/eqP.
          }
          assert (PENDING2: pending job_cost sched j2 t).
          {
            apply scheduled_implies_pending; try by done.
            by apply/existsP; exists cpu'; apply/eqP.
          }
          assert (BUG: j1 = j2).
          {
            apply platform_at_most_one_pending_job_of_each_task with (task_cost0 := task_cost)
            (task_period0 := task_period) (task_deadline0 := task_deadline) (tsk0 := tsk)
            (job_cost0 := job_cost) (job_task0 := job_task) (sched0 := sched) (j0 := j) (t0 := t);
            rewrite ?JOBtsk ?SAMEtsk //; first by apply PARAMS; rewrite -JOBtsk FROMTS.
            intros j0 tsk0 TSK0 LE.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
520
            by apply (COMP t); rewrite ?TSK0.
521
522
          }
          by subst j2; apply SEQ with (j := j1) (t := t).
523
        }
524

525
526
        apply leq_trans with (\sum_(job_arrival j <= t < job_arrival j + R)
                                   total_interference_B t).
527
        {
528
          rewrite big_distrl /=.
529
          apply leq_sum_nat; move => t LEt _.
530
          unfold some_interference_A, total_interference_B. 
531
          destruct (backlogged job_cost sched j t) eqn:BACK;
532
533
            [rewrite mul1n /= | by rewrite has_pred0 //].
          
534
535
536
          destruct (has (fun tsk_k : sporadic_task => (delta <= x tsk_k) &&
                     task_is_scheduled job_task sched tsk_k t) ts_interf) eqn:HAS';
            last by done.
537
          rewrite mul1n; move: HAS => /hasP [tsk_k INk LEk].
538
539
540
541
          unfold cardGE.
          apply leq_trans with (n := num_cpus -
                       count (fun i => (x i >= delta) &&
                          task_is_scheduled job_task sched i t) ts_interf).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
542
          {
543
544
545
546
            apply leq_sub2l.
            rewrite -2!sum1_count big_mkcond /=.
            rewrite [\sum_(_ <- _ | _ <= _)_]big_mkcond /=.
            apply leq_sum; intros i _.
547
            by destruct (task_is_scheduled job_task sched i t);
548
              [by rewrite andbT | by rewrite andbF].
Felipe Cerqueira's avatar
Felipe Cerqueira committed
549
          }
550
551
552
553
          rewrite -count_filter -[count _ ts_interf]count_filter.
          eapply leq_trans with (n := count (predC (fun tsk => delta <= x tsk)) _);
            last by apply eq_leq, eq_in_count; red; ins; rewrite ltnNge.
          rewrite leq_subLR count_predC size_filter.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
554
555
          by apply leq_trans with (n := count (scheduled_task_other_than_tsk t) ts);
            [by rewrite INV | by rewrite count_filter].
556
        }
Felipe Cerqueira's avatar
Felipe Cerqueira committed
557
        {
558
559
560
561
562
563
564
565
566
567
          unfold x at 2, total_interference_B.
          rewrite exchange_big /=; apply leq_sum; intros t _.
          destruct (backlogged job_cost sched j t) eqn:BACK; last by ins.
          rewrite mul1n -sum1_count.
          rewrite big_mkcond [\sum_(i <- ts_interf | _ < _) _]big_mkcond /=.
          apply leq_sum_seq; move => tsk_k IN _.
          destruct (x tsk_k < delta); [rewrite andTb | by rewrite andFb].
          destruct (task_is_scheduled job_task sched tsk_k t) eqn:SCHED; last by done.
          move: SCHED => /existsP [cpu SCHED].
          by rewrite (bigD1 cpu) /= // SCHED.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
568
        }
569
570
      Qed.

571
      (* 6) Next, we prove that, for any interval delta, if the sum of per-task
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
            interference exceeds delta * num_cpus, the same applies for the
            sum of the minimum between the interference and delta. *)
      Lemma bertogna_edf_minimum_exceeds_interference :
        forall delta,
          \sum_(tsk_k <- ts_interf) x tsk_k >= delta * num_cpus ->
             \sum_(tsk_k <- ts_interf) minn (x tsk_k) delta >=
             delta * num_cpus.
      Proof.
        intros delta SUMLESS.
        set more_interf := fun tsk_k => x tsk_k >= delta.
        rewrite [\sum_(_ <- _) minn _ _](bigID more_interf) /=.
        unfold more_interf, minn.
        rewrite [\sum_(_ <- _ | delta <= _)_](eq_bigr (fun i => delta));
          last by intros i COND; rewrite leqNgt in COND; destruct (delta > x i).
        rewrite [\sum_(_ <- _ | ~~_)_](eq_big (fun i => x i < delta)
                                              (fun i => x i));
          [| by red; ins; rewrite ltnNge
           | by intros i COND; rewrite -ltnNge in COND; rewrite COND].

        (* Case 1: cardGE = 0 *)
        destruct (~~ has (fun i => delta <= x i) ts_interf) eqn:HASa.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
593
        {
594
595
596
597
598
599
600
          rewrite [\sum_(_ <- _ | _ <= _) _]big_hasC; last by apply HASa.
          rewrite big_seq_cond; move: HASa => /hasPn HASa.
          rewrite add0n (eq_bigl (fun i => (i \in ts_interf) && true));
            last by red; intros tsk_k; destruct (tsk_k \in ts_interf) eqn:INk;
              [by rewrite andTb ltnNge; apply HASa | by rewrite andFb].
          by rewrite -big_seq_cond.
        } apply negbFE in HASa.
Felix Stutz's avatar
Felix Stutz committed
601
        
602
603
        (* Case 2: cardGE >= num_cpus *)
        destruct (cardGE delta >= num_cpus) eqn:CARD.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
604
        {
605
606
607
608
609
610
611
612
613
614
615
616
          apply leq_trans with (delta * cardGE delta);
            first by rewrite leq_mul2l; apply/orP; right.
          unfold cardGE; rewrite -sum1_count big_distrr /=.
          rewrite -[\sum_(_ <- _ | _) _]addn0.
          by apply leq_add; [by apply leq_sum; ins; rewrite muln1|by ins].
        } apply negbT in CARD; rewrite -ltnNge in CARD.

        (* Case 3: cardGE < num_cpus *)
        rewrite big_const_seq iter_addn addn0; fold cardGE.
        apply leq_trans with (n := delta * cardGE delta +
                                   delta * (num_cpus - cardGE delta));
          first by rewrite -mulnDr subnKC //; apply ltnW.
617
618
        by rewrite leq_add2l; apply bertogna_edf_helper_lemma; apply/andP; split;
          first by rewrite -has_count.
619
620
      Qed.

621
      (* 7) Now, we prove that the Bertogna's interference bound
622
623
624
            is not enough to cover the sum of the "minimum" term over
            all tasks (artifact of the proof by contradiction). *)
      Lemma bertogna_edf_sum_exceeds_total_interference:
625
        \sum_((tsk_other, R_other) <- rt_bounds | jldp_can_interfere_with tsk tsk_other)
626
627
          minn (x tsk_other) (R - task_cost tsk + 1) > I tsk R.
      Proof.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
628
629
630
631
        have GE_COST := bertogna_edf_R_other_ge_cost.
        have EXCEEDS := bertogna_edf_minimum_exceeds_interference.
        have ALLBUSY := bertogna_edf_all_cpus_busy.
        have TOOMUCH := bertogna_edf_too_much_interference.
632
633
634
635
        rename H_rt_bounds_contains_all_tasks into UNZIP,
          H_response_time_is_fixed_point into REC.
        apply leq_trans with (n := \sum_(tsk_other <- ts_interf) minn (x tsk_other) (R - task_cost tsk + 1));
          last first.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
636
        {
637
638
639
          rewrite (eq_bigr (fun i => minn (x (fst i)) (R - task_cost tsk + 1)));
            last by ins; destruct i.
          move: UNZIP => UNZIP.
640
641
          assert (FILTER: filter (jldp_can_interfere_with tsk) (unzip1 rt_bounds) =
                          filter (jldp_can_interfere_with tsk) ts).
642
643
644
645
646
            by f_equal.
          unfold ts_interf; rewrite -FILTER; clear FILTER.
          rewrite -[\sum_(_ <- rt_bounds | _)_]big_filter.
          assert (SUBST: [seq i <- rt_bounds
                 | let '(tsk_other, _) := i in
647
648
                        jldp_can_interfere_with tsk tsk_other] = [seq i <- rt_bounds
                           | jldp_can_interfere_with tsk (fst i)]).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
649
          {
650
651
652
653
            by apply eq_filter; red; intro i; destruct i.
          } rewrite SUBST; clear SUBST.         
          have MAP := big_map (fun x => fst x) (fun i => true) (fun i => minn (x i) (R - task_cost tsk + 1)).
          by rewrite -MAP; apply eq_leq; f_equal; rewrite filter_map.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
654
        }
655
656
657
658
659
660
        
        apply ltn_div_trunc with (d := num_cpus); first by apply H_at_least_one_cpu.
        rewrite -(ltn_add2l (task_cost tsk)) -REC; last by done.
        rewrite -addn1 -leq_subLR.
        rewrite -[R + 1 - _]subh1; last by apply GE_COST.
        rewrite leq_divRL; last by apply H_at_least_one_cpu.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
661
        apply EXCEEDS.
662
        apply leq_trans with (n := X * num_cpus);
Felipe Cerqueira's avatar
Felipe Cerqueira committed
663
664
          last by rewrite ALLBUSY.
        by rewrite leq_mul2r; apply/orP; right; apply TOOMUCH.
665
666
      Qed.

667
      (* 8) After concluding that the sum of the minimum exceeds (R - e_i + 1),
668
669
670
671
672
673
674
            we prove that there exists a tuple (tsk_k, R_k) such that
            min (x_k, R - e_i + 1) > min (W_k, edf_bound, R - e_i + 1). *)
      Lemma bertogna_edf_exists_task_that_exceeds_bound :
        exists tsk_other R_other,
          (tsk_other, R_other) \in rt_bounds /\
          (minn (x tsk_other) (R - task_cost tsk + 1) > interference_bound tsk_other R_other).
      Proof.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
675
676
677
        have SUM := bertogna_edf_sum_exceeds_total_interference.
        have BOUND := bertogna_edf_workload_bounds_interference.
        have EDFBOUND := bertogna_edf_specific_bound_holds.
678
679
680
        rename H_rt_bounds_contains_all_tasks into UNZIP.
        assert (HAS: has (fun tup : task_with_response_time =>
                            let (tsk_other, R_other) := tup in
681
                            (tsk_other \in ts) && jldp_can_interfere_with tsk tsk_other &&
682
683
684
                              (minn (x tsk_other) (R - task_cost tsk + 1)  >
                              interference_bound tsk_other R_other))
                         rt_bounds).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
685
        {
686
          apply/negP; unfold not; intro NOTHAS.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
687
688
689
          move: NOTHAS => /negP /hasPn ALL.
          rewrite -[_ < _]negbK in SUM.
          move: SUM => /negP SUM; apply SUM; rewrite -leqNgt.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
690
          unfold I, total_interference_bound_edf.
691
692
          rewrite big_seq_cond [\sum_(_ <- _ | let _ := _ in _)_]big_seq_cond.
          apply leq_sum; move => tsk_k /andP [INBOUNDSk INTERFk]; destruct tsk_k as [tsk_k R_k].
Felipe Cerqueira's avatar
Felipe Cerqueira committed
693
          specialize (ALL (tsk_k, R_k) INBOUNDSk).
694
          unfold interference_bound_edf; simpl in *.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
695
696
697
698
699
          rewrite leq_min; apply/andP; split.
          {
            unfold interference_bound; rewrite leq_min; apply/andP; split;
              last by rewrite geq_minr.
            apply leq_trans with (n := x tsk_k); first by rewrite geq_minl.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
700
            by apply BOUND.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
701
702
          }
          {
Felipe Cerqueira's avatar
Felipe Cerqueira committed
703
            apply leq_trans with (n := x tsk_k); first by rewrite geq_minl.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
704
            by apply EDFBOUND.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
705
          }
Felipe Cerqueira's avatar
Felipe Cerqueira committed
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
        move: HAS => /hasP HAS; destruct HAS as [[tsk_k R_k] HPk MIN].
        move: MIN => /andP [/andP [INts INTERFk] MINk].
        by exists tsk_k, R_k; repeat split.
      Qed.

      End DerivingContradiction.
      
    End Lemmas.

    Section MainProof.
      
      (* Let (tsk, R) be any task to be analyzed, with its response-time bound R. *)
      Variable tsk: sporadic_task.
      Variable R: time.
      Hypothesis H_tsk_R_in_rt_bounds: (tsk, R) \in rt_bounds.

      (* Using the lemmas above, we prove that R bounds the response time of task tsk. *)
      Theorem bertogna_cirinei_response_time_bound_edf :
        response_time_bounded_by tsk R.
      Proof.
        intros j JOBtsk.
       
        (* First, rewrite the claim in terms of the *absolute* response-time bound (arrival + R) *)
        remember (job_arrival j + R) as ctime.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
731

732
733
734
735
        revert H_tsk_R_in_rt_bounds.
        generalize dependent R; generalize dependent tsk; generalize dependent j.
      
        (* Now, we apply strong induction on the absolute response-time bound. *)
736
        induction ctime as [ctime IH] using strong_ind.
737
738
739
740
741
742
743
744

        intros j tsk' JOBtsk R' EQc INbounds; subst ctime.

        (* First, let's simplify the induction hypothesis. *)
        assert (BEFOREok: forall (j0: JobIn arr_seq) tsk R0,
                                 job_task j0 = tsk ->
                               (tsk, R0) \in rt_bounds ->
                               job_arrival j0 + R0 < job_arrival j + R' ->
745
                               service sched j0 (job_arrival j0 + R0) == job_cost j0).
746
747
748
749
750
751
752
753
        {
            by ins; apply IH with (tsk := tsk0) (R := R0).
        }
        clear IH.
        
        (* 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. *)
754
        destruct (completed job_cost sched j (job_arrival j + R')) eqn:NOTCOMP;
755
756
757
758
759
760
761
762
763
          first by done.
        apply negbT in NOTCOMP; exfalso.
        
        (* Next, we derive a contradiction using the previous lemmas. *)
        exploit (bertogna_edf_exists_task_that_exceeds_bound tsk' R' INbounds j JOBtsk NOTCOMP).
        {
          by ins; apply IH with (tsk := tsk_other) (R := R_other).
        } 
        intro EX; destruct EX as [tsk_other [R_other [HP LTmin]]].
764
        unfold interference_bound_edf, interference_bound_generic in LTmin.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
765
        rewrite minnAC in LTmin; apply min_lt_same in LTmin.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
766
767
768
        have BASICBOUND := bertogna_edf_workload_bounds_interference R' j BEFOREok tsk_other R_other HP.
        have EDFBOUND := (bertogna_edf_specific_bound_holds tsk' R' INbounds j JOBtsk BEFOREok tsk_other R_other HP).
        unfold minn in LTmin; clear -LTmin HP BASICBOUND EDFBOUND tsk; desf.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
769
        {
Felipe Cerqueira's avatar
Felipe Cerqueira committed
770
          by apply (leq_ltn_trans BASICBOUND) in LTmin; rewrite ltnn in LTmin. 
Felipe Cerqueira's avatar
Felipe Cerqueira committed
771
772
        }
        {
Felipe Cerqueira's avatar
Felipe Cerqueira committed
773
          by apply (leq_ltn_trans EDFBOUND) in LTmin; rewrite ltnn in LTmin.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
774
        }
775
      Qed.
Felix Stutz's avatar
Felix Stutz committed
776

777
778
    End MainProof.
    
Felipe Cerqueira's avatar
Felipe Cerqueira committed
779
780
  End ResponseTimeBound.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
781
End ResponseTimeAnalysisEDF.