workload_bound.v 31.6 KB
Newer Older
1 2 3 4 5 6
Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
               rt.model.basic.task_arrival rt.model.basic.response_time
               rt.model.basic.workload rt.model.basic.schedulability.
Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.
Felix Stutz's avatar
Felix Stutz committed
7

8 9
Module WorkloadBound.
  
10
  Import Job SporadicTaskset Schedule ScheduleOfSporadicTask SporadicTaskArrival ResponseTime Schedulability Workload.
11 12

  Section WorkloadBoundDef.
Felix Stutz's avatar
Felix Stutz committed
13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31

    Context {sporadic_task: eqType}.
    Variable task_cost: sporadic_task -> nat.
    Variable task_period: sporadic_task -> nat.
    
    Variable tsk: sporadic_task.
    Variable R_tsk: time. (* Known response-time bound for the task *)
    Variable delta: time. (* Length of the interval *)
    
    (* Bound 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 bound on the workload of a task in an interval of length delta *)
    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.

32
  End WorkloadBoundDef.
Felix Stutz's avatar
Felix Stutz committed
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 125 126 127 128 129 130 131 132 133
  
  Section BasicLemmas.

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

    (* 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. 
           {
             move: LTp => /eqP 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 -> nat.
    Variable task_period: sporadic_task -> nat.
    Variable task_deadline: sporadic_task -> nat.
    
    Context {Job: eqType}.
    Variable job_cost: Job -> nat.
    Variable job_task: Job -> sporadic_task.
    Variable job_deadline: Job -> nat.

    Variable arr_seq: arrival_sequence Job.

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

    (* Assumption: jobs only execute if they arrived.
       This is used to eliminate jobs that arrive after end of the interval t1 + delta. *)
    Hypothesis H_jobs_must_arrive_to_execute:
      jobs_must_arrive_to_execute sched.

    (* Assumption: jobs do not execute after they completed.
       This is used to eliminate jobs that complete before the start of the interval t1. *)
    Hypothesis H_completed_jobs_dont_execute:
146
      completed_jobs_dont_execute job_cost sched.
Felix Stutz's avatar
Felix Stutz committed
147

148
    (* Assumptiom: Jobs do not execute in parallel.
Felix Stutz's avatar
Felix Stutz committed
149 150 151 152 153 154 155 156 157 158
       This is required to use interval lengths as a measure of service. *)
    Hypothesis H_no_parallelism:
      jobs_dont_execute_in_parallel 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. *)
    Hypothesis H_sporadic_tasks: sporadic_task_model task_period arr_seq job_task.

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

Felix Stutz's avatar
Felix Stutz committed
161
    Let workload_of (tsk: sporadic_task) (t1 t2: time) :=
162
      workload job_task sched tsk t1 t2.
Felix Stutz's avatar
Felix Stutz committed
163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183

    (* 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 restricted 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_restricted_deadline: task_deadline tsk <= task_period tsk.
      
184
    (* Consider an interval [t1, t1 + delta). *)
Felix Stutz's avatar
Felix Stutz committed
185 186 187
    Variable t1 delta: time.

    (* Assume that a response-time bound R_tsk for that task in any
188
       schedule of this processor platform is also given, ... *)
Felix Stutz's avatar
Felix Stutz committed
189 190 191 192 193 194 195
    Variable R_tsk: time.

    Hypothesis H_response_time_bound :    
      forall (j: JobIn arr_seq),
      job_task j = tsk ->
      job_arrival j + R_tsk < t1 + delta ->
      job_has_completed_by j (job_arrival j + R_tsk).
196 197 198 199

    (* ... 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.
Felix Stutz's avatar
Felix Stutz committed
200
    
Felipe Cerqueira's avatar
Felipe Cerqueira committed
201
    Section MainProof.
Felix Stutz's avatar
Felix Stutz committed
202

Felipe Cerqueira's avatar
Felipe Cerqueira committed
203 204
      (* In this section, we prove that the workload of a task in the
         interval [t1, t1 + delta) is bounded by W. *)
Felix Stutz's avatar
Felix Stutz committed
205

Felipe Cerqueira's avatar
Felipe Cerqueira committed
206 207 208 209 210
      (* 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.
      
211 212 213
      (* 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 :=
214
        jobs_of_task_scheduled_between job_task sched tsk t1 t2.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
215 216

      (* Now, let's consider the list of interfering jobs sorted by arrival time. *)
217
      Let earlier_arrival := fun (x y: JobIn arr_seq) => job_arrival x <= job_arrival y.
218
      Let sorted_jobs := (sort earlier_arrival scheduled_jobs).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
219 220 221

      (* The first step consists in simplifying the sum corresponding
         to the workload. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
222
      Section SimplifyJobSequence.
Felix Stutz's avatar
Felix Stutz committed
223

224 225
        (* After switching to the definition of workload based on a list
           of jobs, we show that sorting the list preserves the sum. *)
226
        Lemma workload_bound_simpl_by_sorting_scheduled_jobs :
227
          workload_joblist job_task sched tsk t1 t2 =
228
           \sum_(i <- sorted_jobs) service_during sched i t1 t2.
229
        Proof.
230
          unfold workload_joblist; fold scheduled_jobs.
231 232
          rewrite (eq_big_perm sorted_jobs) /= //.
          by rewrite -(perm_sort earlier_arrival).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
233
        Qed.
Felix Stutz's avatar
Felix Stutz committed
234 235

        (* Remember that both sequences have the same set of elements *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
236 237
        Lemma workload_bound_job_in_same_sequence :
          forall j,
238
            (j \in scheduled_jobs) = (j \in sorted_jobs).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
239
        Proof.
240
          by apply perm_eq_mem; rewrite -(perm_sort earlier_arrival).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
241 242
        Qed.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
243 244
        (* Remember that all jobs in the sorted sequence is an
           interfering job of task tsk. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
245 246 247 248
        Lemma workload_bound_all_jobs_from_tsk :
          forall j_i,
            j_i \in sorted_jobs ->
            job_task j_i = tsk /\
249
            service_during sched j_i t1 t2 != 0 /\
Felipe Cerqueira's avatar
Felipe Cerqueira committed
250 251 252
            j_i \in jobs_scheduled_between sched t1 t2.
        Proof.
          intros j_i LTi.
253 254 255 256 257 258 259 260
          rewrite -workload_bound_job_in_same_sequence mem_filter in LTi; des.
          repeat split; [by apply/eqP | | by done].
          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.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
261
        Qed.
Felix Stutz's avatar
Felix Stutz committed
262

Felipe Cerqueira's avatar
Felipe Cerqueira committed
263
        (* Remember that consecutive jobs are ordered by arrival. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
264 265 266
        Lemma workload_bound_jobs_ordered_by_arrival :
          forall i elem,
            i < (size sorted_jobs).-1 ->
267
            earlier_arrival (nth elem sorted_jobs i) (nth elem sorted_jobs i.+1).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
268 269
        Proof.
          intros i elem LT.
270 271
          assert (SORT: sorted earlier_arrival sorted_jobs).
            by apply sort_sorted; unfold total, earlier_arrival; ins; apply leq_total.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
272 273 274 275
          by destruct sorted_jobs; simpl in *; [by rewrite ltn0 in LT | by apply/pathP].
        Qed.

      End SimplifyJobSequence.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
276 277 278

      (* Next, we show that if the number of jobs is no larger than n_k,
         the workload bound trivially holds. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
279 280 281 282
      Section WorkloadNotManyJobs.

        Lemma workload_bound_holds_for_at_most_n_k_jobs :
          size sorted_jobs <= n_k ->
283
          \sum_(i <- sorted_jobs) service_during sched i t1 t2 <=
Felipe Cerqueira's avatar
Felipe Cerqueira committed
284 285 286 287 288 289 290
            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.
        {
291
          rewrite [\sum_(_ <- _) service_during _ _ _ _]big_seq_cond.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
292 293 294 295 296 297 298 299 300 301 302
          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;
            [by apply H_completed_jobs_dont_execute | by apply INi |].
          by apply H_jobs_have_valid_parameters.
        }
      Qed.

      End WorkloadNotManyJobs.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
303 304
      (* Otherwise, assume that the number of jobs is larger than n_k >= 0.
         First, consider the simple case with only one job. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
305 306 307 308 309 310 311
      Section WorkloadSingleJob.

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

        Variable elem: JobIn arr_seq.
        Let j_fst := nth elem sorted_jobs 0.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
312 313

        (* The first job is an interfering job of task tsk. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
314 315
        Lemma workload_bound_j_fst_is_job_of_tsk :
          job_task j_fst = tsk /\
316
          service_during sched j_fst t1 t2 != 0 /\
Felipe Cerqueira's avatar
Felipe Cerqueira committed
317 318 319 320
          j_fst \in jobs_scheduled_between sched t1 t2.
        Proof.
          by apply workload_bound_all_jobs_from_tsk, mem_nth.
        Qed.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
321 322

        (* The workload bound holds for the single job. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
323
        Lemma workload_bound_holds_for_a_single_job :
324
          \sum_(0 <= i < 1) service_during sched (nth elem sorted_jobs i) t1 t2 <=
Felipe Cerqueira's avatar
Felipe Cerqueira committed
325
          workload_bound.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
326 327 328 329 330
        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.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
331
          {
332 333
            rewrite -[service_during _ _ _ _]add0n; rewrite leq_add //.
            rewrite -[service_during _ _ _ _]add0n [_* task_cost tsk]mulSnr.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
334
            apply leq_add; first by done.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
335
            by eapply cumulative_service_le_task_cost;
Felipe Cerqueira's avatar
Felipe Cerqueira committed
336 337
              [| by apply INfst
               | by apply H_jobs_have_valid_parameters].
Felipe Cerqueira's avatar
Felipe Cerqueira committed
338
          }
Felix Stutz's avatar
Felix Stutz committed
339
          {
Felipe Cerqueira's avatar
Felipe Cerqueira committed
340 341 342 343 344 345 346
            rewrite 2!mul0n addn0 subn0 leq_min; apply/andP; split.
            {
              by eapply cumulative_service_le_task_cost;
                 [| by apply INfst
                | by apply H_jobs_have_valid_parameters].
            }
            {
347
              rewrite -addnBA // -[service_during _ _ _ _]addn0.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
348
              apply leq_add; last by done.
349
              by apply cumulative_service_le_delta.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
350
            }
Felix Stutz's avatar
Felix Stutz committed
351
          }
Felipe Cerqueira's avatar
Felipe Cerqueira committed
352
        Qed.
Felix Stutz's avatar
Felix Stutz committed
353

Felipe Cerqueira's avatar
Felipe Cerqueira committed
354
      End WorkloadSingleJob.
Felix Stutz's avatar
Felix Stutz committed
355

Felipe Cerqueira's avatar
Felipe Cerqueira committed
356 357
      (* Next, consider the last case where there are at least two jobs:
         the first job j_fst, and the last job j_lst. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
358 359
      Section WorkloadTwoOrMoreJobs.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
360
        (* There are at least two jobs. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
361 362
        Variable num_mid_jobs: nat.
        Hypothesis H_at_least_two_jobs : size sorted_jobs = num_mid_jobs.+2.
Felix Stutz's avatar
Felix Stutz committed
363
        
Felipe Cerqueira's avatar
Felipe Cerqueira committed
364 365 366 367
        Variable elem: JobIn arr_seq.
        Let j_fst := nth elem sorted_jobs 0.
        Let j_lst := nth elem sorted_jobs num_mid_jobs.+1.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
368
        (* The last job is an interfering job of task tsk. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
369 370
        Lemma workload_bound_j_lst_is_job_of_tsk :
          job_task j_lst = tsk /\
371
          service_during sched j_lst t1 t2 != 0 /\
Felipe Cerqueira's avatar
Felipe Cerqueira committed
372 373 374 375 376 377
          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.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
378
        (* The response time of the first job must fall inside the interval. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
379 380 381 382 383
        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.
Felix Stutz's avatar
Felix Stutz committed
384
          {
Felipe Cerqueira's avatar
Felipe Cerqueira committed
385 386
            apply mem_nth; instantiate (1 := 0).
            apply ltn_trans with (n := 1); [by done | by rewrite H_at_least_two_jobs].
Felix Stutz's avatar
Felix Stutz committed
387
          }
Felipe Cerqueira's avatar
Felipe Cerqueira committed
388 389 390
          instantiate (1 := elem); move => [FSTtsk [/eqP FSTserv FSTin]].
          apply FSTserv.
          apply (cumulative_service_after_job_rt_zero job_cost) with (R := R_tsk);
Felix Stutz's avatar
Felix Stutz committed
391
            try (by done); last by apply ltnW.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
392
          apply H_response_time_bound; first by done.
Felix Stutz's avatar
Felix Stutz committed
393
          by apply leq_trans with (n := t1); last by apply leq_addr.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
394
        Qed.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
395 396

        (* The arrival of the last job must also fall inside the interval. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
397 398 399
        Lemma workload_bound_last_job_arrives_before_end_of_interval :
          job_arrival j_lst < t2.
        Proof.
Felix Stutz's avatar
Felix Stutz committed
400
          rewrite leqNgt; apply/negP; unfold not; intro LT2.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
401 402 403 404 405 406 407 408
          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.
          }  
          instantiate (1 := elem); move => [LSTtsk [/eqP LSTserv LSTin]].
          by unfold service_during; apply LSTserv, cumulative_service_before_job_arrival_zero.
        Qed.
Felix Stutz's avatar
Felix Stutz committed
409 410

        (* Next, we upper-bound the service of the first and last jobs using their arrival times. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
411
        Lemma workload_bound_service_of_first_and_last_jobs :
412 413
          service_during sched j_fst t1 t2 +
          service_during sched j_lst t1 t2 <=
Felipe Cerqueira's avatar
Felipe Cerqueira committed
414 415
            (job_arrival j_fst  + R_tsk - t1) + (t2 - job_arrival j_lst).
        Proof.
Felix Stutz's avatar
Felix Stutz committed
416 417 418 419
          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)
420 421
                                        service_at sched j_fst t);
              last by apply leq_sum; ins; apply service_at_most_one.
Felix Stutz's avatar
Felix Stutz committed
422 423 424 425 426 427 428
            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].
            }
            {
Felipe Cerqueira's avatar
Felipe Cerqueira committed
429 430 431 432 433
              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.
              apply (cumulative_service_after_job_rt_zero job_cost) with (R := R_tsk);
Felix Stutz's avatar
Felix Stutz committed
434
                try (by done); last by apply leqnn.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
435 436 437 438
              apply H_response_time_bound; last by done.
              exploit workload_bound_all_jobs_from_tsk.
                by apply mem_nth; instantiate (1 := 0); rewrite H_at_least_two_jobs.
              by instantiate (1 := elem); move => [FSTtsk _].
Felix Stutz's avatar
Felix Stutz committed
439 440 441 442 443 444 445
            }
          }
          {
            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)
446
                                          service_at sched j_lst t);
Felix Stutz's avatar
Felix Stutz committed
447 448
                first by rewrite -> big_cat_nat with (m := job_arrival j_lst) (n := t1);
                  [by apply leq_addl | by ins | by apply leq_addr].
449
              by apply leq_sum; ins; apply service_at_most_one.
Felix Stutz's avatar
Felix Stutz committed
450 451 452
            }
            {
              apply negbT in LT; rewrite -ltnNge in LT.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
453 454 455
              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].
Felix Stutz's avatar
Felix Stutz committed
456
              rewrite /= -[\sum_(_ <= _ < _) 1]add0n; apply leq_add.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
457 458
              rewrite cumulative_service_before_job_arrival_zero;
                [by apply leqnn | by ins | by apply leqnn].
459
              by apply leq_sum; ins; apply service_at_most_one.
Felix Stutz's avatar
Felix Stutz committed
460 461
            }
          }
Felipe Cerqueira's avatar
Felipe Cerqueira committed
462 463
        Qed.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
464
        (* Simplify the expression from the previous lemma. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
465 466 467 468 469 470
        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.
Felix Stutz's avatar
Felix Stutz committed
471 472 473 474 475
          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.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
476 477 478 479 480
          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.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
481
        (* Bound the service of the middle jobs. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
482 483
        Lemma workload_bound_service_of_middle_jobs :
          \sum_(0 <= i < num_mid_jobs)
484
            service_during sched (nth elem sorted_jobs i.+1) t1 t2 <=
Felipe Cerqueira's avatar
Felipe Cerqueira committed
485 486 487
            num_mid_jobs * task_cost tsk.
        Proof.
          apply leq_trans with (n := num_mid_jobs * task_cost tsk);
Felix Stutz's avatar
Felix Stutz committed
488
            last by rewrite leq_mul2l; apply/orP; right. 
Felipe Cerqueira's avatar
Felipe Cerqueira committed
489
          apply leq_trans with (n := \sum_(0 <= i < num_mid_jobs) task_cost tsk);
Felix Stutz's avatar
Felix Stutz committed
490
            last by rewrite big_const_nat iter_addn addn0 mulnC subn0.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
491
          rewrite big_nat_cond [\sum_(0 <= i < num_mid_jobs) task_cost _]big_nat_cond.
Felix Stutz's avatar
Felix Stutz committed
492
          apply leq_sum; intros i; rewrite andbT; move => /andP LT; des.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
493 494 495 496 497 498 499 500 501 502
          eapply cumulative_service_le_task_cost;
            [by apply H_completed_jobs_dont_execute | | by apply H_jobs_have_valid_parameters].
          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).
          }
          by ins; des.
        Qed.
Felix Stutz's avatar
Felix Stutz committed
503

Felipe Cerqueira's avatar
Felipe Cerqueira committed
504
        (* Conclude that the distance between first and last is at least num_mid_jobs + 1 periods. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
505 506 507 508 509 510 511
        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.
Felix Stutz's avatar
Felix Stutz committed
512 513 514
          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.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
515 516 517 518 519 520 521 522

          (* 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.
Felix Stutz's avatar
Felix Stutz committed
523
             
Felipe Cerqueira's avatar
Felipe Cerqueira committed
524
          (* Show that both cur and next are in the arrival sequence *)
525
          assert (INnth: cur \in scheduled_jobs /\ next \in scheduled_jobs).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
526 527
          {
            rewrite 2!workload_bound_job_in_same_sequence; split.
Felix Stutz's avatar
Felix Stutz committed
528 529 530
              by apply mem_nth, (ltn_trans LT0); destruct sorted_jobs; ins.
              by apply mem_nth; destruct sorted_jobs; ins.
          }
Felipe Cerqueira's avatar
Felipe Cerqueira committed
531
          rewrite 2?mem_filter in INnth; des.
Felix Stutz's avatar
Felix Stutz committed
532

Felipe Cerqueira's avatar
Felipe Cerqueira committed
533 534 535 536 537 538 539 540 541 542 543
          (* 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).
          {
            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.
544
              by rewrite sort_uniq -/scheduled_jobs filter_uniq // undup_uniq.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
545 546 547 548 549
              by move: INnth INnth0 => /eqP INnth /eqP INnth0; rewrite INnth INnth0.  
          }
          by rewrite subh3 // addnC; move: INnth => /eqP INnth; rewrite -INnth.
        Qed.

Felix Stutz's avatar
Felix Stutz committed
550
        (* Prove that n_k is at least the number of the middle jobs *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
551 552 553 554 555
        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.
Felix Stutz's avatar
Felix Stutz committed
556 557 558 559 560 561 562 563
          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.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
564
              by apply ltnW, ltn_ceil, PARAMS0.
Felix Stutz's avatar
Felix Stutz committed
565
            }
Felipe Cerqueira's avatar
Felipe Cerqueira committed
566 567 568
            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.
Felix Stutz's avatar
Felix Stutz committed
569 570
          }
          rewrite <- leq_add2r with (p := job_arrival j_fst) in DISTmax.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
571 572 573 574 575 576
          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.
          }
Felix Stutz's avatar
Felix Stutz committed
577 578
          rewrite -subnBA // subnn subn0 in DISTmax.
          rewrite [delta + task_period tsk]addnC addnA in DISTmax.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
579
          have BEFOREt2 := workload_bound_last_job_arrives_before_end_of_interval.
Felix Stutz's avatar
Felix Stutz committed
580 581 582 583 584
          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_restricted_deadline | apply DISTmax].
Felipe Cerqueira's avatar
Felipe Cerqueira committed
585
          unfold t2; rewrite leq_add2r.
586 587 588
          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.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
589 590
        Qed.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
591 592 593
        (* 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 ->
594 595
          service_during sched j_lst t1 t2 +
            service_during sched j_fst t1 t2 +
Felipe Cerqueira's avatar
Felipe Cerqueira committed
596
            \sum_(0 <= i < num_mid_jobs)
597
             service_during sched (nth elem sorted_jobs i.+1) t1 t2
Felipe Cerqueira's avatar
Felipe Cerqueira committed
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
          <= 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. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
630 631
        Lemma workload_bound_n_k_equals_num_mid_jobs_plus_1 :
          num_mid_jobs.+1 = n_k ->
632 633
          service_during sched j_lst t1 t2 +
            service_during sched j_fst t1 t2 +
Felipe Cerqueira's avatar
Felipe Cerqueira committed
634
            \sum_(0 <= i < num_mid_jobs)
635
             service_during sched (nth elem sorted_jobs i.+1) t1 t2
Felipe Cerqueira's avatar
Felipe Cerqueira committed
636 637 638 639 640 641 642
          <= workload_bound.
        Proof.
          unfold workload_bound, W; fold n_k.
          move => NK; rewrite -NK.
          rewrite -{2}addn1 mulnDl mul1n [_* _ + _]addnC addnA addn_minl.
          apply leq_add; last by apply workload_bound_service_of_middle_jobs. 
          rewrite leq_min; apply/andP; split.
Felix Stutz's avatar
Felix Stutz committed
643
          {
Felipe Cerqueira's avatar
Felipe Cerqueira committed
644 645 646 647
            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.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
648 649
            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
650
          }
Felix Stutz's avatar
Felix Stutz committed
651 652 653 654 655 656 657 658
          {
            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].
            }
Felipe Cerqueira's avatar
Felipe Cerqueira committed
659 660 661 662 663 664 665 666 667 668 669 670
            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.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
671 672

      (* Using the lemmas above, we prove the main theorem about the workload bound. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
673 674 675
      Theorem workload_bounded_by_W :
        workload_of tsk t1 (t1 + delta) <= workload_bound.
      Proof.
676
        unfold workload_of, workload_bound, W in *; ins; des.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
677 678 679
        fold n_k.

        (* Use the definition of workload based on list of jobs. *)
680
        rewrite workload_eq_workload_joblist.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
681 682

        (* Now we order the list by job arrival time. *)
683
        rewrite workload_bound_simpl_by_sorting_scheduled_jobs.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722

        (* 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 *)
        assert (EX: exists elem: JobIn arr_seq, True).
          destruct sorted_jobs; [ by rewrite ltn0 in NUM | by exists j].
        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).
Felix Stutz's avatar
Felix Stutz committed
723 724 725
        }
      Qed.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
726
    End MainProof.
Felix Stutz's avatar
Felix Stutz committed
727 728 729
    
  End ProofWorkloadBound.

730
End WorkloadBound.