bertogna_edf_theory.v 30.9 KB
Newer Older
1 2 3 4
Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
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
5 6 7
               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.
8
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
9 10 11

Module ResponseTimeAnalysisEDF.

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

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

    Context {sporadic_task: eqType}.
21 22 23
    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
24 25
    
    Context {Job: eqType}.
26 27
    Variable job_cost: Job -> time.
    Variable job_deadline: Job -> time.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48
    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:
49
      completed_jobs_dont_execute job_cost sched.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
50

51 52
    (* Also assume that jobs do not execute in parallel and that
       there exists at least one processor. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
53 54 55 56 57 58
    Hypothesis H_no_parallelism:
      jobs_dont_execute_in_parallel sched.
    Hypothesis H_at_least_one_cpu :
      num_cpus > 0.

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

66 67 68 69
    (* ... 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
70
    Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
71
      task_misses_no_deadline job_cost job_deadline job_task sched tsk.
72
    Let response_time_bounded_by (tsk: sporadic_task) :=
73
      is_response_time_bound_of_task job_cost job_task tsk sched.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
74

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

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

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

95 96 97
    (* 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).
98
    
99 100 101
    (* 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). *)
102
    Hypothesis H_ts_is_a_set : uniq ts.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
103

104 105
    (* 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
106

107 108 109 110
      (* 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
111

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

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

119
      (* ... and that is the first job not to satisfy its response-time bound. *)
120 121 122 123 124
      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 ->
125
          completed job_cost sched j_other (job_arrival j_other + R_other).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
126

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

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

      (* 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. *)
148
      Let ts_interf := [seq tsk_other <- ts | jldp_can_interfere_with tsk tsk_other].
149 150

      Section LemmasAboutInterferingTasks.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
151
        
152 153 154 155 156 157
        (* 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.

158
        (* Note that tsk_other is in the task set, ...*)
159 160 161 162 163
        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.

164
        (* ... and R_other is larger than the cost of tsk_other. *)
165 166 167 168 169 170 171 172 173 174 175 176 177
        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 *.
178
          rename H_all_previous_jobs_completed_on_time into BEFOREok,
179 180 181 182 183 184
                 H_valid_job_parameters into PARAMS,
                 H_valid_task_parameters into TASK_PARAMS,
                 H_restricted_deadlines into RESTR,
                 H_tasks_miss_no_deadlines into NOMISS.
          unfold x, task_interference.
          have INts := bertogna_edf_tsk_other_in_ts.
185
          apply leq_trans with (n := workload job_task sched tsk_other
186
                                         (job_arrival j) (job_arrival j + R));
187
            first by apply task_interference_seq_le_workload.
188 189
          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;
190
            [ by apply bertogna_edf_R_other_ge_cost
191
            | by ins; apply NOMISS
192
            | by ins; apply TASK_PARAMS
193 194
            | by ins; apply RESTR
            | by ins; apply BEFOREok with (tsk_other := tsk_other)].
195 196
        Qed.

197
        (* Recall that the edf-specific interference bound also holds for tsk_other. *)
198 199 200
        Lemma bertogna_edf_specific_bound_holds :
          x tsk_other <= edf_specific_bound tsk_other R_other.
        Proof.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
201 202 203 204 205 206
          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). 
207
        Qed.
208
        
209
      End LemmasAboutInterferingTasks.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
210

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

214
      (* 0) Since job j did not complete by its response time bound, it follows that
215 216 217 218 219 220 221 222
            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,
               H_valid_job_parameters into PARAMS,
               H_job_of_tsk into JOBtsk,
               H_j_not_completed into NOTCOMP.
        unfold completed, valid_sporadic_job in *.
223

224 225
        (* Since j has not completed, recall the time when it is not
         executing is the total interference. *)
226
        exploit (complement_of_interf_equals_service job_cost sched j (job_arrival j)
227 228 229 230 231 232
                                                                      (job_arrival j + R));
          last intro EQinterf; ins; unfold has_arrived; first by apply leqnn.
        rewrite {2}[_ + R]addnC -addnBA // subnn addn0 in EQinterf.
        rewrite addn1.
        move: NOTCOMP; rewrite neq_ltn; move => /orP NOTCOMP; des;
          last first.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
233
        {
234 235
          apply (leq_ltn_trans (COMP j (job_arrival j + R))) in NOTCOMP.
          by rewrite ltnn in NOTCOMP.
236
        }
237
        apply leq_trans with (n := R - service sched j (job_arrival j + R)); last first.
238
        {
239 240
          unfold service; rewrite service_before_arrival_eq_service_during; ins.
          rewrite EQinterf subKn; first by done.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
241
          {
242 243 244 245
            unfold total_interference.
            rewrite -{1}[_ j]add0n big_addn addnC -addnBA // subnn addn0.
            rewrite -{2}[R]subn0 -[R-_]mul1n -[1*_]addn0 -iter_addn.
            by rewrite -big_const_nat leq_sum //; ins; apply leq_b1.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
246
          }
247
        }
248
        {
249
          apply ltn_sub2l; last first.
250
          {
251 252
            apply leq_trans with (n := job_cost j); first by ins.
            rewrite -JOBtsk; specialize (PARAMS j); des; apply PARAMS0.
253
          }
254 255 256 257
          apply leq_trans with (n := job_cost j); first by ins.
          apply leq_trans with (n := task_cost tsk);
            first by rewrite -JOBtsk; specialize (PARAMS j); des; apply PARAMS0.
          by rewrite bertogna_edf_R_other_ge_cost.
258
        }
259 260
      Qed.

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 297 298 299 300 301 302 303 304 305 306 307 308
      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,
               H_restricted_deadlines into RESTR,
               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.
          cut (tsk0 \in unzip1 rt_bounds); [intro IN | by rewrite UNZIP -TSK0 FROMTS].
          move: IN => /mapP [p IN EQ]; destruct p as [tsk' R0]; simpl in *; subst tsk'.
          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.
      
309 310 311 312 313 314
      (* 2) Next, we prove that the sum of the interference of each task is equal
            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.
315
        rename H_all_jobs_from_taskset into FROMTS,
316 317 318 319 320 321
               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,
322
               H_rt_bounds_contains_all_tasks into UNZIP,
323 324
               H_restricted_deadlines into RESTR.
        unfold sporadic_task_model in *.
325 326
        unfold x, X, total_interference, task_interference.
        rewrite -big_mkcond -exchange_big big_distrl /=.
327
        rewrite [\sum_(_ <= _ < _ | backlogged _ _ _ _) _]big_mkcond.
328
        apply eq_big_nat; move => t LEt.
329
        destruct (backlogged job_cost sched j t) eqn:BACK;
330 331 332 333
          last by rewrite (eq_bigr (fun i => 0));
            [by rewrite big_const_seq iter_addn mul0n addn0 | by done].
        rewrite big_mkcond mul1n /=.
        rewrite big_filter big_mkcond.
334 335
        rewrite (eq_bigr (fun i => if (scheduled_task_other_than_tsk t i) then 1 else 0));
          last first.
336
        {
337 338
          unfold scheduled_task_other_than_tsk; intros i _; clear -i.
          by destruct (task_is_scheduled job_task sched i t); rewrite ?andFb ?andTb ?andbT //; desf.
339
        }
340 341
        rewrite -big_mkcond sum1_count.
        by apply bertogna_edf_scheduling_invariant.
342 343 344 345 346 347 348 349 350 351 352 353 354 355
      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.

      (* 3) If there is at least one of such tasks (e.g., cardGE > 0), then the
         cumulative interference caused by the complementary set of interfering
         tasks fills at least (num_cpus - cardGE) processors. *)
      Lemma bertogna_edf_helper_lemma :
        forall delta,
          cardGE delta > 0 ->
          \sum_(i <- ts_interf | x i < delta) x i >= delta * (num_cpus - cardGE delta).
      Proof.
356
        rename H_all_jobs_from_taskset into FROMTS,
357 358 359 360 361 362 363 364
               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_restricted_deadlines into RESTR.
        unfold sporadic_task_model in *.
365 366
        intros delta HAS.
        set some_interference_A := fun t =>
367
            backlogged job_cost sched j t &&
368 369 370
            has (fun tsk_k => ((x tsk_k >= delta) &&
                     task_is_scheduled job_task sched tsk_k t)) ts_interf.      
        set total_interference_B := fun t =>
371
            backlogged job_cost sched j t *
372 373 374 375 376 377
            count (fun tsk_k => (x tsk_k < delta) &&
              task_is_scheduled job_task sched tsk_k t) ts_interf.

        rewrite -has_count in HAS.
        apply leq_trans with ((\sum_(job_arrival j <= t < job_arrival j + R)
                              some_interference_A t) * (num_cpus - cardGE delta)).
378
        {
379 380 381 382 383
          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.
          apply leq_sum; ins.
384
          destruct (backlogged job_cost sched j i);
385 386 387 388 389
            [rewrite 2!andTb | by ins].
          destruct (task_is_scheduled job_task sched tsk_a i) eqn:SCHEDa;
            [apply eq_leq; symmetry | by ins].
          apply/eqP; rewrite eqb1.
          by apply/hasP; exists tsk_a; last by apply/andP.
390
        }
391 392
        apply leq_trans with (\sum_(job_arrival j <= t < job_arrival j + R)
                                   total_interference_B t).
393
        {
394
          rewrite big_distrl /=.
395 396
          rewrite big_nat_cond [\sum_(_ <= _ < _ | true)_]big_nat_cond.
          apply leq_sum; move => t /andP [LEt _].
397
          unfold some_interference_A, total_interference_B. 
398
          destruct (backlogged job_cost sched j t) eqn:BACK;
399 400 401 402 403 404
            [rewrite andTb mul1n | by done].
          destruct (has (fun tsk_k : sporadic_task => (delta <= x tsk_k) &&
                     task_is_scheduled job_task sched tsk_k t) ts_interf) eqn:HAS';
            last by done.
          rewrite mul1n; move: HAS => /hasP HAS.
          destruct HAS as [tsk_k INk LEk].
405

406 407
          have COUNT := bertogna_edf_scheduling_invariant t LEt BACK.
               
408 409 410 411 412 413 414 415 416 417 418
          unfold cardGE.
          set interfering_tasks_at_t :=
            [seq tsk_k <- ts_interf | task_is_scheduled job_task
                                                        sched tsk_k t].

          rewrite -(count_filter (fun i => true)) in COUNT.
          fold interfering_tasks_at_t in COUNT.
          rewrite count_predT in COUNT.
          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
419
          {
420 421 422 423 424 425
            apply leq_sub2l.
            rewrite -2!sum1_count big_mkcond /=.
            rewrite [\sum_(_ <- _ | _ <= _)_]big_mkcond /=.
            apply leq_sum; intros i _.
            destruct (task_is_scheduled job_task sched i t);
              [by rewrite andbT | by rewrite andbF].
Felipe Cerqueira's avatar
Felipe Cerqueira committed
426
          }
Felipe Cerqueira's avatar
Felipe Cerqueira committed
427

428 429 430 431 432 433 434 435 436 437
          rewrite leq_subLR -count_predUI.
          apply leq_trans with (n :=
              count (predU (fun i : sporadic_task =>
                              (delta <= x i) &&
                              task_is_scheduled job_task sched i t)
                           (fun tsk_k0 : sporadic_task =>
                              (x tsk_k0 < delta) &&
                              task_is_scheduled job_task sched tsk_k0 t))
                    ts_interf); last by apply leq_addr.
          apply leq_trans with (n := size interfering_tasks_at_t).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
438
          {
439 440 441 442 443
            rewrite -COUNT.
            rewrite leq_eqVlt; apply/orP; left; apply/eqP; f_equal.
            unfold interfering_tasks_at_t.
            rewrite -filter_predI; apply eq_filter; red; simpl.
            by intros i; rewrite andbC.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
444
          }
445 446 447 448 449 450 451 452
          unfold interfering_tasks_at_t.
          rewrite -count_predT count_filter.
          rewrite leq_eqVlt; apply/orP; left; apply/eqP.
          apply eq_count; red; simpl.
          intros i.
          destruct (task_is_scheduled job_task sched i t);
            rewrite 3?andTb ?andFb ?andbF ?andbT /=; try ins.
          by rewrite leqNgt orNb. 
453
        }
Felipe Cerqueira's avatar
Felipe Cerqueira committed
454
        {
455 456 457
            unfold x at 2, task_interference.
            rewrite exchange_big /=; apply leq_sum; intros t _.
            unfold total_interference_B.
458
            destruct (backlogged job_cost sched j t); last by ins.
459 460 461
            rewrite mul1n -sum1_count.
            rewrite big_seq_cond big_mkcond [\sum_(i <- ts_interf | _ < _) _]big_mkcond.
            by apply leq_sum; ins; clear -i; desf; des; rewrite ?Heq2.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
462
        }
463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486
      Qed.

      (* 4) Next, we prove that, for any interval delta, if the sum of per-task
            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
487
        {
488 489 490 491 492 493 494
          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
495
        
496 497
        (* Case 2: cardGE >= num_cpus *)
        destruct (cardGE delta >= num_cpus) eqn:CARD.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
498
        {
499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517
          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.
        by rewrite leq_add2l; apply bertogna_edf_helper_lemma; rewrite -has_count.
      Qed.

      (* 5) Now, we prove that the Bertogna's interference bound
            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:
518
        \sum_((tsk_other, R_other) <- rt_bounds | jldp_can_interfere_with tsk tsk_other)
519 520 521 522 523 524 525
          minn (x tsk_other) (R - task_cost tsk + 1) > I tsk R.
      Proof.
        rename H_rt_bounds_contains_all_tasks into UNZIP,
          H_response_time_is_fixed_point into REC.
        have GE_COST := bertogna_edf_R_other_ge_cost.
        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
526
        {
527 528 529
          rewrite (eq_bigr (fun i => minn (x (fst i)) (R - task_cost tsk + 1)));
            last by ins; destruct i.
          move: UNZIP => UNZIP.
530 531
          assert (FILTER: filter (jldp_can_interfere_with tsk) (unzip1 rt_bounds) =
                          filter (jldp_can_interfere_with tsk) ts).
532 533 534 535 536
            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
537 538
                        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
539
          {
540 541 542 543
            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
544
        }
545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568
        
        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.
        apply bertogna_edf_minimum_exceeds_interference.
        apply leq_trans with (n := X * num_cpus);
          last by rewrite bertogna_edf_all_cpus_busy.
        rewrite leq_mul2r; apply/orP; right.
        by apply bertogna_edf_too_much_interference.
      Qed.

      (* 6) After concluding that the sum of the minimum exceeds (R - e_i + 1),
            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.
        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
569
                            (tsk_other \in ts) && jldp_can_interfere_with tsk tsk_other &&
570 571 572
                              (minn (x tsk_other) (R - task_cost tsk + 1)  >
                              interference_bound tsk_other R_other))
                         rt_bounds).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
573
        {
574
          apply/negP; unfold not; intro NOTHAS.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
575
          move: NOTHAS => /negP /hasPn ALL.
576
          have SUM := bertogna_edf_sum_exceeds_total_interference.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
577 578
          rewrite -[_ < _]negbK in SUM.
          move: SUM => /negP SUM; apply SUM; rewrite -leqNgt.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
579
          unfold I, total_interference_bound_edf.
580 581
          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
582
          specialize (ALL (tsk_k, R_k) INBOUNDSk).
583
          unfold interference_bound_edf; simpl in *.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
584 585 586 587 588
          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.
589
            by apply bertogna_edf_workload_bounds_interference.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
590 591
          }
          {
Felipe Cerqueira's avatar
Felipe Cerqueira committed
592
            apply leq_trans with (n := x tsk_k); first by rewrite geq_minl.
593
            by apply bertogna_edf_specific_bound_holds.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
594
          }
Felipe Cerqueira's avatar
Felipe Cerqueira committed
595
        }
596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619
        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
620

621 622 623 624
        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. *)
625
        induction ctime as [ctime IH] using strong_ind.
626 627 628 629 630 631 632 633

        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' ->
634
                               service sched j0 (job_arrival j0 + R0) == job_cost j0).
635 636 637 638 639 640 641 642
        {
            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. *)
643
        destruct (completed job_cost sched j (job_arrival j + R')) eqn:NOTCOMP;
644 645 646 647 648 649 650 651 652
          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]]].
653
        unfold interference_bound_edf, interference_bound_generic in LTmin.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
654
        rewrite minnAC in LTmin; apply min_lt_same in LTmin.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
655 656 657
        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
658
        {
Felipe Cerqueira's avatar
Felipe Cerqueira committed
659
          by apply (leq_ltn_trans BASICBOUND) in LTmin; rewrite ltnn in LTmin. 
Felipe Cerqueira's avatar
Felipe Cerqueira committed
660 661
        }
        {
Felipe Cerqueira's avatar
Felipe Cerqueira committed
662
          by apply (leq_ltn_trans EDFBOUND) in LTmin; rewrite ltnn in LTmin.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
663
        }
664
      Qed.
Felix Stutz's avatar
Felix Stutz committed
665

666 667
    End MainProof.
    
Felipe Cerqueira's avatar
Felipe Cerqueira committed
668 669
  End ResponseTimeBound.

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