schedule.v 6.39 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73
Require Import rt.util.all.
Require Import rt.model.time rt.model.arrival.basic.task rt.model.arrival.basic.job.
Require Import rt.model.schedule.uni.schedule.
Require Import rt.model.arrival.jitter.arrival_sequence.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

(* In this file, we prove additional definitions and lemmas about jitter-aware schedules. *)
Module UniprocessorScheduleWithJitter.

  (* To formalize jitter, we import the original uniprocessor schedule and
     redefine some of the properties. *)
  Export ArrivalSequenceWithJitter UniprocessorSchedule.
  
  (* In this section we redefine properties that depend on the arrival time. *)
  Section RedefiningProperties.

    Context {Job: eqType}.
    Variable job_cost: Job -> time.
    Variable job_jitter: Job -> time.

    (* Consider any uniprocessor schedule. *)
    Context {arr_seq: arrival_sequence Job}.
    Variable sched: schedule arr_seq.

    (* First, we redefine some job properties. *)
    Section JobProperties.
      
      (* Let j be any job in the arrival sequence. *)
      Variable j: JobIn arr_seq.

      (* Then, we say that job j is pending at time t iff the jitter has passed but
         j has not completed by time t. *)
      Definition pending (t: time) :=
        jitter_has_passed job_jitter j t && ~~ completed_by job_cost sched j t.

      (* Finally, we say that job j is backlogged at time t iff it is pending and not scheduled. *)
      Definition backlogged (t: time) :=
        pending t && ~~ scheduled_at sched j t.

    End JobProperties.

    (* Next, we define properties of a valid jitter-aware schedule. *)
    Section ValidSchedules.

      (* In any jitter-aware schedule, a job can only be scheduled after
         the jitter has passed. *)
      Definition jobs_execute_after_jitter :=
        forall j t,
          scheduled_at sched j t -> jitter_has_passed job_jitter j t.

    End ValidSchedules.
  
    (* In this section, we prove some basic lemmas about jitter-aware schedules. *)   
    Section Lemmas.

      (* We begin by proving properties related to job arrivals. *)
      Section Arrival.

        (* Assume that jobs only execute after the jitter has passed. *)
        Hypothesis H_jobs_execute_after_jitter: jobs_execute_after_jitter.

        (* First, we show that every job in the schedule only executes after its arrival time. *)
        Lemma jobs_with_jitter_must_arrive_to_execute:
          jobs_must_arrive_to_execute sched.
        Proof.
          intros j t SCHED.
          apply leq_trans with (n := actual_arrival job_jitter j); first by apply leq_addr.
          by apply H_jobs_execute_after_jitter.
        Qed.

        (* Now, let j be any job in the arrival sequence. *)
        Variable j: JobIn arr_seq.

74 75 76 77 78 79 80 81 82 83
        (* Next, we show that if the jitter has passed, then the job must have arrived. *)
        Lemma jitter_has_passed_implies_arrived:
          forall t,
            jitter_has_passed job_jitter j t -> has_arrived j t.
        Proof.
          by intros t PASS; apply: leq_trans PASS; apply leq_addr.
        Qed.
        
        (* Now we prove that job j does not receive service at any time t before
           its actual arrival time. *)
84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164
        Lemma service_before_jitter_is_zero :
          forall t,
            t < actual_arrival job_jitter j ->
            service_at sched j t = 0.
        Proof.
          rename H_jobs_execute_after_jitter into ARR; red in ARR; intros t LT.
          specialize (ARR j t).
          apply contra with (c := scheduled_at sched j t)
                              (b := jitter_has_passed job_jitter j t) in ARR;
            last by rewrite -ltnNge.
            by apply/eqP; rewrite eqb0.
        Qed.

        (* Note that the same property applies to the cumulative service. *)
        Lemma cumulative_service_before_jitter_is_zero :
          forall t1 t2,
            t2 <= actual_arrival job_jitter j ->
            \sum_(t1 <= i < t2) service_at sched j i = 0.
        Proof.
          intros t1 t2 LE; apply/eqP; rewrite -leqn0.
          apply leq_trans with (n := \sum_(t1 <= i < t2) 0);
            last by rewrite big_const_nat iter_addn mul0n addn0.
          rewrite big_nat_cond [\sum_(_ <= _ < _) 0]big_nat_cond.
          apply leq_sum; intro i; rewrite andbT; move => /andP LTi; des.
          rewrite service_before_jitter_is_zero; first by ins.
            by apply leq_trans with (n := t2); ins.
        Qed.

        (* Hence, one can ignore the service received by a job before the jitter. *)
        Lemma ignore_service_before_jitter:
          forall t1 t2,
            t1 <= actual_arrival job_jitter j <= t2 ->
            \sum_(t1 <= t < t2) service_at sched j t =
            \sum_(actual_arrival job_jitter j <= t < t2) service_at sched j t.
        Proof.
          move => t1 t2 /andP [LE1 GE2].
          rewrite -> big_cat_nat with (n := actual_arrival job_jitter j); try (by done).
          by rewrite /= cumulative_service_before_jitter_is_zero; [rewrite add0n | apply leqnn].
        Qed.

      End Arrival.

      (* In this section, we prove properties about pending jobs. *)
      Section Pending.

        (* Assume that jobs only execute after the jitter has passed... *)
        Hypothesis H_jobs_execute_after_jitter: jobs_execute_after_jitter.

        (* ...and that completed jobs do not execute. *)
        Hypothesis H_completed_jobs:
          completed_jobs_dont_execute job_cost sched.

        (* Let j be any job in the arrival sequence. *)
        Variable j: JobIn arr_seq.

        (* First, we show that if job j is scheduled, then it must be pending. *)
        Lemma scheduled_implies_pending:
          forall t,
            scheduled_at sched j t -> pending j t.
        Proof.
          rename H_jobs_execute_after_jitter into ARR,
          H_completed_jobs into COMP.
          unfold jobs_must_arrive_to_execute, completed_jobs_dont_execute in *.
          intros t SCHED.
          unfold pending; apply/andP; split; first by apply ARR.
          apply/negP; unfold not; intro COMPLETED.
          have BUG := COMP j t.+1.
          rewrite leqNgt in BUG; move: BUG => /negP BUG; apply BUG.
          unfold service, service_during; rewrite -addn1 big_nat_recr // /=.
          apply leq_add;
            first by move: COMPLETED => /eqP COMPLETED; rewrite -COMPLETED.
            by rewrite /service_at SCHED.
        Qed.

      End Pending.

    End Lemmas.

  End RedefiningProperties.

End UniprocessorScheduleWithJitter.