workload_bound.v 12.8 KB
Newer Older
1 2 3
Require Export rt.restructuring.analysis.basic_facts.workload.
Require Export rt.restructuring.analysis.basic_facts.ideal_schedule.
Require Export rt.restructuring.model.arrival.arrival_curves.
4 5 6 7 8 9

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.

(** * Task Workload Bounded by Arrival Curves *)
Section TaskWorkloadBoundedByArrivalCurves.

10
  (** Consider any type of tasks ... *)
11 12 13
  Context {Task : TaskType}.
  Context `{TaskCost Task}.

14
  (**  ... and any type of jobs associated with these tasks. *)
15 16 17 18 19
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.
  
20
  (** Consider any arrival sequence with consistent, non-duplicate arrivals... *)
21 22 23 24
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
  Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.

25
  (** ... and any ideal uniprocessor schedule of this arrival sequence.*)
26 27 28
  Variable sched : schedule (ideal.processor_state Job).
  Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.

29
  (** Consider an FP policy that indicates a higher-or-equal priority relation. *)
30 31 32
  Variable higher_eq_priority : FP_policy Task.
  Let jlfp_higher_eq_priority := FP_to_JLFP Job Task.

33
  (** For simplicity, let's define some local names. *)
34 35
  Let arrivals_between := arrivals_between arr_seq.
  
36
  (** We define the notion of request bound function. *)
37 38
  Section RequestBoundFunction.
    
39
    (** Let MaxArrivals denote any function that takes a task and an interval length
40 41 42
       and returns the associated number of job arrivals of the task. *) 
    Context `{MaxArrivals Task}.
    
43
    (** In this section, we define a bound for the workload of a single task
44 45 46
       under uniprocessor FP scheduling. *)
    Section SingleTask.

47
      (** Consider any task tsk that is to be scheduled in an interval of length delta. *)
48 49 50
      Variable tsk : Task.
      Variable delta : duration.

51
      (** We define the following workload bound for the task. *)
52 53 54 55
      Definition task_request_bound_function := task_cost tsk * max_arrivals tsk delta.

    End SingleTask.

56
    (** In this section, we define a bound for the workload of multiple tasks. *)
57 58
    Section AllTasks.

59
      (** Consider a task set ts... *)
60 61
      Variable ts : list Task.

62
      (** ...and let tsk be any task in task set. *)
63 64
      Variable tsk : Task.
      
65
      (** Let delta be the length of the interval of interest. *)
66 67
      Variable delta : duration.
      
68
      (** Recall the definition of higher-or-equal-priority task and
69 70 71 72
         the per-task workload bound for FP scheduling. *)
      Let is_hep_task tsk_other := higher_eq_priority tsk_other tsk.
      Let is_other_hep_task tsk_other := higher_eq_priority tsk_other tsk && (tsk_other != tsk).

73
      (** Using the sum of individual workload bounds, we define the following bound
74 75 76 77
         for the total workload of tasks in any interval of length delta. *)
      Definition total_request_bound_function :=
        \sum_(tsk <- ts) task_request_bound_function tsk delta.
      
78
      (** Similarly, we define the following bound for the total workload of tasks of 
79 80 81 82 83
         higher-or-equal priority (with respect to tsk) in any interval of length delta. *)
      Definition total_hep_request_bound_function_FP :=
        \sum_(tsk_other <- ts | is_hep_task tsk_other)
         task_request_bound_function tsk_other delta.
      
84
      (** We also define a bound for the total workload of higher-or-equal 
85 86 87 88 89 90 91 92 93
         priority tasks other than tsk in any interval of length delta. *)
      Definition total_ohep_request_bound_function_FP :=
        \sum_(tsk_other <- ts | is_other_hep_task tsk_other)
         task_request_bound_function tsk_other delta.
      
    End AllTasks.

  End RequestBoundFunction.

94
  (** In this section we prove some lemmas about request bound functions. *)
95 96
  Section ProofWorkloadBound.

97
    (** Consider a task set ts... *)
98 99
    Variable ts : list Task.

100
    (** ...and let tsk be any task in ts. *)
101 102 103
    Variable tsk : Task.
    Hypothesis H_tsk_in_ts : tsk \in ts.

104
    (** Assume that the job costs are no larger than the task costs. *)
105 106 107
    Hypothesis H_job_cost_le_task_cost :
      cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.

108
    (** Next, we assume that all jobs come from the task set. *)
109 110
    Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
      
111
    (** Let max_arrivals be any arrival bound for taskset ts. *)
112 113 114
    Context `{MaxArrivals Task}.
    Hypothesis H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts. 
    
115
    (** Let's define some local names for clarity. *)
116 117 118 119 120
    Let task_rbf := task_request_bound_function tsk.
    Let total_rbf := total_request_bound_function ts.
    Let total_hep_rbf := total_hep_request_bound_function_FP ts tsk.
    Let total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk.

121
    (** Next, we consider any job j of tsk. *)
122 123 124 125
    Variable j : Job.
    Hypothesis H_j_arrives : arrives_in arr_seq j.
    Hypothesis H_job_of_tsk : job_task j = tsk.
    
126
    (** Next, we say that two jobs j1 and j2 are in relation other_higher_eq_priority, iff 
127 128 129
       j1 has higher or equal priority than j2 and is produced by a different task. *)
    Let other_higher_eq_priority j1 j2 := jlfp_higher_eq_priority j1 j2 && (~~ same_task j1 j2).

130
    (** Next, we recall the notions of total workload of jobs... *)
131 132
    Let total_workload t1 t2 := workload_of_jobs predT (arrivals_between t1 t2).
    
133
    (** ...notions of workload of higher or equal priority jobs... *)
134 135 136
    Let total_hep_workload t1 t2 :=
      workload_of_jobs (fun j_other => jlfp_higher_eq_priority j_other j) (arrivals_between t1 t2).
    
137
    (** ... workload of other higher or equal priority jobs... *)
138 139 140
    Let total_ohep_workload t1 t2 :=
      workload_of_jobs (fun j_other => other_higher_eq_priority j_other j) (arrivals_between t1 t2).

141
    (** ... and the workload of jobs of the same task as job j. *)
142 143 144
    Let task_workload t1 t2 :=
      workload_of_jobs (job_of_task tsk) (arrivals_between t1 t2).
    
145
    (** In this section we prove that the workload of any jobs is 
146 147 148
       no larger than the request bound function. *) 
    Section WorkloadIsBoundedByRBF.

149
      (** Consider any time t and any interval of length delta. *)
150 151 152
      Variable t : instant.
      Variable delta : instant.

153
      (** First, we show that workload of task tsk is bounded by 
154 155 156 157 158 159 160 161 162 163 164 165 166
         the number of arrivals of the task times the cost of the task. *)
      Lemma task_workload_le_num_of_arrivals_times_cost:
        task_workload t (t + delta)
        <= task_cost tsk * number_of_task_arrivals arr_seq tsk t (t + delta).
      Proof.
        rewrite // /number_of_task_arrivals -sum1_size big_distrr /= big_filter.
        rewrite /task_workload_between /workload.task_workload_between /task_workload /workload_of_jobs.
        rewrite /same_task -H_job_of_tsk muln1.
        apply leq_sum_seq; move => j0 IN0 /eqP EQ.
        rewrite -EQ; apply in_arrivals_implies_arrived in IN0; auto.
          by apply H_job_cost_le_task_cost.
      Qed.
      
167
      (** As a corollary, we prove that workload of task is 
168 169 170 171 172 173 174 175 176 177 178 179
         no larger the than task request bound function. *)
      Corollary task_workload_le_task_rbf:
        task_workload t (t + delta) <= task_rbf delta.
      Proof.    
        apply leq_trans with
            (task_cost tsk *  number_of_task_arrivals arr_seq tsk t (t + delta));
          first by apply task_workload_le_num_of_arrivals_times_cost.
        rewrite leq_mul2l; apply/orP; right.
        rewrite -{2}[delta](addKn t).
          by apply H_is_arrival_bound; last rewrite leq_addr.
      Qed.

180
      (** Next, we prove that total workload of other tasks with
181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215
         higher-or-equal priority is no larger than the total
         request bound function. *)
      Lemma total_workload_le_total_rbf:
        total_ohep_workload t (t + delta) <= total_ohep_rbf delta.
      Proof.        
        set l := arrivals_between t (t + delta).
        set hep := higher_eq_priority.        
        apply leq_trans with
            (\sum_(tsk' <- ts | hep tsk' tsk && (tsk' != tsk))
              (\sum_(j0 <- l | job_task j0 == tsk') job_cost j0)).
        { intros.
          rewrite /total_ohep_workload /workload_of_jobs /other_higher_eq_priority.
          rewrite /jlfp_higher_eq_priority /FP_to_JLFP /same_task H_job_of_tsk. 
          have EXCHANGE := exchange_big_dep (fun x => hep (job_task x) tsk && (job_task x != tsk)).
          rewrite EXCHANGE /=; last by move => tsk0 j0 HEP /eqP JOB0; rewrite JOB0.
          rewrite /workload_of_jobs -/l big_seq_cond [X in _ <= X]big_seq_cond.
          apply leq_sum; move => j0 /andP [IN0 HP0].
          rewrite big_mkcond (big_rem (job_task j0)) /=; first by rewrite HP0 andTb eq_refl; apply leq_addr.
            by apply in_arrivals_implies_arrived in IN0; apply H_all_jobs_from_taskset.
        }
        apply leq_sum_seq; intros tsk0 INtsk0 HP0.
        apply leq_trans with
            (task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta))).
        { rewrite -sum1_size big_distrr /= big_filter.
          rewrite /workload_of_jobs.
          rewrite  muln1 /l /arrivals_between /arrival_sequence.arrivals_between. 
          apply leq_sum_seq; move => j0 IN0 /eqP EQ.
            by rewrite -EQ; apply H_job_cost_le_task_cost; apply in_arrivals_implies_arrived in IN0.
        }
        { rewrite leq_mul2l; apply/orP; right.
          rewrite -{2}[delta](addKn t).
            by apply H_is_arrival_bound; last rewrite leq_addr.
        }
      Qed.

216
      (** Next, we prove that total workload of tasks with higher-or-equal 
217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250
         priority is no larger than the total request bound function. *)
      Lemma total_workload_le_total_rbf':
        total_hep_workload t (t + delta) <= total_hep_rbf delta.
      Proof.
        set l := arrivals_between t (t + delta).
        set hep := higher_eq_priority.
        apply leq_trans with
            (n := \sum_(tsk' <- ts | hep tsk' tsk)
                   (\sum_(j0 <- l | job_task j0 == tsk') job_cost j0)).
        { rewrite /total_hep_workload /jlfp_higher_eq_priority /FP_to_JLFP H_job_of_tsk. 
          have EXCHANGE := exchange_big_dep (fun x => hep (job_task x) tsk).
          rewrite EXCHANGE /=; clear EXCHANGE; last by move => tsk0 j0 HEP /eqP JOB0; rewrite JOB0.
          rewrite /workload_of_jobs -/l big_seq_cond [X in _ <= X]big_seq_cond.
          apply leq_sum; move => j0 /andP [IN0 HP0].
          rewrite big_mkcond (big_rem (job_task j0)) /=; first by rewrite HP0 andTb eq_refl; apply leq_addr.
            by apply in_arrivals_implies_arrived in IN0; apply H_all_jobs_from_taskset.
        }
        apply leq_sum_seq; intros tsk0 INtsk0 HP0.
        apply leq_trans with
            (task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta))).
        { rewrite -sum1_size big_distrr /= big_filter.
          rewrite -/l /workload_of_jobs.
          rewrite muln1.
          apply leq_sum_seq; move => j0 IN0 /eqP EQ.
          rewrite -EQ.
          apply H_job_cost_le_task_cost.
            by apply in_arrivals_implies_arrived in IN0.
        }
        { rewrite leq_mul2l; apply/orP; right.
          rewrite -{2}[delta](addKn t).
            by apply H_is_arrival_bound; last rewrite leq_addr.
        }
      Qed.
      
251
      (** Next, we prove that total workload of tasks is 
252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291
         no larger than the total request bound function. *)
      Lemma total_workload_le_total_rbf'':
        total_workload t (t + delta) <= total_rbf delta.
      Proof.
        set l := arrivals_between t (t + delta).
        apply leq_trans with
            (n := \sum_(tsk' <- ts)
                   (\sum_(j0 <- l | job_task j0 == tsk') job_cost j0)).
        { rewrite /total_workload.
          have EXCHANGE := exchange_big_dep predT.
          rewrite EXCHANGE /=; clear EXCHANGE; last by done. 
          rewrite /workload_of_jobs -/l big_seq_cond [X in _ <= X]big_seq_cond.
          apply leq_sum; move => j0 /andP [IN0 HP0].
          rewrite big_mkcond (big_rem (job_task j0)) /=.
          rewrite eq_refl; apply leq_addr.
            by apply in_arrivals_implies_arrived in IN0;
              apply H_all_jobs_from_taskset.
        }
        apply leq_sum_seq; intros tsk0 INtsk0 HP0.
        apply leq_trans with
            (task_cost tsk0 * size (task_arrivals_between arr_seq tsk0 t (t + delta))).
        { rewrite -sum1_size big_distrr /= big_filter.
          rewrite -/l /workload_of_jobs.
          rewrite muln1.
          apply leq_sum_seq; move => j0 IN0 /eqP EQ.
          rewrite -EQ.
          apply H_job_cost_le_task_cost.
            by apply in_arrivals_implies_arrived in IN0.
        }
        { rewrite leq_mul2l; apply/orP; right.
          rewrite -{2}[delta](addKn t).
            by apply H_is_arrival_bound; last rewrite leq_addr.
        }
      Qed.  

    End WorkloadIsBoundedByRBF.

  End ProofWorkloadBound.
  
End TaskWorkloadBoundedByArrivalCurves.