schedule.v 21 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 *)
79
    Definition carried_out (t1 t2: time) := arrived_between j t1 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
269
270
271
          [by rewrite COMPt | by apply extend_sum].
      Qed.
      
      (* Also, the service received by job j in any interval is no larger than its cost. *)
      Lemma cumulative_service_le_job_cost :
Felipe Cerqueira's avatar
Felipe Cerqueira committed
272
        forall t t',
Felipe Cerqueira's avatar
Felipe Cerqueira committed
273
          service_during sched j t t' <= job_cost j.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
274
      Proof.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
275
        unfold service_during; rename H_completed_jobs into COMP; red in COMP; ins.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
276
277
        destruct (t > t') eqn:GT.
          by rewrite big_geq // -ltnS; apply ltn_trans with (n := t); ins.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
278
          apply leq_trans with
Felipe Cerqueira's avatar
Felipe Cerqueira committed
279
              (n := \sum_(0 <= t0 < t') service_at sched j t0);
Felipe Cerqueira's avatar
Felipe Cerqueira committed
280
281
282
283
            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
284
      
Felipe Cerqueira's avatar
Felipe Cerqueira committed
285
286
287
288
    End Completion.

    Section Arrival.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
289
290
      (* Assume that jobs must arrive to execute. *)
      Hypothesis H_jobs_must_arrive:
291
        jobs_must_arrive_to_execute sched.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
292

Felipe Cerqueira's avatar
Felipe Cerqueira committed
293
294
295
      (* Then, job j does not receive service at any time t prior to its arrival. *)
      Lemma service_before_job_arrival_zero :
        forall t (LT: t < job_arrival j),
Felipe Cerqueira's avatar
Felipe Cerqueira committed
296
          service_at sched j t = 0.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
297
      Proof.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
298
299
300
301
        rename H_jobs_must_arrive into ARR; red in ARR; ins.
        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
302
          last by rewrite -ltnNge.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
303
        apply/eqP; rewrite -leqn0; unfold service_at.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
304
305
        rewrite -> eq_bigr with (F2 := fun cpu => 0);
          first by rewrite big_const_seq iter_addn mul0n addn0.
306
        intros i SCHED; move: ARR; rewrite negb_exists_in; move => /forall_inP ARR.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
307
        by exploit (ARR i); [by ins | ins]; destruct (sched i t == Some j).
Felipe Cerqueira's avatar
Felipe Cerqueira committed
308
309
      Qed.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
310
311
      (* The same applies for the cumulative service received by job j. *)
      Lemma cumulative_service_before_job_arrival_zero :
Felipe Cerqueira's avatar
Felipe Cerqueira committed
312
        forall t1 t2 (LT: t2 <= job_arrival j),
Felipe Cerqueira's avatar
Felipe Cerqueira committed
313
          \sum_(t1 <= i < t2) service_at sched j i = 0.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
314
315
316
317
318
319
      Proof.
        ins; 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.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
320
        rewrite service_before_job_arrival_zero; first by ins.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
321
322
323
        by apply leq_trans with (n := t2); ins.
      Qed.

Felix Stutz's avatar
Felix Stutz committed
324
      (* Hence, you can ignore the service received by a job before its arrival time. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
325
326
      Lemma service_before_arrival_eq_service_during :
        forall t0 t (LT: t0 <= job_arrival j),
Felipe Cerqueira's avatar
Felipe Cerqueira committed
327
328
          \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
329
330
      Proof.
        ins; rewrite -> big_cat_nat with (n := job_arrival j); [| by ins | by apply leq_addr].
Felipe Cerqueira's avatar
Felipe Cerqueira committed
331
        by rewrite /= cumulative_service_before_job_arrival_zero; [rewrite add0n | apply leqnn].
Felipe Cerqueira's avatar
Felipe Cerqueira committed
332
333
      Qed.
      
Felipe Cerqueira's avatar
Felipe Cerqueira committed
334
335
    End Arrival.

336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
    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
371

372
373
374
375
376
377
378
379
380
381
382
383
  (* 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.

384
    (* A job is in the list of scheduled jobs iff it is scheduled. *)
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
    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.
    
    Section Uniqueness.

407
      (* Suppose there's no job parallelism. *)
408
409
      Hypothesis H_no_parallelism :
        jobs_dont_execute_in_parallel sched.
410
411

      (* Then, the list of jobs scheduled at any time t has no duplicates. *)
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
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
      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.
    
  End ScheduledJobsLemmas.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
461
End Schedule.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
462
463

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

Felipe Cerqueira's avatar
Felipe Cerqueira committed
466
  Import SporadicTask Job.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
467
  Export Schedule.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
468

469
  Section Properties.
470

471
472
    Context {sporadic_task: eqType}.
    Context {Job: eqType}.    
Felipe Cerqueira's avatar
Felipe Cerqueira committed
473
474
475
    Variable job_cost: Job -> nat.
    Variable job_task: Job -> sporadic_task.

476
    (* Consider any schedule. *)
477
478
    Context {arr_seq: arrival_sequence Job}.
    Context {num_cpus: nat}.
479
    Variable sched: schedule num_cpus arr_seq.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
480

481
    (* Next we define intra-task parallelism, ... *)
482
483
484
    Definition jobs_of_same_task_dont_execute_in_parallel :=
      forall (j j': JobIn arr_seq) t,
        job_task j = job_task j' ->
485
        scheduled sched j t -> scheduled sched j' t -> j = j'.
486
487
488
489
490
491
492

    (* ... 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
493
    
494
  End Properties.
495

Felipe Cerqueira's avatar
Felipe Cerqueira committed
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
  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
515
       completed_jobs_dont_execute job_cost sched.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
516
517
518
519
520
521
522
523
524
525
526

    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
527
          service_during sched j t t' <= task_cost tsk.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
528
529
530
531
532
533
534
535
536
    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.
  
537
End ScheduleOfSporadicTask.
538

Felipe Cerqueira's avatar
Felipe Cerqueira committed
539
(* Specific properties for a schedule of sporadic tasks with jitter. *)
540
541
Module ScheduleOfTaskWithJitter.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
542
  Export ScheduleOfSporadicTask.
543
544
545
  
  Section ArrivalAfterJitter.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
546
    (* Assume the job cost, task and jitter are known. *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
547
    Context {sporadic_task: eqType}.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
548
    Context {Job: eqType}.    
549
    Variable job_cost: Job -> nat.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
550
    Variable job_task: Job -> sporadic_task.
551
    Variable job_jitter: Job -> nat.
Felipe Cerqueira's avatar
Felipe Cerqueira committed
552

Felipe Cerqueira's avatar
Felipe Cerqueira committed
553
    (* Then, in a valid schedule of sporadic jobs with jitter, ... *)
Felipe Cerqueira's avatar
Felipe Cerqueira committed
554
555
    Context {arr_seq: arrival_sequence Job}.
    Context {num_cpus: nat}.
556
    Variable sched: schedule num_cpus arr_seq.
557

Felipe Cerqueira's avatar
Felipe Cerqueira committed
558
    (* ... a job can only be scheduled after the jitter. *)
559
560
561
562
    Definition jobs_execute_after_jitter :=
      forall j t,
        scheduled sched j t ->
        job_arrival j + job_jitter j <= t.
563
564
565

    Section BasicLemmas.

Felipe Cerqueira's avatar
Felipe Cerqueira committed
566
567
      (* Note that if a job only executes after the jitter, it also only
         executes after its arrival time. *)
568
569
570
571
572
573
574
575
576
577
578
579
      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.
580
581
582
583
 
  End ArrivalAfterJitter.

End ScheduleOfTaskWithJitter.