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

Felipe Cerqueira's avatar
Felipe Cerqueira committed
12
Module ResponseTimeAnalysisFP.
13

Felipe Cerqueira's avatar
Felipe Cerqueira committed
14 15
  Export JobWithJitter SporadicTaskset ScheduleOfSporadicTaskWithJitter
         Workload Interference Platform ConstrainedDeadlines Schedulability
16
         ResponseTime Priority TaskArrival WorkloadBoundJitter
Felipe Cerqueira's avatar
Felipe Cerqueira committed
17
         Interference InterferenceBoundFP.
18
    
Felipe Cerqueira's avatar
Felipe Cerqueira committed
19 20 21 22 23
  (* In this section, we prove that any fixed point in Bertogna and
     Cirinei's RTA for FP scheduling modified to account for jitter
     yields a safe response-time bound. This is an extension of the
     analysis found in Chapter 18.2 of Baruah et al.'s book
     Multiprocessor Scheduling for Real-time Systems. *)
24
  Section ResponseTimeBound.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
25

26
    Context {sporadic_task: eqType}.
27 28 29 30
    Variable task_cost: sporadic_task -> time.
    Variable task_period: sporadic_task -> time.
    Variable task_deadline: sporadic_task -> time.
    Variable task_jitter: sporadic_task -> time.
31
    
32
    Context {Job: eqType}.
33
    Variable job_arrival: Job -> time.
34 35
    Variable job_cost: Job -> time.
    Variable job_deadline: Job -> time.
36
    Variable job_task: Job -> sporadic_task.
37
    Variable job_jitter: Job -> time.
38 39
    
    (* Assume any job arrival sequence... *)
40
    Context {arr_seq: arrival_sequence Job}.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
41

Felipe Cerqueira's avatar
Felipe Cerqueira committed
42
    (* ... in which jobs arrive sporadically and have valid parameters. *)
43
    Hypothesis H_sporadic_tasks:
44
      sporadic_task_model task_period job_arrival job_task arr_seq.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
45
    Hypothesis H_valid_job_parameters:
46 47
      forall j,
        arrives_in arr_seq j ->
48 49
        valid_sporadic_job_with_jitter task_cost task_deadline task_jitter job_cost
                                       job_deadline job_task job_jitter j.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
50

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

    (* ... and that all jobs in the arrival sequence come from the task set. *)
    Hypothesis H_all_jobs_from_taskset:
61 62
      forall j,
        arrives_in arr_seq j -> job_task j \in ts.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
63

64
    (* Next, consider any schedule of this arrival sequence such that...*)
65
    Variable num_cpus: nat.
66 67
    Variable sched: schedule Job num_cpus.
    Hypothesis H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq.
68

Felipe Cerqueira's avatar
Felipe Cerqueira committed
69 70 71
    (* ...jobs are sequential, do not execute before the jitter
       has passed and nor longer than their execution costs. *)
    Hypothesis H_sequential_jobs: sequential_jobs sched.
72
    Hypothesis H_jobs_execute_after_jitter:
73
      jobs_execute_after_jitter job_arrival job_jitter sched.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
74
    Hypothesis H_completed_jobs_dont_execute:
Felipe Cerqueira's avatar
Felipe Cerqueira committed
75
      completed_jobs_dont_execute job_cost sched.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
76

Felipe Cerqueira's avatar
Felipe Cerqueira committed
77
    (* Assume that there exists at least one processor. *)
78
    Hypothesis H_at_least_one_cpu: num_cpus > 0.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
79

Felipe Cerqueira's avatar
Felipe Cerqueira committed
80 81
    (* Consider a given FP policy, ... *)
    Variable higher_eq_priority: FP_policy sporadic_task.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
82

83
    (* ...and assume that the schedule is work-conserving and respects this policy. *)
84
    Hypothesis H_work_conserving: work_conserving job_arrival job_cost job_jitter arr_seq sched.
85
    Hypothesis H_respects_priority:
86
      respects_FP_policy job_arrival job_cost job_task job_jitter arr_seq sched higher_eq_priority.
87

Felipe Cerqueira's avatar
Felipe Cerqueira committed
88
    (* Let's define some local names to avoid passing many parameters. *)
89
    Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
90
      task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched tsk.
91
    Let response_time_bounded_by (tsk: sporadic_task) :=
92
      is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched tsk.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
93

Felipe Cerqueira's avatar
Felipe Cerqueira committed
94 95 96 97
    (* Next, we consider the response-time recurrence.
       Let tsk be a task in ts that is to be analyzed. *)
    Variable tsk: sporadic_task.
    Hypothesis task_in_ts: tsk \in ts.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
98

Felipe Cerqueira's avatar
Felipe Cerqueira committed
99 100 101
    (* Let is_hp_task denote whether a task is a higher-priority task
       (with respect to tsk). *)
    Let is_hp_task := higher_priority_task higher_eq_priority tsk.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
102

Felipe Cerqueira's avatar
Felipe Cerqueira committed
103 104 105
    (* Assume a response-time bound is known... *)
    Let task_with_response_time := (sporadic_task * time)%type.
    Variable hp_bounds: seq task_with_response_time.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
106 107 108
    Hypothesis H_response_time_of_interfering_tasks_is_known:
      forall hp_tsk R,
        (hp_tsk, R) \in hp_bounds ->
109
        response_time_bounded_by hp_tsk (task_jitter hp_tsk + R).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
110 111 112 113 114 115 116 117
    
    (* ... for every higher-priority task. *)
    Hypothesis H_hp_bounds_has_interfering_tasks:
      forall hp_tsk,
        hp_tsk \in ts ->
        is_hp_task hp_tsk ->
        exists R,
          (hp_tsk, R) \in hp_bounds.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
118 119 120 121 122 123

    (* Assume that the response-time bounds are larger than task costs. *)
    Hypothesis H_response_time_bounds_ge_cost:
      forall hp_tsk R,
        (hp_tsk, R) \in hp_bounds -> R >= task_cost hp_tsk.
    
Felipe Cerqueira's avatar
Felipe Cerqueira committed
124
    (* Assume that no deadline is missed by any higher-priority task. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
125 126
    Hypothesis H_interfering_tasks_miss_no_deadlines:
      forall hp_tsk R,
Felipe Cerqueira's avatar
Felipe Cerqueira committed
127 128
        (hp_tsk, R) \in hp_bounds ->
        task_jitter hp_tsk + R <= task_deadline hp_tsk.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
129
    
Felipe Cerqueira's avatar
Felipe Cerqueira committed
130
    (* Let R be the fixed point of Bertogna and Cirinei's recurrence, ...*)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
131 132 133 134
    Variable R: time.
    Hypothesis H_response_time_recurrence_holds :
      R = task_cost tsk +
          div_floor
135
            (total_interference_bound_fp task_cost task_period task_jitter
Felipe Cerqueira's avatar
Felipe Cerqueira committed
136
                                         tsk hp_bounds R)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
137 138
            num_cpus.

139
    (* ... and assume that jitter + R is no larger than the deadline of tsk.*)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
140
    Hypothesis H_response_time_no_larger_than_deadline:
141
      task_jitter tsk + R <= task_deadline tsk.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
142

Felipe Cerqueira's avatar
Felipe Cerqueira committed
143
    (* In order to prove that R is a response-time bound, we first provide some lemmas. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
144 145 146
    Section Lemmas.

      (* Consider any job j of tsk. *)
147 148
      Variable j: Job.
      Hypothesis H_job_arrives: arrives_in arr_seq j.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
149
      Hypothesis H_job_of_tsk: job_task j = tsk.
150

151 152 153 154 155 156
      (* Let t1 be the first point in time where j can actually be scheduled. *)
      Let t1 := job_arrival j + job_jitter j.

      (* Assume that job j is the first job of tsk not to complete by the response time bound. *)
      Hypothesis H_j_not_completed: ~~ completed job_cost sched j (t1 + R).
      Hypothesis H_previous_jobs_of_tsk_completed :
157 158
        forall j0,
          arrives_in arr_seq j0 ->
159 160 161
          job_task j0 = tsk ->
          job_arrival j0 < job_arrival j ->
          completed job_cost sched j0 (job_arrival j0 + task_jitter tsk + R).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
162
      
Felipe Cerqueira's avatar
Felipe Cerqueira committed
163 164
      (* Let's call x the interference incurred by job j due to tsk_other, ...*)
      Let x (tsk_other: sporadic_task) :=
165
        task_interference job_arrival job_cost job_task job_jitter sched j tsk_other t1 (t1 + R).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
166

Felipe Cerqueira's avatar
Felipe Cerqueira committed
167
      (* ...and X the total interference incurred by job j due to any task. *)
168
      Let X := total_interference job_arrival job_cost job_jitter sched j t1 (t1 + R).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
169 170 171

      (* Recall Bertogna and Cirinei's workload bound. *)
      Let workload_bound (tsk_other: sporadic_task) (R_other: time) :=
172
        W_jitter task_cost task_period task_jitter tsk_other R_other R.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
173

Felipe Cerqueira's avatar
Felipe Cerqueira committed
174 175
      (* Let hp_tasks denote the set of higher-priority tasks. *)
      Let hp_tasks := [seq tsk_other <- ts | is_hp_task tsk_other].
Felipe Cerqueira's avatar
Felipe Cerqueira committed
176

Felipe Cerqueira's avatar
Felipe Cerqueira committed
177 178
      (* Now we establish results the higher-priority tasks. *)
      Section LemmasAboutHPTasks.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
179 180 181 182 183 184 185
        
        (* Let (tsk_other, R_other) be any pair of higher-priority task and
           response-time bound computed in previous iterations. *)
        Variable tsk_other: sporadic_task.
        Variable R_other: time.
        Hypothesis H_response_time_of_tsk_other: (tsk_other, R_other) \in hp_bounds.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
186 187
        (* Since tsk_other cannot interfere more than it executes, we show that
           the interference caused by tsk_other is no larger than workload bound W. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
188 189 190
        Lemma bertogna_fp_workload_bounds_interference :
          x tsk_other <= workload_bound tsk_other R_other.
        Proof.
191
          unfold response_time_bounded_by, is_response_time_bound_of_task,
Felipe Cerqueira's avatar
Felipe Cerqueira committed
192 193
                 completed, completed_jobs_dont_execute, valid_sporadic_job in *.
          rename H_valid_job_parameters into PARAMS,
Felipe Cerqueira's avatar
Felipe Cerqueira committed
194
                 H_all_jobs_from_taskset into FROMTS,
Felipe Cerqueira's avatar
Felipe Cerqueira committed
195
                 H_valid_task_parameters into TASK_PARAMS,
196
                 H_constrained_deadlines into RESTR,
Felipe Cerqueira's avatar
Felipe Cerqueira committed
197 198 199 200
                 H_response_time_of_interfering_tasks_is_known into RESP,
                 H_interfering_tasks_miss_no_deadlines into NOMISS,
                 H_response_time_bounds_ge_cost into GE_COST.
          unfold x, workload_bound.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219
          destruct ([exists t: 'I_(t1 + R),
                       task_is_scheduled job_task sched tsk_other t]) eqn: SCHED;
            last first.
          {
            apply negbT in SCHED; rewrite negb_exists in SCHED.
            move: SCHED => /forallP SCHED.
            apply leq_trans with (n := 0); last by done.
            apply leq_trans with (n := \sum_(t1 <= t < t1 + R) 0);
              last by rewrite big1.
            apply leq_sum_nat; move => t /andP [_ LTt] _.
            unfold t1 in LTt.
            specialize (SCHED (Ordinal LTt)).
            rewrite negb_exists in SCHED; move: SCHED => /forallP SCHED.
            rewrite big1 //; intros cpu _.
            specialize (SCHED cpu); apply negbTE in SCHED.
            by rewrite SCHED andbF.
          }
          move: SCHED => /existsP [t /existsP [cpu SCHED]].
          unfold task_scheduled_on in SCHED.
220
          destruct (sched cpu t) as [j0 |] eqn:SCHED0; last by done.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
221
          assert (INts: tsk_other \in ts).
222 223 224 225
          {
            move: SCHED => /eqP <-. apply FROMTS, (H_jobs_come_from_arrival_sequence j0 t).
            by apply/existsP; exists cpu; apply/eqP.
          }
226
          apply leq_trans with (n := workload job_task sched tsk_other t1 (t1 + R));
227 228 229
            first by apply task_interference_le_workload.
          apply workload_bounded_by_W with (task_deadline0 := task_deadline)
              (job_arrival0 := job_arrival) (arr_seq0 := arr_seq)
230
              (job_jitter0 := job_jitter) (job_cost0 := job_cost) (job_deadline0 := job_deadline);
Felipe Cerqueira's avatar
Felipe Cerqueira committed
231
            try (by ins); last 2 first;
232 233
              [ by apply NOMISS
              | by ins; rewrite -addnA; apply RESP
Felipe Cerqueira's avatar
Felipe Cerqueira committed
234
              | by ins; apply TASK_PARAMS
235
              | by ins; apply RESTR
236
              | by ins; apply GE_COST]. 
Felipe Cerqueira's avatar
Felipe Cerqueira committed
237 238
        Qed.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
239
      End LemmasAboutHPTasks.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
240

Felipe Cerqueira's avatar
Felipe Cerqueira committed
241
      (* Next we prove some lemmas that help to derive a contradiction.*)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
242 243
      Section DerivingContradiction.

244 245 246 247 248 249 250 251 252 253 254 255 256 257
        (* 0) Since job j did not complete by its response time bound, it follows that
              the total interference X >= R - e_k + 1. *)
        Lemma bertogna_fp_too_much_interference : X >= R - task_cost tsk + 1.
        Proof.
          rename H_completed_jobs_dont_execute into COMP,
                 H_valid_job_parameters into PARAMS,
                 H_response_time_recurrence_holds into REC,
                 H_job_of_tsk into JOBtsk, H_j_not_completed into NOTCOMP.
          unfold completed, valid_sporadic_job_with_jitter, valid_sporadic_job in *.
          unfold X, total_interference; rewrite addn1.
          rewrite -(ltn_add2r (task_cost tsk)).
          rewrite subh1; last by rewrite [R](REC) // leq_addr.
          rewrite -addnBA // subnn addn0.
          move: (NOTCOMP) => /negP NOTCOMP'.
258 259
          rewrite -ltnNge in NOTCOMP.

260
          apply leq_ltn_trans with (n := (\sum_(t1 <= t < t1 + R)
261
                                       backlogged job_arrival job_cost job_jitter sched j t) +
262 263 264 265
                                     service sched j (t1 + R)); last first.
          {
            rewrite -addn1 -addnA leq_add2l addn1.
            apply leq_trans with (n := job_cost j); first by done.
266
            by specialize (PARAMS j H_job_arrives); des; rewrite -JOBtsk.
267
          }
268
          unfold service.
269
          rewrite -> big_cat_nat with (n := t1) (m := 0); rewrite ?leq_addr // /=.
270
          rewrite (cumulative_service_before_jitter_zero job_arrival job_jitter) // add0n.
271 272 273 274
          rewrite -big_split /=.
          apply leq_trans with (n := \sum_(t1 <= i < t1 + R) 1);
            first by simpl_sum_const; rewrite addKn.
          apply leq_sum_nat; move => i /andP [GEi LTi] _.
275
          destruct (backlogged job_arrival job_cost job_jitter sched j i) eqn:BACK;
276 277 278 279 280 281 282 283 284 285
            first by rewrite -addn1 addnC; apply leq_add.
          apply negbT in BACK.
          rewrite add0n lt0n -not_scheduled_no_service negbK.
          rewrite /backlogged negb_and negbK in BACK.
          move: BACK => /orP [/negP NOTPENDING | SCHED]; last by done.
          exfalso; apply NOTPENDING; unfold pending; apply/andP; split; first by done.
          apply/negP; red; intro BUG; apply NOTCOMP'.
          by apply completion_monotonic with (t := i); try (by done); apply ltnW.
        Qed.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
286 287 288 289 290
        (* 1) Next, we prove that during the scheduling window of j, any job that is
              scheduled while j is backlogged comes from a different task.
              This follows from the fact that j is the first job not to complete
              by its response-time bound, so previous jobs of j's task must have
              completed by their periods and cannot be pending. *)
291 292 293
        Lemma bertogna_fp_interference_by_different_tasks :
          forall t j_other,
            t1 <= t < t1 + R ->
294 295
            arrives_in arr_seq j_other ->
            backlogged job_arrival job_cost job_jitter sched j t ->
296 297 298 299 300 301 302 303 304 305 306
            scheduled sched j_other t ->
            job_task j_other != tsk.
        Proof.
          rename H_all_jobs_from_taskset into FROMTS,
                 H_valid_job_parameters into JOBPARAMS, H_valid_task_parameters into PARAMS,
                 H_job_of_tsk into JOBtsk, H_sporadic_tasks into SPO,
                 H_work_conserving into WORK,
                 H_constrained_deadlines into CONSTR,
                 H_previous_jobs_of_tsk_completed into PREV,
                 H_response_time_no_larger_than_deadline into NOMISS.
          unfold valid_sporadic_job_with_jitter, valid_sporadic_job in *.
307
          move => t j_other /andP [LEt GEt] ARRother BACK SCHED.
308 309
          apply/eqP; red; intro SAMEtsk.
          move: SCHED => /existsP [cpu SCHED].
310
          have SCHED': scheduled sched j_other t by apply/existsP; exists cpu.
311 312
          clear SCHED; rename SCHED' into SCHED.
          move: (SCHED) => PENDING.
313 314
          apply scheduled_implies_pending with (job_arrival0 := job_arrival)
                (job_cost0 := job_cost) (job_jitter0 := job_jitter) in PENDING; try (by done).
315 316 317
          destruct (ltnP (job_arrival j_other) (job_arrival j)) as [BEFOREother | BEFOREj].
          {
            move: (BEFOREother) => LT; rewrite -(ltn_add2r R) in LT.
318
            specialize (PREV j_other ARRother SAMEtsk BEFOREother).
319 320 321 322 323 324 325 326 327 328 329
            move: PENDING => /andP [_ /negP NOTCOMP]; apply NOTCOMP.
            apply completion_monotonic with (t0 := job_arrival j_other + task_jitter tsk + R);
              try by done.
            apply leq_trans with (n := job_arrival j);
              last by apply leq_trans with (n := t1); [by apply leq_addr | by done].
            apply leq_trans with (n := job_arrival j_other + task_period tsk).
            {
              rewrite -addnA leq_add2l.
              by apply leq_trans with (n := task_deadline tsk);
                [by apply NOMISS | by apply CONSTR; rewrite -JOBtsk FROMTS].
            }
330
            rewrite -SAMEtsk; apply SPO; [ | by done | by done | by rewrite JOBtsk | by apply ltnW].
331 332 333 334
            by red; intro EQ; subst j_other; rewrite ltnn in BEFOREother.
          }
          {
            move: PENDING => /andP [ARRIVED _].
335
            exploit (SPO j j_other); try (by done); [ | by rewrite SAMEtsk | ]; last first.
336 337 338 339 340 341 342 343 344
            {
              apply/negP; rewrite -ltnNge JOBtsk.
              apply leq_trans with (n := job_arrival j + task_deadline tsk);
                last by rewrite leq_add2l; apply CONSTR; rewrite -JOBtsk FROMTS.
              apply leq_trans with (n := job_arrival j + task_jitter tsk + R);
                last by rewrite -addnA leq_add2l; apply NOMISS.
              apply leq_trans with (n := t1 + R); last first.
              {
                rewrite leq_add2r leq_add2l -JOBtsk.
345
                by specialize (JOBPARAMS j H_job_arrives); des.
346 347 348 349 350 351 352 353 354
              }
              apply leq_ltn_trans with (n := job_arrival j_other + job_jitter j_other);
                first by apply leq_addr.
              by apply leq_ltn_trans with (n := t).
            }
            by intros EQtsk; subst j_other; rewrite /backlogged SCHED andbF in BACK.
          }
        Qed.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
355 356 357 358 359 360 361 362 363 364 365
        (* Let's define a predicate to identify the other tasks that are scheduled. *)
        Let other_scheduled_task (t: time) (tsk_other: sporadic_task) :=
          task_is_scheduled job_task sched tsk_other t &&
          is_hp_task tsk_other.
      
        (* 2) Now we prove that, at all times that j is backlogged, the number
              of tasks other than tsk that are scheduled is exactly the number
              of processors in the system. This is required to prove lemma (3). *)
        Lemma bertogna_fp_all_cpus_are_busy:
          forall t,
            t1 <= t < t1 + R ->
366
            backlogged job_arrival job_cost job_jitter sched j t ->
Felipe Cerqueira's avatar
Felipe Cerqueira committed
367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384
            count (other_scheduled_task t) ts = num_cpus.
        Proof.
          rename H_valid_task_parameters into PARAMS,
                 H_job_of_tsk into JOBtsk,
                 H_all_jobs_from_taskset into FROMTS,
                 H_sporadic_tasks into SPO,
                 H_valid_job_parameters into JOBPARAMS,
                 H_constrained_deadlines into RESTR,
                 H_hp_bounds_has_interfering_tasks into HAS,
                 H_interfering_tasks_miss_no_deadlines into NOMISS,
                 H_response_time_of_interfering_tasks_is_known into PREV,
                 H_previous_jobs_of_tsk_completed into PREVtsk.
          unfold sporadic_task_model, is_response_time_bound_of_task,
                 valid_sporadic_job_with_jitter in *.
          move => t /andP [LEt LTt] BACK.

          apply platform_fp_cpus_busy_with_interfering_tasks with (task_cost0 := task_cost)
          (task_period0 := task_period) (task_deadline0 := task_deadline) (job_task0 := job_task)
385 386
          (ts0 := ts) (tsk0 := tsk) (higher_eq_priority0 := higher_eq_priority) (arr_seq0 := arr_seq)
            in BACK; try (by done); first by apply PARAMS; rewrite -JOBtsk FROMTS.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
387 388 389 390 391
          {
            apply leq_trans with (n := job_arrival j + job_jitter j + R); first by done.
            rewrite -addnA leq_add2l.
            apply leq_trans with (n := task_deadline tsk); last by apply RESTR.
            apply leq_trans with (n := task_jitter tsk + R); last by done.
392
            by rewrite leq_add2r -JOBtsk; specialize (JOBPARAMS j H_job_arrives); des.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
393 394
          }
          {
395
            intros j_other tsk_other ARRother JOBother INTERF.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
396 397 398 399
            feed (HAS tsk_other); first by rewrite -JOBother FROMTS.
            move: (HAS INTERF) => [R' IN].
            apply completion_monotonic with (t0 := job_arrival j_other + task_jitter tsk_other + R');
              try (by done); last by rewrite -addnA; apply PREV.
400 401
            rewrite -addnA leq_add2l; apply leq_trans with (n := task_deadline tsk_other);
              [by apply NOMISS | by apply RESTR; rewrite -JOBother; apply FROMTS].
Felipe Cerqueira's avatar
Felipe Cerqueira committed
402 403 404 405 406 407 408 409 410 411 412 413 414 415
          }
          {
            ins; apply completion_monotonic with (t0 := job_arrival j0 + task_jitter tsk + R);
              try (by done); last by apply PREVtsk.
            rewrite -addnA leq_add2l.
            by apply leq_trans with (n := task_deadline tsk); [by done | by apply RESTR].
          }
        Qed.

        (* 3) Now we prove that, at all times that j is backlogged, the number
              of tasks other than tsk that are scheduled is exactly the number
              of processors in the system. This is required to prove lemma (4). *)
        Lemma bertogna_fp_interference_on_all_cpus:
          \sum_(tsk_k <- hp_tasks) x tsk_k = X * num_cpus.
416
        Proof.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
417
          have DIFFTASK := bertogna_fp_interference_by_different_tasks.
418
          rename H_all_jobs_from_taskset into FROMTS,
419
                 H_valid_task_parameters into PARAMS, H_jobs_come_from_arrival_sequence into SEQ,
420
                 H_job_of_tsk into JOBtsk, H_sporadic_tasks into SPO,
421
                 H_work_conserving into WORK, H_constrained_deadlines into CONSTR,
422
                 H_previous_jobs_of_tsk_completed into PREV,
423
                 H_respects_priority into FP, H_response_time_no_larger_than_deadline into NOMISS.
424 425 426
          unfold sporadic_task_model in *.
          unfold x, X, total_interference, task_interference.
          rewrite -big_mkcond -exchange_big big_distrl /= mul1n.
427
          rewrite [\sum_(_ <= _ < _ | backlogged _ _ _ _ _ _) _]big_mkcond.
428
          apply eq_big_nat; move => t /andP [GEt LTt].
429
          destruct (backlogged job_arrival job_cost job_jitter sched j t) eqn:BACK;
430 431 432 433 434
            last by rewrite big1 //; ins; rewrite big1.
          rewrite big_mkcond /=.
          rewrite exchange_big /=.
          apply eq_trans with (y := \sum_(cpu < num_cpus) 1); last by simpl_sum_const.
          apply eq_bigr; intros cpu _.
435
          move: (WORK j t H_job_arrives BACK cpu) => [j_other /eqP SCHED]; unfold scheduled_on in *.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
436
          rewrite (bigD1_seq (job_task j_other)) /=; last by rewrite filter_uniq; destruct ts.
437 438 439 440 441 442
          {
            rewrite (eq_bigr (fun i => 0));
              last by intros i DIFF; rewrite /task_scheduled_on SCHED;apply/eqP;rewrite eqb0 eq_sym.
            simpl_sum_const; apply/eqP; rewrite eqb1.
            by unfold task_scheduled_on; rewrite SCHED.
          }
443 444
          have ARRother: arrives_in arr_seq j_other.
            by apply (SEQ j_other t); apply/existsP; exists cpu; apply/eqP.
445
          rewrite mem_filter; apply/andP; split; last by apply FROMTS.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
446
          unfold is_hp_task, higher_priority_task; apply/andP; split.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
447
          {
448 449
            rewrite -JOBtsk; apply FP with (t := t); try by done.
            by apply/existsP; exists cpu; apply/eqP.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
450
          }
451
          apply DIFFTASK with (t := t); [by auto | by done | by done |].
452 453
          by apply/existsP; exists cpu; apply/eqP.
        Qed.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
454

Felipe Cerqueira's avatar
Felipe Cerqueira committed
455 456 457
        (* Before stating the next lemma, let (num_tasks_exceeding delta) be the
           number of interfering tasks whose interference x is larger than delta. *)
        Let num_tasks_exceeding delta := count (fun i => x i >= delta) (hp_tasks).
458

Felipe Cerqueira's avatar
Felipe Cerqueira committed
459 460 461 462 463
        (* 4) Now we prove that, for any delta, if (num_task_exceeding delta > 0), then the
              cumulative interference caused by the complementary set of interfering tasks fills
              the remaining, not-completely-full (num_cpus - num_tasks_exceeding delta)
              processors. *)
        Lemma bertogna_fp_interference_in_non_full_processors :
464
          forall delta,
Felipe Cerqueira's avatar
Felipe Cerqueira committed
465 466
            0 < num_tasks_exceeding delta < num_cpus ->
            \sum_(i <- hp_tasks | x i < delta) x i >= delta * (num_cpus - num_tasks_exceeding delta).
467
        Proof.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
468
          have INV := bertogna_fp_all_cpus_are_busy.
469
          rename H_all_jobs_from_taskset into FROMTS,
470 471
                 H_valid_task_parameters into PARAMS, H_valid_job_parameters into JOBPARAMS,
                 H_job_of_tsk into JOBtsk, H_sporadic_tasks into SPO,
472 473 474
                 H_previous_jobs_of_tsk_completed into BEFOREok,
                 H_response_time_no_larger_than_deadline into NOMISS,
                 H_constrained_deadlines into CONSTR,
475 476
                 H_sequential_jobs into SEQ, H_jobs_come_from_arrival_sequence into FROMSEQ,
                 H_respects_priority into FP, H_hp_bounds_has_interfering_tasks into HASHP,
477 478 479 480 481 482
                 H_interfering_tasks_miss_no_deadlines into NOMISSHP.
          unfold sporadic_task_model, valid_sporadic_job_with_jitter, valid_sporadic_job in *.
          move => delta /andP [HAS LT]. 
          rewrite -has_count in HAS.

          set some_interference_A := fun t =>
483
            has (fun tsk_k => backlogged job_arrival job_cost job_jitter sched j t &&
484
                              (x tsk_k >= delta) &&
Felipe Cerqueira's avatar
Felipe Cerqueira committed
485
                              task_is_scheduled job_task sched tsk_k t) hp_tasks.
486
          set total_interference_B := fun t =>
487
              backlogged job_arrival job_cost job_jitter sched j t *
488
              count (fun tsk_k => (x tsk_k < delta) &&
Felipe Cerqueira's avatar
Felipe Cerqueira committed
489
                    task_is_scheduled job_task sched tsk_k t) hp_tasks.
490 491

          apply leq_trans with ((\sum_(t1 <= t < t1 + R)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
492
                                some_interference_A t) * (num_cpus - num_tasks_exceeding delta)).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
493
          {
494 495 496 497 498
            rewrite leq_mul2r; apply/orP; right.
            move: HAS => /hasP HAS; destruct HAS as [tsk_a INa LEa].
            apply leq_trans with (n := x tsk_a); first by apply LEa.
            unfold x, task_interference, some_interference_A.
            apply leq_sum_nat; move => t /andP [GEt LTt] _.
499
            destruct (backlogged job_arrival job_cost job_jitter sched j t) eqn:BACK;
500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524
              last by rewrite (eq_bigr (fun x => 0)); [by simpl_sum_const | by ins].
            destruct ([exists cpu, task_scheduled_on job_task sched tsk_a cpu t]) eqn:SCHED;
              last first.
            {
              apply negbT in SCHED; rewrite negb_exists in SCHED; move: SCHED => /forallP ALL.
              rewrite (eq_bigr (fun x => 0)); first by simpl_sum_const.
              by intros cpu _; specialize (ALL cpu); apply negbTE in ALL; rewrite ALL.
            }
            move: SCHED => /existsP [cpu SCHED].
            apply leq_trans with (n := 1); last first.
            {
              rewrite lt0b; apply/hasP; exists tsk_a; first by done.
              by rewrite LEa 2!andTb; apply/existsP; exists cpu.
            }
            rewrite (bigD1 cpu) /= // SCHED.
            rewrite (eq_bigr (fun x => 0)); first by simpl_sum_const; rewrite leq_b1.
            intros cpu' DIFF.
            apply/eqP; rewrite eqb0; apply/negP.
            intros SCHED'. 
            move: DIFF => /negP DIFF; apply DIFF; apply/eqP.
            unfold task_scheduled_on in *.
            destruct (sched cpu t) as [j1|] eqn:SCHED1; last by done.
            destruct (sched cpu' t) as [j2|] eqn:SCHED2; last by done.
            move: SCHED SCHED' => /eqP JOB /eqP JOB'.
            subst tsk_a; symmetry in JOB'.
525 526 527 528 529
            have ARR1: arrives_in arr_seq j1.
              by apply (FROMSEQ j1 t); apply/existsP; exists cpu; apply/eqP. 
            have ARR2: arrives_in arr_seq j2.
              by apply (FROMSEQ j2 t); apply/existsP; exists cpu'; apply/eqP. 
            assert (PENDING1: pending job_arrival job_cost job_jitter sched j1 t).
530 531 532 533
            {
              apply scheduled_implies_pending; try by done.
              by apply/existsP; exists cpu; apply/eqP.
            }
534
            assert (PENDING2: pending job_arrival job_cost job_jitter sched j2 t).
535 536 537 538 539 540 541 542 543 544 545
            {
              apply scheduled_implies_pending; try by done.
              by apply/existsP; exists cpu'; apply/eqP.
            }
            assert (BUG: j1 = j2).
            {
              destruct (job_task j1 == tsk) eqn:SAMEtsk.
              {
                move: SAMEtsk => /eqP SAMEtsk.
                move: (PENDING1) => SAMEjob. 
                apply platform_fp_no_multiple_jobs_of_tsk with (task_cost0 := task_cost)
546
                  (task_period0 := task_period) (task_deadline0 := task_deadline) (arr_seq0 := arr_seq)
547 548 549 550 551 552
                  (job_task0 := job_task) (tsk0 := tsk) (j0 := j) in SAMEjob; try (by done);
                  [ | by apply PARAMS | |]; last 2 first.
                {
                  apply (leq_trans LTt); rewrite -addnA leq_add2l.
                  apply leq_trans with (n := task_deadline tsk); last by apply CONSTR.
                  apply leq_trans with (n := task_jitter tsk + R); last by apply NOMISS.
553
                  by rewrite leq_add2r -JOBtsk; specialize (JOBPARAMS j H_job_arrives); des.
554 555
                }
                {
556 557 558
                  intros j0 ARR0 JOB0 LT0.
                  apply completion_monotonic with (t0 := job_arrival j0 + task_jitter tsk + R);
                    try (by done); last by apply BEFOREok.
559 560 561 562 563 564 565
                  rewrite -addnA leq_add2l.
                  by apply leq_trans with (n := task_deadline tsk); last by apply CONSTR.
                }
                move: BACK => /andP [_ /negP NOTSCHED]; exfalso; apply NOTSCHED.
                by rewrite -SAMEjob; apply/existsP; exists cpu; apply/eqP.
              }
              {
Felipe Cerqueira's avatar
Felipe Cerqueira committed
566
                assert (INTERF: is_hp_task (job_task j1)).
567 568
                {
                  apply/andP; split; last by rewrite SAMEtsk.
569
                  rewrite -JOBtsk; apply FP with (t := t); try (by done).
570 571 572
                  by apply/existsP; exists cpu; apply/eqP.
                }
                apply platform_fp_no_multiple_jobs_of_interfering_tasks with
573
                 (task_period0 := task_period) (tsk0 := tsk) (job_arrival0 := job_arrival)
574
                 (higher_eq_priority0 := higher_eq_priority) (job_jitter0 := job_jitter)
575
                 (arr_seq0 := arr_seq)
576 577 578
                 (job_cost0 := job_cost) (job_task0 := job_task) (sched0 := sched) (t0 := t);
                  rewrite ?JOBtsk ?SAMEtsk //.
                {
579
                  intros j0 tsk0 ARR0 JOB0 INTERF0.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
580 581
                  feed (HASHP tsk0); first by rewrite -JOB0 FROMTS.
                  move: (HASHP INTERF0) => [R0 IN0].
582 583 584 585 586 587 588 589
                  apply completion_monotonic with (t0 := job_arrival j0 + task_jitter tsk0 + R0);
                    try (by done).
                  {
                    rewrite -addnA leq_add2l.
                    by apply leq_trans with (n := task_deadline tsk0);
                      [by apply NOMISSHP | by apply CONSTR; rewrite -JOB0 FROMTS].
                  }
                  rewrite -addnA.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
590
                  by eapply H_response_time_of_interfering_tasks_is_known; first by apply IN0.
591 592 593 594
                }
              }
            }
            by subst j2; apply SEQ with (j := j1) (t := t).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
595
          }
596 597 598 599 600 601 602

          apply leq_trans with (\sum_(t1 <= t < t1 + R)
                                     total_interference_B t).
          {
            rewrite big_distrl /=.
            apply leq_sum_nat; move => t LEt _.
            unfold some_interference_A, total_interference_B. 
603
            destruct (backlogged job_arrival job_cost job_jitter sched j t) eqn:BACK;
604 605 606
              [rewrite mul1n /= | by rewrite has_pred0 //].

            destruct (has (fun tsk_k : sporadic_task => (delta <= x tsk_k) &&
Felipe Cerqueira's avatar
Felipe Cerqueira committed
607
                       task_is_scheduled job_task sched tsk_k t) hp_tasks) eqn:HAS';
608 609
              last by done.
            rewrite mul1n; move: HAS => /hasP [tsk_k INk LEk].
Felipe Cerqueira's avatar
Felipe Cerqueira committed
610
            unfold num_tasks_exceeding.
611 612
            apply leq_trans with (n := num_cpus -
                         count (fun i => (x i >= delta) &&
Felipe Cerqueira's avatar
Felipe Cerqueira committed
613
                            task_is_scheduled job_task sched i t) hp_tasks).
614 615 616 617 618 619 620 621
            {
              apply leq_sub2l.
              rewrite -2!sum1_count big_mkcond /=.
              rewrite [\sum_(_ <- _ | _ <= _)_]big_mkcond /=.
              apply leq_sum; intros i _.
              by destruct (task_is_scheduled job_task sched i t);
                [by rewrite andbT | by rewrite andbF].
            }
Felipe Cerqueira's avatar
Felipe Cerqueira committed
622
            rewrite -count_filter -[count _ hp_tasks]count_filter.
623 624 625
            eapply leq_trans with (n := count (predC (fun tsk => delta <= x tsk)) _);
              last by apply eq_leq, eq_in_count; red; ins; rewrite ltnNge.
            rewrite leq_subLR count_predC size_filter.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
626
            by apply leq_trans with (n := count (other_scheduled_task t) ts);
Felipe Cerqueira's avatar
Felipe Cerqueira committed
627
              [by rewrite INV | by rewrite count_filter].            
628 629 630
          }
          {
            unfold x at 2, total_interference_B.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
631
            rewrite exchange_big /=; apply leq_sum; intros t _.
632
            destruct (backlogged job_arrival job_cost job_jitter sched j t) eqn:BACK; last by ins.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
633
            rewrite mul1n -sum1_count.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
634
            rewrite big_mkcond [\sum_(i <- hp_tasks | _ < _) _]big_mkcond /=.
635 636 637 638 639 640 641 642
            apply leq_sum_seq; move => tsk_k IN _.
            destruct (x tsk_k < delta); [rewrite andTb | by rewrite andFb].
            destruct (task_is_scheduled job_task sched tsk_k t) eqn:SCHED; last by done.
            move: SCHED => /existsP [cpu SCHED].
            by rewrite (bigD1 cpu) /= // SCHED.
          }
        Qed.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
643 644 645
        (* 5) Based on lemma (4), we prove that, for any interval delta, if the sum of per-task
              interference exceeds (delta * num_cpus), the same applies for the
              sum of the minimum of the interference and delta. *)
646 647
        Lemma bertogna_fp_minimum_exceeds_interference :
          forall delta,
Felipe Cerqueira's avatar
Felipe Cerqueira committed
648 649
            \sum_(tsk_k <- hp_tasks) x tsk_k >= delta * num_cpus ->
               \sum_(tsk_k <- hp_tasks) minn (x tsk_k) delta >=
650 651 652 653 654 655 656 657 658 659 660 661 662
               delta * num_cpus.
        Proof.
          intros delta SUMLESS.
          set more_interf := fun tsk_k => x tsk_k >= delta.
          rewrite [\sum_(_ <- _) minn _ _](bigID more_interf) /=.
          unfold more_interf, minn.
          rewrite [\sum_(_ <- _ | delta <= _)_](eq_bigr (fun i => delta));
            last by intros i COND; rewrite leqNgt in COND; destruct (delta > x i).
          rewrite [\sum_(_ <- _ | ~~_)_](eq_big (fun i => x i < delta)
                                                (fun i => x i));
            [| by red; ins; rewrite ltnNge
             | by intros i COND; rewrite -ltnNge in COND; rewrite COND].

Felipe Cerqueira's avatar
Felipe Cerqueira committed
663 664
          (* Case 1: num_tasks_exceeding = 0 *)
          destruct (~~ has (fun i => delta <= x i) hp_tasks) eqn:HASa.
665 666 667
          {
            rewrite [\sum_(_ <- _ | _ <= _) _]big_hasC; last by apply HASa.
            rewrite big_seq_cond; move: HASa => /hasPn HASa.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
668 669
            rewrite add0n (eq_bigl (fun i => (i \in hp_tasks) && true));
              last by red; intros tsk_k; destruct (tsk_k \in hp_tasks) eqn:INk;
670 671 672 673
                [by rewrite andTb ltnNge; apply HASa | by rewrite andFb].
            by rewrite -big_seq_cond.
          } apply negbFE in HASa.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
674 675
          (* Case 2: num_tasks_exceeding >= num_cpus *)
          destruct (num_tasks_exceeding delta >= num_cpus) eqn:CARD.
676
          {
Felipe Cerqueira's avatar
Felipe Cerqueira committed
677
            apply leq_trans with (delta * num_tasks_exceeding delta);
678
              first by rewrite leq_mul2l; apply/orP; right.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
679
            unfold num_tasks_exceeding; rewrite -sum1_count big_distrr /=.
680 681 682 683
            rewrite -[\sum_(_ <- _ | _) _]addn0.
            by apply leq_add; [by apply leq_sum; ins; rewrite muln1|by ins].
          } apply negbT in CARD; rewrite -ltnNge in CARD.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
684 685 686 687
          (* Case 3: num_tasks_exceeding < num_cpus *)
          rewrite big_const_seq iter_addn addn0; fold num_tasks_exceeding.
          apply leq_trans with (n := delta * num_tasks_exceeding delta +
                                     delta * (num_cpus - num_tasks_exceeding delta));
688
            first by rewrite -mulnDr subnKC //; apply ltnW.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
689
          rewrite leq_add2l; apply bertogna_fp_interference_in_non_full_processors.
690 691 692
          by apply/andP; split; first by rewrite -has_count.
        Qed.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
693 694 695
        (* 6) Next, using lemmas (0), (3) and (5) we prove that the reduction-based
              interference bound is not enough to cover the sum of the minima over all tasks
              (artifact of the proof by contradiction). *)
696 697 698
        Lemma bertogna_fp_sum_exceeds_total_interference:
          \sum_((tsk_k, R_k) <- hp_bounds)
            minn (x tsk_k) (R - task_cost tsk + 1) >
Felipe Cerqueira's avatar
Felipe Cerqueira committed
699
          total_interference_bound_fp task_cost task_period task_jitter tsk hp_bounds R.
700
        Proof.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
701
          have EXCEEDS := bertogna_fp_minimum_exceeds_interference.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
702
          have ALLBUSY := bertogna_fp_interference_on_all_cpus.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
703
          have TOOMUCH := bertogna_fp_too_much_interference.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
704
          rename H_hp_bounds_has_interfering_tasks into HAS,
705
                 H_response_time_recurrence_holds into REC.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
706
          apply leq_trans with (n := \sum_(tsk_k <- hp_tasks) minn (x tsk_k) (R - task_cost tsk + 1));
707 708 709 710
            last first.
          {
            rewrite (eq_bigr (fun i => minn (x (fst i)) (R - task_cost tsk + 1)));
              last by ins; destruct i.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
711 712 713 714 715 716 717 718 719
            have MAP := @big_map _ 0 addn _ _ (fun x => fst x) hp_bounds (fun x => true) (fun y => minn (x y) (R - task_cost tsk + 1)).
            rewrite -MAP.
            apply leq_sum_sub_uniq; first by apply filter_uniq; destruct ts.
            red; move => tsk0 IN0.
            rewrite mem_filter in IN0; move: IN0 => /andP [INTERF0 IN0].
            apply/mapP.
            feed (HAS tsk0); first by done.
            move: (HAS INTERF0) => [R0 IN].
            by exists (tsk0, R0).
720 721 722 723 724 725 726 727
          }
          apply ltn_div_trunc with (d := num_cpus);
            first by apply H_at_least_one_cpu.
          unfold div_floor in REC. 
          rewrite -(ltn_add2l (task_cost tsk)) -REC.
          rewrite -addn1 -leq_subLR.
          rewrite -[R + 1 - _]subh1; last by rewrite REC; apply leq_addr.
          rewrite leq_divRL; last by apply H_at_least_one_cpu.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
728 729 730
          apply EXCEEDS.
          apply leq_trans with (n := X * num_cpus); last by rewrite ALLBUSY.
          by rewrite leq_mul2r; apply/orP; right; apply TOOMUCH.
731 732
        Qed.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
733 734 735 736 737
        (* 7) After concluding that the sum of the minima exceeds (R - e_i + 1),
              we prove that there exists a tuple (tsk_k, R_k) that satisfies
              min (x_k, R - e_i + 1) > min (W_k', R - e_i + 1).
              This implies that x_k > W_k', which is of course a contradiction,
              since W_k is a valid task interference bound. *)
738 739 740 741 742 743
        Lemma bertogna_fp_exists_task_that_exceeds_bound :
          exists tsk_k R_k,
            (tsk_k, R_k) \in hp_bounds /\
            (minn (x tsk_k) (R - task_cost tsk + 1) >
              minn (workload_bound tsk_k R_k) (R - task_cost tsk + 1)).
        Proof.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
744
          have SUM := bertogna_fp_sum_exceeds_total_interference.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
745
          rename H_hp_bounds_has_interfering_tasks into HASHP.
746 747 748 749 750 751
          assert (HAS: has (fun tup : task_with_response_time =>
                             let (tsk_k, R_k) := tup in
                               (minn (x tsk_k) (R - task_cost tsk + 1) >
                                minn (workload_bound tsk_k R_k)(R - task_cost tsk + 1)))
                            hp_bounds).
          {
Felipe Cerqueira's avatar
Felipe Cerqueira committed
752 753 754 755 756 757 758 759 760 761 762 763
              apply/negP; unfold not; intro NOTHAS.
              move: NOTHAS => /negP /hasPn ALL.
              rewrite -[_ < _]negbK in SUM.
              move: SUM => /negP SUM; apply SUM; rewrite -leqNgt.
              rewrite (eq_bigr (fun i => minn (x (fst i)) (R - task_cost tsk + 1)));
                last by ins; destruct i.
              unfold total_interference_bound_fp.
              rewrite big_seq_cond.
              rewrite [\sum_(_ <- _ | true)_]big_seq_cond.
              apply leq_sum.
              intros p; rewrite andbT; intros IN.
              by specialize (ALL p IN); destruct p; rewrite leqNgt.
764 765 766 767
          }
          move: HAS => /hasP HAS; destruct HAS as [[tsk_k R_k] HPk MINk]; exists tsk_k, R_k.
          by repeat split.
        Qed.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
768
      
Felipe Cerqueira's avatar
Felipe Cerqueira committed
769 770 771 772
      End DerivingContradiction.

    End Lemmas.
    
773
    (* Using the lemmas above, we prove that R' bounds the response time of task tsk. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
774
    Theorem bertogna_cirinei_response_time_bound_fp :
775
      response_time_bounded_by tsk (task_jitter tsk + R).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
776
    Proof.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
777 778
      have EX := bertogna_fp_exists_task_that_exceeds_bound.
      have WORKLOAD := bertogna_fp_workload_bounds_interference.
779 780
      rename H_valid_job_parameters into PARAMS.
      unfold valid_sporadic_job_with_jitter, valid_sporadic_job in *.
781
      intros j ARRj JOBtsk.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
782

783 784 785 786 787 788 789
      (* First, rewrite the claim in terms of the *absolute* response-time bound (arrival + R) *)
      remember (job_arrival j + (task_jitter tsk + R)) as ctime.
      
      (* Now, we apply strong induction on the absolute response-time bound. *)
      generalize dependent j.
      induction ctime as [ctime IH] using strong_ind.

790
      intros j ARRj JOBtsk EQc; subst ctime.
791 792

      (* First, let's simplify the induction hypothesis. *)
793 794
      assert (BEFOREok: forall j0,
                          arrives_in arr_seq j0 ->
795 796 797 798 799 800 801
                          job_task j0 = tsk ->
                          job_arrival j0 < job_arrival j ->
                          completed job_cost sched j0 (job_arrival j0 + task_jitter tsk + R)).
      {
        by ins; rewrite -addnA; apply IH; try (by done); first by rewrite ltn_add2r.
      } clear IH.
      
Felipe Cerqueira's avatar
Felipe Cerqueira committed
802
      (* Now we start the proof. Assume by contradiction that job j
803 804
         is not complete at time (job_arrival j + job_jitter j + R'). *)
      rewrite addnA.
805
      apply completion_monotonic with (t := job_arrival j + job_jitter j + R).
806 807
      {
        rewrite leq_add2r leq_add2l.
808
        specialize (PARAMS j ARRj); des.
809 810 811
        by rewrite -JOBtsk; apply PARAMS0.
      }
      destruct (completed job_cost sched j (job_arrival j + job_jitter j + R)) eqn:NOTCOMP;
Felipe Cerqueira's avatar
Felipe Cerqueira committed
812
        first by done.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
813 814 815
      apply negbT in NOTCOMP; exfalso.

      (* We derive a contradiction using the previous lemmas. *)
816
      specialize (EX j ARRj JOBtsk NOTCOMP BEFOREok).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
817
      destruct EX as [tsk_k [R_k [HPk LTmin]]].
Felipe Cerqueira's avatar
Felipe Cerqueira committed
818
      unfold minn at 1 in LTmin.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
819
      specialize (WORKLOAD j tsk_k R_k HPk).
820 821
      destruct (W_jitter task_cost task_period task_jitter tsk_k R_k R < R - task_cost tsk + 1);
        rewrite leq_min in LTmin; 
Felipe Cerqueira's avatar
Felipe Cerqueira committed
822 823
        last by move: LTmin => /andP [_ BUG]; rewrite ltnn in BUG.
      move: LTmin => /andP [BUG _]; des.
824 825
      by apply leq_trans with (p := W_jitter task_cost task_period task_jitter tsk_k R_k R) in BUG;
        first by rewrite ltnn in BUG.