bertogna_edf_comp.v 43.5 KB
Newer Older
1 2 3 4
Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas rt.util.divround.
Require Import rt.analysis.basic.bertogna_edf_theory.
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
5 6 7

Module ResponseTimeIterationEDF.

8
  Import ResponseTimeAnalysisEDF.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
9

10
  (* In this section, we define the algorithm for Bertogna and Cirinei's
Felipe Cerqueira's avatar
Felipe Cerqueira committed
11
     response-time analysis for EDF scheduling. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
12 13 14
  Section Analysis.
    
    Context {sporadic_task: eqType}.
15 16 17
    Variable task_cost: sporadic_task -> time.
    Variable task_period: sporadic_task -> time.
    Variable task_deadline: sporadic_task -> time.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
18

19
    (* As input for each iteration of the algorithm, we consider pairs
Felipe Cerqueira's avatar
Felipe Cerqueira committed
20
       of tasks and computed response-time bounds. *)
21
    Let task_with_response_time := (sporadic_task * time)%type.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
22 23
    
    Context {Job: eqType}.
24 25
    Variable job_cost: Job -> time.
    Variable job_deadline: Job -> time.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
26 27
    Variable job_task: Job -> sporadic_task.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
28
    (* Consider a platform with num_cpus processors. *)  
Felipe Cerqueira's avatar
Felipe Cerqueira committed
29 30
    Variable num_cpus: nat.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
31
    (* First, recall the interference bound under EDF, ... *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
32 33 34
    Let I (rt_bounds: seq task_with_response_time)
          (tsk: sporadic_task) (delta: time) :=
      total_interference_bound_edf task_cost task_period task_deadline tsk rt_bounds delta.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
35 36

    (* ..., which yields the following response-time bound. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
37 38
    Definition edf_response_time_bound (rt_bounds: seq task_with_response_time)
                                           (tsk: sporadic_task) (delta: time) :=
Felipe Cerqueira's avatar
Felipe Cerqueira committed
39
      task_cost tsk + div_floor (I rt_bounds tsk delta) num_cpus.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
40

Felipe Cerqueira's avatar
Felipe Cerqueira committed
41 42 43 44 45 46 47 48 49 50 51 52
    (* Also note that a response-time is only valid if it is no larger
       than the deadline. *)
    Definition R_le_deadline (pair: task_with_response_time) :=
      let (tsk, R) := pair in
        R <= task_deadline tsk.

    (* Next we define the fixed-point iteration for computing
       Bertogna's response-time bound of a task set. *)
    
    (* Given a sequence 'rt_bounds' of task and response-time bounds
       from the previous iteration, we compute the response-time
       bound of a single task using the RTA for EDF. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
53
    Definition update_bound (rt_bounds: seq task_with_response_time)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
54 55
                        (pair : task_with_response_time) :=
      let (tsk, R) := pair in
Felipe Cerqueira's avatar
Felipe Cerqueira committed
56
        (tsk, edf_response_time_bound rt_bounds tsk R).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
57

Felipe Cerqueira's avatar
Felipe Cerqueira committed
58 59 60 61 62 63 64 65
    (* To compute the response-time bounds of the entire task set,
       We start the iteration with a sequence of tasks and costs:
       <(task1, cost1), (task2, cost2), ...>. *)
    Let initial_state (ts: taskset_of sporadic_task) :=
      map (fun t => (t, task_cost t)) ts.

    (* Then, we successively update the the response-time bounds based
       on the slack computed in the previous iteration. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
66
    Definition edf_rta_iteration (rt_bounds: seq task_with_response_time) :=
Felipe Cerqueira's avatar
Felipe Cerqueira committed
67
      map (update_bound rt_bounds) rt_bounds.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
68

69 70 71
    (* To ensure that the procedure converges, we stop the iteration
       after a "sufficient" number of times, which corresponds to
       the time complexity of the procedure. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
72 73 74
    Let max_steps (ts: taskset_of sporadic_task) :=
      \sum_(tsk <- ts) (task_deadline tsk - task_cost tsk) + 1.

75 76 77
    (* This yields the following definition for the RTA. At the end
       we check if all computed response-time bounds are less than
       or equal to the deadline, in which case they are valid. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
78
    Definition edf_claimed_bounds (ts: taskset_of sporadic_task) :=
Felipe Cerqueira's avatar
Felipe Cerqueira committed
79 80 81 82
      let R_values := iter (max_steps ts) edf_rta_iteration (initial_state ts) in
        if (all R_le_deadline R_values) then
          Some R_values
        else None.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
83

Felipe Cerqueira's avatar
Felipe Cerqueira committed
84 85 86
    (* The schedulability test simply checks if we got a list of
       response-time bounds (i.e., if the computation did not fail). *)
    Definition edf_schedulable (ts: taskset_of sporadic_task) :=
Felipe Cerqueira's avatar
Felipe Cerqueira committed
87
      edf_claimed_bounds ts != None.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
88

Felipe Cerqueira's avatar
Felipe Cerqueira committed
89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112
    (* In the following section, we prove several helper lemmas about the
       list of tasks/response-time bounds. *)
    Section SimpleLemmas.

      (* Updating a single response-time bound does not modify the task. *)
      Lemma edf_claimed_bounds_unzip1_update_bound :
        forall l rt_bounds,
          unzip1 (map (update_bound rt_bounds) l) = unzip1 l.
      Proof.
        induction l; first by done.
        intros rt_bounds.
        simpl; f_equal; last by done.
        by unfold update_bound; desf.
      Qed.

      (* At any point of the iteration, the tasks are the same. *)
      Lemma edf_claimed_bounds_unzip1_iteration :
        forall l k,
          unzip1 (iter k edf_rta_iteration (initial_state l)) = l.
      Proof.
        intros l k; clear -k.
        induction k; simpl.
        {
          unfold initial_state.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
113
          induction l; first by done.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148
          by simpl; rewrite IHl.
        }
        {
          unfold edf_rta_iteration. 
          by rewrite edf_claimed_bounds_unzip1_update_bound.
        }
      Qed.

      (* The iteration preserves the size of the list. *)
      Lemma edf_claimed_bounds_size :
        forall l k,
          size (iter k edf_rta_iteration (initial_state l)) = size l.
      Proof.
        intros l k; clear -k.
        induction k; simpl; first by rewrite size_map.
        by rewrite size_map.
      Qed.

      (* If the analysis succeeds, the computed response-time bounds are no smaller
         than the task cost. *)
      Lemma edf_claimed_bounds_ge_cost :
        forall l k tsk R,
          (tsk, R) \in (iter k edf_rta_iteration (initial_state l)) ->
          R >= task_cost tsk.
      Proof.
        intros l k tsk R IN.
        destruct k.
        {
          move: IN => /mapP IN; destruct IN as [x IN EQ]; inversion EQ.
          by apply leqnn.
        }
        {
          rewrite iterS in IN.
          move: IN => /mapP IN; destruct IN as [x IN EQ].
          unfold update_bound in EQ; destruct x; inversion EQ.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
149
          by unfold edf_response_time_bound; apply leq_addr.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194
        }
      Qed.

      (* If the analysis suceeds, the computed response-time bounds are no larger
         than the deadline. *)
      Lemma edf_claimed_bounds_le_deadline :
        forall ts rt_bounds tsk R,
          edf_claimed_bounds ts = Some rt_bounds ->
          (tsk, R) \in rt_bounds ->
          R <= task_deadline tsk.
      Proof.
        intros ts rt_bounds tsk R SOME PAIR; unfold edf_claimed_bounds in SOME.
        destruct (all R_le_deadline (iter (max_steps ts)
                                          edf_rta_iteration (initial_state ts))) eqn:DEADLINE;
          last by done.
        move: DEADLINE => /allP DEADLINE.
        inversion SOME as [EQ]; rewrite -EQ in PAIR.
        by specialize (DEADLINE (tsk, R) PAIR).
      Qed.

      (* The list contains a response-time bound for every task in the task set. *)
      Lemma edf_claimed_bounds_has_R_for_every_task :
        forall ts rt_bounds tsk,
          edf_claimed_bounds ts = Some rt_bounds ->
          tsk \in ts ->
          exists R,
            (tsk, R) \in rt_bounds.
      Proof.
        intros ts rt_bounds tsk SOME IN.
        unfold edf_claimed_bounds in SOME.
        destruct (all R_le_deadline (iter (max_steps ts) edf_rta_iteration (initial_state ts)));
          last by done.
        inversion SOME as [EQ]; clear SOME EQ.
        generalize dependent tsk.
        induction (max_steps ts) as [| step]; simpl in *.
        {
          intros tsk IN; unfold initial_state.
          exists (task_cost tsk).
          by apply/mapP; exists tsk.
        }
        {
          intros tsk IN.
          set prev_state := iter step edf_rta_iteration (initial_state ts).
          fold prev_state in IN, IHstep.
          specialize (IHstep tsk IN); des.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
195
          exists (edf_response_time_bound prev_state tsk R).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
196 197 198 199 200 201
          by apply/mapP; exists (tsk, R); [by done | by f_equal].
        }
      Qed.
     
    End SimpleLemmas.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
202 203 204 205
    (* In this section, we prove the convergence of the RTA procedure.
       Since we define the RTA procedure as the application of a function
       a fixed number of times, this translates into proving that the value
       of the iteration at (max_steps ts) is equal to the value at (max_steps ts) + 1. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240
    Section Convergence.

      (* Consider any valid task set. *)
      Variable ts: taskset_of sporadic_task.
      Hypothesis H_valid_task_parameters:
        valid_sporadic_taskset task_cost task_period task_deadline ts.
      
      (* To simplify, let f denote the RTA procedure. *)
      Let f (k: nat) := iter k edf_rta_iteration (initial_state ts).

      (* Since the iteration is applied directly to a list of tasks and response-times,
         we define a corresponding relation "<=" over those lists. *)

      (* Let 'all_le' be a binary relation over lists of tasks/response-time bounds.
         It states that every element of list l1 has a response-time bound R that is less
         than or equal to the corresponding response-time bound R' in list l2 (point-wise).
         In addition, the relation states that the tasks of both lists are unchanged. *)
      Let all_le := fun (l1 l2: list task_with_response_time) =>
        (unzip1 l1 == unzip1 l2) &&
        all (fun p => (snd (fst p)) <= (snd (snd p))) (zip l1 l2).

      (* Similarly, we define a strict version of 'all_le' called 'one_lt', which states that
         there exists at least one element whose response-time bound increases. *)
      Let one_lt := fun (l1 l2: list task_with_response_time) =>
        (unzip1 l1 == unzip1 l2) &&
        has (fun p => (snd (fst p)) < (snd (snd p))) (zip l1 l2).

      (* Next, we prove some basic properties about the relation all_le. *)
      Section RelationProperties.

        (* The relation is reflexive, ... *)
        Lemma all_le_reflexive : reflexive all_le.
        Proof.
          intros l; unfold all_le; rewrite eq_refl andTb.
          destruct l; first by done.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
241
          by apply/(zipP (fun x y => snd x <= snd y)).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
242 243
        Qed.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
244 245
        (* ... and transitive. *)
        Lemma all_le_transitive: transitive all_le.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
246
        Proof.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
247 248 249 250 251 252 253 254 255 256 257
          unfold transitive, all_le.
          move => y x z /andP [/eqP ZIPxy LExy] /andP [/eqP ZIPyz LEyz].
          apply/andP; split; first by rewrite ZIPxy -ZIPyz.
          move: LExy => /(zipP (fun x y => snd x <= snd y)) LExy.
          move: LEyz => /(zipP (fun x y => snd x <= snd y)) LEyz.
          assert (SIZExy: size (unzip1 x) = size (unzip1 y)).
            by rewrite ZIPxy.
          assert (SIZEyz: size (unzip1 y) = size (unzip1 z)).
            by rewrite ZIPyz.
          rewrite 2!size_map in SIZExy; rewrite 2!size_map in SIZEyz.
          destruct y.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
258
          {
Felipe Cerqueira's avatar
Felipe Cerqueira committed
259 260
            apply size0nil in SIZExy; symmetry in SIZEyz.
            by apply size0nil in SIZEyz; subst.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
261
          }
Felipe Cerqueira's avatar
Felipe Cerqueira committed
262 263 264 265
          apply/(zipP (fun x y => snd x <= snd y));
            [by apply (t, 0) | by rewrite SIZExy -SIZEyz|]. 
          intros i LTi.
          exploit LExy; first by rewrite SIZExy.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
266
          {
Felipe Cerqueira's avatar
Felipe Cerqueira committed
267 268
            rewrite size_zip -SIZEyz -SIZExy minnn in LTi.
            by rewrite size_zip -SIZExy minnn; apply LTi.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
269
          }
Felipe Cerqueira's avatar
Felipe Cerqueira committed
270 271 272 273 274 275 276
          instantiate (1 := t); intro LE.
          exploit LEyz; first by apply SIZEyz.
          {
            rewrite size_zip SIZExy SIZEyz minnn in LTi.
            by rewrite size_zip SIZEyz minnn; apply LTi.
          }
          by instantiate (1 := t); intro LE'; apply (leq_trans LE).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
277 278
        Qed.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
279 280 281 282
        (* At any step of the iteration, the corresponding list
           is larger than or equal to the initial state. *)
        Lemma bertogna_edf_comp_iteration_preserves_minimum :
          forall step, all_le (initial_state ts) (f step). 
Felipe Cerqueira's avatar
Felipe Cerqueira committed
283
        Proof.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318
          unfold f.
          intros step; destruct step; first by apply all_le_reflexive.
          apply/andP; split.
          {
            assert (UNZIP0 := edf_claimed_bounds_unzip1_iteration ts 0).
            by simpl in UNZIP0; rewrite UNZIP0 edf_claimed_bounds_unzip1_iteration.
          }  
          destruct ts as [| tsk0 ts'].
          {
            clear -step; induction step; first by done.
            by rewrite iterSr IHstep.
          }

          apply/(zipP (fun x y => snd x <= snd y));
            [by apply (tsk0,0)|by rewrite edf_claimed_bounds_size size_map |].

          intros i LTi; rewrite iterS; unfold edf_rta_iteration at 1.
          have MAP := @nth_map _ (tsk0,0) _ (tsk0,0).
          rewrite size_zip edf_claimed_bounds_size size_map minnn in LTi.
          rewrite MAP; clear MAP; last by rewrite edf_claimed_bounds_size.
          destruct (nth (tsk0, 0) (initial_state (tsk0 :: ts')) i) as [tsk_i R_i] eqn:SUBST.
          rewrite SUBST; unfold update_bound.
          unfold initial_state in SUBST.
          have MAP := @nth_map _ tsk0 _ (tsk0, 0).
          rewrite ?MAP // in SUBST; inversion SUBST; clear MAP. 
          assert (EQtsk: tsk_i = fst (nth (tsk0, 0) (iter step edf_rta_iteration
                                                         (initial_state (tsk0 :: ts'))) i)).
          {
            have MAP := @nth_map _ (tsk0,0) _ tsk0 (fun x => fst x).
            rewrite -MAP; clear MAP; last by rewrite edf_claimed_bounds_size.
            have UNZIP := edf_claimed_bounds_unzip1_iteration; unfold unzip1 in UNZIP.
            by rewrite UNZIP; symmetry. 
          }
          destruct (nth (tsk0, 0) (iter step edf_rta_iteration (initial_state (tsk0 :: ts')))) as [tsk_i' R_i'].
          by simpl in EQtsk; rewrite -EQtsk; subst; apply leq_addr.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
319
        Qed.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
320

321 322 323 324 325 326 327 328 329
        (* The application of the function is inductive. *)
        Lemma bertogna_edf_comp_iteration_inductive (P : seq task_with_response_time -> Type) :
          P (initial_state ts) ->
          (forall k, P (f k) -> P (f (k.+1))) ->
          P (f (max_steps ts)).
        Proof.
          by intros P0 Pn; induction (max_steps ts); last by apply Pn.
        Qed.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
330 331 332 333 334 335 336 337
        (* As a last step, we show that edf_rta_iteration preserves order, i.e., for any
           list l1 no smaller than the initial state, and list l2 such that
           l1 <= l2, we have (edf_rta_iteration l1) <= (edf_rta_iteration l2). *)
        Lemma bertogna_edf_comp_iteration_preserves_order :
          forall l1 l2,
            all_le (initial_state ts) l1 ->
            all_le l1 l2 ->
            all_le (edf_rta_iteration l1) (edf_rta_iteration l2).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
338
        Proof.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
339 340 341 342 343
          rename H_valid_task_parameters into VALID.
          intros x1 x2 LEinit LE.
          move: LE => /andP [/eqP ZIP LE]; unfold all_le.

          assert (UNZIP': unzip1 (edf_rta_iteration x1) = unzip1 (edf_rta_iteration x2)).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
344
          {
Felipe Cerqueira's avatar
Felipe Cerqueira committed
345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367
            by rewrite 2!edf_claimed_bounds_unzip1_update_bound.
          }

          apply/andP; split; first by rewrite UNZIP'.
          apply f_equal with (B := nat) (f := fun x => size x) in UNZIP'.
          rename UNZIP' into SIZE.
          rewrite size_map [size (unzip1 _)]size_map in SIZE.
          move: LE => /(zipP (fun x y => snd x <= snd y)) LE.
          destruct x1 as [| p0 x1'], x2 as [| p0' x2']; try (by ins).
          apply/(zipP (fun x y => snd x <= snd y));
            [by apply (p0,0) | by done |].

          intros i LTi.
          exploit LE; first by rewrite 2!size_map in SIZE.
          {
            by rewrite size_zip 2!size_map -size_zip in LTi; apply LTi.
          }
          rewrite 2!size_map in SIZE.
          instantiate (1 := p0); intro LEi.
          rewrite (nth_map p0);
            last by rewrite size_zip 2!size_map -SIZE minnn in LTi.
          rewrite (nth_map p0);
            last by rewrite size_zip 2!size_map SIZE minnn in LTi.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
368
          unfold update_bound, edf_response_time_bound; desf; simpl.
369
          rename s into tsk_i, s0 into tsk_i', t into R_i, t0 into R_i', Heq into EQ, Heq0 into EQ'.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
370 371 372 373 374 375 376
          assert (EQtsk: tsk_i = tsk_i').
          {
            destruct p0 as [tsk0 R0], p0' as [tsk0' R0']; simpl in H2; subst.
            have MAP := @nth_map _ (tsk0',R0) _ tsk0' (fun x => fst x) i ((tsk0', R0) :: x1').
            have MAP' := @nth_map _ (tsk0',R0) _ tsk0' (fun x => fst x) i ((tsk0', R0') :: x2').
            assert (FSTeq: fst (nth (tsk0', R0)((tsk0', R0) :: x1') i) =
                           fst (nth (tsk0',R0) ((tsk0', R0') :: x2') i)).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
377
            {
Felipe Cerqueira's avatar
Felipe Cerqueira committed
378 379 380 381 382
              rewrite -MAP;
                last by simpl; rewrite size_zip 2!size_map /= -H0 minnn in LTi.
              rewrite -MAP';
                last by simpl; rewrite size_zip 2!size_map /= H0 minnn in LTi.
              by f_equal; simpl; f_equal.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
383
            }
Felipe Cerqueira's avatar
Felipe Cerqueira committed
384 385 386 387 388 389 390 391 392 393 394 395 396 397 398
            apply f_equal with (B := sporadic_task) (f := fun x => fst x) in EQ.
            apply f_equal with (B := sporadic_task) (f := fun x => fst x) in EQ'.
            by rewrite FSTeq EQ' /= in EQ; rewrite EQ.
          }
          subst tsk_i'; rewrite leq_add2l.
          unfold I, total_interference_bound_edf; apply leq_div2r.
          rewrite 2!big_cons.
          destruct p0 as [tsk0 R0], p0' as [tsk0' R0'].
          simpl in H2; subst tsk0'.
          rename R_i into delta, R_i' into delta'.
          rewrite EQ EQ' in LEi; simpl in LEi.
          rename H0 into SIZE, H1 into UNZIP; clear EQ EQ'.

          assert (SUBST: forall l delta,
                    \sum_(j <- l | let '(tsk_other, _) := j in
399
                      jldp_can_interfere_with tsk_i tsk_other)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
400 401 402
                        (let '(tsk_other, R_other) := j in
                          interference_bound_edf task_cost task_period task_deadline tsk_i delta
                            (tsk_other, R_other)) =
403
                    \sum_(j <- l | jldp_can_interfere_with tsk_i (fst j))
Felipe Cerqueira's avatar
Felipe Cerqueira committed
404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429
                      interference_bound_edf task_cost task_period task_deadline tsk_i delta j).
          {
            intros l x; clear -l.
            induction l; first by rewrite 2!big_nil.
            by rewrite 2!big_cons; rewrite IHl; desf; rewrite /= Heq in Heq0.
          } rewrite 2!SUBST; clear SUBST.

          assert (VALID': valid_sporadic_taskset task_cost task_period task_deadline
                                                       (unzip1 ((tsk0, R0) :: x1'))).
          {
            move: LEinit => /andP [/eqP EQinit _].
            rewrite -EQinit; unfold valid_sporadic_taskset.
            move => tsk /mapP IN. destruct IN as [p INinit EQ]; subst.
            by move: INinit => /mapP INinit; destruct INinit as [tsk INtsk]; subst; apply VALID.
          }

          assert (GE_COST: all (fun p => task_cost (fst p) <= snd p) ((tsk0, R0) :: x1')). 
          {
            clear LE; move: LEinit => /andP [/eqP UNZIP' LE].
            move: LE => /(zipP (fun x y => snd x <= snd y)) LE.
            specialize (LE (tsk0, R0)).
            apply/(all_nthP (tsk0,R0)).
            intros j LTj; generalize UNZIP'; simpl; intro SIZE'.
            have F := @f_equal _ _ size (unzip1 (initial_state ts)).
            apply F in SIZE'; clear F; rewrite /= 3!size_map in SIZE'.
            exploit LE; [by rewrite size_map /= | |].
Felipe Cerqueira's avatar
Felipe Cerqueira committed
430
            {
Felipe Cerqueira's avatar
Felipe Cerqueira committed
431 432
              rewrite size_zip size_map /= SIZE' minnn.
              by simpl in LTj; apply LTj.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
433
            }
Felipe Cerqueira's avatar
Felipe Cerqueira committed
434 435 436 437 438 439 440 441 442 443 444
            clear LE; intro LE.
            unfold initial_state in LE.
            have MAP := @nth_map _ tsk0 _ (tsk0,R0).
            rewrite MAP /= in LE;
              [clear MAP | by rewrite SIZE'; simpl in LTj].
            apply leq_trans with (n := task_cost (nth tsk0 ts j));
              [apply eq_leq; f_equal | by done].
            have MAP := @nth_map _ (tsk0, R0) _ tsk0 (fun x => fst x).
            rewrite -MAP; [clear MAP | by done].
            unfold unzip1 in UNZIP'; rewrite -UNZIP'; f_equal.
            clear -ts; induction ts; [by done | by simpl; f_equal].
Felipe Cerqueira's avatar
Felipe Cerqueira committed
445
          }
Felipe Cerqueira's avatar
Felipe Cerqueira committed
446 447
          move: GE_COST => /allP GE_COST.

448 449
          assert (LESUM: \sum_(j <- x1' | jldp_can_interfere_with tsk_i (fst j))
                        interference_bound_edf task_cost task_period task_deadline tsk_i delta j <=                                  \sum_(j <- x2' | jldp_can_interfere_with tsk_i (fst j))
Felipe Cerqueira's avatar
Felipe Cerqueira committed
450
                        interference_bound_edf task_cost task_period task_deadline tsk_i delta' j).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
451
          {
Felipe Cerqueira's avatar
Felipe Cerqueira committed
452 453
            set elem := (tsk0, R0); rewrite 2!(big_nth elem).
            rewrite -SIZE.
454
            rewrite big_mkcond [\sum_(_ <- _ | jldp_can_interfere_with _ _)_]big_mkcond.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
455 456 457 458 459 460 461 462
            rewrite big_seq_cond [\sum_(_ <- _ | true) _]big_seq_cond.
            apply leq_sum; intros j; rewrite andbT; intros INj.
            rewrite mem_iota add0n subn0 in INj; move: INj => /andP [_ INj].
            assert (FSTeq: fst (nth elem x1' j) = fst (nth elem x2' j)).
            {
              have MAP := @nth_map _ elem _ tsk0 (fun x => fst x).
              by rewrite -2?MAP -?SIZE //; f_equal.
            } rewrite -FSTeq.
463
            destruct (jldp_can_interfere_with tsk_i (fst (nth elem x1' j))) eqn:INTERF;
Felipe Cerqueira's avatar
Felipe Cerqueira committed
464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481
              last by done.
            {
              exploit (LE elem); [by rewrite /= SIZE | | intro LEj].
              {
                rewrite size_zip 2!size_map /= -SIZE minnn in LTi.
                by rewrite size_zip /= -SIZE minnn; apply (leq_ltn_trans INj).
              }
              simpl in LEj.
              exploit (VALID' (fst (nth elem x1' j))); last intro VALIDj.
              {
                apply/mapP; exists (nth elem x1' j); last by done.
                by rewrite in_cons; apply/orP; right; rewrite mem_nth.
              }
              exploit (GE_COST (nth elem x1' j)); last intro GE_COSTj.
              {
                by rewrite in_cons; apply/orP; right; rewrite mem_nth.
              }
              unfold is_valid_sporadic_task in *.
482 483 484
              destruct (nth elem x1' j) as [tsk_j R_j] eqn:SUBST1,
                       (nth elem x2' j) as [tsk_j' R_j'] eqn:SUBST2.
              rewrite SUBST1 SUBST2 in LEj; clear SUBST1 SUBST2.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
485 486 487 488
              simpl in FSTeq; rewrite -FSTeq; simpl in LEj; simpl in VALIDj; des.
              by apply interference_bound_edf_monotonic.
            }
          }
489
          destruct (jldp_can_interfere_with tsk_i tsk0) eqn:INTERFtsk0; last by done.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
490 491 492 493 494 495 496 497
          apply leq_add; last by done.
          {             
            exploit (LE (tsk0, R0)); [by rewrite /= SIZE | | intro LEj];
              first by instantiate (1 := 0); rewrite size_zip /= -SIZE minnn.
            exploit (VALID' tsk0); first by rewrite in_cons; apply/orP; left.
            exploit (GE_COST (tsk0, R0)); first by rewrite in_cons eq_refl orTb.
            unfold is_valid_sporadic_task; intros GE_COST0 VALID0; des; simpl in LEj.
            by apply interference_bound_edf_monotonic.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
498 499 500
          }
        Qed.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526
        (* It follows from the properties above that the iteration is monotonically increasing. *)
        Lemma bertogna_edf_comp_iteration_monotonic: forall k, all_le (f k) (f k.+1).
        Proof.
          unfold f; intros k.
          apply fun_mon_iter_mon_generic with (x1 := k) (x2 := k.+1);
            try (by done);
            [ by apply all_le_reflexive
            | by apply all_le_transitive
            | by apply bertogna_edf_comp_iteration_preserves_order
            | by apply bertogna_edf_comp_iteration_preserves_minimum].
        Qed.

      End RelationProperties.

      (* Knowing that the iteration is monotonically increasing (with respect to all_le),
         we show that the RTA procedure converges to a fixed point. *)

      (* First, note that when there are no tasks, the iteration trivially converges. *)
      Lemma bertogna_edf_comp_f_converges_with_no_tasks :
        size ts = 0 ->
        f (max_steps ts) = f (max_steps ts).+1.
      Proof.
        intro SIZE; destruct ts; last by inversion SIZE.
        unfold max_steps; rewrite big_nil /=.
        by unfold edf_rta_iteration.
      Qed.
527

Felipe Cerqueira's avatar
Felipe Cerqueira committed
528 529
      (* Otherwise, if the iteration reached a fixed point before (max_steps ts), then
         the value at (max_steps ts) is still at a fixed point. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552
      Lemma bertogna_edf_comp_f_converges_early :
        (exists k, k <= max_steps ts /\ f k = f k.+1) ->
        f (max_steps ts) = f (max_steps ts).+1.
      Proof.
        by intros EX; des; apply iter_fix with (k := k).
      Qed.

      (* Else, we derive a contradiction. *)
      Section DerivingContradiction.

        (* Assume that there are tasks. *)
        Hypothesis H_at_least_one_task: size ts > 0.

        (* Assume that the iteration continued to diverge. *)
        Hypothesis H_keeps_diverging:
          forall k,
            k <= max_steps ts -> f k != f k.+1.

        (* Since the iteration is monotonically increasing, it must be
           strictly increasing. *)
        Lemma bertogna_edf_comp_f_increases :
          forall k,
            k <= max_steps ts -> one_lt (f k) (f k.+1).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
553
        Proof.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
554 555 556 557 558 559 560 561
          rename H_at_least_one_task into NONEMPTY.
          intros step LEstep; unfold one_lt; apply/andP; split;
            first by rewrite 2!edf_claimed_bounds_unzip1_iteration.
          rewrite -[has _ _]negbK; apply/negP; unfold not; intro ALL.
          rewrite -all_predC in ALL.
          move: ALL => /allP ALL.
          exploit (H_keeps_diverging step); [by done | intro DIFF].
          assert (DUMMY: exists tsk: sporadic_task, True).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
562
          {
Felipe Cerqueira's avatar
Felipe Cerqueira committed
563 564
            destruct ts as [|tsk0]; first by rewrite ltnn in NONEMPTY.
            by exists tsk0.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
565
          }
Felipe Cerqueira's avatar
Felipe Cerqueira committed
566 567 568 569
          des; clear DUMMY.
          move: DIFF => /eqP DIFF; apply DIFF.
          apply eq_from_nth with (x0 := (tsk, 0));
            first by simpl; rewrite size_map.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
570
          {
Felipe Cerqueira's avatar
Felipe Cerqueira committed
571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606
            intros i LTi.
            remember (nth (tsk, 0)(f step) i) as p_i;rewrite -Heqp_i.
            remember (nth (tsk, 0)(f step.+1) i) as p_i';rewrite -Heqp_i'.
            rename Heqp_i into EQ, Heqp_i' into EQ'.
            exploit (ALL (p_i, p_i')).
            {
              rewrite EQ EQ'.
              rewrite -nth_zip; last by unfold f; rewrite iterS size_map.
              apply mem_nth; rewrite size_zip.
              unfold f; rewrite iterS size_map.
              by rewrite minnn.
            }
            unfold predC; simpl; rewrite -ltnNge; intro LTp.

            have GROWS := bertogna_edf_comp_iteration_monotonic step.
            move: GROWS => /andP [_ /allP GROWS].
            exploit (GROWS (p_i, p_i')).
            {
              rewrite EQ EQ'.
              rewrite -nth_zip; last by unfold f; rewrite iterS size_map.
              apply mem_nth; rewrite size_zip.
              unfold f; rewrite iterS size_map.
              by rewrite minnn.
            }
            simpl; intros LE.
            destruct p_i as [tsk_i R_i], p_i' as [tsk_i' R_i'].
            simpl in *.
            assert (EQtsk: tsk_i = tsk_i').
            {
              unfold edf_rta_iteration in EQ'.
              rewrite (nth_map (tsk, 0)) in EQ'; last by done.
              by unfold update_bound in EQ'; desf.
            }
            rewrite EQtsk; f_equal.
            by apply/eqP; rewrite eqn_leq; apply/andP; split.
          }
Felipe Cerqueira's avatar
Felipe Cerqueira committed
607 608
        Qed.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
609 610 611 612 613 614 615
        (* In the end, each response-time bound is so high that the sum
           of all response-time bounds exceeds the sum of all deadlines.
           Contradiction! *)
        Lemma bertogna_edf_comp_rt_grows_too_much :
          forall k,
            k <= max_steps ts ->
            \sum_((tsk, R) <- f k) (R - task_cost tsk) + 1 > k.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
616
        Proof.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
617 618 619 620 621
          rename H_at_least_one_task into NONEMPTY.
          unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
          rename H_valid_task_parameters into VALID.
          intros step LE.
          assert (DUMMY: exists tsk: sporadic_task, True).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
622
          {
Felipe Cerqueira's avatar
Felipe Cerqueira committed
623 624 625 626 627 628 629
            destruct ts as [|tsk0]; first by rewrite ltnn in NONEMPTY.
            by exists tsk0.
          } destruct DUMMY as [elem _].

          induction step.
          {
            by rewrite addn1.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
630 631
          }
          {
Felipe Cerqueira's avatar
Felipe Cerqueira committed
632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659
            rewrite -addn1 ltn_add2r.
            apply leq_ltn_trans with (n := \sum_(i <- f step) (let '(tsk, R) := i in R - task_cost tsk)).
            {
              rewrite -ltnS; rewrite addn1 in IHstep.
              by apply IHstep, ltnW.
            }
            rewrite (eq_bigr (fun x => snd x - task_cost (fst x)));
              last by ins; destruct i.
            rewrite [\sum_(_ <- f step.+1)_](eq_bigr (fun x => snd x - task_cost (fst x)));
              last by ins; destruct i.
            unfold f at 2; rewrite iterS.
            rewrite big_map; fold (f step).
            rewrite -(ltn_add2r (\sum_(i <- f step) task_cost (fst i))).
            rewrite -2!big_split /=.
            rewrite big_seq_cond [\sum_(_ <- _ | true)_]big_seq_cond.
            rewrite (eq_bigr (fun i => snd i)); last first.
            {
              intro i; rewrite andbT; intro IN;
              rewrite subh1; first by rewrite -addnBA // subnn addn0.
              have GE_COST := edf_claimed_bounds_ge_cost ts step.
              by destruct i; apply GE_COST.
            }
            rewrite [\sum_(_ <- _ | _)(_ - _ + _)](eq_bigr (fun i => snd (update_bound (f step) i))); last first.
            {
              intro i; rewrite andbT; intro IN.
              unfold update_bound; destruct i; simpl.
              rewrite subh1; first by rewrite -addnBA // subnn addn0.
              apply (edf_claimed_bounds_ge_cost ts step.+1).
660
              by rewrite iterS; apply/mapP; exists (s, t).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713
            }
            rewrite -2!big_seq_cond.
           
            have LT := bertogna_edf_comp_f_increases step (ltnW LE).
            have MONO := bertogna_edf_comp_iteration_monotonic step.
            
            move: LT => /andP [_ LT]; move: LT => /hasP LT.
            destruct LT as [[x1 x2] INzip LT]; simpl in *.
            move: MONO => /andP [_ /(zipP (fun x y => snd x <= snd y)) MONO].
            rewrite 2!(big_nth (elem, 0)).
            apply mem_zip_exists with (elem := (elem, 0)) (elem' := (elem, 0)) in INzip; des;
              last by rewrite size_map.
            rewrite -> big_cat_nat with (m := 0) (n := idx) (p := size (f step));
              [simpl | by done | by apply ltnW].
            rewrite -> big_cat_nat with (m := idx) (n := idx.+1) (p := size (f step));
              [simpl | by done | by done].
            rewrite big_nat_recr /=; last by done.
            rewrite -> big_cat_nat with (m := 0) (n := idx) (p := size (f step));
              [simpl | by done | by apply ltnW].
            rewrite -> big_cat_nat with (m := idx) (n := idx.+1) (p := size (f step));
              [simpl | by done | by done].
            rewrite big_nat_recr /=; last by done.
            rewrite [\sum_(idx <= i < idx) _]big_geq // add0n.
            rewrite [\sum_(idx <= i < idx) _]big_geq // add0n.
            rewrite -addn1 -addnA; apply leq_add.
            {
              rewrite big_nat_cond [\sum_(_ <= _ < _ | true) _]big_nat_cond.
              apply leq_sum; move => i /andP [/andP [LT1 LT2] _].
              exploit (MONO (elem,0)); [by rewrite size_map | | intro LEi].
              {
                rewrite size_zip; apply (ltn_trans LT2).
                by apply leq_trans with (n := size (f step));
                  [by done | by rewrite size_map minnn].
              }
              unfold edf_rta_iteration in LEi.
              by rewrite -> nth_map with (x1 := (elem, 0)) in LEi;
                last by apply (ltn_trans LT2).
            }
            rewrite -addnA [_ + 1]addnC addnA; apply leq_add.
            {
              unfold edf_rta_iteration in INzip2; rewrite addn1.
              rewrite -> nth_map with (x1 := (elem, 0)) in INzip2; last by done.
              by rewrite -INzip2 -INzip1.
            }
            {
              rewrite big_nat_cond [\sum_(_ <= _ < _ | true) _]big_nat_cond.
              apply leq_sum; move => i /andP [/andP [LT1 LT2] _].
              exploit (MONO (elem,0));
                [ by rewrite size_map
                | by rewrite size_zip; apply (leq_trans LT2); rewrite size_map minnn | intro LEi ].
              unfold edf_rta_iteration in LEi.
              by rewrite -> nth_map with (x1 := (elem, 0)) in LEi; last by done.
            }
Felipe Cerqueira's avatar
Felipe Cerqueira committed
714 715
          }
        Qed.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
716 717 718

      End DerivingContradiction. 

719 720 721
      (* Using the lemmas above, we prove that edf_rta_iteration reaches
         a fixed point after (max_steps ts) step, ... *)
      Lemma edf_claimed_bounds_finds_fixed_point_of_list :
Felipe Cerqueira's avatar
Felipe Cerqueira committed
722 723 724
        forall rt_bounds,
          edf_claimed_bounds ts = Some rt_bounds ->
          valid_sporadic_taskset task_cost task_period task_deadline ts ->
725
          f (max_steps ts) = edf_rta_iteration (f (max_steps ts)). 
Felipe Cerqueira's avatar
Felipe Cerqueira committed
726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804
      Proof.
        intros rt_bounds SOME VALID.
        unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
        unfold edf_claimed_bounds in SOME; desf.
        rename Heq into LE.
        fold (f (max_steps ts)) in *; fold (f (max_steps ts).+1).

        (* Either the task set is empty or not. *)
        destruct (size ts == 0) eqn:EMPTY;
          first by apply bertogna_edf_comp_f_converges_with_no_tasks; apply/eqP.
        apply negbT in EMPTY; rewrite -lt0n in EMPTY.

        (* Either f converges by the deadline or not. *)
        destruct ([exists k in 'I_((max_steps ts).+1), f k == f k.+1]) eqn:EX.
        {
          move: EX => /exists_inP EX; destruct EX as [k _ ITERk].
          destruct k as [k LTk]; simpl in ITERk.
          apply bertogna_edf_comp_f_converges_early.
          exists k; split; [by apply LTk | by apply/eqP].
        }

        (* If not, then we reach a contradiction *)
        apply negbT in EX; rewrite negb_exists_in in EX.
        move: EX => /forall_inP EX.

        assert (SAMESUM: \sum_(tsk <- ts) task_cost tsk = \sum_(p <- f (max_steps ts)) task_cost (fst p)).
        {
          have MAP := @big_map _ 0 addn _ _ (fun x => fst x) (f (max_steps ts))
                               (fun x => true) (fun x => task_cost x).
          have UNZIP := edf_claimed_bounds_unzip1_iteration ts (max_steps ts).
          fold (f (max_steps ts)) in UNZIP; unfold unzip1 in UNZIP.
          by rewrite UNZIP in MAP; rewrite MAP.
        }
        
        (* Show that the sum is less than the sum of all deadlines. *)
        assert (SUM: \sum_(p <- f (max_steps ts)) (snd p - task_cost (fst p)) + 1 <= max_steps ts). 
        {
          unfold max_steps at 2; rewrite leq_add2r.
          rewrite -(leq_add2r (\sum_(tsk <- ts) task_cost tsk)).
          rewrite {1}SAMESUM -2!big_split /=.
          rewrite big_seq_cond [\sum_(_ <- _ | true)_]big_seq_cond.
          rewrite (eq_bigr (fun x => snd x)); last first.
          {
            intro i; rewrite andbT; intro IN.
            rewrite subh1; first by rewrite -addnBA // subnn addn0.
            have GE_COST := edf_claimed_bounds_ge_cost ts (max_steps ts).
            fold (f (max_steps ts)) in GE_COST.
            by destruct i; apply GE_COST.
          }
          rewrite (eq_bigr (fun x => task_deadline x)); last first.
          {
            intro i; rewrite andbT; intro IN.
            rewrite subh1; first by rewrite -addnBA // subnn addn0.
            by specialize (VALID i IN); des.
          }
          rewrite -2!big_seq_cond.
          have MAP := @big_map _ 0 addn _ _ (fun x => fst x) (f (max_steps ts))
                               (fun x => true) (fun x => task_deadline x).
          have UNZIP := edf_claimed_bounds_unzip1_iteration ts (max_steps ts).
          fold (f (max_steps ts)) in UNZIP; unfold unzip1 in UNZIP.
          rewrite UNZIP in MAP; rewrite MAP.
          rewrite big_seq_cond [\sum_(_ <- _|true)_]big_seq_cond.
          apply leq_sum; intro i; rewrite andbT; intro IN.
          move: LE => /allP LE; unfold R_le_deadline in LE.
          by specialize (LE i IN); destruct i.
        }

        have TOOMUCH :=
          bertogna_edf_comp_rt_grows_too_much EMPTY _ (max_steps ts) (leqnn (max_steps ts)).
        exploit TOOMUCH; [| intro BUG].
        {
          intros k LEk; rewrite -ltnS in LEk.
          by exploit (EX (Ordinal LEk)); [by done | by ins].
        }
        rewrite (eq_bigr (fun i => snd i - task_cost (fst i))) in BUG;
          last by ins; destruct i.
        by apply (leq_ltn_trans SUM) in BUG; rewrite ltnn in BUG. 
      Qed.

805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826
      (* ...and since there cannot be a vector of response-time bounds with values less than
         the task costs, this solution is also the least fixed point. *)
      Lemma edf_claimed_bounds_finds_least_fixed_point :
        forall v,
          all_le (initial_state ts) v ->
          v = edf_rta_iteration v ->
          all_le (f (max_steps ts)) v.
      Proof.
        intros v GE0 EQ.
        apply bertogna_edf_comp_iteration_inductive; first by done.
        intros k GEk.
        rewrite EQ.
        apply bertogna_edf_comp_iteration_preserves_order; last by done.
        by apply bertogna_edf_comp_iteration_preserves_minimum.
      Qed.

      (* Therefore, with regard to the response-time bound recurrence, ...*)
      Let rt_recurrence (tsk: sporadic_task) (rt_bounds: seq task_with_response_time) (R: time) :=
        task_cost tsk + div_floor (I rt_bounds tsk R) num_cpus.
      
      (* ..., the individual response-time bounds (elements of the list) are also fixed points. *)
      Theorem edf_claimed_bounds_finds_fixed_point_for_each_bound :
Felipe Cerqueira's avatar
Felipe Cerqueira committed
827 828 829
        forall tsk R rt_bounds,
          edf_claimed_bounds ts = Some rt_bounds ->
          (tsk, R) \in rt_bounds ->
830
          R = rt_recurrence tsk rt_bounds R.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
831 832
      Proof.
        intros tsk R rt_bounds SOME IN.
833 834
        have CONV := edf_claimed_bounds_finds_fixed_point_of_list rt_bounds.
        rewrite -iterS in CONV; fold (f (max_steps ts).+1) in CONV.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
835 836
        unfold edf_claimed_bounds in *; desf.
        exploit (CONV); [by done | by done | intro ITER; clear CONV].
Felipe Cerqueira's avatar
Felipe Cerqueira committed
837
        unfold f in ITER.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854

        cut (update_bound (iter (max_steps ts)
               edf_rta_iteration (initial_state ts)) (tsk,R) = (tsk, R)).
        {
          intros EQ.
          have F := @f_equal _ _ (fun x => snd x) _ (tsk, R).
          by apply F in EQ; simpl in EQ.
        }
        set s := iter (max_steps ts) edf_rta_iteration (initial_state ts).
        fold s in ITER, IN.
        move: IN => /(nthP (tsk,0)) IN; destruct IN as [i LT EQ].
        generalize EQ; rewrite ITER iterS in EQ; intro EQ'.
        fold s in EQ.
        unfold edf_rta_iteration in EQ.
        have MAP := @nth_map _ (tsk,0) _ _ (update_bound s). 
        by rewrite MAP // EQ' in EQ; rewrite EQ.
      Qed.
855
      
Felipe Cerqueira's avatar
Felipe Cerqueira committed
856 857 858
    End Convergence.

    Section MainProof.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889

      (* Consider a task set ts. *)
      Variable ts: taskset_of sporadic_task.
      
      (* Assume the task set has no duplicates, ... *)
      Hypothesis H_ts_is_a_set: uniq ts.

      (* ...all tasks have valid parameters, ... *)
      Hypothesis H_valid_task_parameters:
        valid_sporadic_taskset task_cost task_period task_deadline ts.

      (* ...restricted deadlines, ...*)
      Hypothesis H_restricted_deadlines:
        forall tsk, tsk \in ts -> task_deadline tsk <= task_period tsk.

      (* Next, consider any arrival sequence such that...*)
      Context {arr_seq: arrival_sequence Job}.

     (* ...all jobs come from task set ts, ...*)
      Hypothesis H_all_jobs_from_taskset:
        forall (j: JobIn arr_seq), job_task j \in ts.
      
      (* ...they have valid parameters,...*)
      Hypothesis H_valid_job_parameters:
        forall (j: JobIn arr_seq),
          valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
      
      (* ... and satisfy the sporadic task model.*)
      Hypothesis H_sporadic_tasks:
        sporadic_task_model task_period arr_seq job_task.
      
890
      (* Then, consider any platform with at least one CPU such that...*)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
891 892 893 894 895 896 897 898 899
      Variable sched: schedule num_cpus arr_seq.
      Hypothesis H_at_least_one_cpu :
        num_cpus > 0.

      (* ...jobs only execute after they arrived and no longer
         than their execution costs,... *)
      Hypothesis H_jobs_must_arrive_to_execute:
        jobs_must_arrive_to_execute sched.
      Hypothesis H_completed_jobs_dont_execute:
900
        completed_jobs_dont_execute job_cost sched.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
901 902 903 904

      (* ...and do not execute in parallel. *)
      Hypothesis H_no_parallelism:
        jobs_dont_execute_in_parallel sched.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
905

906 907 908
      (* Assume a work-conserving scheduler with EDF policy. *)
      Hypothesis H_work_conserving: work_conserving job_cost sched.
      Hypothesis H_edf_policy: enforces_JLDP_policy job_cost sched (EDF job_deadline).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
909 910

      Definition no_deadline_missed_by_task (tsk: sporadic_task) :=
911
        task_misses_no_deadline job_cost job_deadline job_task sched tsk.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
912
      Definition no_deadline_missed_by_job :=
913
        job_misses_no_deadline job_cost job_deadline sched.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
914

Felipe Cerqueira's avatar
Felipe Cerqueira committed
915
      (* In the following theorem, we prove that any response-time bound contained
Felipe Cerqueira's avatar
Felipe Cerqueira committed
916
         in edf_claimed_bounds is safe. The proof follows by direct application of
Felipe Cerqueira's avatar
Felipe Cerqueira committed
917 918 919 920 921 922
         the main Theorem from bertogna_edf_theory.v. *)
      Theorem edf_analysis_yields_response_time_bounds :
        forall tsk R,
          (tsk, R) \In edf_claimed_bounds ts ->
          forall j : JobIn arr_seq,
            job_task j = tsk ->
923
            completed job_cost sched j (job_arrival j + R).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
924 925 926 927 928 929 930 931 932 933
      Proof.
        intros tsk R IN j JOBj.
        destruct (edf_claimed_bounds ts) as [rt_bounds |] eqn:SOME; last by done.
        unfold edf_rta_iteration in *.
        have BOUND := bertogna_cirinei_response_time_bound_edf.
        unfold is_response_time_bound_of_task in *.
        apply BOUND with (task_cost := task_cost) (task_period := task_period)
           (task_deadline := task_deadline) (job_deadline := job_deadline)
           (job_task := job_task) (ts := ts) (tsk := tsk) (rt_bounds := rt_bounds); try (by ins).
          by unfold edf_claimed_bounds in SOME; desf; rewrite edf_claimed_bounds_unzip1_iteration.
934
          by ins; apply edf_claimed_bounds_finds_fixed_point_for_each_bound with (ts := ts).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
935 936
          by ins; rewrite (edf_claimed_bounds_le_deadline ts rt_bounds).
      Qed.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
937
      
Felipe Cerqueira's avatar
Felipe Cerqueira committed
938
      (* Therefore, if the schedulability test suceeds, ...*)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
939 940
      Hypothesis H_test_succeeds: edf_schedulable ts.
      
Felipe Cerqueira's avatar
Felipe Cerqueira committed
941
      (*... no task misses its deadline. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
942
      Theorem taskset_schedulable_by_edf_rta :
Felipe Cerqueira's avatar
Felipe Cerqueira committed
943 944 945 946 947 948 949 950 951 952 953 954 955 956
        forall tsk, tsk \in ts -> no_deadline_missed_by_task tsk.
      Proof.
        unfold no_deadline_missed_by_task, task_misses_no_deadline,
               job_misses_no_deadline, completed,
               edf_schedulable,
               valid_sporadic_job in *.
        rename H_valid_job_parameters into JOBPARAMS,
               H_valid_task_parameters into TASKPARAMS,
               H_restricted_deadlines into RESTR,
               H_completed_jobs_dont_execute into COMP,
               H_jobs_must_arrive_to_execute into MUSTARRIVE,
               H_all_jobs_from_taskset into ALLJOBS,
               H_test_succeeds into TEST.
        
957
        move => tsk INtsk j JOBtsk.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
958 959 960
        have RLIST := (edf_analysis_yields_response_time_bounds).
        have DL := (edf_claimed_bounds_le_deadline ts).
        have HAS := (edf_claimed_bounds_has_R_for_every_task ts).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
961
        
Felipe Cerqueira's avatar
Felipe Cerqueira committed
962
        destruct (edf_claimed_bounds ts) as [rt_bounds |] eqn:SOME; last by ins.
Felix Stutz's avatar
Felix Stutz committed
963
        exploit (HAS rt_bounds tsk); [by ins | by ins | clear HAS; intro HAS; des].
Felipe Cerqueira's avatar
Felipe Cerqueira committed
964
        have COMPLETED := RLIST tsk R HAS j JOBtsk.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
965 966
        exploit (DL rt_bounds tsk R);
          [by ins | by ins | clear DL; intro DL].
Felix Stutz's avatar
Felix Stutz committed
967
   
968
        rewrite eqn_leq; apply/andP; split; first by apply cumulative_service_le_job_cost.
969
        apply leq_trans with (n := service sched j (job_arrival j + R)); last first.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
970 971
        {
          unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
972
          apply extend_sum; rewrite // leq_add2l.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
973 974 975 976
          specialize (JOBPARAMS j); des; rewrite JOBPARAMS1.
          by rewrite JOBtsk.
        }
        rewrite leq_eqVlt; apply/orP; left; rewrite eq_sym.
Felix Stutz's avatar
Felix Stutz committed
977
        by apply COMPLETED.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
978 979 980 981 982
      Qed.

      (* For completeness, since all jobs of the arrival sequence
         are spawned by the task set, we conclude that no job misses
         its deadline. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
983
      Theorem jobs_schedulable_by_edf_rta :
Felipe Cerqueira's avatar
Felipe Cerqueira committed
984 985 986
        forall (j: JobIn arr_seq), no_deadline_missed_by_job j.
      Proof.
        intros j.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
987
        have SCHED := taskset_schedulable_by_edf_rta.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
988
        unfold no_deadline_missed_by_task, task_misses_no_deadline in *.
989
        apply SCHED with (tsk := job_task j); last by done.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
990 991 992
        by apply H_all_jobs_from_taskset.
      Qed.
      
Felipe Cerqueira's avatar
Felipe Cerqueira committed
993
    End MainProof.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
994 995 996 997

  End Analysis.

End ResponseTimeIterationEDF.