schedule.v 22.2 KB
Newer Older
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1
Require Import Vbase job task util_lemmas arrival_sequence
Felipe Cerqueira's avatar
Felipe Cerqueira committed
2
3
               ssreflect ssrbool eqtype ssrnat seq fintype bigop.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
4
(* Definition, properties and lemmas about schedules. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
5
6
Module Schedule.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
7
  Export ArrivalSequence.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
8

Felipe Cerqueira's avatar
Felipe Cerqueira committed
9
10
  (* A processor is defined as a bounded natural number: [0, num_cpus). *)
  Definition processor (num_cpus: nat) := 'I_num_cpus.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
11
  
Felipe Cerqueira's avatar
Felipe Cerqueira committed
12
  Section ScheduleDef.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
13

14
    Context {Job: eqType}.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
15
16

    (* Given the number of processors and an arrival sequence, ...*)
17
    Variable num_cpus: nat.
18
    Variable arr_seq: arrival_sequence Job.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
19

Felipe Cerqueira's avatar
Felipe Cerqueira committed
20
21
    (* ... we define a schedule as a mapping such that each processor
       at each time contains either a job from the sequence or none. *)
22
    Definition schedule :=
23
      processor num_cpus -> time -> option (JobIn arr_seq).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
24

Felipe Cerqueira's avatar
Felipe Cerqueira committed
25
  End ScheduleDef.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
26
27

  (* Next, we define properties of jobs in a schedule. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
28
  Section ScheduledJobs.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
29

Felipe Cerqueira's avatar
Felipe Cerqueira committed
30
31
32
    Context {Job: eqType}.

    (* Given an arrival sequence, ... *)
33
34
    Context {arr_seq: arrival_sequence Job}.
    
Felipe Cerqueira's avatar
Felipe Cerqueira committed
35
36
    Variable job_cost: Job -> nat. (* ... a job cost function, ... *)

Felipe Cerqueira's avatar
Felipe Cerqueira committed
37
    (* ... and the number of processors, ...*)
38
    Context {num_cpus: nat}.
39

Felipe Cerqueira's avatar
Felipe Cerqueira committed
40
41
    (* ... we define the following properties for job j in schedule sched. *)
    Variable sched: schedule num_cpus arr_seq.
42
    Variable j: JobIn arr_seq.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
43

Felipe Cerqueira's avatar
Felipe Cerqueira committed
44
    (* A job j is scheduled at time t iff there exists a cpu where it is mapped.*)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
45
    Definition scheduled (t: time) :=
Felipe Cerqueira's avatar
Felipe Cerqueira committed
46
      [exists cpu in 'I_(num_cpus), sched cpu t == Some j].
Felipe Cerqueira's avatar
Felipe Cerqueira committed
47

Felipe Cerqueira's avatar
Felipe Cerqueira committed
48
    (* A processor cpu is idle at time t if it doesn't contain any jobs. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
49
50
51
    Definition is_idle (cpu: 'I_(num_cpus)) (t: time) :=
      sched cpu t = None.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
52
53
54
    (* The instantaneous service of job j at time t is the number of cpus
       where it is scheduled on. Note that we use a sum to account for
       parallelism if required. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
55
    Definition service_at (t: time) :=
Felipe Cerqueira's avatar
Felipe Cerqueira committed
56
      \sum_(cpu < num_cpus | sched cpu t == Some j) 1.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
57

Felipe Cerqueira's avatar
Felipe Cerqueira committed
58
    (* The cumulative service received by job j during [0, t'). *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
59
    Definition service (t': time) := \sum_(0 <= t < t') service_at t.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
60

Felipe Cerqueira's avatar
Felipe Cerqueira committed
61
    (* The cumulative service received by job j during [t1, t2). *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
62
63
    Definition service_during (t1 t2: time) := \sum_(t1 <= t < t2) service_at t.
    
Felipe Cerqueira's avatar
Felipe Cerqueira committed
64
    (* Job j has completed at time t if it received enough service. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
65
    Definition completed (t: time) := service t == job_cost j.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
66

Felipe Cerqueira's avatar
Felipe Cerqueira committed
67
    (* Job j is pending at time t iff it has arrived but has not completed. *)
68
    Definition pending (t: time) := has_arrived j t && ~~completed t.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
69

Felipe Cerqueira's avatar
Felipe Cerqueira committed
70
    (* Job j is backlogged at time t iff it is pending and not scheduled. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
71
72
    Definition backlogged (t: time) := pending t && ~~scheduled t.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
73
74
    (* Job j is carry-in in interval [t1, t2) iff it arrives before t1 and is
       not complete at time t1 *)
75
    Definition carried_in (t1: time) := arrived_before j t1 && ~~ completed t1.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
76

Felipe Cerqueira's avatar
Felipe Cerqueira committed
77
78
    (* Job j is carry-out in interval [t1, t2) iff it arrives after t1 and is
       not complete at time t2 *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
79
    Definition carried_out (t1 t2: time) := arrived_before j t2 && ~~ completed t2.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
80

Felipe Cerqueira's avatar
Felipe Cerqueira committed
81
82
    (* The list of scheduled jobs at time t is the concatenation of the jobs
       scheduled on each processor. *)
83
84
85
    Definition jobs_scheduled_at (t: time) :=
      \cat_(cpu < num_cpus) make_sequence (sched cpu t).
    
Felipe Cerqueira's avatar
Felipe Cerqueira committed
86
87
    (* The list of jobs scheduled during the interval [t1, t2) is the
       the duplicate-free concatenation of the jobs scheduled at instant. *)
88
89
90
    Definition jobs_scheduled_between (t1 t2: time) :=
      undup (\cat_(t1 <= t < t2) jobs_scheduled_at t).

Felipe Cerqueira's avatar
Felipe Cerqueira committed
91
92
  End ScheduledJobs.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
93
  (* In this section, we define properties of valid schedules. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
94
95
  Section ValidSchedules.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
96
97
    Context {Job: eqType}. (* Assume a job type with decidable equality, ...*)
    Context {arr_seq: arrival_sequence Job}. (* ..., an arrival sequence, ...*)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
98

Felipe Cerqueira's avatar
Felipe Cerqueira committed
99
    Variable job_cost: Job -> nat. (* ... a cost function, .... *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
100

Felipe Cerqueira's avatar
Felipe Cerqueira committed
101
102
    (* ... and a schedule. *)
    Context {num_cpus: nat}.
103
    Variable sched: schedule num_cpus arr_seq.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
104

Felipe Cerqueira's avatar
Felipe Cerqueira committed
105
    (* Next, we define whether job parallelism is disallowed, ... *)
106
107
    Definition jobs_dont_execute_in_parallel :=
      forall j t cpu1 cpu2,
108
        sched cpu1 t = Some j -> sched cpu2 t = Some j -> cpu1 = cpu2.
109

Felipe Cerqueira's avatar
Felipe Cerqueira committed
110
    (* ... whether a job can only be scheduled if it has arrived, ... *)
111
112
    Definition jobs_must_arrive_to_execute :=
      forall j t, scheduled sched j t -> has_arrived j t.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
113

Felipe Cerqueira's avatar
Felipe Cerqueira committed
114
    (* ... whether a job can be scheduled after it completes. *)
115
    Definition completed_jobs_dont_execute :=
Felipe Cerqueira's avatar
Felipe Cerqueira committed
116
      forall j t, service sched j t <= job_cost j.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
117
118
119

  End ValidSchedules.

120
121
  (* In this section, we prove some basic lemmas about a job. *)
  Section JobLemmas.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
122

Felipe Cerqueira's avatar
Felipe Cerqueira committed
123
    (* Consider an arrival sequence, ...*)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
124
    Context {Job: eqType}.
125
    Context {arr_seq: arrival_sequence Job}.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
126
127

    (* ... a job cost function, ...*)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
128
129
    Variable job_cost: Job -> nat.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
130
    (* ..., and a particular schedule. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
131
    Context {num_cpus: nat}.
132
    Variable sched: schedule num_cpus arr_seq.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
133
134

    (* Next, we prove some lemmas about the service received by a job j. *)
135
    Variable j: JobIn arr_seq.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
136

Felipe Cerqueira's avatar
Felipe Cerqueira committed
137
138
    Section Basic.

139
      (* At any time t, job j is not scheduled iff it doesn't get service. *)
140
141
      Lemma not_scheduled_no_service :
        forall t,
142
          ~~ scheduled sched j t = (service_at sched j t == 0).
143
      Proof.
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
        unfold scheduled, service_at; intros t; apply/idP/idP.
        {
          intros NOTSCHED.
          rewrite negb_exists_in in NOTSCHED.
          move: NOTSCHED => /forall_inP NOTSCHED.
          rewrite big_seq_cond.
          rewrite -> eq_bigr with (F2 := fun i => 0);
            first by rewrite big_const_seq iter_addn mul0n addn0.
          move => cpu /andP [_ SCHED].
          exploit (NOTSCHED cpu); [by ins | clear NOTSCHED].
          by move: SCHED => /eqP SCHED; rewrite SCHED eq_refl.
        }
        {
          intros NOSERV; rewrite big_mkcond -sum_nat_eq0_nat in NOSERV.
          move: NOSERV => /allP ALL.
          rewrite negb_exists; apply/forall_inP.
          move => x /andP [IN SCHED].
          by exploit (ALL x); [by apply mem_index_enum | by desf].
        }
163
164
      Qed.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
165
166
      (* If the cumulative service during a time interval is not zero, there
         must be a time t in this interval where the service is not 0. *) 
Felipe Cerqueira's avatar
Felipe Cerqueira committed
167
168
      Lemma job_scheduled_during_interval :
        forall t1 t2,
Felipe Cerqueira's avatar
Felipe Cerqueira committed
169
          service_during sched j t1 t2 != 0 ->
Felipe Cerqueira's avatar
Felipe Cerqueira committed
170
171
          exists t,
            t1 <= t < t2 /\ 
Felipe Cerqueira's avatar
Felipe Cerqueira committed
172
            service_at sched j t != 0.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
173
174
      Proof.
        intros t1 t2 NONZERO.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
175
        destruct ([exists t: 'I_t2, (t >= t1) && (service_at sched j t != 0)]) eqn:EX.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
        {
          move: EX => /existsP EX; destruct EX as [x EX]. move: EX => /andP [GE SERV].
          exists x; split; last by done.
          by apply/andP; split; [by done | apply ltn_ord].
        }
        {
          apply negbT in EX; rewrite negb_exists in EX; move: EX => /forallP EX.
          unfold service_during in NONZERO; rewrite big_nat_cond in NONZERO.
          rewrite (eq_bigr (fun x => 0)) in NONZERO;
            first by rewrite -big_nat_cond big_const_nat iter_addn mul0n addn0 in NONZERO.
          intros i; rewrite andbT; move => /andP [GT LT].
          specialize (EX (Ordinal LT)); simpl in EX.
          by rewrite GT andTb negbK in EX; apply/eqP.
        }
      Qed.
      
Felipe Cerqueira's avatar
Felipe Cerqueira committed
192
    End Basic.
193
    
Felipe Cerqueira's avatar
Felipe Cerqueira committed
194
    Section NoParallelism.
195

Felipe Cerqueira's avatar
Felipe Cerqueira committed
196
      (* If jobs cannot execute in parallel, then... *)
197
198
199
      Hypothesis no_parallelism:
        jobs_dont_execute_in_parallel sched.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
200
201
202
      (* ..., the service received by job j at any time t is at most 1, ... *)
      Lemma service_at_most_one :
        forall t, service_at sched j t <= 1.
203
204
      Proof.
        unfold service_at, jobs_dont_execute_in_parallel in *; ins.
205
        destruct (scheduled sched j t) eqn:SCHED; unfold scheduled in SCHED.
206
        {
207
          move: SCHED => /exists_inP SCHED; des.
208
          move: H2 => /eqP SCHED.
209
          rewrite -big_filter.
210
          rewrite (bigD1_seq x);
211
212
213
214
215
            [simpl | | by rewrite filter_index_enum enum_uniq]; last first.
          {
            by rewrite mem_filter; apply/andP; split;
              [by apply/eqP | by rewrite mem_index_enum].
          }
216
217
          rewrite -big_filter -filter_predI big_filter.
          rewrite -> eq_bigr with (F2 := fun cpu => 0);
Felipe Cerqueira's avatar
Felipe Cerqueira committed
218
            first by rewrite /= big_const_seq iter_addn mul0n 2!addn0.
219
220
          intro i; move => /andP [/eqP NEQ /eqP SCHEDi].
          by apply no_parallelism with (cpu1 := x) in SCHEDi; subst.
221
222
223
        }
        {
          apply negbT in SCHED; rewrite negb_exists_in in SCHED.
224
225
          move: SCHED => /forall_inP SCHED.
          by rewrite big_pred0; red; ins; apply negbTE, SCHED.
226
227
        }
      Qed.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247

      (* ..., which implies that the service receive during a interval
         of length delta is at most delta. *)
      Lemma cumulative_service_le_delta :
        forall t delta, service_during sched j t (t + delta) <= delta.
      Proof.
        unfold service_at, jobs_dont_execute_in_parallel in *; ins.
        generalize dependent t.
        induction delta.
        {
          ins; unfold service_during; rewrite addn0.
          by rewrite big_geq.
        }
        {
          unfold service_during; intro t.
          rewrite -addn1 addnA addn1 big_nat_recr; last by apply leq_addr.
          apply leq_add; first by apply IHdelta.
          by apply service_at_most_one.
        }
      Qed.
248
        
Felipe Cerqueira's avatar
Felipe Cerqueira committed
249
    End NoParallelism.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
250
        
Felipe Cerqueira's avatar
Felipe Cerqueira committed
251
252
    Section Completion.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
253
254
      (* Assume that completed jobs do not execute. *)
      Hypothesis H_completed_jobs:
Felipe Cerqueira's avatar
Felipe Cerqueira committed
255
        completed_jobs_dont_execute job_cost sched.
256
              
Felipe Cerqueira's avatar
Felipe Cerqueira committed
257
258
259
260
      (* Then, after job j completes, it remains completed. *)
      Lemma completion_monotonic :
        forall t t',
          t <= t' ->
Felipe Cerqueira's avatar
Felipe Cerqueira committed
261
262
          completed job_cost sched j t ->
          completed job_cost sched j t'.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
263
264
265
      Proof.
        unfold completed; move => t t' LE /eqP COMPt.
        rewrite eqn_leq; apply/andP; split; first by apply H_completed_jobs.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
266
        by apply leq_trans with (n := service sched j t);
Felipe Cerqueira's avatar
Felipe Cerqueira committed
267
268
          [by rewrite COMPt | by apply extend_sum].
      Qed.
269
270
271
272
273
274
275
276
277
278
279
280
281
282

      (* A completed job cannot be scheduled. *)
      Lemma completed_implies_not_scheduled :
        forall t,
          completed job_cost sched j t ->
          ~~ scheduled sched j t.
      Proof.
        rename H_completed_jobs into COMP.
        unfold completed_jobs_dont_execute in *.
        intros t COMPLETED.
        apply/negP; red; intro SCHED.
        have BUG := COMP j t.+1.
        rewrite leqNgt in BUG; move: BUG => /negP BUG; apply BUG.
        unfold service; rewrite big_nat_recr // /= -addn1.
283
        apply leq_add; first by move: COMPLETED => /eqP <-.
284
285
286
287
        by rewrite lt0n -not_scheduled_no_service negbK.
      Qed.
        
      (* The service received by job j in any interval is no larger than its cost. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
288
      Lemma cumulative_service_le_job_cost :
Felipe Cerqueira's avatar
Felipe Cerqueira committed
289
        forall t t',
Felipe Cerqueira's avatar
Felipe Cerqueira committed
290
          service_during sched j t t' <= job_cost j.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
291
      Proof.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
292
        unfold service_during; rename H_completed_jobs into COMP; red in COMP; ins.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
293
294
        destruct (t > t') eqn:GT.
          by rewrite big_geq // -ltnS; apply ltn_trans with (n := t); ins.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
295
          apply leq_trans with
Felipe Cerqueira's avatar
Felipe Cerqueira committed
296
              (n := \sum_(0 <= t0 < t') service_at sched j t0);
Felipe Cerqueira's avatar
Felipe Cerqueira committed
297
298
299
300
            last by apply COMP.
          rewrite -> big_cat_nat with (m := 0) (n := t);
            [by apply leq_addl | by ins | by rewrite leqNgt negbT //].
      Qed.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
301
      
Felipe Cerqueira's avatar
Felipe Cerqueira committed
302
303
304
305
    End Completion.

    Section Arrival.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
306
307
      (* Assume that jobs must arrive to execute. *)
      Hypothesis H_jobs_must_arrive:
308
        jobs_must_arrive_to_execute sched.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
309

Felipe Cerqueira's avatar
Felipe Cerqueira committed
310
311
      (* Then, job j does not receive service at any time t prior to its arrival. *)
      Lemma service_before_job_arrival_zero :
312
313
        forall t,
          t < job_arrival j ->
Felipe Cerqueira's avatar
Felipe Cerqueira committed
314
          service_at sched j t = 0.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
315
      Proof.
316
        rename H_jobs_must_arrive into ARR; red in ARR; intros t LT.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
317
318
319
        specialize (ARR j t).
        apply contra with (c := scheduled sched j t)
                            (b := has_arrived j t) in ARR;
Felipe Cerqueira's avatar
Felipe Cerqueira committed
320
          last by rewrite -ltnNge.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
321
        apply/eqP; rewrite -leqn0; unfold service_at.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
322
323
        rewrite -> eq_bigr with (F2 := fun cpu => 0);
          first by rewrite big_const_seq iter_addn mul0n addn0.
324
        intros i SCHED; move: ARR; rewrite negb_exists_in; move => /forall_inP ARR.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
325
        by exploit (ARR i); [by ins | ins]; destruct (sched i t == Some j).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
326
327
      Qed.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
328
329
      (* The same applies for the cumulative service received by job j. *)
      Lemma cumulative_service_before_job_arrival_zero :
330
331
        forall t1 t2,
          t2 <= job_arrival j ->
Felipe Cerqueira's avatar
Felipe Cerqueira committed
332
          \sum_(t1 <= i < t2) service_at sched j i = 0.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
333
      Proof.
334
        intros t1 t2 LE; apply/eqP; rewrite -leqn0.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
335
336
337
338
        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.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
339
        rewrite service_before_job_arrival_zero; first by ins.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
340
341
342
        by apply leq_trans with (n := t2); ins.
      Qed.

Felix Stutz's avatar
Felix Stutz committed
343
      (* Hence, you can ignore the service received by a job before its arrival time. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
344
      Lemma service_before_arrival_eq_service_during :
345
346
        forall t0 t,
          t0 <= job_arrival j ->
Felipe Cerqueira's avatar
Felipe Cerqueira committed
347
348
          \sum_(t0 <= t < job_arrival j + t) service_at sched j t =
          \sum_(job_arrival j <= t < job_arrival j + t) service_at sched j t.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
349
      Proof.
350
        intros t0 t LE; rewrite -> big_cat_nat with (n := job_arrival j); [| by ins | by apply leq_addr].
Felipe Cerqueira's avatar
Felipe Cerqueira committed
351
        by rewrite /= cumulative_service_before_job_arrival_zero; [rewrite add0n | apply leqnn].
Felipe Cerqueira's avatar
Felipe Cerqueira committed
352
353
      Qed.
      
Felipe Cerqueira's avatar
Felipe Cerqueira committed
354
355
    End Arrival.

356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
    Section Pending.

      (* Assume that jobs must arrive to execute. *)
      Hypothesis H_jobs_must_arrive:
        jobs_must_arrive_to_execute sched.
      
     (* Assume that completed jobs do not execute. *)
      Hypothesis H_completed_jobs:
        completed_jobs_dont_execute job_cost sched.

      (* Then, if job j is scheduled, it must be pending. *)
      Lemma scheduled_implies_pending:
        forall t,
          scheduled sched j t ->
          pending job_cost sched j t.
      Proof.
        rename H_jobs_must_arrive into ARRIVE,
               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 ARRIVE.
        apply/negP; unfold not; intro COMPLETED.
        have BUG := COMP j t.+1.
        rewrite leqNgt in BUG; move: BUG => /negP BUG; apply BUG.
        unfold service; rewrite -addn1 big_nat_recr // /=.
        apply leq_add;
          first by move: COMPLETED => /eqP COMPLETED; rewrite -COMPLETED.
        rewrite lt0n; apply/eqP; red; move => /eqP NOSERV.
        rewrite -not_scheduled_no_service in NOSERV.
        by rewrite SCHED in NOSERV.
      Qed.

    End Pending.
    
  End JobLemmas.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
391

392
393
394
395
396
397
398
399
400
401
402
403
  (* In this section, we prove some lemmas about the list of jobs
     scheduled at time t. *)
  Section ScheduledJobsLemmas.

    (* Consider an arrival sequence ...*)
    Context {Job: eqType}.
    Context {arr_seq: arrival_sequence Job}.

    (* ... and some schedule. *)
    Context {num_cpus: nat}.
    Variable sched: schedule num_cpus arr_seq.

404
405
    Section Membership.
      
406
    (* A job is in the list of scheduled jobs iff it is scheduled. *)
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
      Lemma mem_scheduled_jobs_eq_scheduled :
        forall j t,
          j \in jobs_scheduled_at sched t = scheduled sched j t.
      Proof.
        unfold jobs_scheduled_at, scheduled.
        intros j t; apply/idP/idP.
        {
          intros IN.
          apply mem_bigcat_ord_exists in IN; des.
          apply/exists_inP; exists i; first by done.
          destruct (sched i t); last by done.
          by rewrite mem_seq1 in IN; move: IN => /eqP IN; subst.
        }
        {
          move => /exists_inP EX; destruct EX as [i IN SCHED].
          apply mem_bigcat_ord with (j := i); first by apply ltn_ord.
          by move: SCHED => /eqP SCHED; rewrite SCHED /= mem_seq1 eq_refl.
        }
      Qed.

    End Membership.
428
429
430
    
    Section Uniqueness.

431
      (* Suppose there's no job parallelism. *)
432
433
      Hypothesis H_no_parallelism :
        jobs_dont_execute_in_parallel sched.
434
435

      (* Then, the list of jobs scheduled at any time t has no duplicates. *)
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
      Lemma scheduled_jobs_uniq :
        forall t,
          uniq (jobs_scheduled_at sched t).
      Proof.
        intros t; rename H_no_parallelism into SEQUENTIAL.
        unfold jobs_dont_execute_in_parallel in SEQUENTIAL.
        clear -SEQUENTIAL.
        unfold jobs_scheduled_at.
        induction num_cpus; first by rewrite big_ord0.
        {

          rewrite big_ord_recr cat_uniq; apply/andP; split.
          {
            apply bigcat_ord_uniq;
              first by intro i; unfold make_sequence; desf.
            intros x i1 i2 IN1 IN2; unfold make_sequence in *.
            desf; move: Heq0 Heq => SOME1 SOME2.
            rewrite mem_seq1 in IN1; rewrite mem_seq1 in IN2.
            move: IN1 IN2 => /eqP IN1 /eqP IN2; subst x j0.
            specialize (SEQUENTIAL j t (widen_ord (leqnSn n) i1)
                           (widen_ord (leqnSn n) i2) SOME1 SOME2).
            by inversion SEQUENTIAL; apply ord_inj.
          }
          apply/andP; split; last by unfold make_sequence; destruct (sched ord_max).
          {
            rewrite -all_predC; apply/allP; unfold predC; simpl.
            intros x INx.
            unfold make_sequence in INx.
            destruct (sched ord_max t) eqn:SCHED;
              last by rewrite in_nil in INx.
            apply/negP; unfold not; intro IN'.
            have EX := mem_bigcat_ord_exists _ x n.
            apply EX in IN'; des; clear EX.
            unfold make_sequence in IN'.
            desf; rename Heq into SCHEDi.
            rewrite mem_seq1 in INx; rewrite mem_seq1 in IN'.
            move: INx IN' => /eqP INx /eqP IN'; subst x j0.
            specialize (SEQUENTIAL j t ord_max (widen_ord (leqnSn n) i) SCHED SCHEDi).
            inversion SEQUENTIAL; destruct i as [i EQ]; simpl in *.
            clear SEQUENTIAL SCHEDi.
            by rewrite H0 ltnn in EQ.
          }
        }
      Qed.

    End Uniqueness.
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497

    Section NumberOfJobs.

      (* The number of scheduled jobs is no larger than the number of cpus. *)
      Lemma num_scheduled_jobs_le_num_cpus :
        forall t,
          size (jobs_scheduled_at sched t) <= num_cpus.
      Proof.
        intros t.
        unfold jobs_scheduled_at.
        destruct num_cpus; first by rewrite big_ord0.
        apply size_bigcat_ord; first by apply (Ordinal (ltnSn n)).
        by ins; unfold make_sequence; desf.
      Qed.

    End NumberOfJobs.
498
499
500
    
  End ScheduledJobsLemmas.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
501
End Schedule.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
502
503

(* Specific properties of a schedule of sporadic jobs. *)
504
Module ScheduleOfSporadicTask.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
505

Felipe Cerqueira's avatar
Felipe Cerqueira committed
506
  Import SporadicTask Job.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
507
  Export Schedule.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
508

509
  Section Properties.
510

511
512
    Context {sporadic_task: eqType}.
    Context {Job: eqType}.    
Felipe Cerqueira's avatar
Felipe Cerqueira committed
513
514
515
    Variable job_cost: Job -> nat.
    Variable job_task: Job -> sporadic_task.

516
    (* Consider any schedule. *)
517
518
    Context {arr_seq: arrival_sequence Job}.
    Context {num_cpus: nat}.
519
    Variable sched: schedule num_cpus arr_seq.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
520

521
    (* Next we define intra-task parallelism, ... *)
522
523
524
    Definition jobs_of_same_task_dont_execute_in_parallel :=
      forall (j j': JobIn arr_seq) t,
        job_task j = job_task j' ->
525
        scheduled sched j t -> scheduled sched j' t -> j = j'.
526
527
528
529
530
531
532

    (* ... and task precedence constraints. *)
    Definition task_precedence_constraints :=
      forall (j j': JobIn arr_seq) t,
        job_task j = job_task j' ->
        job_arrival j < job_arrival j' ->
        pending job_cost sched j t -> ~~ scheduled sched j' t.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
533
    
534
  End Properties.
535

Felipe Cerqueira's avatar
Felipe Cerqueira committed
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
  Section BasicLemmas.

    (* Assume the job cost and task are known. *)
    Context {sporadic_task: eqType}.
    Variable task_cost: sporadic_task -> nat.
    Variable task_deadline: sporadic_task -> nat.
    
    Context {Job: eqType}.    
    Variable job_cost: Job -> nat.
    Variable job_deadline: Job -> nat.
    Variable job_task: Job -> sporadic_task.

    (* Then, in a valid schedule of sporadic tasks ...*)
    Context {arr_seq: arrival_sequence Job}.
    Context {num_cpus: nat}.
    Variable sched: schedule num_cpus arr_seq.

    (* ...such that jobs do not execute after completion, ...*)
    Hypothesis jobs_dont_execute_after_completion :
Felipe Cerqueira's avatar
Felipe Cerqueira committed
555
       completed_jobs_dont_execute job_cost sched.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
556
557
558
559
560
561
562
563
564
565
566

    Variable tsk: sporadic_task.
    
    Variable j: JobIn arr_seq.
    Hypothesis H_job_of_task: job_task j = tsk.
    Hypothesis valid_job:
      valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
    
    (* Remember that for any job of tsk, service <= task_cost tsk *)
    Lemma cumulative_service_le_task_cost :
        forall t t',
Felipe Cerqueira's avatar
Felipe Cerqueira committed
567
          service_during sched j t t' <= task_cost tsk.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
568
569
570
571
572
573
574
575
576
    Proof.
      rename valid_job into VALID; unfold valid_sporadic_job in *; ins; des.
      apply leq_trans with (n := job_cost j);
        last by rewrite -H_job_of_task; apply VALID0.
      by apply cumulative_service_le_job_cost.
    Qed.

  End BasicLemmas.
  
577
End ScheduleOfSporadicTask.
578

Felipe Cerqueira's avatar
Felipe Cerqueira committed
579
(* Specific properties for a schedule of sporadic tasks with jitter. *)
580
581
Module ScheduleOfTaskWithJitter.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
582
  Export ScheduleOfSporadicTask.
583
584
585
  
  Section ArrivalAfterJitter.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
586
    (* Assume the job cost, task and jitter are known. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
587
    Context {sporadic_task: eqType}.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
588
    Context {Job: eqType}.    
589
    Variable job_cost: Job -> nat.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
590
    Variable job_task: Job -> sporadic_task.
591
    Variable job_jitter: Job -> nat.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
592

Felipe Cerqueira's avatar
Felipe Cerqueira committed
593
    (* Then, in a valid schedule of sporadic jobs with jitter, ... *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
594
595
    Context {arr_seq: arrival_sequence Job}.
    Context {num_cpus: nat}.
596
    Variable sched: schedule num_cpus arr_seq.
597

Felipe Cerqueira's avatar
Felipe Cerqueira committed
598
    (* ... a job can only be scheduled after the jitter. *)
599
600
601
602
    Definition jobs_execute_after_jitter :=
      forall j t,
        scheduled sched j t ->
        job_arrival j + job_jitter j <= t.
603
604
605

    Section BasicLemmas.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
606
607
      (* Note that if a job only executes after the jitter, it also only
         executes after its arrival time. *)
608
609
610
611
612
613
614
615
616
617
618
619
      Lemma arrival_before_jitter :
        jobs_execute_after_jitter ->
        jobs_must_arrive_to_execute sched.
      Proof.
        unfold jobs_execute_after_jitter, jobs_must_arrive_to_execute.
        intros ARRIVE j t SCHED; unfold has_arrived.
        rewrite -(leq_add2r (job_jitter j)).
        by apply leq_trans with (n := t);
          [by apply ARRIVE | by apply leq_addr].
      Qed.
      
    End BasicLemmas.
620
621
622
623
 
  End ArrivalAfterJitter.

End ScheduleOfTaskWithJitter.