workload_bound.v 32.2 KB
Newer Older
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1
Require Import rt.util.all rt.util.divround.
2 3 4 5
Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.task_arrival.
Require Import rt.model.schedule.global.response_time rt.model.schedule.global.schedulability
               rt.model.schedule.global.workload.
Require Import rt.model.schedule.global.basic.schedule.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
6 7 8 9
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.

Module WorkloadBound.
  
10
  Import Job SporadicTaskset Schedule ScheduleOfSporadicTask TaskArrival ResponseTime Schedulability Workload.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 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 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124

  Section WorkloadBoundDef.

    Context {sporadic_task: eqType}.
    Variable task_cost: sporadic_task -> time.
    Variable task_period: sporadic_task -> time.

    (* Consider any task tsk with response-time bound R_tsk,
       that is scheduled in an interval of length delta. *)
    Variable tsk: sporadic_task.
    Variable R_tsk: time.
    Variable delta: time.
    
    (* Based on the number of jobs that execute completely in the interval, ... *)
    Definition max_jobs :=
      div_floor (delta + R_tsk - task_cost tsk) (task_period tsk).

    (* ... Bertogna and Cirinei's workload bound is defined as follows. *)
    Definition W :=
      let e_k := (task_cost tsk) in
      let p_k := (task_period tsk) in            
        minn e_k (delta + R_tsk - e_k - max_jobs * p_k) + max_jobs * e_k.

  End WorkloadBoundDef.
  
  Section BasicLemmas.

    Context {sporadic_task: eqType}.
    Variable task_cost: sporadic_task -> time.
    Variable task_period: sporadic_task -> time.

    (* Let tsk be any task...*)
    Variable tsk: sporadic_task.

    (* ... with period > 0. *)
    Hypothesis H_period_positive: task_period tsk > 0.

    (* Let R1 <= R2 be two response-time bounds that
       are larger than the cost of the tsk. *)
    Variable R1 R2: time.
    Hypothesis H_R_lower_bound: R1 >= task_cost tsk.
    Hypothesis H_R1_le_R2: R1 <= R2.
      
    Let workload_bound := W task_cost task_period tsk.

    (* Then, Bertogna and Cirinei's workload bound is monotonically increasing. *) 
    Lemma W_monotonic :
      forall t1 t2,
        t1 <= t2 ->
        workload_bound R1 t1 <= workload_bound R2 t2.
    Proof.
      intros t1 t2 LEt.
      unfold workload_bound, W, max_jobs, div_floor; rewrite 2!subndiv_eq_mod.
      set e := task_cost tsk; set p := task_period tsk.
      set x1 := t1 + R1.
      set x2 := t2 + R2.
      set delta := x2 - x1.
      rewrite -[x2](addKn x1) -addnBA; fold delta;
        last by apply leq_add.
      
      induction delta; first by rewrite addn0 leqnn.
      {
         apply (leq_trans IHdelta).

         (* Prove special case for p <= 1. *)
         destruct (leqP p 1) as [LTp | GTp].
         {
           rewrite leq_eqVlt in LTp; move: LTp => /orP LTp; des;
             last by rewrite ltnS in LTp; apply (leq_trans H_period_positive) in LTp. 
           {
             rewrite LTp 2!modn1 2!divn1.
             rewrite leq_add2l leq_mul2r; apply/orP; right.
             by rewrite leq_sub2r // leq_add2l.
           }
         }
         (* Harder case: p > 1. *)
         {
           assert (EQ: (x1 + delta.+1 - e) = (x1 + delta - e).+1).
           {
             rewrite -[(x1 + delta - e).+1]addn1.
             rewrite [_+1]addnC addnBA; last first.
             {
               apply (leq_trans H_R_lower_bound).
               by rewrite -addnA addnC -addnA leq_addr.
             }
             by rewrite [1 + _]addnC -addnA addn1.
           } rewrite -> EQ in *; clear EQ.
         
         have DIV := divSn_cases (x1 + delta - e) p GTp; des.
         {
           rewrite DIV leq_add2r leq_min; apply/andP; split;
             first by rewrite geq_minl.
           by apply leq_trans with (n := (x1 + delta - e) %% p);
             [by rewrite geq_minr | by rewrite -DIV0 addn1 leqnSn].
         }
         {
           rewrite -[minn e _]add0n -addnA; apply leq_add; first by ins.
           rewrite -DIV mulnDl mul1n [_ + e]addnC.
           by apply leq_add; [by rewrite geq_minl | by ins].
         }
       }
     }
   Qed.

  End BasicLemmas.
 
  Section ProofWorkloadBound.
 
    Context {sporadic_task: eqType}.
    Variable task_cost: sporadic_task -> time.
    Variable task_period: sporadic_task -> time.
    Variable task_deadline: sporadic_task -> time.
    
    Context {Job: eqType}.
125
    Variable job_arrival: Job -> time.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
126 127 128 129 130 131 132 133
    Variable job_cost: Job -> time.
    Variable job_task: Job -> sporadic_task.
    Variable job_deadline: Job -> time.

    Variable arr_seq: arrival_sequence Job.

    (* Assume that all jobs have valid parameters *)
    Hypothesis H_jobs_have_valid_parameters :
134 135
      forall j,
        arrives_in arr_seq j ->
Felipe Cerqueira's avatar
Felipe Cerqueira committed
136 137 138 139
        valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
    
    (* Consider any schedule. *)
    Context {num_cpus: nat}.
140 141 142
    Variable sched: schedule Job num_cpus.
    Hypothesis H_jobs_come_from_arrival_sequence:
      jobs_come_from_arrival_sequence sched arr_seq.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
143 144 145

    (* Assumption: jobs only execute if they arrived.
       This is used to eliminate jobs that arrive after end of the interval t1 + delta. *)
146
    Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute job_arrival sched.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
147 148 149

    (* Assumption: jobs do not execute after they completed.
       This is used to eliminate jobs that complete before the start of the interval t1. *)
150
    Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
151 152 153 154 155 156 157 158

    (* Assumption: Jobs are sequential.
       This is required to use interval lengths as a measure of service. *)
    Hypothesis H_sequential_jobs: sequential_jobs sched.

    (* Assumption: sporadic task model.
       This is necessary to conclude that consecutive jobs ordered by arrival times
       are separated by at least 'period' times units. *)
159
    Hypothesis H_sporadic_tasks: sporadic_task_model task_period job_arrival job_task arr_seq.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
160 161 162 163

    (* Before starting the proof, let's give simpler names to the definitions. *)
    Let job_has_completed_by := completed job_cost sched.

164
    Let workload_of (tsk: sporadic_task) (t1 t2: time) := workload job_task sched tsk t1 t2.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193

    (* Now we define the theorem. Let tsk be any task in the taskset. *)
    Variable tsk: sporadic_task.

    (* Assumption: the task must have valid parameters:
         a) period > 0 (used in divisions)
         b) deadline of the jobs = deadline of the task
         c) cost <= period
            (used to prove that the distance between the first and last
             jobs is at least (cost + n*period), where n is the number
             of middle jobs. If cost >> period, the claim does not hold
             for every task set. *)
    Hypothesis H_valid_task_parameters:
      is_valid_sporadic_task task_cost task_period task_deadline tsk.

    (* Assumption: the task must have a constrained deadline.
       This is required to prove that n_k (max_jobs) from Bertogna
       and Cirinei's formula accounts for at least the number of
       middle jobs (i.e., number of jobs - 2 in the worst case). *)
    Hypothesis H_constrained_deadline: task_deadline tsk <= task_period tsk.
      
    (* Consider an interval [t1, t1 + delta). *)
    Variable t1 delta: time.

    (* Assume that a response-time bound R_tsk for that task in any
       schedule of this processor platform is also given, ... *)
    Variable R_tsk: time.

    Hypothesis H_response_time_bound :    
194 195 196 197 198
      forall j,
        arrives_in arr_seq j ->
        job_task j = tsk ->
        job_arrival j + R_tsk < t1 + delta ->
        job_has_completed_by j (job_arrival j + R_tsk).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219

    (* ... such that R_tsk >= task_cost tsk and R_tsk <= task_deadline tsk. *)    
    Hypothesis H_response_time_ge_cost: R_tsk >= task_cost tsk.
    Hypothesis H_no_deadline_miss: R_tsk <= task_deadline tsk.
    
    Section MainProof.

      (* In this section, we prove that the workload of a task in the
         interval [t1, t1 + delta) is bounded by W. *)

      (* Let's simplify the names a bit. *)
      Let t2 := t1 + delta.
      Let n_k := max_jobs task_cost task_period tsk R_tsk delta.
      Let workload_bound := W task_cost task_period tsk R_tsk delta.
      
      (* Since we only care about the workload of tsk, we restrict
         our view to the set of jobs of tsk scheduled in [t1, t2). *)
      Let scheduled_jobs :=
        jobs_of_task_scheduled_between job_task sched tsk t1 t2.

      (* Now, let's consider the list of interfering jobs sorted by arrival time. *)
220 221
      Let earlier_arrival := fun x y => job_arrival x <= job_arrival y.
      Let sorted_jobs := sort earlier_arrival scheduled_jobs.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250

      (* The first step consists in simplifying the sum corresponding
         to the workload. *)
      Section SimplifyJobSequence.

        (* After switching to the definition of workload based on a list
           of jobs, we show that sorting the list preserves the sum. *)
        Lemma workload_bound_simpl_by_sorting_scheduled_jobs :
          workload_joblist job_task sched tsk t1 t2 =
           \sum_(i <- sorted_jobs) service_during sched i t1 t2.
        Proof.
          unfold workload_joblist; fold scheduled_jobs.
          rewrite (eq_big_perm sorted_jobs) /= //.
          by rewrite -(perm_sort earlier_arrival).
        Qed.

        (* Remember that both sequences have the same set of elements *)
        Lemma workload_bound_job_in_same_sequence :
          forall j,
            (j \in scheduled_jobs) = (j \in sorted_jobs).
        Proof.
          by apply perm_eq_mem; rewrite -(perm_sort earlier_arrival).
        Qed.

        (* Remember that all jobs in the sorted sequence is an
           interfering job of task tsk. *)
        Lemma workload_bound_all_jobs_from_tsk :
          forall j_i,
            j_i \in sorted_jobs ->
251
            arrives_in arr_seq j_i /\
Felipe Cerqueira's avatar
Felipe Cerqueira committed
252 253 254 255
            job_task j_i = tsk /\
            service_during sched j_i t1 t2 != 0 /\
            j_i \in jobs_scheduled_between sched t1 t2.
        Proof.
256
          rename H_jobs_come_from_arrival_sequence into FROMarr.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
257 258
          intros j_i LTi.
          rewrite -workload_bound_job_in_same_sequence mem_filter in LTi; des.
259 260 261 262 263
          have IN := LTi0.
          unfold jobs_scheduled_between in *; rewrite mem_undup in IN.
          apply mem_bigcat_nat_exists in IN; des.
          rewrite mem_scheduled_jobs_eq_scheduled in IN.
          repeat split; try (by done); first by apply (FROMarr j_i i).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
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
          unfold jobs_scheduled_between in *; rewrite mem_undup in LTi0.
          apply mem_bigcat_nat_exists in LTi0; des.
          rewrite mem_scheduled_jobs_eq_scheduled in LTi0.
          apply service_implies_cumulative_service with (t := i);
            first by apply/andP; split.
          by rewrite -not_scheduled_no_service negbK.
        Qed.

        (* Remember that consecutive jobs are ordered by arrival. *)
        Lemma workload_bound_jobs_ordered_by_arrival :
          forall i elem,
            i < (size sorted_jobs).-1 ->
            earlier_arrival (nth elem sorted_jobs i) (nth elem sorted_jobs i.+1).
        Proof.
          intros i elem LT.
          assert (SORT: sorted earlier_arrival sorted_jobs).
            by apply sort_sorted; unfold total, earlier_arrival; ins; apply leq_total.
          by destruct sorted_jobs; simpl in *; [by rewrite ltn0 in LT | by apply/pathP].
        Qed.

      End SimplifyJobSequence.

      (* Next, we show that if the number of jobs is no larger than n_k,
         the workload bound trivially holds. *)
      Section WorkloadNotManyJobs.

        Lemma workload_bound_holds_for_at_most_n_k_jobs :
          size sorted_jobs <= n_k ->
          \sum_(i <- sorted_jobs) service_during sched i t1 t2 <=
            workload_bound.
        Proof.
        intros LEnk.
        rewrite -[\sum_(_ <- _ | _) _]add0n leq_add //.
        apply leq_trans with (n := \sum_(x <- sorted_jobs) task_cost tsk);
          last by rewrite big_const_seq iter_addn addn0 mulnC leq_mul2r; apply/orP; right.
        {
          rewrite [\sum_(_ <- _) service_during _ _ _ _]big_seq_cond.
          rewrite [\sum_(_ <- _) task_cost _]big_seq_cond.
          apply leq_sum; intros j_i; move/andP => [INi _].
          apply workload_bound_all_jobs_from_tsk in INi; des. 
          eapply cumulative_service_le_task_cost;
305
            [by apply H_completed_jobs_dont_execute | by apply INi0 |].
Felipe Cerqueira's avatar
Felipe Cerqueira committed
306 307 308 309 310 311 312 313 314 315 316 317 318
          by apply H_jobs_have_valid_parameters.
        }
      Qed.

      End WorkloadNotManyJobs.

      (* Otherwise, assume that the number of jobs is larger than n_k >= 0.
         First, consider the simple case with only one job. *)
      Section WorkloadSingleJob.

        (* Assume that there's at least one job in the sorted list. *)
        Hypothesis H_at_least_one_job: size sorted_jobs > 0.

319
        Variable elem: Job.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
320 321 322 323
        Let j_fst := nth elem sorted_jobs 0.

        (* The first job is an interfering job of task tsk. *)
        Lemma workload_bound_j_fst_is_job_of_tsk :
324
          arrives_in arr_seq j_fst /\
Felipe Cerqueira's avatar
Felipe Cerqueira committed
325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345
          job_task j_fst = tsk /\
          service_during sched j_fst t1 t2 != 0 /\
          j_fst \in jobs_scheduled_between sched t1 t2.
        Proof.
          by apply workload_bound_all_jobs_from_tsk, mem_nth.
        Qed.

        (* The workload bound holds for the single job. *)
        Lemma workload_bound_holds_for_a_single_job :
          \sum_(0 <= i < 1) service_during sched (nth elem sorted_jobs i) t1 t2 <=
          workload_bound.
        Proof.
          unfold workload_bound, W; fold n_k.
          have INfst := workload_bound_j_fst_is_job_of_tsk; des.
          rewrite big_nat_recr // big_geq // [nth]lock /= -lock add0n.
          destruct n_k; last first.
          {
            rewrite -[service_during _ _ _ _]add0n; rewrite leq_add //.
            rewrite -[service_during _ _ _ _]add0n [_* task_cost tsk]mulSnr.
            apply leq_add; first by done.
            by eapply cumulative_service_le_task_cost;
346
              [| by apply INfst0
Felipe Cerqueira's avatar
Felipe Cerqueira committed
347 348 349 350 351 352
               | by apply H_jobs_have_valid_parameters].
          }
          {
            rewrite 2!mul0n addn0 subn0 leq_min; apply/andP; split.
            {
              by eapply cumulative_service_le_task_cost;
353
                 [| by apply INfst0
Felipe Cerqueira's avatar
Felipe Cerqueira committed
354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373
                | by apply H_jobs_have_valid_parameters].
            }
            {
              rewrite -addnBA // -[service_during _ _ _ _]addn0.
              apply leq_add; last by done.
              by apply cumulative_service_le_delta.
            }
          }
        Qed.

      End WorkloadSingleJob.

      (* Next, consider the last case where there are at least two jobs:
         the first job j_fst, and the last job j_lst. *)
      Section WorkloadTwoOrMoreJobs.

        (* There are at least two jobs. *)
        Variable num_mid_jobs: nat.
        Hypothesis H_at_least_two_jobs : size sorted_jobs = num_mid_jobs.+2.
        
374
        Variable elem: Job.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
375 376 377 378 379
        Let j_fst := nth elem sorted_jobs 0.
        Let j_lst := nth elem sorted_jobs num_mid_jobs.+1.

        (* The last job is an interfering job of task tsk. *)
        Lemma workload_bound_j_lst_is_job_of_tsk :
380
          arrives_in arr_seq j_lst /\
Felipe Cerqueira's avatar
Felipe Cerqueira committed
381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398
          job_task j_lst = tsk /\
          service_during sched j_lst t1 t2 != 0 /\
          j_lst \in jobs_scheduled_between sched t1 t2.
        Proof.
          apply workload_bound_all_jobs_from_tsk, mem_nth.
          by rewrite H_at_least_two_jobs.
        Qed.

        (* The response time of the first job must fall inside the interval. *)
        Lemma workload_bound_response_time_of_first_job_inside_interval :
          t1 <= job_arrival j_fst + R_tsk.
        Proof.
          rewrite leqNgt; apply /negP; unfold not; intro LTt1.
          exploit workload_bound_all_jobs_from_tsk.
          {
            apply mem_nth; instantiate (1 := 0).
            apply ltn_trans with (n := 1); [by done | by rewrite H_at_least_two_jobs].
          }
399
          instantiate (1 := elem); move => [FSTarr [FSTtsk [/eqP FSTserv FSTin]]].
Felipe Cerqueira's avatar
Felipe Cerqueira committed
400
          apply FSTserv.
401
          apply (cumulative_service_after_job_rt_zero job_arrival job_cost) with (R := R_tsk);
Felipe Cerqueira's avatar
Felipe Cerqueira committed
402
            try (by done); last by apply ltnW.
403
          apply H_response_time_bound; try (by done).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
404 405 406 407 408 409 410 411 412 413 414 415 416
          by apply leq_trans with (n := t1); last by apply leq_addr.
        Qed.

        (* The arrival of the last job must also fall inside the interval. *)
        Lemma workload_bound_last_job_arrives_before_end_of_interval :
          job_arrival j_lst < t2.
        Proof.
          rewrite leqNgt; apply/negP; unfold not; intro LT2.
          exploit workload_bound_all_jobs_from_tsk.
          {
            apply mem_nth; instantiate (1 := num_mid_jobs.+1).
            by rewrite -(ltn_add2r 1) addn1 H_at_least_two_jobs addn1.
          }  
417 418 419
          instantiate (1 := elem); move => [LSTarr [LSTtsk [/eqP LSTserv LSTin]]].
          unfold service_during; apply LSTserv.
          by apply cumulative_service_before_job_arrival_zero with (job_arrival0 := job_arrival).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444
        Qed.

        (* Next, we upper-bound the service of the first and last jobs using their arrival times. *)
        Lemma workload_bound_service_of_first_and_last_jobs :
          service_during sched j_fst t1 t2 +
          service_during sched j_lst t1 t2 <=
            (job_arrival j_fst  + R_tsk - t1) + (t2 - job_arrival j_lst).
        Proof.
          apply leq_add; unfold service_during.
          {
            rewrite -[_ + _ - _]mul1n -[1*_]addn0 -iter_addn -big_const_nat.
            apply leq_trans with (n := \sum_(t1 <= t < job_arrival j_fst + R_tsk)
                                        service_at sched j_fst t);
              last by apply leq_sum; ins; apply service_at_most_one.
            destruct (job_arrival j_fst + R_tsk < t2) eqn:LEt2; last first.
            {
              unfold t2; apply negbT in LEt2; rewrite -ltnNge in LEt2.
              rewrite -> big_cat_nat with (n := t1 + delta) (p := job_arrival j_fst + R_tsk);
                [by apply leq_addr | by apply leq_addr | by done].
            }
            {
              rewrite -> big_cat_nat with (n := job_arrival j_fst + R_tsk);
                [| by apply workload_bound_response_time_of_first_job_inside_interval
                 | by apply ltnW].
              rewrite -{2}[\sum_(_ <= _ < _) _]addn0 /= leq_add2l leqn0; apply/eqP.
445
              apply (cumulative_service_after_job_rt_zero job_arrival job_cost) with (R := R_tsk); try (by done).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
446 447
              exploit workload_bound_all_jobs_from_tsk.
                by apply mem_nth; instantiate (1 := 0); rewrite H_at_least_two_jobs.
448 449
              instantiate (1 := elem); move => [FSTarr [FSTtsk _]].
              by apply H_response_time_bound.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467
            }
          }
          {
            rewrite -[_ - _]mul1n -[1 * _]addn0 -iter_addn -big_const_nat.
            destruct (job_arrival j_lst <= t1) eqn:LT.
            {
              apply leq_trans with (n := \sum_(job_arrival j_lst <= t < t2)
                                          service_at sched j_lst t);
                first by rewrite -> big_cat_nat with (m := job_arrival j_lst) (n := t1);
                  [by apply leq_addl | by ins | by apply leq_addr].
              by apply leq_sum; ins; apply service_at_most_one.
            }
            {
              apply negbT in LT; rewrite -ltnNge in LT.
              rewrite -> big_cat_nat with (n := job_arrival j_lst);
                [| by apply ltnW
                 | by apply ltnW, workload_bound_last_job_arrives_before_end_of_interval].
              rewrite /= -[\sum_(_ <= _ < _) 1]add0n; apply leq_add.
468
              rewrite (cumulative_service_before_job_arrival_zero job_arrival);
Felipe Cerqueira's avatar
Felipe Cerqueira committed
469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509
                [by apply leqnn | by ins | by apply leqnn].
              by apply leq_sum; ins; apply service_at_most_one.
            }
          }
        Qed.

        (* Simplify the expression from the previous lemma. *)
        Lemma workload_bound_simpl_expression_with_first_and_last :
          job_arrival j_fst + R_tsk - t1 + (t2 - job_arrival j_lst) =
                       delta + R_tsk - (job_arrival j_lst - job_arrival j_fst).
        Proof.
          have lemma1 := workload_bound_last_job_arrives_before_end_of_interval.
          have lemma2 := workload_bound_response_time_of_first_job_inside_interval.
          rewrite addnBA; last by apply ltnW.
          rewrite subh1 // -addnBA; last by apply leq_addr.
          rewrite addnC [job_arrival _ + _]addnC.
          unfold t2; rewrite [t1 + _]addnC -[delta + t1 - _]subnBA // subnn subn0.
          rewrite addnA -subnBA; first by ins.
          unfold j_fst, j_lst. rewrite -[_.+1]add0n.
          apply prev_le_next; last by rewrite H_at_least_two_jobs add0n leqnn.
          by ins; apply workload_bound_jobs_ordered_by_arrival.
        Qed.

        (* Bound the service of the middle jobs. *)
        Lemma workload_bound_service_of_middle_jobs :
          \sum_(0 <= i < num_mid_jobs)
            service_during sched (nth elem sorted_jobs i.+1) t1 t2 <=
            num_mid_jobs * task_cost tsk.
        Proof.
          apply leq_trans with (n := num_mid_jobs * task_cost tsk);
            last by rewrite leq_mul2l; apply/orP; right. 
          apply leq_trans with (n := \sum_(0 <= i < num_mid_jobs) task_cost tsk);
            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.
          exploit workload_bound_all_jobs_from_tsk.
          {
            instantiate (1 := nth elem sorted_jobs i.+1).
            apply mem_nth; rewrite H_at_least_two_jobs.
            by rewrite ltnS; apply leq_trans with (n := num_mid_jobs).
          }
510 511
          move => [ARR [TSK _]].
          by eapply cumulative_service_le_task_cost; eauto 2.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533
        Qed.

        (* Conclude that the distance between first and last is at least num_mid_jobs + 1 periods. *)
        Lemma workload_bound_many_periods_in_between :
          job_arrival j_lst - job_arrival j_fst >= num_mid_jobs.+1 * (task_period tsk).
        Proof.
          assert (EQnk: num_mid_jobs.+1=(size sorted_jobs).-1).
            by rewrite H_at_least_two_jobs.
          unfold j_fst, j_lst; rewrite EQnk telescoping_sum;
            last by ins; apply workload_bound_jobs_ordered_by_arrival.
          rewrite -[_ * _ tsk]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.

          (* To simplify, call the jobs 'cur' and 'next' *)
          set cur := nth elem sorted_jobs i.
          set next := nth elem sorted_jobs i.+1.

          (* Show that cur arrives earlier than next *)
          assert (ARRle: job_arrival cur <= job_arrival next).
            by unfold cur, next; apply workload_bound_jobs_ordered_by_arrival.
             
534 535 536 537 538 539 540
          feed (workload_bound_all_jobs_from_tsk cur).
            by apply mem_nth, (ltn_trans LT0); destruct sorted_jobs.
          intros [CURarr [CURtsk [_ CURin]]].

          feed (workload_bound_all_jobs_from_tsk next).
            by apply mem_nth; destruct sorted_jobs.
          intros [NEXTarr [NEXTtsk [_ NEXTin]]].
Felipe Cerqueira's avatar
Felipe Cerqueira committed
541 542 543 544 545 546 547

          (* 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).
          {
548
            apply H_sporadic_tasks; try (by done).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
549 550 551 552 553
            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 -/scheduled_jobs filter_uniq // undup_uniq.
554
              by rewrite CURtsk.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
555
          }
556
          by rewrite subh3 // addnC -CURtsk.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 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 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646
        Qed.

        (* Prove that n_k is at least the number of the middle jobs *)
        Lemma workload_bound_n_k_covers_middle_jobs :
          n_k >= num_mid_jobs.
        Proof.
          rename H_valid_task_parameters into PARAMS.
          unfold is_valid_sporadic_task in *; des.
          rewrite leqNgt; apply/negP; unfold not; intro LTnk.
          assert (DISTmax: job_arrival j_lst - job_arrival j_fst >= delta + task_period tsk).
          {
            apply leq_trans with (n := n_k.+2 * task_period tsk).
            {
              rewrite -addn1 mulnDl mul1n leq_add2r.
              apply leq_trans with (n := delta + R_tsk - task_cost tsk);
                first by rewrite -addnBA //; apply leq_addr.
              by apply ltnW, ltn_ceil, PARAMS0.
            }
            apply leq_trans with (num_mid_jobs.+1 * task_period tsk); 
              first by rewrite leq_mul2r; apply/orP; right.
            by apply workload_bound_many_periods_in_between.
          }
          rewrite <- leq_add2r with (p := job_arrival j_fst) in DISTmax.
          rewrite addnC subh1 in DISTmax; last first.
          {
            unfold j_fst, j_lst; rewrite -[_.+1]add0n.
            apply prev_le_next; last by rewrite H_at_least_two_jobs add0n leqnn.
            by ins; apply workload_bound_jobs_ordered_by_arrival.
          }
          rewrite -subnBA // subnn subn0 in DISTmax.
          rewrite [delta + task_period tsk]addnC addnA in DISTmax.
          have BEFOREt2 := workload_bound_last_job_arrives_before_end_of_interval.
          generalize BEFOREt2; move: BEFOREt2; rewrite {1}ltnNge; move => /negP BEFOREt2'.
          intros BEFOREt2; apply BEFOREt2'; clear BEFOREt2'.
          apply leq_trans with (n := job_arrival j_fst + task_deadline tsk + delta);
            last by apply leq_trans with (n := job_arrival j_fst + task_period tsk + delta);
              [rewrite leq_add2r leq_add2l; apply H_constrained_deadline | apply DISTmax].
          unfold t2; rewrite leq_add2r.
          apply leq_trans with (n := job_arrival j_fst + R_tsk);
            last by rewrite leq_add2l.
          by apply workload_bound_response_time_of_first_job_inside_interval.
        Qed.

        (* If n_k = num_mid_jobs, then the workload bound holds. *)
        Lemma workload_bound_n_k_equals_num_mid_jobs :
          num_mid_jobs = n_k ->
          service_during sched j_lst t1 t2 +
            service_during sched j_fst t1 t2 +
            \sum_(0 <= i < num_mid_jobs)
             service_during sched (nth elem sorted_jobs i.+1) t1 t2
          <= workload_bound.
        Proof.
          rename H_valid_task_parameters into PARAMS.
          unfold is_valid_sporadic_task in *; des.
          unfold workload_bound, W; fold n_k.
          move => NK; rewrite -NK.
          apply leq_add;
            last by apply workload_bound_service_of_middle_jobs.
          apply leq_trans with (delta + R_tsk - (job_arrival j_lst - job_arrival j_fst)).
          {
            rewrite addnC -workload_bound_simpl_expression_with_first_and_last.
            by apply workload_bound_service_of_first_and_last_jobs.
          }
          rewrite leq_min; apply/andP; split.
          {
            rewrite leq_subLR [_ + task_cost _]addnC -leq_subLR.
            apply leq_trans with (num_mid_jobs.+1 * task_period tsk);
              last by apply workload_bound_many_periods_in_between.
            rewrite NK ltnW // -ltn_divLR;
              last by apply PARAMS0.
            by unfold n_k, max_jobs, div_floor.
          }
          {
            rewrite -subnDA; apply leq_sub2l.
            apply leq_trans with (n := num_mid_jobs.+1 * task_period tsk);
              last by apply workload_bound_many_periods_in_between.
            rewrite -addn1 addnC mulnDl mul1n.
            by rewrite leq_add2l; last by apply PARAMS3.
          }
        Qed.

        (* If n_k = num_mid_jobs + 1, then the workload bound holds. *)
        Lemma workload_bound_n_k_equals_num_mid_jobs_plus_1 :
          num_mid_jobs.+1 = n_k ->
          service_during sched j_lst t1 t2 +
            service_during sched j_fst t1 t2 +
            \sum_(0 <= i < num_mid_jobs)
             service_during sched (nth elem sorted_jobs i.+1) t1 t2
          <= workload_bound.
        Proof.
647 648
          have MID := workload_bound_service_of_middle_jobs. 
          rename H_jobs_have_valid_parameters into JOBPARAMS.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
649 650 651
          unfold workload_bound, W; fold n_k.
          move => NK; rewrite -NK.
          rewrite -{2}addn1 mulnDl mul1n [_* _ + _]addnC addnA addn_minl.
652
          apply leq_add; last by apply MID.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
653 654 655 656 657 658
          rewrite leq_min; apply/andP; split.
          {
            assert (SIZE: 0 < size sorted_jobs).
              by rewrite H_at_least_two_jobs.
            have INfst := workload_bound_j_fst_is_job_of_tsk SIZE elem;
            have INlst := workload_bound_j_lst_is_job_of_tsk; des.
659 660 661 662 663
            have PARAMSfst := JOBPARAMS j_fst INfst; des.
            have PARAMSlst := JOBPARAMS j_lst INlst; des.
            by apply leq_add; apply cumulative_service_le_task_cost with
                    (task_deadline0 := task_deadline)
                    (job_cost0 := job_cost) (job_deadline0 := job_deadline) (job_task0 := job_task).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705
          }
          {
            rewrite subnAC subnK; last first.
            {
              assert (TMP: delta + R_tsk = task_cost tsk + (delta + R_tsk - task_cost tsk));
                first by rewrite subnKC; [by ins | by rewrite -[task_cost _]add0n; apply leq_add].
              rewrite TMP; clear TMP.
              rewrite -{1}[task_cost _]addn0 -addnBA NK; [by apply leq_add | by apply leq_trunc_div].
            }
            apply leq_trans with (delta + R_tsk - (job_arrival j_lst - job_arrival j_fst)).
            {
              rewrite addnC -workload_bound_simpl_expression_with_first_and_last.
              by apply workload_bound_service_of_first_and_last_jobs.
            }
            {
              by apply leq_sub2l, workload_bound_many_periods_in_between.
            }
          }
        Qed.
        
      End WorkloadTwoOrMoreJobs.

      (* Using the lemmas above, we prove the main theorem about the workload bound. *)
      Theorem workload_bounded_by_W :
        workload_of tsk t1 (t1 + delta) <= workload_bound.
      Proof.
        unfold workload_of, workload_bound, W in *; ins; des.
        fold n_k.

        (* Use the definition of workload based on list of jobs. *)
        rewrite workload_eq_workload_joblist.

        (* Now we order the list by job arrival time. *)
        rewrite workload_bound_simpl_by_sorting_scheduled_jobs.

        (* Next, we show that the workload bound holds if n_k
           is no larger than the number of interferings jobs. *)
        destruct (size sorted_jobs <= n_k) eqn:NUM;
          first by apply workload_bound_holds_for_at_most_n_k_jobs.
        apply negbT in NUM; rewrite -ltnNge in NUM.

        (* Find some dummy element to use in the nth function *)
706 707
        assert (EX: exists elem: Job, True).
          destruct sorted_jobs; [ by rewrite ltn0 in NUM | by exists s].
Felipe Cerqueira's avatar
Felipe Cerqueira committed
708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744
        destruct EX as [elem _].

        (* Now we index the sum to access the first and last elements. *)
        rewrite (big_nth elem).

        (* First, we show that the bound holds for an empty list of jobs. *)
        destruct (size sorted_jobs) as [| n] eqn:SIZE;
          first by rewrite big_geq.
        
        (* Then, we show the same for a singleton set of jobs. *)
        destruct n as [| num_mid_jobs];
          first by apply workload_bound_holds_for_a_single_job; rewrite SIZE.
        
        (* Knowing that we have at least two elements, we take first and last out of the sum *) 
        rewrite [nth]lock big_nat_recl // big_nat_recr // /= -lock.
        rewrite addnA addnC addnA.
    
        (* There are two cases to be analyze since n <= n_k < n + 2,
           where n is the number of middle jobs. *)
        have NK := workload_bound_n_k_covers_middle_jobs num_mid_jobs SIZE elem.
        move: NK; rewrite leq_eqVlt orbC leq_eqVlt; move => /orP [NK | /eqP NK].
        move: NK => /orP [/eqP NK | NK]; last by rewrite ltnS leqNgt NK in NUM.
        {
          (* Case 1: n_k = n + 1, where n is the number of middle jobs. *)
          by apply (workload_bound_n_k_equals_num_mid_jobs_plus_1 num_mid_jobs).
        }
        {
          (* Case 2: n_k = n, where n is the number of middle jobs. *)
          by apply (workload_bound_n_k_equals_num_mid_jobs num_mid_jobs).
        }
      Qed.

    End MainProof.
    
  End ProofWorkloadBound.

End WorkloadBound.