interference_bound_edf.v 61.1 KB
Newer Older
1 2
Add LoadPath "../../" as rt.
Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
3
Require Import rt.model.jitter.job rt.model.jitter.task rt.model.jitter.task_arrival
4 5 6
               rt.model.jitter.schedule rt.model.jitter.platform rt.model.jitter.response_time
               rt.model.jitter.priority rt.model.jitter.workload rt.model.jitter.schedulability
               rt.model.jitter.interference rt.model.jitter.interference_edf.
7
Require Import rt.analysis.jitter.workload_bound rt.analysis.jitter.interference_bound.
8 9 10 11 12 13 14 15 16 17 18
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.

Module InterferenceBoundEDFJitter.

  Import JobWithJitter SporadicTaskset ScheduleWithJitter ScheduleOfSporadicTask Schedulability
         ResponseTime WorkloadBoundJitter Priority SporadicTaskArrival Interference InterferenceEDF.
  Export InterferenceBoundJitter.

  (* In this section, we define Bertogna and Cirinei's EDF-specific
     interference bound. *)
  Section SpecificBoundDef.
19 20 21 22 23
    
    Context {sporadic_task: eqType}.
    Variable task_cost: sporadic_task -> nat.
    Variable task_period: sporadic_task -> nat.
    Variable task_deadline: sporadic_task -> nat.
24
    Variable task_jitter: sporadic_task -> nat.
25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42
    
    (* Let tsk be the task to be analyzed. *)
    Variable tsk: sporadic_task.

    (* Consider the interference incurred by tsk in a window of length delta... *)
    Variable delta: time.

    (* due to a different task tsk_other, with response-time bound R_other. *)
    Variable tsk_other: sporadic_task.
    Variable R_other: time.

    (* Bertogna and Cirinei define the following bound for task interference
       under EDF scheduling. *)
    Definition edf_specific_interference_bound :=
      let d_tsk := task_deadline tsk in
      let e_other := task_cost tsk_other in
      let p_other := task_period tsk_other in
      let d_other := task_deadline tsk_other in
43
      let j_other := task_jitter tsk_other in
44
        (div_floor d_tsk p_other) * e_other +
45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88
        minn e_other ((d_tsk %% p_other) - (d_other - R_other - j_other)).

  End SpecificBoundDef.

  (* Next, we define the total interference bound for EDF, which combines the generic
     and the EDF-specific bounds. *)
  Section TotalInterferenceBoundEDF.

    Context {sporadic_task: eqType}.
    Variable task_cost: sporadic_task -> nat.
    Variable task_period: sporadic_task -> nat.
    Variable task_deadline: sporadic_task -> nat.
    Variable task_jitter: sporadic_task -> nat.
    
    (* Let tsk be the task to be analyzed. *)
    Variable tsk: sporadic_task.

    Let task_with_response_time := (sporadic_task * time)%type.
    
    (* Assume a known response-time bound for each interfering task ... *)
    Variable R_prev: seq task_with_response_time.

    (* ... and an interval length delta. *)
    Variable delta: time.

    Section PerTask.

      Variable tsk_R: task_with_response_time.
      Let tsk_other := fst tsk_R.
      Let R_other := snd tsk_R.

      (* By combining Bertogna's interference bound for a work-conserving
         scheduler ... *)
      Let basic_interference_bound := interference_bound_generic task_cost task_period task_jitter tsk delta tsk_R.

      (* ... with and EDF-specific interference bound, ... *)
      Let edf_specific_bound := edf_specific_interference_bound task_cost task_period task_deadline task_jitter tsk tsk_other R_other.

      (* Bertogna and Cirinei define the following interference bound
         under EDF scheduling. *)
      Definition interference_bound_edf :=
        minn basic_interference_bound edf_specific_bound.

    End PerTask.
89

90
    Section AllTasks.
91

92 93 94 95 96 97 98 99 100 101 102 103 104 105
      Let can_interfere_with_tsk := jldp_can_interfere_with tsk.
      
      (* The total interference incurred by tsk is bounded by the sum
         of individual task interferences. *)
      Definition total_interference_bound_edf :=
        \sum_((tsk_other, R_other) <- R_prev | can_interfere_with_tsk tsk_other)
           interference_bound_edf (tsk_other, R_other).

    End AllTasks.

  End TotalInterferenceBoundEDF.
  
  (* In this section, we show that the EDF-specific interference bound is safe. *)
  Section ProofSpecificBound.
106

107
    Import ScheduleWithJitter Interference Platform SporadicTaskset.
108 109 110 111 112
    
    Context {sporadic_task: eqType}.
    Variable task_cost: sporadic_task -> nat.
    Variable task_period: sporadic_task -> nat.
    Variable task_deadline: sporadic_task -> nat.
113
    Variable task_jitter: sporadic_task -> nat.
114 115 116 117 118
    
    Context {Job: eqType}.
    Variable job_cost: Job -> nat.
    Variable job_deadline: Job -> nat.
    Variable job_task: Job -> sporadic_task.
119
    Variable job_jitter: Job -> nat.
120 121 122 123 124 125 126 127 128
    
    (* 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),
129
        valid_sporadic_job_with_jitter task_cost task_deadline task_jitter job_cost job_deadline job_task job_jitter j.
130 131 132 133 134

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

135 136 137
    (* ...jobs do not execute before jitter nor longer than their execution costs. *)
    Hypothesis H_jobs_execute_after_jitter:
      jobs_execute_after_jitter job_jitter sched.
138
    Hypothesis H_completed_jobs_dont_execute:
139
      completed_jobs_dont_execute job_cost sched.
140

141 142
    (* Also assume that jobs do not execute in parallel and that
       there exists at least one processor. *)
143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158
    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
       parameters and restricted deadlines. *)
    Variable ts: taskset_of sporadic_task.
    Hypothesis all_jobs_from_taskset:
      forall (j: JobIn arr_seq), job_task j \in ts.
    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.

    Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
159
      task_misses_no_deadline job_cost job_deadline job_task sched tsk.
160
    Let response_time_bounded_by (tsk: sporadic_task) :=
161
      is_response_time_bound_of_task job_cost job_task tsk sched.
162

163 164 165
    (* Assume that we have a work-conserving EDF scheduler. *)
    Hypothesis H_work_conserving: work_conserving job_cost job_jitter sched.
    Hypothesis H_edf_policy: enforces_JLDP_policy job_cost job_jitter sched (EDF job_deadline).
166 167 168

    (* Let tsk_i be the task to be analyzed, ...*)
    Variable tsk_i: sporadic_task.
169 170
    Hypothesis H_tsk_i_in_task_set: tsk_i \in ts.
    
171 172 173 174
    (* and j_i one of its jobs. *)
    Variable j_i: JobIn arr_seq.
    Hypothesis H_job_of_tsk_i: job_task j_i = tsk_i.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
175
    (* Let tsk_k denote any interfering task, ... *)
176
    Variable tsk_k: sporadic_task.
177
    Hypothesis H_tsk_k_in_task_set: tsk_k \in ts.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
178 179

    (* ...and R_k its response-time bound. *)
180
    Variable R_k: time.
181
    Hypothesis H_R_k_le_deadline: task_jitter tsk_k + R_k <= task_deadline tsk_k.
182
    
Felipe Cerqueira's avatar
Felipe Cerqueira committed
183
    (* Consider a time window of length delta <= D_i, starting with j_i's arrival time. *)
184
    Variable delta: time.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
185
    Hypothesis H_delta_le_deadline: delta <= task_deadline tsk_i.
186 187 188 189 190

    (* Assume that the jobs of tsk_k satisfy the response-time bound before the end of the interval *)
    Hypothesis H_all_previous_jobs_completed_on_time :
      forall (j_k: JobIn arr_seq),
        job_task j_k = tsk_k ->
191 192
        job_arrival j_k + task_jitter tsk_k + R_k < job_arrival j_i + task_jitter tsk_i + delta ->
        completed job_cost sched j_k (job_arrival j_k + task_jitter tsk_k + R_k).
193

Felipe Cerqueira's avatar
Felipe Cerqueira committed
194 195
    (* In this section, we prove that Bertogna and Cirinei's EDF interference bound
       indeed bounds the interference caused by task tsk_k in the interval [t1, t1 + delta). *)
196
    Section MainProof.
197 198 199 200 201

      (* Let t1 be the first point in time where j can actually be scheduled. *)
      Let t1 := job_arrival j_i + job_jitter j_i.
      Let t2 := t1 + delta.
      
202 203
      (* Let's call x the task interference incurred by job j due to tsk_k. *)
      Let x :=
204
        task_interference job_cost job_task job_jitter sched j_i tsk_k t1 t2.
205 206 207

      (* Also, recall the EDF-specific interference bound for EDF. *)
      Let interference_bound :=
208
        edf_specific_interference_bound task_cost task_period task_deadline task_jitter tsk_i tsk_k R_k.
209 210

      (* Let's simplify the names a bit. *)
211
      Let a_i := job_arrival j_i.
212 213 214
      Let D_i := task_deadline tsk_i.
      Let D_k := task_deadline tsk_k.
      Let p_k := task_period tsk_k.
215 216
      Let J_i := task_jitter tsk_i.
      Let J_k := task_jitter tsk_k.
217 218

      Let n_k := div_floor D_i p_k.
219 220

      (* Let's give a simpler name to job interference. *)
221
      Let interference_caused_by := job_interference job_cost job_jitter sched j_i.
222 223 224 225
      
      (* Identify the subset of jobs that actually cause interference *)
      Let interfering_jobs :=
        filter (fun (x: JobIn arr_seq) =>
226
                 (job_task x == tsk_k) && (interference_caused_by x t1 t2 != 0))
227 228 229
               (jobs_scheduled_between sched t1 t2).
      
      (* Now, consider the list of interfering jobs sorted by arrival time. *)
230 231
      Let earlier_arrival := fun (x y: JobIn arr_seq) => job_arrival x <= job_arrival y.
      Let sorted_jobs := (sort earlier_arrival interfering_jobs).
232 233 234 235

      (* Now we proceed with the proof.
         The first step consists in simplifying the sum corresponding to the workload. *)
      Section SimplifyJobSequence.
236 237 238 239

        (* Use the alternative definition of task interference, based on
           individual job interference. *)
        Lemma interference_bound_edf_use_another_definition :
240
          x <= \sum_(j <- jobs_scheduled_between sched t1 t2 | job_task j == tsk_k)
241 242
                interference_caused_by j t1 t2.
        Proof.
243
          apply interference_le_interference_joblist.
244 245
        Qed.

246 247 248 249 250 251 252 253 254 255
        (* Remove the elements that we don't care about from the sum *)
        Lemma interference_bound_edf_simpl_by_filtering_interfering_jobs :
          \sum_(j <- jobs_scheduled_between sched t1 t2 | job_task j == tsk_k)
             interference_caused_by j t1 t2 = 
          \sum_(j <- interfering_jobs) interference_caused_by j t1 t2.
        Proof.
          unfold interfering_jobs; rewrite big_filter.
          rewrite big_mkcond; rewrite [\sum_(_ <- _ | _) _]big_mkcond /=.
          apply eq_bigr; intros i _; clear -i.
          destruct (job_task i == tsk_k); rewrite ?andTb ?andFb; last by done.
256
          destruct (interference_caused_by i t1 t2 != 0) eqn:DIFF; first by done.
257 258 259 260
          by apply negbT in DIFF; rewrite negbK in DIFF; apply/eqP.
        Qed.

        (* Then, we consider the sum over the sorted sequence of jobs. *)
261
        Lemma interference_bound_edf_simpl_by_sorting_interfering_jobs :
262 263 264
          \sum_(j <- interfering_jobs) interference_caused_by j t1 t2 =
           \sum_(j <- sorted_jobs) interference_caused_by j t1 t2.
        Proof.
265
          by rewrite (eq_big_perm sorted_jobs) /=; last by rewrite -(perm_sort earlier_arrival).
266 267
        Qed.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
268
        (* Note that both sequences have the same set of elements. *)
269 270 271 272
        Lemma interference_bound_edf_job_in_same_sequence :
          forall j,
            (j \in interfering_jobs) = (j \in sorted_jobs).
        Proof.
273
          by apply perm_eq_mem; rewrite -(perm_sort earlier_arrival).
274 275
        Qed.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
276
        (* Also recall that all jobs in the sorted sequence is an interfering job of tsk_k, ... *)
277 278 279 280 281 282 283 284 285 286 287 288
        Lemma interference_bound_edf_all_jobs_from_tsk_k :
          forall j,
            j \in sorted_jobs ->
            job_task j = tsk_k /\
            interference_caused_by j t1 t2 != 0 /\
            j \in jobs_scheduled_between sched t1 t2.
        Proof.
          intros j LT.
          rewrite -interference_bound_edf_job_in_same_sequence mem_filter in LT.
          by move: LT => /andP [/andP [/eqP JOBi SERVi] INi]; repeat split.
        Qed.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
289
        (* ...and consecutive jobs are ordered by arrival. *)
290 291 292
        Lemma interference_bound_edf_jobs_ordered_by_arrival :
          forall i elem,
            i < (size sorted_jobs).-1 ->
293
            earlier_arrival (nth elem sorted_jobs i) (nth elem sorted_jobs i.+1).
294 295
        Proof.
          intros i elem LT.
296 297
          assert (SORT: sorted earlier_arrival sorted_jobs).
            by apply sort_sorted; unfold total, earlier_arrival; ins; apply leq_total.
298 299 300
          by destruct sorted_jobs; simpl in *; [by rewrite ltn0 in LT | by apply/pathP].
        Qed.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
301
        (* Also, for any job of task tsk_k, the interference is bounded by the task cost. *)
302
        Lemma interference_bound_edf_interference_le_task_cost :
303 304
          forall j,
            j \in interfering_jobs ->
305 306
            interference_caused_by j t1 t2 <= task_cost tsk_k.
        Proof.
307
          rename H_valid_job_parameters into PARAMS.
308
          unfold valid_sporadic_job_with_jitter, valid_sporadic_job in *.
309
          intros j; rewrite mem_filter; move => /andP [/andP [/eqP JOBj _] _].
310
          specialize (PARAMS j); des.
311 312
          apply leq_trans with (n := service_during sched j t1 t2);
            first by apply job_interference_le_service.
313 314 315 316
          by apply cumulative_service_le_task_cost with (job_task0 := job_task)
                              (task_deadline0 := task_deadline) (job_cost0 := job_cost)
                                                        (job_deadline0 := job_deadline).
        Qed.
317 318 319

      End SimplifyJobSequence.

320 321 322 323 324
      (* Next, we show that if the number of jobs is no larger than n_k,
         the workload bound trivially holds. *)
      Section InterferenceFewJobs.

        Hypothesis H_few_jobs: size sorted_jobs <= n_k.
325
        
326 327 328 329
        Lemma interference_bound_edf_holds_for_at_most_n_k_jobs :
           \sum_(j <- sorted_jobs) interference_caused_by j t1 t2 <=
             interference_bound.
        Proof.
330 331 332 333
          rewrite -[\sum_(_ <- _ | _) _]addn0 leq_add //.
          apply leq_trans with (n := \sum_(x <- sorted_jobs) task_cost tsk_k);
            last by rewrite big_const_seq iter_addn addn0 mulnC leq_mul2r; apply/orP; right.
          {
334
            rewrite [\sum_(_ <- _) interference_caused_by _ _ _]big_seq_cond.
335
            rewrite [\sum_(_ <- _) task_cost _]big_seq_cond.
336 337 338
            apply leq_sum; intros i; move/andP => [INi _].
            rewrite -interference_bound_edf_job_in_same_sequence in INi.
            by apply interference_bound_edf_interference_le_task_cost.
339
          }
340
        Qed.
341

342 343 344 345
      End InterferenceFewJobs.

      (* Otherwise, assume that the number of jobs is larger than n_k >= 0. *)
      Section InterferenceManyJobs.
346

347 348
        Hypothesis H_many_jobs: n_k < size sorted_jobs.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
349
        (* This trivially implies that there's at least one job. *)
350 351 352 353 354 355 356 357 358 359
        Lemma interference_bound_edf_at_least_one_job: size sorted_jobs > 0.
        Proof.
          by apply leq_ltn_trans with (n := n_k).
        Qed.

        (* Let j_fst be the first job, and a_fst its arrival time. *)
        Variable elem: JobIn arr_seq.
        Let j_fst := nth elem sorted_jobs 0.
        Let a_fst := job_arrival j_fst.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
360 361 362 363 364 365 366 367 368 369 370 371
        (* In this section, we prove some basic lemmas about j_fst. *)
        Section FactsAboutFirstJob.
          
          (* The first job is an interfering job of task tsk_k. *)
          Lemma interference_bound_edf_j_fst_is_job_of_tsk_k :
            job_task j_fst = tsk_k /\
            interference_caused_by j_fst t1 t2 != 0 /\
            j_fst \in jobs_scheduled_between sched t1 t2.
          Proof.
            by apply interference_bound_edf_all_jobs_from_tsk_k, mem_nth,
                     interference_bound_edf_at_least_one_job.
          Qed.
372

Felipe Cerqueira's avatar
Felipe Cerqueira committed
373 374 375 376
          (* The deadline of j_fst is the deadline of tsk_k. *)
          Lemma interference_bound_edf_j_fst_deadline :
            job_deadline j_fst = task_deadline tsk_k.
          Proof.
377
            unfold valid_sporadic_job_with_jitter, valid_sporadic_job in *.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
378 379 380
            rename H_valid_job_parameters into PARAMS.
            have FST := interference_bound_edf_j_fst_is_job_of_tsk_k.
            destruct FST as [FSTtask _].
381
            by specialize (PARAMS j_fst); des; rewrite PARAMS2 FSTtask.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
382 383 384 385 386 387
          Qed.

          (* The deadline of j_i is the deadline of tsk_i. *)
          Lemma interference_bound_edf_j_i_deadline :
            job_deadline j_i = task_deadline tsk_i.
          Proof.
388
            unfold valid_sporadic_job_with_jitter, valid_sporadic_job in *.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
389 390
            rename H_valid_job_parameters into PARAMS,
                   H_job_of_tsk_i into JOBtsk.
391
            by specialize (PARAMS j_i); des; rewrite PARAMS2 JOBtsk.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
392 393 394 395 396
          Qed.

          (* If j_fst completes by its response-time bound, then t1 <= a_fst + R_k,
             where t1 is the beginning of the time window (arrival of j_i). *)
          Lemma interference_bound_edf_j_fst_completion_implies_rt_bound_inside_interval :
397 398
            completed job_cost sched j_fst (a_fst + J_k + R_k) ->
            t1 <= a_fst + J_k + R_k.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
399 400 401 402 403 404
          Proof.
            intros RBOUND.
            rewrite leqNgt; apply/negP; unfold not; intro BUG.
            have FST := interference_bound_edf_j_fst_is_job_of_tsk_k.
            destruct FST as [_ [ FSTserv _]].
            move: FSTserv => /negP FSTserv; apply FSTserv.
405 406
            rewrite -leqn0; apply leq_trans with (n := service_during sched j_fst t1 t2);
              first by apply job_interference_le_service.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
407
            rewrite leqn0; apply/eqP.
408 409 410
            unfold service_during.
            by apply cumulative_service_after_job_rt_zero with (job_cost0 := job_cost) (R := J_k + R_k);
              try (by done); rewrite addnA; last by apply ltnW.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
411 412 413
          Qed. 
          
        End FactsAboutFirstJob.
414

415
        
Felipe Cerqueira's avatar
Felipe Cerqueira committed
416
        (* Now, let's prove the interference bound for the particular case of a single job.
417
           This case must be solved separately because the single job can simultaneously
Felipe Cerqueira's avatar
Felipe Cerqueira committed
418
           be carry-in and carry-out job, so its response time is not necessarily
Felipe Cerqueira's avatar
Felipe Cerqueira committed
419
           bounded by R_k (from the hypothesis H_all_previous_jobs_completed_on_time). *)
420 421 422 423 424 425 426
        Section InterferenceSingleJob.

          (* Assume that there's at least one job in the sorted list. *)
          Hypothesis H_only_one_job: size sorted_jobs = 1.
          
          (* Since there's only one job, we simplify the terms in the interference bound. *)
          Lemma interference_bound_edf_simpl_when_there's_one_job :
427
            D_i %% p_k - (D_k - R_k - J_k) = D_i - (D_k - R_k - J_k).
428 429 430 431 432 433 434 435 436 437 438 439 440 441
          Proof.
            rename H_many_jobs into NUM,
                   H_valid_task_parameters into TASK_PARAMS,
                   H_tsk_k_in_task_set into INk.
            unfold valid_sporadic_taskset, is_valid_sporadic_task,
                   interference_bound, edf_specific_interference_bound in *.
            rewrite H_only_one_job in NUM.
            rewrite ltnS leqn0 in NUM; move: NUM => /eqP EQnk.
            move: EQnk => /eqP EQnk; unfold n_k, div_floor in EQnk.
            rewrite -leqn0 leqNgt divn_gt0 in EQnk;
              last by specialize (TASK_PARAMS tsk_k INk); des.
            by rewrite -ltnNge in EQnk; rewrite modn_small //.
          Qed.

442
          
Felipe Cerqueira's avatar
Felipe Cerqueira committed
443 444 445
          (* Next, we show that if j_fst completes by its response-time bound R_k,
             then then interference bound holds. *)
          Section ResponseTimeOfSingleJobBounded.
446

Felipe Cerqueira's avatar
Felipe Cerqueira committed
447
            Hypothesis H_j_fst_completed_by_rt_bound :
448
              completed job_cost sched j_fst (a_fst + J_k + R_k).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
449 450
            
            Lemma interference_bound_edf_holds_for_single_job_that_completes_on_time :
451
              job_interference job_cost job_jitter sched j_i j_fst t1 t2 <= D_i - (D_k - R_k - J_k).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
452 453 454 455 456 457
            Proof.
              rename H_j_fst_completed_by_rt_bound into RBOUND.
              have AFTERt1 :=
                interference_bound_edf_j_fst_completion_implies_rt_bound_inside_interval RBOUND.
              have FST := interference_bound_edf_j_fst_is_job_of_tsk_k.
              destruct FST as [_ [ LEdl _]].            
458 459
              apply interference_under_edf_implies_shorter_deadlines with
                   (job_deadline0 := job_deadline) in LEdl; try (by done).
460
              destruct (D_k - R_k - J_k <= D_i) eqn:LEdk; last first.
461
              {
Felipe Cerqueira's avatar
Felipe Cerqueira committed
462 463
                apply negbT in LEdk; rewrite -ltnNge in LEdk.
                apply leq_trans with (n := 0); last by done.
464 465 466 467 468 469 470 471
                apply leq_trans with (n := job_interference job_cost job_jitter sched j_i j_fst (a_fst + J_k + R_k) t2); last first.
                {
                  apply leq_trans with (n := service_during sched j_fst (a_fst + J_k + R_k) t2);
                    first by apply job_interference_le_service.
                  unfold service_during; rewrite leqn0; apply/eqP.
                  by apply cumulative_service_after_job_rt_zero with (job_cost0 := job_cost) (R := J_k + R_k);
                    try (by done); rewrite addnA // leqnn.
                }
Felipe Cerqueira's avatar
Felipe Cerqueira committed
472 473 474 475 476
                {
                  apply extend_sum; last by apply leqnn.
                  rewrite -(leq_add2r D_i).
                  rewrite interference_bound_edf_j_fst_deadline
                          interference_bound_edf_j_i_deadline in LEdl.
477 478 479 480 481 482 483 484
                  apply leq_trans with (n := a_fst + D_k); last first.
                  {
                    apply leq_trans with (n := job_arrival j_i + D_i); first by done.
                    by rewrite leq_add2r leq_addr.
                  }
                  rewrite -2!addnA leq_add2l.
                  rewrite addnA.
                  by apply ltnW; rewrite -ltn_subRL addnC subnDA.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
485
                }
486
              }
487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503
              apply leq_trans with (n := job_interference job_cost job_jitter sched j_i j_fst a_i t2);
                first by apply extend_sum; [by apply leq_addr | by apply leqnn].
              
              rewrite -(leq_add2r (D_k - R_k - J_k)) subh1 // -addnBA // subnn addn0.

              assert (SUBST: D_k - R_k - J_k = \sum_(a_fst + J_k + R_k <= i < a_fst + D_k) 1).
              {
                rewrite big_const_nat iter_addn mul1n addn0.
                rewrite [_ + D_k]addnC.
                rewrite -subnBA; last by rewrite -addnA leq_addr.
                rewrite [a_fst + _]addnC -addnA [a_fst + R_k]addnC addnA.
                rewrite -addnBA // subnn addn0.
                by rewrite [_ + R_k]addnC subnDA.
              }
              
              apply leq_trans with (n := job_interference job_cost job_jitter sched j_i j_fst a_i
                                                            (a_fst + D_k) + (D_k - R_k - J_k)).
504
              {
505 506
                rewrite leq_add2r.
                destruct (t2 <= a_fst + J_k + R_k) eqn:LEt2.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
507
                {
508 509 510 511
                  apply extend_sum; first by apply leqnn.
                  apply leq_trans with (n := a_fst + J_k + R_k); first by done.
                  rewrite -addnA leq_add2l.
                  by apply H_R_k_le_deadline.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
512 513
                }
                {
514 515 516 517
                  unfold job_interference.
                  apply negbT in LEt2; rewrite -ltnNge in LEt2.
                  rewrite -> big_cat_nat with (n := a_fst + J_k + R_k);
                    [simpl | | by apply ltnW]; last first.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
518
                  {
519
                      by apply leq_trans with (n := t1); first by apply leq_addr.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
520
                  }
521 522
                  apply leq_trans with (n := job_interference job_cost job_jitter sched j_i j_fst a_i
                                 (a_fst + J_k + R_k) + service_during sched j_fst (a_fst + J_k + R_k) t2).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
523
                  {
524 525
                    rewrite leq_add2l.
                    by apply job_interference_le_service.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
526
                  }
527 528 529 530 531 532 533
                  unfold service_during.
                  rewrite -> cumulative_service_after_job_rt_zero with (job_cost0 := job_cost)
                                                                                     (R := J_k + R_k);
                      try (by done); rewrite ?addnA //; last by apply leqnn.
                  rewrite addn0; apply extend_sum; first by apply leqnn.
                  rewrite -addnA leq_add2l.
                  by apply H_R_k_le_deadline.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
534
                }
535
              }
Felipe Cerqueira's avatar
Felipe Cerqueira committed
536

537 538 539 540 541 542 543 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 569 570 571 572
              unfold job_interference.
              rewrite -> big_cat_nat with (n := a_fst + J_k + R_k);
                [simpl | | ]; last first.
              {
                rewrite -addnA leq_add2l.
                by apply H_R_k_le_deadline.
              }
              {
                by apply leq_trans with (n := t1); first by apply leq_addr.
              }
              apply leq_trans with (n := job_interference job_cost job_jitter sched j_i j_fst a_i
                  (a_fst + J_k + R_k) + service_during sched j_fst (a_fst + J_k + R_k) (a_fst + D_k) + (D_k - R_k - J_k)).
              {
                rewrite leq_add2r leq_add2l.
                by apply job_interference_le_service.
              }
              unfold service_during.
              rewrite -> cumulative_service_after_job_rt_zero with (job_cost0 := job_cost) (R:=J_k + R_k);
                  try (by done); rewrite ?addnA //; last by apply leqnn.
              rewrite addn0.
              apply leq_trans with (n := (\sum_(a_i <= t < a_fst + J_k + R_k) 1) +
                                           \sum_(a_fst + J_k + R_k <= t < a_fst + D_k) 1).
              {
                apply leq_add; last by rewrite SUBST.
                by unfold job_interference; apply leq_sum; ins; apply leq_b1.
              }
   
              rewrite -big_cat_nat; simpl; last first.
              {
                rewrite -addnA leq_add2l.
                by apply H_R_k_le_deadline.
              }
              {
                by apply leq_trans with (n := t1); first by apply leq_addr.
              }
              {
Felipe Cerqueira's avatar
Felipe Cerqueira committed
573
                rewrite big_const_nat iter_addn mul1n addn0 leq_subLR.
574 575 576 577
                unfold D_i, D_k, t1, a_fst.
                by  rewrite -interference_bound_edf_j_fst_deadline
                            -interference_bound_edf_j_i_deadline.
              }
Felipe Cerqueira's avatar
Felipe Cerqueira committed
578 579 580 581 582 583 584 585 586
            Qed.

          End ResponseTimeOfSingleJobBounded.

          (* Else, if j_fst did not complete by its response-time bound, then
             we need a separate proof. *)
          Section ResponseTimeOfSingleJobNotBounded.

            Hypothesis H_j_fst_not_complete_by_rt_bound :
587
              ~~ completed job_cost sched j_fst (a_fst + J_k + R_k).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
588

Felipe Cerqueira's avatar
Felipe Cerqueira committed
589
            (* This trivially implies that a_fst + R_k lies after the end of the interval,
Felipe Cerqueira's avatar
Felipe Cerqueira committed
590 591
               otherwise j_fst would have completed by its response-time bound. *)
            Lemma interference_bound_edf_response_time_bound_of_j_fst_after_interval :
592
              job_arrival j_fst + J_k + R_k >= job_arrival j_i + J_i + delta.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
593 594 595 596 597 598 599 600
            Proof.
              have FST := interference_bound_edf_j_fst_is_job_of_tsk_k.
              destruct FST as [FSTtask _].            
              rewrite leqNgt; apply/negP; intro LT.
              move: H_j_fst_not_complete_by_rt_bound => /negP BUG; apply BUG.
              by apply H_all_previous_jobs_completed_on_time.
            Qed.

601
            (* If the slack is too big (D_i < D_k - R_k - J_k), j_fst causes no interference. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
602
            Lemma interference_bound_edf_holds_for_single_job_with_big_slack :
603
              D_i < D_k - R_k - J_k ->
Felipe Cerqueira's avatar
Felipe Cerqueira committed
604 605
              interference_caused_by j_fst t1 t2 = 0.
            Proof.
606 607
              unfold valid_sporadic_job_with_jitter, valid_sporadic_job in *.
              have PARAMS := H_valid_job_parameters j_i; des.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
608
              intro LTdk.
609 610
              rewrite 2!ltn_subRL addnA [R_k + _]addnC in LTdk.
              rewrite -(ltn_add2l a_fst) 2!addnA in LTdk.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
611 612 613 614
              apply leq_ltn_trans with (m := t1 + D_i) in LTdk; last first.
              {
                rewrite leq_add2r.
                apply leq_trans with (n := t1 + delta); first by apply leq_addr.
615 616 617 618 619
                apply leq_trans with (n := job_arrival j_i + J_i + delta).
                {
                  unfold J_i;rewrite leq_add2r leq_add2l.
                  rewrite -H_job_of_tsk_i; apply PARAMS0.
                }
Felipe Cerqueira's avatar
Felipe Cerqueira committed
620
                by apply interference_bound_edf_response_time_bound_of_j_fst_after_interval.
621
              }
Felipe Cerqueira's avatar
Felipe Cerqueira committed
622
              apply/eqP; rewrite -[_ _ _ _ == 0]negbK; apply/negP; red; intro BUG.
623 624
              apply interference_under_edf_implies_shorter_deadlines with
                     (job_deadline0 := job_deadline) in BUG; try (by done).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
625 626
              rewrite interference_bound_edf_j_fst_deadline
                      interference_bound_edf_j_i_deadline in BUG.
627 628
              apply leq_ltn_trans with (m := job_arrival j_i + D_i) in LTdk;
                last by rewrite leq_add2r leq_addr.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
629 630 631
              by apply (leq_trans LTdk) in BUG; rewrite ltnn in BUG.
            Qed.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
632
            (* Else, if the slack is small, j_fst causes interference for no longer than
633
               D_i - (D_k - R_k - J_k). *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
634
            Lemma interference_bound_edf_holds_for_single_job_with_small_slack :
635 636
              D_i >= D_k - R_k - J_k ->
              interference_caused_by j_fst t1 t2 <= D_i - (D_k - R_k - J_k).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
637
            Proof.
638 639
              unfold valid_sporadic_job_with_jitter, valid_sporadic_job in *.
              have PARAMS := H_valid_job_parameters j_i; des.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
640 641 642 643 644
              intro LEdk.
              have FST := interference_bound_edf_j_fst_is_job_of_tsk_k.
              destruct FST as [FSTtask [LEdl _]].            
              have LTr := interference_bound_edf_response_time_bound_of_j_fst_after_interval.
              apply subh3; last by apply LEdk.
645 646 647 648 649 650 651 652 653 654 655
              apply leq_trans with (n := job_interference job_cost job_jitter sched j_i j_fst t1
                                                          (job_arrival j_fst + J_k + R_k) + (D_k - R_k - J_k)).
              {
                rewrite leq_add2r; apply extend_sum; first by apply leqnn.
                apply leq_trans with (n := job_arrival j_i + J_i + delta);
                  last by done.
                rewrite leq_add2r leq_add2l.
                by unfold J_i; rewrite -H_job_of_tsk_i; apply PARAMS0.
              }
              apply leq_trans with (n := \sum_(t1 <= t < a_fst + J_k + R_k) 1 +
                                         \sum_(a_fst + J_k + R_k <= t < a_fst + D_k)1).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
656 657 658 659
              {
                apply leq_add; unfold job_interference;
                  first by apply leq_sum; ins; apply leq_b1.
                rewrite big_const_nat iter_addn mul1n addn0 addnC.
660 661 662 663
                rewrite -subnBA; last by rewrite -addnA leq_addr.
                rewrite [a_fst + _]addnC -addnA [a_fst + _]addnC addnA.
                rewrite -addnBA // subnn addn0.
                by rewrite addnC subnDA.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
664 665 666 667
              }
              rewrite -big_cat_nat; simpl; last 2 first.
              {
                apply leq_trans with (n := t1 + delta); first by apply leq_addr.
668 669 670 671 672
                apply leq_trans with (n := job_arrival j_i + J_i + delta).
                {
                  rewrite leq_add2r leq_add2l.
                  unfold J_i; rewrite -H_job_of_tsk_i; apply PARAMS0.
                }
Felipe Cerqueira's avatar
Felipe Cerqueira committed
673
                by apply interference_bound_edf_response_time_bound_of_j_fst_after_interval.
674 675 676 677
              }
              {
                by rewrite -addnA leq_add2l; apply H_R_k_le_deadline.
              }
Felipe Cerqueira's avatar
Felipe Cerqueira committed
678
              rewrite big_const_nat iter_addn mul1n addn0 leq_subLR.
679 680 681 682 683
              unfold D_i, D_k, t1, a_fst.
              rewrite -interference_bound_edf_j_fst_deadline
                      -interference_bound_edf_j_i_deadline.
              apply leq_trans with (n := a_i + job_deadline j_i);
                last by rewrite leq_add2r leq_addr.
684 685
              by apply interference_under_edf_implies_shorter_deadlines with
                (job_deadline0 := job_deadline) in LEdl.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
686 687 688 689
            Qed.

          End ResponseTimeOfSingleJobNotBounded.
          
Felipe Cerqueira's avatar
Felipe Cerqueira committed
690 691
          (* By combining the results above, we prove that the interference caused by the single job
             is bounded by D_i - (D_k - R_k), ... *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
692
          Lemma interference_bound_edf_interference_of_j_fst_limited_by_slack :
693
            interference_caused_by j_fst t1 t2 <= D_i - (D_k - R_k - J_k).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
694
          Proof.
695
            destruct (completed job_cost sched j_fst (a_fst + J_k + R_k)) eqn:COMP;
Felipe Cerqueira's avatar
Felipe Cerqueira committed
696 697
              first by apply interference_bound_edf_holds_for_single_job_that_completes_on_time. 
            apply negbT in COMP.
698
            destruct (ltnP D_i (D_k - R_k - J_k)) as [LEdk | LTdk].
Felipe Cerqueira's avatar
Felipe Cerqueira committed
699 700 701
              by rewrite interference_bound_edf_holds_for_single_job_with_big_slack.
              by apply interference_bound_edf_holds_for_single_job_with_small_slack.
          Qed.
702

Felipe Cerqueira's avatar
Felipe Cerqueira committed
703
          (* ... and thus the interference bound holds. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
704 705 706 707 708 709 710 711 712
          Lemma interference_bound_edf_holds_for_a_single_job :
            interference_caused_by j_fst t1 t2 <= interference_bound.
          Proof.
            rename H_many_jobs into NUM, H_only_one_job into SIZE.
            unfold interference_caused_by, interference_bound, edf_specific_interference_bound.
            fold D_i D_k p_k n_k.
            rewrite SIZE ltnS leqn0 in NUM; move: NUM => /eqP EQnk.
            rewrite EQnk mul0n add0n.
            rewrite leq_min; apply/andP; split.
713
            {
Felipe Cerqueira's avatar
Felipe Cerqueira committed
714 715 716
              apply interference_bound_edf_interference_le_task_cost.
              rewrite interference_bound_edf_job_in_same_sequence.
              by apply mem_nth; rewrite SIZE.
717
            }
Felipe Cerqueira's avatar
Felipe Cerqueira committed
718 719 720 721
            rewrite interference_bound_edf_simpl_when_there's_one_job.
            by apply interference_bound_edf_interference_of_j_fst_limited_by_slack.
          Qed.

722 723
        End InterferenceSingleJob.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
724
        (* Next, consider the other case where there are at least two jobs:
725 726 727 728 729 730 731
           the first job j_fst, and the last job j_lst. *)
        Section InterferenceTwoOrMoreJobs.

          (* Assume there are at least two jobs. *)
          Variable num_mid_jobs: nat.
          Hypothesis H_at_least_two_jobs : size sorted_jobs = num_mid_jobs.+2.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752
          (* Let j_lst be the last job of the sequence and a_lst its arrival time. *)
          Let j_lst := nth elem sorted_jobs num_mid_jobs.+1.
          Let a_lst := job_arrival j_lst.

          (* In this section, we prove some basic lemmas about the first and last jobs. *)
          Section FactsAboutFirstAndLastJobs.

            (* The last job is an interfering job of task tsk_k. *)
            Lemma interference_bound_edf_j_lst_is_job_of_tsk_k :
              job_task j_lst = tsk_k /\
              interference_caused_by j_lst t1 t2 != 0 /\
              j_lst \in jobs_scheduled_between sched t1 t2.
            Proof.
              apply interference_bound_edf_all_jobs_from_tsk_k, mem_nth.
              by rewrite H_at_least_two_jobs.
            Qed.

            (* The deadline of j_lst is the deadline of tsk_k. *)
            Lemma interference_bound_edf_j_lst_deadline :
              job_deadline j_lst = task_deadline tsk_k.
            Proof.
753
              unfold valid_sporadic_job_with_jitter, valid_sporadic_job in *.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
754 755 756
              rename H_valid_job_parameters into PARAMS.
              have LST := interference_bound_edf_j_lst_is_job_of_tsk_k.
              destruct LST as [LSTtask _].
757
              by specialize (PARAMS j_lst); des; rewrite PARAMS2 LSTtask.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781
            Qed.

            (* The first job arrives before the last job. *)
            Lemma interference_bound_edf_j_fst_before_j_lst :
              job_arrival j_fst <= job_arrival j_lst.
            Proof.
              rename H_at_least_two_jobs into SIZE.
              unfold j_fst, j_lst; rewrite -[num_mid_jobs.+1]add0n.
              apply prev_le_next; last by rewrite SIZE leqnn.
              by intros i LT; apply interference_bound_edf_jobs_ordered_by_arrival.
            Qed.

            (* The last job arrives before the end of the interval. *)
            Lemma interference_bound_edf_last_job_arrives_before_end_of_interval :
              job_arrival j_lst < t2.
            Proof.
              rewrite leqNgt; apply/negP; unfold not; intro LT2.
              exploit interference_bound_edf_all_jobs_from_tsk_k.
              {
                apply mem_nth; instantiate (1 := num_mid_jobs.+1).
                by rewrite -(ltn_add2r 1) addn1 H_at_least_two_jobs addn1.
              }  
              instantiate (1 := elem); move => [LSTtsk [/eqP LSTserv LSTin]].
              apply LSTserv; apply/eqP; rewrite -leqn0.
782 783
              apply leq_trans with (n := service_during sched j_lst t1 t2);
                first by apply job_interference_le_service.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
784
              rewrite leqn0; apply/eqP; unfold service_during.
785 786
              apply cumulative_service_before_job_arrival_zero; last by done.
              by apply arrival_before_jitter with (job_jitter0 := job_jitter).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
787 788 789
            Qed.

            (* Since there are multiple jobs, j_fst is far enough from the end of
Felipe Cerqueira's avatar
Felipe Cerqueira committed
790
               the interval that its response-time bound is valid
Felipe Cerqueira's avatar
Felipe Cerqueira committed
791 792
               (by the assumption H_all_previous_jobs_completed_on_time). *)
            Lemma interference_bound_edf_j_fst_completed_on_time :
793
              completed job_cost sched j_fst (a_fst + J_k + R_k).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
794
            Proof.
795 796
              have PARAMS := H_valid_job_parameters j_i.
              unfold valid_sporadic_job_with_jitter, valid_sporadic_job in *; des.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
797 798 799 800 801 802 803 804 805 806
              have FST := interference_bound_edf_j_fst_is_job_of_tsk_k; des.
              set j_snd := nth elem sorted_jobs 1.
              exploit interference_bound_edf_all_jobs_from_tsk_k.
              {
                by apply mem_nth; instantiate (1 := 1); rewrite H_at_least_two_jobs.
              }
              instantiate (1 := elem); move => [SNDtsk [/eqP SNDserv _]].
              apply H_all_previous_jobs_completed_on_time; try (by done).
              apply leq_ltn_trans with (n := job_arrival j_snd); last first.
              {
807 808 809 810 811
                apply leq_trans with (n := t2); last first.
                {
                  unfold t2, t1; rewrite leq_add2r leq_add2l.
                  by rewrite -H_job_of_tsk_i; apply PARAMS0.
                }
Felipe Cerqueira's avatar
Felipe Cerqueira committed
812
                rewrite ltnNge; apply/negP; red; intro BUG; apply SNDserv.
813
                apply/eqP; rewrite -leqn0; apply leq_trans with (n := service_during
Felipe Cerqueira's avatar
Felipe Cerqueira committed
814
                                                                          sched j_snd t1 t2);
815
                  first by apply job_interference_le_service.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
816
                rewrite leqn0; apply/eqP.
817 818
                apply cumulative_service_before_job_arrival_zero; last by done.
                by apply arrival_before_jitter with (job_jitter0 := job_jitter).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
819 820 821
              }
              apply leq_trans with (n := a_fst + p_k).
              {
822 823 824
                apply leq_trans with (n := job_arrival j_fst + D_k);
                  first by rewrite -addnA leq_add2l.
                by rewrite leq_add2l; apply H_restricted_deadlines. 
Felipe Cerqueira's avatar
Felipe Cerqueira committed
825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847
              }
            
              (* Since jobs are sporadic, we know that the first job arrives
                 at least p_k units before the second. *)
              unfold p_k; rewrite -FST.
              apply H_sporadic_tasks; [| by rewrite SNDtsk | ]; last first.
              {
                apply interference_bound_edf_jobs_ordered_by_arrival.
                by rewrite H_at_least_two_jobs.
              }
              red; move => /eqP BUG.
              by rewrite nth_uniq in BUG; rewrite ?SIZE //;
                [ by apply interference_bound_edf_at_least_one_job
                | by rewrite H_at_least_two_jobs
                | by rewrite sort_uniq; apply filter_uniq, undup_uniq].
            Qed.

          End FactsAboutFirstAndLastJobs.

          (* Next, we prove that the distance between the first and last jobs is at least
             num_mid_jobs + 1 periods. *)
          Lemma interference_bound_edf_many_periods_in_between :
            a_lst - a_fst >= num_mid_jobs.+1 * p_k.
848
          Proof.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
849 850 851 852 853 854 855 856
            unfold a_fst, a_lst, j_fst, j_lst. 
            assert (EQnk: num_mid_jobs.+1=(size sorted_jobs).-1).
              by rewrite H_at_least_two_jobs.
            rewrite EQnk telescoping_sum;
              last by ins; apply interference_bound_edf_jobs_ordered_by_arrival.
            rewrite -[_ * _ tsk_k]addn0 mulnC -iter_addn -{1}[_.-1]subn0 -big_const_nat. 
            rewrite big_nat_cond [\sum_(0 <= i < _)(_-_)]big_nat_cond.
            apply leq_sum; intros i; rewrite andbT; move => /andP LT; des.
857

Felipe Cerqueira's avatar
Felipe Cerqueira committed
858 859 860
            (* To simplify, call the jobs 'cur' and 'next' *)
            set cur := nth elem sorted_jobs i.
            set next := nth elem sorted_jobs i.+1.
861

Felipe Cerqueira's avatar
Felipe Cerqueira committed
862 863 864 865 866 867 868 869 870 871 872 873
            (* Show that cur arrives earlier than next *)
            assert (ARRle: job_arrival cur <= job_arrival next).
              by unfold cur, next; apply interference_bound_edf_jobs_ordered_by_arrival.
             
            (* Show that both cur and next are in the arrival sequence *)
            assert (INnth: cur \in interfering_jobs /\ next \in interfering_jobs).
            {
              rewrite 2!interference_bound_edf_job_in_same_sequence; split.
                by apply mem_nth, (ltn_trans LT0); destruct sorted_jobs; ins.
                by apply mem_nth; destruct sorted_jobs; ins.
            }
            rewrite 2?mem_filter in INnth; des.
874

Felipe Cerqueira's avatar
Felipe Cerqueira committed
875 876 877 878 879
            (* Use the sporadic task model to conclude that cur and next are separated
               by at least (task_period tsk) units. Of course this only holds if cur != next.
               Since we don't know much about the list (except that it's sorted), we must
               also prove that it doesn't contain duplicates. *)
            assert (CUR_LE_NEXT: job_arrival cur + task_period (job_task cur) <= job_arrival next).
880
            {
Felipe Cerqueira's avatar
Felipe Cerqueira committed
881 882 883 884 885 886 887 888 889
              apply H_sporadic_tasks; last by ins.
              unfold cur, next, not; intro EQ; move: EQ => /eqP EQ.
              rewrite nth_uniq in EQ; first by move: EQ => /eqP EQ; intuition.
                by apply ltn_trans with (n := (size sorted_jobs).-1); destruct sorted_jobs; ins.
                by destruct sorted_jobs; ins.
                by rewrite sort_uniq -/interfering_jobs filter_uniq // undup_uniq.
                by move: INnth INnth0 => /eqP INnth /eqP INnth0; rewrite INnth INnth0.  
            }
            by rewrite subh3 // addnC; move: INnth => /eqP INnth; rewrite -INnth.
890 891
          Qed.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
892 893
          (* Using the lemma above, we prove that the ratio n_k is at least the number of
             middle jobs + 1, ... *)
894 895 896 897 898 899 900
          Lemma interference_bound_edf_n_k_covers_middle_jobs_plus_one :
            n_k >= num_mid_jobs.+1.
          Proof.
            rename H_valid_task_parameters into TASK_PARAMS,
                   H_tsk_k_in_task_set into INk.
            unfold valid_sporadic_taskset, is_valid_sporadic_task,
                   interference_bound, edf_specific_interference_bound in *.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
901 902 903 904
            have DIST := interference_bound_edf_many_periods_in_between.
            have AFTERt1 :=
                interference_bound_edf_j_fst_completion_implies_rt_bound_inside_interval
                interference_bound_edf_j_fst_completed_on_time.
905 906
            rewrite leqNgt; apply/negP; unfold not; intro LTnk; unfold n_k in LTnk.
            rewrite ltn_divLR in LTnk; last by specialize (TASK_PARAMS tsk_k INk); des.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
907
            apply (leq_trans LTnk) in DIST; rewrite ltn_subRL in DIST.
908 909
            rewrite -(ltn_add2r (J_k + R_k)) -addnA [D_i + _]addnC addnA in DIST.
            unfold t1 in *.
910 911
            apply leq_ltn_trans with (m := job_arrival j_i + D_i) in DIST; last first.
            {
912 913 914
              rewrite addnA leq_add2r.
              by apply leq_trans with (n := job_arrival j_i + job_jitter j_i);
                first by apply leq_addr.
915
            }
916 917
            apply leq_trans with (p := a_lst + D_k) in DIST;
              last by rewrite leq_add2l.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
918 919
            have LST := interference_bound_edf_j_lst_is_job_of_tsk_k.
            destruct LST as [_ [ LEdl _]].  
920 921
            apply interference_under_edf_implies_shorter_deadlines with
                (job_deadline0 := job_deadline) in LEdl; try (by done).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
922 923
            unfold D_i, D_k in DIST; rewrite interference_bound_edf_j_lst_deadline
                                             interference_bound_edf_j_i_deadline in LEdl.
924
            by apply (leq_trans DIST) in LEdl; rewrite ltnn in LEdl.
925 926
          Qed.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
927 928
          (* ... which allows bounding the interference of the middle and last jobs
             using n_k multiplied by the cost. *)
929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957
          Lemma interference_bound_edf_holds_for_middle_and_last_jobs :
            interference_caused_by j_lst t1 t2 +
              \sum_(0 <= i < num_mid_jobs)
                interference_caused_by (nth elem sorted_jobs i.+1) t1 t2
            <= n_k * task_cost tsk_k.
          Proof.
            apply leq_trans with (n := num_mid_jobs.+1 * task_cost tsk_k); last first.
            {
              rewrite leq_mul2r; apply/orP; right.
              by apply interference_bound_edf_n_k_covers_middle_jobs_plus_one.
            }
            rewrite mulSn; apply leq_add.
            {
              apply interference_bound_edf_interference_le_task_cost.
              rewrite interference_bound_edf_job_in_same_sequence.
              by apply mem_nth; rewrite H_at_least_two_jobs.
            }
            {
              apply leq_trans with (n := \sum_(0 <= i < num_mid_jobs) task_cost tsk_k);
                last by rewrite big_const_nat iter_addn addn0 mulnC subn0.
              rewrite big_nat_cond [\sum_(0 <= i < num_mid_jobs) task_cost _]big_nat_cond.
              apply leq_sum; intros i; rewrite andbT; move => /andP LT; des.
              apply interference_bound_edf_interference_le_task_cost.
              rewrite interference_bound_edf_job_in_same_sequence.
              apply mem_nth; rewrite H_at_least_two_jobs.
              by rewrite ltnS; apply leq_trans with (n := num_mid_jobs).
            }
          Qed.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
958
          (* Now, since n_k < sorted_jobs = num_mid_jobs + 2, it follows that
Felipe Cerqueira's avatar
Felipe Cerqueira committed
959 960 961
             n_k = num_mid_jobs + 1. *)
          Lemma interference_bound_edf_n_k_equals_num_mid_jobs_plus_one :
            n_k = num_mid_jobs.+1.
962
          Proof.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
963 964 965 966 967
            rename H_many_jobs into NUM, H_at_least_two_jobs into SIZE.
            have NK := interference_bound_edf_n_k_covers_middle_jobs_plus_one.
            move: NK; rewrite leq_eqVlt orbC; move => /orP NK; des;
             first by rewrite SIZE ltnS leqNgt NK in NUM.
            by move: NK => /eqP NK; rewrite NK. 
968 969
          Qed.
          
Felipe Cerqueira's avatar
Felipe Cerqueira committed
970 971
          (* After proving the bounds of the middle and last jobs, we do the same for
             the first job. This requires a different proof in order to exploit the slack. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
972 973
          Section InterferenceOfFirstJob.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
974 975
            (* As required by the next lemma, in order to move (D_i %% p_k) to the left of
               the inequality (<=), we must show that it is no smaller than the slack. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
976
            Lemma interference_bound_edf_remainder_ge_slack :
977
              D_k - R_k - J_k <= D_i %% p_k.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
978 979 980 981 982 983 984
            Proof.
              have AFTERt1 :=
                interference_bound_edf_j_fst_completion_implies_rt_bound_inside_interval
                interference_bound_edf_j_fst_completed_on_time.
              have NK := interference_bound_edf_n_k_equals_num_mid_jobs_plus_one.
              have DIST := interference_bound_edf_many_periods_in_between.
              rewrite -NK in DIST.
985
              rewrite 2!leq_subLR addnA [R_k + _]addnC -subndiv_eq_mod.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
986 987
              fold (div_floor D_i p_k) n_k.
              rewrite addnBA; last by apply leq_trunc_div.
988
              apply leq_trans with (n := J_k + R_k + D_i - (a_lst - a_fst)); last by apply leq_sub2l.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
989 990 991 992 993 994 995 996
              rewrite subnBA; last by apply interference_bound_edf_j_fst_before_j_lst.
              rewrite -(leq_add2r a_lst) subh1; last first.
              {
                apply leq_trans with (n := t2);
                  [by apply ltnW, interference_bound_edf_last_job_arrives_before_end_of_interval|].
                rewrite addnC addnA.
                apply leq_trans with (n := t1 + D_i).
                  unfold t2; rewrite leq_add2l; apply H_delta_le_deadline.
997
                by rewrite leq_add2r addnA; apply AFTERt1.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
998 999
              }
              rewrite -addnBA // subnn addn0 [D_k + _]addnC.
1000 1001 1002 1003 1004
              apply leq_trans with (n := job_arrival j_i + D_i); last first.
              {
                rewrite [_ + a_fst]addnC 2!addnA leq_add2r.
                by apply leq_trans with (n := t1); first by apply leq_addr.
              }
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1005 1006 1007 1008
              have LST := interference_bound_edf_j_lst_is_job_of_tsk_k.
              destruct LST as [_ [ LSTserv _]].
              unfold D_i, D_k, a_lst, t1; rewrite -interference_bound_edf_j_lst_deadline
                                                  -interference_bound_edf_j_i_deadline.
1009 1010
              by apply interference_under_edf_implies_shorter_deadlines with
                                (job_deadline0 := job_deadline) in LSTserv.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1011 1012
            Qed.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
1013 1014 1015
            (* To conclude that the interference bound holds, it suffices to show that
               this reordered inequality holds. *)
            Lemma interference_bound_edf_simpl_by_moving_to_left_side :
1016 1017
              interference_caused_by j_fst t1 t2 + (D_k - R_k - J_k) + D_i %/ p_k * p_k <= D_i ->
              interference_caused_by j_fst t1 t2 <= D_i %% p_k - (D_k - R_k - J_k).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1018 1019 1020 1021 1022 1023 1024 1025
            Proof.
              intro LE.
              apply subh3; last by apply interference_bound_edf_remainder_ge_slack.
              by rewrite -subndiv_eq_mod; apply subh3; last by apply leq_trunc_div.
            Qed.
              
            (* Next, we prove that interference caused by j_fst is bounded by the length
               of the interval [t1, a_fst + R_k), ... *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1026
            Lemma interference_bound_edf_interference_of_j_fst_bounded_by_response_time :
1027
               interference_caused_by j_fst t1 t2 <= \sum_(t1 <= t < a_fst + J_k + R_k) 1.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1028
            Proof.
1029
              assert (AFTERt1: t1 <= a_fst + J_k + R_k).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1030 1031 1032 1033
              {
                apply interference_bound_edf_j_fst_completion_implies_rt_bound_inside_interval.
                by apply interference_bound_edf_j_fst_completed_on_time.
              }
1034
              destruct (leqP t2 (a_fst + J_k + R_k)) as [LEt2 | GTt2].
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1035
              {
1036 1037
                apply leq_trans with (n := job_interference job_cost job_jitter sched j_i j_fst t1
                                                                              (a_fst + J_k + R_k));
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1038 1039 1040 1041 1042
                  first by apply extend_sum; rewrite ?leqnn.
                by apply leq_sum; ins; rewrite leq_b1.
              }
              {
                unfold interference_caused_by, job_interference.
1043
                rewrite -> big_cat_nat with (n := a_fst + J_k + R_k);
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1044 1045 1046
                  [simpl | by apply AFTERt1 | by apply ltnW].
                rewrite -[\sum_(_ <= _ < _) 1]addn0; apply leq_add;
                  first by apply leq_sum; ins; apply leq_b1.
1047
                apply leq_trans with (n := service_during sched j_fst (a_fst + J_k + R_k) t2);
1048
                  first by apply job_interference_le_service.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1049
                rewrite leqn0; apply/eqP.
1050 1051
                apply cumulative_service_after_job_rt_zero with (job_cost0 := job_cost) (R := J_k + R_k);
                  [ by done | rewrite addnA | by rewrite addnA leqnn].
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1052 1053 1054 1055
                by apply interference_bound_edf_j_fst_completed_on_time.
              }
            Qed.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
1056
            (* ..., which leads to the following bounds based on interval lengths. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1057
            Lemma interference_bound_edf_bounding_interference_with_interval_lengths :
1058 1059 1060
              interference_caused_by j_fst t1 t2 + (D_k - R_k - J_k) + D_i %/ p_k * p_k <=
              \sum_(t1 <= t < a_fst + J_k + R_k) 1
              + \sum_(a_fst + J_k + R_k <= t < a_fst + D_k) 1
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1061 1062
              + \sum_(a_fst + D_k <= t < a_lst + D_k) 1.
            Proof.
1063
              apply leq_trans with (n := \sum_(t1 <= t < a_fst + J_k + R_k) 1 + (D_k - R_k - J_k) +
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1064 1065 1066 1067 1068
                                                                       D_i %/ p_k * p_k).
              {
                rewrite 2!leq_add2r.
                apply interference_bound_edf_interference_of_j_fst_bounded_by_response_time.
              }
1069
              apply leq_trans with (n := \sum_(t1 <= t < a_fst + J_k + R_k) 1 + (D_k - R_k - J_k) +
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1070 1071 1072 1073 1074 1075
                                                                        (a_lst - a_fst)).
              {
                rewrite leq_add2l; fold (div_floor D_i p_k) n_k.
                rewrite interference_bound_edf_n_k_equals_num_mid_jobs_plus_one.
                by apply interference_bound_edf_many_periods_in_between.
              }
1076 1077
              apply leq_trans with (n := \sum_(t1 <= t < a_fst + J_k + R_k) 1 +
                  \sum_(a_fst + J_k + R_k <= t < a_fst + D_k) 1 + \sum_(a_fst + D_k <= t < a_lst + D_k) 1).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1078
              {
1079
                rewrite -3!addnA leq_add2l; apply leq_add;
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1080
                rewrite big_const_nat iter_addn mul1n addn0;
1081
                [by rewrite subnDl addnC subnDA | by rewrite subnDr leqnn].
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1082 1083 1084 1085
              }
              by apply leqnn.
            Qed.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
1086 1087
            (* To conclude, we show that the concatenation of these interval lengths equals
               (a_lst + D_k) - 1, ... *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1088
            Lemma interference_bound_edf_simpl_by_concatenation_of_intervals :
1089 1090
              \sum_(t1 <= t < a_fst + J_k + R_k) 1
              + \sum_(a_fst + J_k + R_k <= t < a_fst + D_k) 1
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1091 1092
              + \sum_(a_fst + D_k <= t < a_lst + D_k) 1 = (a_lst + D_k) - t1.
            Proof.
1093
              assert (AFTERt1: t1 <= a_fst + J_k + R_k).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1094 1095 1096 1097 1098
              {
                apply interference_bound_edf_j_fst_completion_implies_rt_bound_inside_interval.
                by apply interference_bound_edf_j_fst_completed_on_time.
              }
              rewrite -big_cat_nat;
1099 1100
                [simpl | by apply AFTERt1 | by rewrite -addnA leq_add2l; apply H_R_k_le_deadline].
              
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1101 1102
              rewrite -big_cat_nat; simpl; last 2 first.
              {
1103
                by apply (leq_trans AFTERt1); rewrite -addnA leq_add2l.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1104 1105 1106 1107 1108 1109 1110 1111 1112 1113
              }
              {
                rewrite leq_add2r; unfold a_fst, a_lst, j_fst, j_lst.
                rewrite -[num_mid_jobs.+1]add0n; apply prev_le_next;
                  last by rewrite add0n H_at_least_two_jobs ltnSn.
                by ins; apply interference_bound_edf_jobs_ordered_by_arrival.
              }
              by rewrite big_const_nat iter_addn mul1n addn0.
            Qed.
            
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1114
            (* ... which results in proving that (a_lst + D_k) - t1 <= D_i.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1115 1116
               This holds because high-priority jobs have earlier deadlines. Therefore,
               the interference caused by the first job is bounded by D_i %% p_k - (D_k - R_k). *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1117
            Lemma interference_bound_edf_interference_of_j_fst_limited_by_remainder_and_slack :
1118
              interference_caused_by j_fst t1 t2 <= D_i %% p_k - (D_k - R_k - J_k).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1119
            Proof.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1120
              apply interference_bound_edf_simpl_by_moving_to_left_side.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1121 1122 1123 1124 1125 1126
              apply (leq_trans interference_bound_edf_bounding_interference_with_interval_lengths).
              rewrite interference_bound_edf_simpl_by_concatenation_of_intervals leq_subLR.
              have LST := interference_bound_edf_j_lst_is_job_of_tsk_k.
              destruct LST as [_ [ LSTserv _]].
              unfold D_i, D_k, a_lst, t1; rewrite -interference_bound_edf_j_lst_deadline
                                                  -interference_bound_edf_j_i_deadline.
1127 1128
              apply leq_trans with (n := a_i + job_deadline j_i);
                last by rewrite -addnA leq_add2l leq_addl.
1129 1130
              by apply interference_under_edf_implies_shorter_deadlines
                with (job_deadline0 := job_deadline) in LSTserv.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1131 1132 1133
            Qed.

          End InterferenceOfFirstJob.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159

          (* Using the lemmas above we show that the interference bound works in the
             case of two or more jobs. *)
          Lemma interference_bound_edf_holds_for_multiple_jobs :