definitions.v 11.3 KB
Newer Older
1
Require Export rt.restructuring.model.task.concept.
Sergey Bozhko's avatar
Sergey Bozhko committed
2
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
3 4

(** Throughout this file, we assume ideal uniprocessor schedules. *)
Sergey Bozhko's avatar
Sergey Bozhko committed
5
Require Import rt.restructuring.model.processor.ideal.  
Sergey Bozhko's avatar
Sergey Bozhko committed
6 7 8 9 10 11

(** * Definitions for Abstract Response-Time Analysis *)
(** In this module, we propose a set of definitions for the general framework for response-time analysis (RTA) 
    of uniprocessor scheduling of real-time tasks with arbitrary arrival models. *)
Section AbstractRTADefinitions. 

12
  (** In this section, we introduce all the abstract notions required by the analysis. *)
Sergey Bozhko's avatar
Sergey Bozhko committed
13 14
  Section Definitions.

15
    (** Consider any type of job associated with any type of tasks... *)
Sergey Bozhko's avatar
Sergey Bozhko committed
16 17 18 19
    Context {Job : JobType}.
    Context {Task : TaskType}.
    Context `{JobTask Job Task}.

20
    (** ... with arrival times and costs. *)
Sergey Bozhko's avatar
Sergey Bozhko committed
21 22 23
    Context `{JobArrival Job}.
    Context `{JobCost Job}.

24
    (** Consider any arrival sequence... *) 
Sergey Bozhko's avatar
Sergey Bozhko committed
25 26
    Variable arr_seq : arrival_sequence Job.

27
    (** ... and any ideal uniprocessor schedule of this arrival sequence. *)
Sergey Bozhko's avatar
Sergey Bozhko committed
28 29
    Variable sched : schedule (ideal.processor_state Job).

30
    (** Let tsk be any task that is to be analyzed *)
Sergey Bozhko's avatar
Sergey Bozhko committed
31 32
    Variable tsk : Task.
    
33
    (** For simplicity, let's define some local names. *)
Sergey Bozhko's avatar
Sergey Bozhko committed
34 35 36
    Let job_scheduled_at := scheduled_at sched.
    Let job_completed_by := completed_by sched.

37
    (** Recall that a job j is pending_earlier_and_at a time instant t iff job
Sergey Bozhko's avatar
Sergey Bozhko committed
38 39 40
       j arrived before time t and is still not completed by time t. *)
    Let job_pending_earlier_and_at := pending_earlier_and_at sched.

41
    (** We are going to introduce two main variables of the analysis: 
Sergey Bozhko's avatar
Sergey Bozhko committed
42 43 44
       (a) interference, and (b) interfering workload. *)

    (** a) Interference *)
45
    (** Execution of a job may be postponed by the environment and/or the system due to different
Sergey Bozhko's avatar
Sergey Bozhko committed
46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62
       factors (preemption by higher-priority jobs, jitter, black-out periods in hierarchical 
       scheduling, lack of budget, etc.), which we call interference. 

       Besides, note that even the n’th activation of a task can suffer from interference at 
       the beggining of its busy interval (despite the fact that this job hasn’t even arrived 
       at that moment!). Thus, it makes more sense (at least for the current busy-interval 
       analysis) to think about interference of a job as any interference within the 
       corresponding busy interval, and not after release of the job.

       Based on that, assume a predicate that expresses whether a job j under consideration 
       incurs interference at a given time t (in the context of the schedule under consideration).
       This will be used later to upper-bound job j's response time. Note that a concrete 
       realization of the function may depend on the schedule, but here we do not require this 
       for the sake of simplicity and generality. *)
    Variable interference : Job -> instant -> bool.

    (** b) Interfering Workload *)
63
    (** In addition to interference, the analysis assumes that at any time t, we know an upper 
Sergey Bozhko's avatar
Sergey Bozhko committed
64 65 66 67 68 69 70 71 72 73
       bound on the potential cumulative interference that can be incurred in the future by any
       job (i.e., the total remaining potential delays). Based on that, assume a function 
       interfering_workload that indicates for any job j, at any time t, the amount of potential 
       interference for job j that is introduced into the system at time t. This function will be
       later used to upper-bound the length of the busy window of a job.
       One example of workload function is the "total cost of jobs that arrive at time t and 
       have higher-or-equal priority than job j". In some task models, this function expresses 
       the amount of the potential interference on job j that "arrives" in the system at time t. *)
    Variable interfering_workload : Job -> instant -> duration.

74
    (** In order to bound the response time of a job, we must to consider the cumulative 
Sergey Bozhko's avatar
Sergey Bozhko committed
75 76 77 78 79
       interference and cumulative interfering workload. *)
    Definition cumul_interference j t1 t2 := \sum_(t1 <= t < t2) interference j t.
    Definition cumul_interfering_workload j t1 t2 := \sum_(t1 <= t < t2) interfering_workload j t.

    (** Definition of Busy Interval *)
80
    (** Further analysis will be based on the notion of a busy interval. The overall idea of the 
Sergey Bozhko's avatar
Sergey Bozhko committed
81 82 83 84
       busy interval is to take into account the workload that cause a job under consideration to 
       incur interference. In this section, we provide a definition of an abstract busy interval. *)
    Section BusyInterval.

85
      (** We say that time instant t is a quiet time for job j iff two conditions hold. 
Sergey Bozhko's avatar
Sergey Bozhko committed
86 87 88 89 90 91 92 93 94 95 96
         First, the cumulative interference at time t must be equal to the cumulative
         interfering workload, to indicate that the potential interference seen so far 
         has been fully "consumed" (i.e., there is no more higher-priority work or other 
         kinds of delay pending). Second, job j cannot be pending at any time earlier
         than t _and_ at time instant t (i.e., either it was pending earlier but is no 
         longer pending now, or it was previously not pending and may or may not be 
         released now), to ensure that the busy window captures the execution of job j. *)
      Definition quiet_time (j : Job) (t : instant) :=
        cumul_interference j 0 t = cumul_interfering_workload j 0 t /\
        ~~ job_pending_earlier_and_at j t.
      
97
      (** Based on the definition of quiet time, we say that interval [t1, t2) is 
Sergey Bozhko's avatar
Sergey Bozhko committed
98 99 100 101 102 103 104 105
         a (potentially unbounded) busy-interval prefix w.r.t. job j iff the 
         interval (a) contains the arrival of job j, (b) starts with a quiet
         time and (c) remains non-quiet. *)
      Definition busy_interval_prefix (j : Job) (t1 t2 : instant) :=
        t1 <= job_arrival j < t2 /\
        quiet_time j t1 /\
        (forall t, t1 < t < t2 -> ~ quiet_time j t). 

106
      (** Next, we say that an interval [t1, t2) is a busy interval iff
Sergey Bozhko's avatar
Sergey Bozhko committed
107 108 109 110 111
         [t1, t2) is a busy-interval prefix and t2 is a quiet time. *)
      Definition busy_interval (j : Job) (t1 t2 : instant) :=
        busy_interval_prefix j t1 t2 /\
        quiet_time j t2.

112
      (** Note that the busy interval, if it exists, is unique. *)
Sergey Bozhko's avatar
Sergey Bozhko committed
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
      Lemma busy_interval_is_unique:
        forall j t1 t2 t1' t2',
          busy_interval j t1 t2 ->
          busy_interval j t1' t2' ->
          t1 = t1' /\ t2 = t2'.
      Proof.
        intros ? ? ? ? ? BUSY BUSY'.
        have EQ: t1 = t1'.
        { apply/eqP.
          apply/negPn/negP; intros CONTR.
          move: BUSY => [[IN [QT1 NQ]] _].
          move: BUSY' => [[IN' [QT1' NQ']] _].
          move: CONTR; rewrite neq_ltn; move => /orP [LT|GT].
          { apply NQ with t1'; try done; clear NQ.
            apply/andP; split; first by done.
            move: IN IN' => /andP [_ T1] /andP [T2 _].
              by apply leq_ltn_trans with (job_arrival j).
          }
          { apply NQ' with t1; try done; clear NQ'.
            apply/andP; split; first by done.
            move: IN IN' => /andP [T1 _] /andP [_ T2].
              by apply leq_ltn_trans with (job_arrival j).
          }
        } subst t1'.
        have EQ: t2 = t2'.
        { apply/eqP.
          apply/negPn/negP; intros CONTR.
          move: BUSY => [[IN [_ NQ]] QT2].
          move: BUSY' => [[IN' [_ NQ']] QT2'].
          move: CONTR; rewrite neq_ltn; move => /orP [LT|GT].
          { apply NQ' with t2; try done; clear NQ'.
            apply/andP; split; last by done.
            move: IN IN' => /andP [_ T1] /andP [T2 _].
              by apply leq_ltn_trans with (job_arrival j).
          }
          { apply NQ with t2'; try done; clear NQ.
            apply/andP; split; last by done.
            move: IN IN' => /andP [T1 _] /andP [_ T2].
              by apply leq_ltn_trans with (job_arrival j).
          }
        } by subst t2'.
      Qed.
      
    End BusyInterval.

158
    (** In this section, we introduce some assumptions about the
Sergey Bozhko's avatar
Sergey Bozhko committed
159 160 161
       busy interval that are fundamental for the analysis. *)
    Section BusyIntervalProperties.

162
      (** We say that a schedule is "work_conserving" iff for any job j from task tsk and 
Sergey Bozhko's avatar
Sergey Bozhko committed
163 164 165 166 167 168 169 170 171 172 173
         at any time t within a busy interval, there are only two options:
         either (a) interference(j, t) holds or (b) job j is scheduled at time t. *)
      Definition work_conserving :=
        forall j t1 t2 t,
          arrives_in arr_seq j ->
          job_task j = tsk ->
          job_cost j > 0 ->
          busy_interval j t1 t2 ->
          t1 <= t < t2 ->
          ~ interference j t <-> job_scheduled_at j t.

174
      (** Next, we say that busy intervals of task tsk are bounded by L iff, for any job j of task
Sergey Bozhko's avatar
Sergey Bozhko committed
175 176 177 178 179 180 181 182 183 184 185 186 187 188
         tsk, there exists a busy interval with length at most L. Note that the existence of such a
         bounded busy interval is not guaranteed if the schedule is overloaded with work. 
         Therefore, in the later concrete analyses, we will have to introduce an additional 
         condition that prevents overload. *)
      Definition busy_intervals_are_bounded_by L :=
        forall j,
          arrives_in arr_seq j ->
          job_task j = tsk ->
          job_cost j > 0 -> 
          exists t1 t2,
            t1 <= job_arrival j < t2 /\
            t2 <= t1 + L /\
            busy_interval j t1 t2.

189
      (** Although we have defined the notion of cumulative interference of a job, it cannot be used in 
Sergey Bozhko's avatar
Sergey Bozhko committed
190 191 192 193 194 195 196 197 198
         a response-time analysis because of the variability of job parameters. To address this 
         issue, we define the notion of an interference bound. Note that according to the definition of
         a work conserving schedule, interference does _not_ include execution of a job itself. Therefore,
         an interference bound is not obliged to take into account the execution of this job. We say that 
         the job interference is bounded by an interference_bound_function (IBF) iff for any job j of 
         task tsk the cumulative interference incurred by j in the subinterval [t1, t1 + delta) of busy
         interval [t1, t2) does not exceed interference_bound_function(tsk, A, delta), where A is a 
         relative arrival time of job j (with respect to time t1). *)
      Definition job_interference_is_bounded_by (interference_bound_function: Task -> duration -> duration -> duration) :=
199
        (** Let's examine this definition in more detail. *)
Sergey Bozhko's avatar
Sergey Bozhko committed
200
        forall t1 t2 delta j,
201
          (** First, we require j to be a job of task tsk. *)
Sergey Bozhko's avatar
Sergey Bozhko committed
202 203
          arrives_in arr_seq j ->
          job_task j = tsk ->
204
          (** Next, we require the IBF to bound the interference only within the interval [t1, t1 + delta). *)
Sergey Bozhko's avatar
Sergey Bozhko committed
205 206
          busy_interval j t1 t2 ->
          t1 + delta < t2 ->
207
          (** Next, we require the IBF to bound the interference only until the job is 
Sergey Bozhko's avatar
Sergey Bozhko committed
208 209
             completed, after which the function can behave arbitrarily. *)
          ~~ job_completed_by j (t1 + delta) ->
210
          (** And finally, the IBF function might depend not only on the length 
Sergey Bozhko's avatar
Sergey Bozhko committed
211
             of the interval, but also on the relative arrival time of job j (offset). *)
212
          (** While the first three conditions are needed for discarding excessive cases, offset adds 
Sergey Bozhko's avatar
Sergey Bozhko committed
213 214 215 216 217 218 219 220 221
             flexibility to the IBF, which is important, for instance, when analyzing EDF scheduling. *)
          let offset := job_arrival j - t1 in 
          cumul_interference j t1 (t1 + delta) <= interference_bound_function tsk offset delta.

    End BusyIntervalProperties.

  End Definitions.

End AbstractRTADefinitions.