service.v 23.9 KB
Newer Older
 Sergey Bozhko committed Dec 04, 2019 1 Require Export rt.util.all.  Björn Brandenburg committed Nov 20, 2019 2 Require Export rt.restructuring.analysis.basic_facts.ideal_schedule.  Sergey Bozhko committed Dec 04, 2019 3 4  From mathcomp Require Import ssrnat ssrbool fintype.  Björn Brandenburg committed May 13, 2019 5 6 7 8 9  (** In this file, we establish basic facts about the service received by jobs. *) Section Composition.  Björn Brandenburg committed May 16, 2019 10 11  (** To begin with, we provide some simple but handy rewriting rules for [service] and [service_during]. *)  Björn Brandenburg committed May 13, 2019 12   Björn Brandenburg committed Oct 15, 2019 13  (** Consider any job type and any processor state. *)  Björn Brandenburg committed Jun 25, 2019 14  Context {Job: JobType}.  Björn Brandenburg committed May 13, 2019 15 16 17  Context {PState: Type}. Context {ProcessorState Job PState}.  Björn Brandenburg committed Oct 15, 2019 18  (** For any given schedule... *)  Björn Brandenburg committed May 13, 2019 19 20  Variable sched: schedule PState.  Björn Brandenburg committed Oct 15, 2019 21  (** ...and any given job... *)  Björn Brandenburg committed May 13, 2019 22 23  Variable j: Job.  Björn Brandenburg committed Oct 15, 2019 24  (** ...we establish a number of useful rewriting rules that decompose  Björn Brandenburg committed May 13, 2019 25 26  the service received during an interval into smaller intervals. *)  Björn Brandenburg committed Oct 15, 2019 27  (** As a trivial base case, no job receives any service during an empty  Björn Brandenburg committed May 13, 2019 28 29 30 31 32 33 34 35 36  interval. *) Lemma service_during_geq: forall t1 t2, t1 >= t2 -> service_during sched j t1 t2 = 0. Proof. move=> t1 t2 t1t2. rewrite /service_during big_geq //. Qed.  Björn Brandenburg committed Oct 15, 2019 37  (** Equally trivially, no job has received service prior to time zero. *)  Björn Brandenburg committed May 13, 2019 38 39 40 41 42 43  Corollary service0: service sched j 0 = 0. Proof. rewrite /service service_during_geq //. Qed.  Björn Brandenburg committed Oct 15, 2019 44  (** Trivially, an interval consiting of one time unit is equivalent to  Björn Brandenburg committed May 13, 2019 45 46 47 48 49 50 51 52 53  service_at. *) Lemma service_during_instant: forall t, service_during sched j t t.+1 = service_at sched j t. Proof. move => t. by rewrite /service_during big_nat_recr ?big_geq //. Qed.  Björn Brandenburg committed Oct 15, 2019 54  (** Next, we observe that we can look at the service received during an  Björn Brandenburg committed May 13, 2019 55 56 57 58 59 60 61 62 63 64 65 66 67  interval [t1, t3) as the sum of the service during [t1, t2) and [t2, t3) for any t2 \in [t1, t3]. (The "_cat" suffix denotes the concatenation of the two intervals.) *) Lemma service_during_cat: forall t1 t2 t3, t1 <= t2 <= t3 -> (service_during sched j t1 t2) + (service_during sched j t2 t3) = service_during sched j t1 t3. Proof. move => t1 t2 t3 /andP [t1t2 t2t3]. by rewrite /service_during -big_cat_nat /=. Qed.  Björn Brandenburg committed Oct 15, 2019 68  (** Since [service] is just a special case of [service_during], the same holds  Björn Brandenburg committed May 13, 2019 69 70 71 72 73 74 75 76 77 78 79  for [service]. *) Lemma service_cat: forall t1 t2, t1 <= t2 -> (service sched j t1) + (service_during sched j t1 t2) = service sched j t2. Proof. move=> t1 t2 t1t2. rewrite /service service_during_cat //. Qed.  Björn Brandenburg committed Oct 15, 2019 80  (** As a special case, we observe that the service during an interval can be  Björn Brandenburg committed May 13, 2019 81 82 83 84 85 86 87 88 89 90 91 92 93  decomposed into the first instant and the rest of the interval. *) Lemma service_during_first_plus_later: forall t1 t2, t1 < t2 -> (service_at sched j t1) + (service_during sched j t1.+1 t2) = service_during sched j t1 t2. Proof. move => t1 t2 t1t2. have TIMES: t1 <= t1.+1 <= t2 by rewrite /(_ && _) ifT //. have SPLIT := service_during_cat t1 t1.+1 t2 TIMES. by rewrite -service_during_instant //. Qed.  Björn Brandenburg committed Oct 15, 2019 94  (** Symmetrically, we have the same for the end of the interval. *)  Björn Brandenburg committed May 13, 2019 95 96 97 98 99  Lemma service_during_last_plus_before: forall t1 t2, t1 <= t2 -> (service_during sched j t1 t2) + (service_at sched j t2) = service_during sched j t1 t2.+1.  Björn Brandenburg committed May 16, 2019 100 101 102 103 104  Proof. move=> t1 t2 t1t2. rewrite -(service_during_cat t1 t2 t2.+1); last by rewrite /(_ && _) ifT //. rewrite service_during_instant //. Qed.  Björn Brandenburg committed May 13, 2019 105   Björn Brandenburg committed Oct 15, 2019 106  (** And hence also for [service]. *)  Björn Brandenburg committed May 16, 2019 107 108 109 110 111 112 113 114  Corollary service_last_plus_before: forall t, (service sched j t) + (service_at sched j t) = service sched j t.+1. Proof. move=> t. rewrite /service. rewrite -service_during_last_plus_before //. Qed.  Björn Brandenburg committed May 13, 2019 115   Björn Brandenburg committed Oct 15, 2019 116  (** Finally, we deconstruct the service received during an interval [t1, t3)  Björn Brandenburg committed May 13, 2019 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131  into the service at a midpoint t2 and the service in the intervals before and after. *) Lemma service_split_at_point: forall t1 t2 t3, t1 <= t2 < t3 -> (service_during sched j t1 t2) + (service_at sched j t2) + (service_during sched j t2.+1 t3) = service_during sched j t1 t3. Proof. move => t1 t2 t3 /andP [t1t2 t2t3]. rewrite -addnA service_during_first_plus_later// service_during_cat// /(_ && _) ifT//. by exact: ltnW. Qed. End Composition.  Björn Brandenburg committed May 16, 2019 132 133 134 135 136  Section UnitService. (** As a common special case, we establish facts about schedules in which a job receives either 1 or 0 service units at all times. *)  Björn Brandenburg committed Oct 15, 2019 137  (** Consider any job type and any processor state. *)  Björn Brandenburg committed May 16, 2019 138 139 140 141  Context {Job: JobType}. Context {PState: Type}. Context {ProcessorState Job PState}.  Björn Brandenburg committed Oct 15, 2019 142  (** Let's consider a unit-service model... *)  Björn Brandenburg committed Oct 16, 2019 143  Hypothesis H_unit_service: unit_service_proc_model PState.  Björn Brandenburg committed May 16, 2019 144   Björn Brandenburg committed Oct 15, 2019 145  (** ...and a given schedule. *)  Björn Brandenburg committed May 16, 2019 146 147  Variable sched: schedule PState.  Björn Brandenburg committed Oct 15, 2019 148  (** Let j be any job that is to be scheduled. *)  Björn Brandenburg committed May 16, 2019 149 150  Variable j: Job.  Björn Brandenburg committed Oct 15, 2019 151  (** First, we prove that the instantaneous service cannot be greater than 1, ... *)  Björn Brandenburg committed May 16, 2019 152 153 154 155 156 157  Lemma service_at_most_one: forall t, service_at sched j t <= 1. Proof. by move=> t; rewrite /service_at. Qed.  Björn Brandenburg committed Oct 15, 2019 158  (** ...which implies that the cumulative service received by job j in any  Björn Brandenburg committed May 16, 2019 159 160 161 162 163 164 165  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_during; intros t delta. apply leq_trans with (n := \sum_(t <= t0 < t + delta) 1);  Björn Brandenburg committed Nov 15, 2019 166 167  last by rewrite sum_of_ones. by apply: leq_sum => t' _; apply: service_at_most_one.  Björn Brandenburg committed May 16, 2019 168 169 170 171  Qed. Section ServiceIsAStepFunction.  Björn Brandenburg committed Oct 15, 2019 172  (** We show that the service received by any job j is a step function. *)  Björn Brandenburg committed May 16, 2019 173 174 175 176 177 178 179 180  Lemma service_is_a_step_function: is_step_function (service sched j). Proof. rewrite /is_step_function => t. rewrite addn1 -service_last_plus_before leq_add2l. apply service_at_most_one. Qed.  Björn Brandenburg committed Oct 15, 2019 181  (** Next, consider any time t... *)  Björn Brandenburg committed May 16, 2019 182 183  Variable t: instant.  Björn Brandenburg committed Oct 15, 2019 184  (** ...and let s0 be any value less than the service received  Björn Brandenburg committed May 16, 2019 185 186 187 188  by job j by time t. *) Variable s0: duration. Hypothesis H_less_than_s: s0 < service sched j t.  Björn Brandenburg committed Oct 15, 2019 189  (** Then, we show that there exists an earlier time t0 where job j had s0  Björn Brandenburg committed May 16, 2019 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206  units of service. *) Corollary exists_intermediate_service: exists t0, t0 < t /\ service sched j t0 = s0. Proof. feed (exists_intermediate_point (service sched j)); [by apply service_is_a_step_function | intros EX]. feed (EX 0 t); first by done. feed (EX s0); first by rewrite /service /service_during big_geq //. by move: EX => /= [x_mid EX]; exists x_mid. Qed. End ServiceIsAStepFunction. End UnitService.  Björn Brandenburg committed May 13, 2019 207 208 209 Section Monotonicity. (** We establish a basic fact about the monotonicity of service. *)  Björn Brandenburg committed Oct 15, 2019 210  (** Consider any job type and any processor model. *)  Björn Brandenburg committed May 13, 2019 211 212 213 214  Context {Job: JobType}. Context {PState: Type}. Context {ProcessorState Job PState}.  Björn Brandenburg committed Oct 15, 2019 215  (** Consider any given schedule... *)  Björn Brandenburg committed May 13, 2019 216 217  Variable sched: schedule PState.  Björn Brandenburg committed Oct 15, 2019 218  (** ...and a given job that is to be scheduled. *)  Björn Brandenburg committed May 13, 2019 219 220  Variable j: Job.  Björn Brandenburg committed Oct 15, 2019 221  (** We observe that the amount of service received is monotonic by definition. *)  Björn Brandenburg committed May 13, 2019 222 223 224 225 226 227 228 229 230 231 232 233  Lemma service_monotonic: forall t1 t2, t1 <= t2 -> service sched j t1 <= service sched j t2. Proof. move=> t1 t2 let1t2. by rewrite -(service_cat sched j t1 t2 let1t2); apply: leq_addr. Qed. End Monotonicity. Section RelationToScheduled.  Björn Brandenburg committed Oct 15, 2019 234  (** Consider any job type and any processor model. *)  Björn Brandenburg committed May 13, 2019 235 236 237 238  Context {Job: JobType}. Context {PState: Type}. Context {ProcessorState Job PState}.  Björn Brandenburg committed Oct 15, 2019 239  (** Consider any given schedule... *)  Björn Brandenburg committed May 13, 2019 240 241  Variable sched: schedule PState.  Björn Brandenburg committed Oct 15, 2019 242  (** ...and a given job that is to be scheduled. *)  Björn Brandenburg committed May 13, 2019 243 244  Variable j: Job.  Björn Brandenburg committed Oct 15, 2019 245  (** We observe that a job that isn't scheduled cannot possibly receive service. *)  Björn Brandenburg committed May 13, 2019 246 247 248 249 250 251 252 253 254  Lemma not_scheduled_implies_no_service: forall t, ~~ scheduled_at sched j t -> service_at sched j t = 0. Proof. rewrite /service_at /scheduled_at. move=> t NOT_SCHED. rewrite service_implies_scheduled //. Qed.  Björn Brandenburg committed Oct 15, 2019 255  (** Conversely, if a job receives service, then it must be scheduled. *)  Björn Brandenburg committed May 16, 2019 256 257 258 259 260 261 262 263 264  Lemma service_at_implies_scheduled_at: forall t, service_at sched j t > 0 -> scheduled_at sched j t. Proof. move=> t. destruct (scheduled_at sched j t) eqn:SCHEDULED; first trivial. rewrite not_scheduled_implies_no_service // negbT //. Qed.  Björn Brandenburg committed Oct 15, 2019 265  (** Thus, if the cumulative amount of service changes, then it must be  Björn Brandenburg committed May 16, 2019 266 267 268 269 270 271 272 273 274 275  scheduled, too. *) Lemma service_delta_implies_scheduled: forall t, service sched j t < service sched j t.+1 -> scheduled_at sched j t. Proof. move => t. rewrite -service_last_plus_before -{1}(addn0 (service sched j t)) ltn_add2l. apply: service_at_implies_scheduled_at. Qed.  Björn Brandenburg committed Oct 15, 2019 276  (** We observe that a job receives cumulative service during some interval iff  Björn Brandenburg committed May 16, 2019 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291  it receives services at some specific time in the interval. *) Lemma service_during_service_at: forall t1 t2, service_during sched j t1 t2 > 0 <-> exists t, t1 <= t < t2 /\ service_at sched j t > 0. Proof. split. { move=> NONZERO. case (boolP([exists t: 'I_t2, (t >= t1) && (service_at sched j t > 0)])) => [EX | ALL]. - move: EX => /existsP [x /andP [GE SERV]].  Björn Brandenburg committed Nov 15, 2019 292 293  exists x; split => //. apply /andP; by split.  Björn Brandenburg committed May 16, 2019 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313  - rewrite negb_exists in ALL; move: ALL => /forallP ALL. rewrite /service_during big_nat_cond in NONZERO. rewrite big1 ?ltn0 // in NONZERO => i. rewrite andbT; move => /andP [GT LT]. specialize (ALL (Ordinal LT)); simpl in ALL. rewrite GT andTb -eqn0Ngt in ALL. apply /eqP => //. } { move=> [t [TT SERVICE]]. case (boolP (0 < service_during sched j t1 t2)) => // NZ. exfalso. rewrite -eqn0Ngt in NZ. move/eqP: NZ. rewrite big_nat_eq0 => IS_ZERO. have NO_SERVICE := IS_ZERO t TT. apply lt0n_neq0 in SERVICE. by move/neqP in SERVICE; contradiction. } Qed.  Björn Brandenburg committed Oct 15, 2019 314  (** Thus, any job that receives some service during an interval must be  Björn Brandenburg committed May 16, 2019 315 316  scheduled at some point during the interval... *) Corollary cumulative_service_implies_scheduled:  Björn Brandenburg committed May 16, 2019 317 318 319 320 321 322  forall t1 t2, service_during sched j t1 t2 > 0 -> exists t, t1 <= t < t2 /\ scheduled_at sched j t. Proof.  Björn Brandenburg committed May 16, 2019 323 324 325 326 327 328  move=> t1 t2. rewrite service_during_service_at. move=> [t' [TIMES SERVICED]]. exists t'; split => //. by apply: service_at_implies_scheduled_at. Qed.  Björn Brandenburg committed May 16, 2019 329   Björn Brandenburg committed Oct 15, 2019 330  (** ...which implies that any job with positive cumulative service must have  Björn Brandenburg committed May 16, 2019 331 332  been scheduled at some point. *) Corollary positive_service_implies_scheduled_before:  Björn Brandenburg committed May 16, 2019 333 334 335  forall t, service sched j t > 0 -> exists t', (t' < t /\ scheduled_at sched j t'). Proof.  Björn Brandenburg committed May 16, 2019 336 337 338  move=> t2. rewrite /service => NONZERO. have EX_SCHED := cumulative_service_implies_scheduled 0 t2 NONZERO.  Björn Brandenburg committed May 16, 2019 339  by move: EX_SCHED => [t [TIMES SCHED_AT]]; exists t; split.  Björn Brandenburg committed May 16, 2019 340 341  Qed.  Björn Brandenburg committed May 16, 2019 342  Section GuaranteedService.  Björn Brandenburg committed Oct 15, 2019 343  (** If we can assume that a scheduled job always receives service, we can  Björn Brandenburg committed May 16, 2019 344 345  further prove the converse. *)  Björn Brandenburg committed Oct 15, 2019 346  (** Assume j always receives some positive service. *)  Björn Brandenburg committed Oct 16, 2019 347  Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model PState.  Björn Brandenburg committed May 16, 2019 348   Björn Brandenburg committed Oct 15, 2019 349  (** In other words, not being scheduled is equivalent to receiving zero  Björn Brandenburg committed May 16, 2019 350 351 352 353 354 355 356  service. *) Lemma no_service_not_scheduled: forall t, ~~ scheduled_at sched j t <-> service_at sched j t = 0. Proof. move=> t. rewrite /scheduled_at /service_at. split => [NOT_SCHED | NO_SERVICE].  Maxime Lesourd committed Oct 15, 2019 357  - by rewrite service_implies_scheduled //.  Björn Brandenburg committed Aug 13, 2019 358  - apply (contra (H_scheduled_implies_serviced j (sched t))).  Björn Brandenburg committed May 16, 2019 359 360 361  by rewrite -eqn0Ngt; apply /eqP => //. Qed.  Björn Brandenburg committed Oct 15, 2019 362  (** Then, if a job does not receive any service during an interval, it  Björn Brandenburg committed May 16, 2019 363 364 365 366 367 368 369 370 371 372 373 374 375 376  is not scheduled. *) Lemma no_service_during_implies_not_scheduled: forall t1 t2, service_during sched j t1 t2 = 0 -> forall t, t1 <= t < t2 -> ~~ scheduled_at sched j t. Proof. move=> t1 t2 ZERO_SUM t /andP [GT_t1 LT_t2]. rewrite no_service_not_scheduled. move: ZERO_SUM. rewrite /service_during big_nat_eq0 => IS_ZERO. by apply (IS_ZERO t); apply /andP; split => //. Qed.  Björn Brandenburg committed Oct 15, 2019 377  (** If a job is scheduled at some point in an interval, it receivees  Björn Brandenburg committed May 16, 2019 378 379 380 381 382 383 384 385 386 387 388 389  positive cumulative service during the interval... *) Lemma scheduled_implies_cumulative_service: forall t1 t2, (exists t, t1 <= t < t2 /\ scheduled_at sched j t) -> service_during sched j t1 t2 > 0. Proof. move=> t1 t2 [t' [TIMES SCHED]]. rewrite service_during_service_at. exists t'; split => //. move: SCHED. rewrite /scheduled_at /service_at.  Björn Brandenburg committed Aug 13, 2019 390  by apply (H_scheduled_implies_serviced j (sched t')).  Björn Brandenburg committed May 16, 2019 391 392  Qed.  Björn Brandenburg committed Oct 15, 2019 393  (** ...which again applies to total service, too. *)  Björn Brandenburg committed May 16, 2019 394 395 396 397 398 399 400 401 402 403 404 405 406 407  Corollary scheduled_implies_nonzero_service: forall t, (exists t', t' < t /\ scheduled_at sched j t') -> service sched j t > 0. Proof. move=> t [t' [TT SCHED]]. rewrite /service. apply scheduled_implies_cumulative_service. exists t'; split => //. Qed. End GuaranteedService.  Björn Brandenburg committed May 16, 2019 408  Section AfterArrival.  Björn Brandenburg committed Oct 15, 2019 409  (** Futhermore, if we know that jobs are not released early, then we can  Björn Brandenburg committed May 16, 2019 410 411 412 413  narrow the interval during which they must have been scheduled. *) Context {JobArrival Job}.  Björn Brandenburg committed Oct 15, 2019 414  (** Assume that jobs must arrive to execute. *)  Björn Brandenburg committed May 16, 2019 415 416 417  Hypothesis H_jobs_must_arrive: jobs_must_arrive_to_execute sched.  Björn Brandenburg committed Oct 15, 2019 418  (** We prove that any job with positive cumulative service at time [t] must  Björn Brandenburg committed May 16, 2019 419 420 421  have been scheduled some time since its arrival and before time [t]. *) Lemma positive_service_implies_scheduled_since_arrival: forall t,  Björn Brandenburg committed May 16, 2019 422 423  service sched j t > 0 -> exists t', (job_arrival j <= t' < t /\ scheduled_at sched j t').  Björn Brandenburg committed May 16, 2019 424 425 426 427 428 429 430 431 432 433  Proof. move=> t SERVICE. have EX_SCHED := positive_service_implies_scheduled_before t SERVICE. inversion EX_SCHED as [t'' [TIMES SCHED_AT]]. exists t''; split; last by assumption. rewrite /(_ && _) ifT //. move: H_jobs_must_arrive. rewrite /jobs_must_arrive_to_execute /has_arrived => ARR. by apply: ARR; exact. Qed.  Björn Brandenburg committed May 16, 2019 434 435 436 437 438 439 440 441  Lemma not_scheduled_before_arrival: forall t, t < job_arrival j -> ~~ scheduled_at sched j t. Proof. move=> t EARLY. apply: (contra (H_jobs_must_arrive j t)). rewrite /has_arrived -ltnNge //. Qed.  Björn Brandenburg committed Oct 15, 2019 442  (** We show that job j does not receive service at any time t prior to its  Björn Brandenburg committed May 16, 2019 443 444 445 446 447 448 449 450 451 452  arrival. *) Lemma service_before_job_arrival_zero: forall t, t < job_arrival j -> service_at sched j t = 0. Proof. move=> t NOT_ARR. rewrite not_scheduled_implies_no_service // not_scheduled_before_arrival //. Qed.  Björn Brandenburg committed Oct 15, 2019 453  (** Note that the same property applies to the cumulative service. *)  Björn Brandenburg committed May 16, 2019 454 455 456 457 458 459 460 461  Lemma cumulative_service_before_job_arrival_zero : forall t1 t2 : instant, t2 <= job_arrival j -> service_during sched j t1 t2 = 0. Proof. move=> t1 t2 EARLY. rewrite /service_during. have ZERO_SUM: \sum_(t1 <= t < t2) service_at sched j t = \sum_(t1 <= t < t2) 0;  Björn Brandenburg committed May 16, 2019 462  last by rewrite ZERO_SUM sum0.  Björn Brandenburg committed May 16, 2019 463 464 465 466 467 468  rewrite big_nat_cond [in RHS]big_nat_cond. apply: eq_bigr => i /andP [TIMES _]. move: TIMES => /andP [le_t1_i lt_i_t2]. apply (service_before_job_arrival_zero i). by apply leq_trans with (n := t2); auto. Qed.  Björn Brandenburg committed Oct 15, 2019 469  (** Hence, one can ignore the service received by a job before its arrival  Björn Brandenburg committed May 16, 2019 470 471 472 473 474 475 476 477 478 479 480 481 482  time... *) Lemma ignore_service_before_arrival: forall t1 t2, t1 <= job_arrival j -> t2 >= job_arrival j -> service_during sched j t1 t2 = service_during sched j (job_arrival j) t2. Proof. move=> t1 t2 le_t1 le_t2. rewrite -(service_during_cat sched j t1 (job_arrival j) t2). rewrite cumulative_service_before_job_arrival_zero //. by apply/andP; split; exact. Qed.  Björn Brandenburg committed Oct 15, 2019 483  (** ... which we can also state in terms of cumulative service. *)  Björn Brandenburg committed May 16, 2019 484 485 486 487 488 489 490 491  Corollary no_service_before_arrival: forall t, t <= job_arrival j -> service sched j t = 0. Proof. move=> t EARLY. rewrite /service cumulative_service_before_job_arrival_zero //. Qed.  Björn Brandenburg committed May 16, 2019 492 493  End AfterArrival.  Björn Brandenburg committed May 16, 2019 494 495 496 497  Section TimesWithSameService. (** In this section, we prove some lemmas about time instants with same service. *)  Björn Brandenburg committed Oct 15, 2019 498  (** Consider any time instants t1 and t2... *)  Björn Brandenburg committed May 16, 2019 499 500  Variable t1 t2: instant.  Björn Brandenburg committed Oct 15, 2019 501  (** ...where t1 is no later than t2... *)  Björn Brandenburg committed May 16, 2019 502 503  Hypothesis H_t1_le_t2: t1 <= t2.  Björn Brandenburg committed Oct 15, 2019 504  (** ...and where job j has received the same amount of service. *)  Björn Brandenburg committed May 16, 2019 505 506  Hypothesis H_same_service: service sched j t1 = service sched j t2.  Björn Brandenburg committed Oct 15, 2019 507  (** First, we observe that this means that the job receives no service  Björn Brandenburg committed May 16, 2019 508 509 510 511 512 513 514 515 516  during [t1, t2)... *) Lemma constant_service_implies_no_service_during: service_during sched j t1 t2 = 0. Proof. move: H_same_service. rewrite -(service_cat sched j t1 t2) // -[service sched j t1 in LHS]addn0 => /eqP. by rewrite eqn_add2l => /eqP //. Qed.  Björn Brandenburg committed Oct 15, 2019 517  (** ...which of course implies that it does not receive service at any  Björn Brandenburg committed May 16, 2019 518 519 520 521 522 523 524 525 526 527 528  point, either. *) Lemma constant_service_implies_not_scheduled: forall t, t1 <= t < t2 -> service_at sched j t = 0. Proof. move=> t /andP [GE_t1 LT_t2]. move: constant_service_implies_no_service_during. rewrite /service_during big_nat_eq0 => IS_ZERO. apply IS_ZERO. apply /andP; split => //. Qed.  Björn Brandenburg committed Oct 15, 2019 529  (** We show that job j receives service at some point t < t1 iff j receives  Björn Brandenburg committed May 16, 2019 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551  service at some point t' < t2. *) Lemma same_service_implies_serviced_at_earlier_times: [exists t: 'I_t1, service_at sched j t > 0] = [exists t': 'I_t2, service_at sched j t' > 0]. Proof. apply /idP/idP => /existsP [t SERVICED]. { have LE: t < t2 by apply: (leq_trans _ H_t1_le_t2) => //. by apply /existsP; exists (Ordinal LE). } { case (boolP (t < t1)) => LE. - by apply /existsP; exists (Ordinal LE). - exfalso. have TIMES: t1 <= t < t2 by apply /andP; split => //; rewrite leqNgt //. have NO_SERVICE := constant_service_implies_not_scheduled t TIMES. by rewrite NO_SERVICE in SERVICED. } Qed.  Björn Brandenburg committed Oct 15, 2019 552  (** Then, under the assumption that scheduled jobs receives service,  Björn Brandenburg committed May 16, 2019 553 554  we can translate this into a claim about scheduled_at. *)  Björn Brandenburg committed Oct 15, 2019 555  (** Assume j always receives some positive service. *)  Björn Brandenburg committed Oct 16, 2019 556  Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model PState.  Björn Brandenburg committed May 16, 2019 557   Björn Brandenburg committed Oct 15, 2019 558  (** We show that job j is scheduled at some point t < t1 iff j is scheduled  Björn Brandenburg committed May 16, 2019 559 560 561 562 563 564 565 566 567 568  at some point t' < t2. *) Lemma same_service_implies_scheduled_at_earlier_times: [exists t: 'I_t1, scheduled_at sched j t] = [exists t': 'I_t2, scheduled_at sched j t']. Proof. have CONV: forall B, [exists b: 'I_B, scheduled_at sched j b] = [exists b: 'I_B, service_at sched j b > 0]. { move=> B. apply/idP/idP => /existsP [b P]; apply /existsP; exists b. - by move: P; rewrite /scheduled_at /service_at;  Björn Brandenburg committed Aug 13, 2019 569  apply (H_scheduled_implies_serviced j (sched b)).  Björn Brandenburg committed May 16, 2019 570 571 572 573 574 575 576  - by apply service_at_implies_scheduled_at. } rewrite !CONV. apply same_service_implies_serviced_at_earlier_times. Qed. End TimesWithSameService.  Björn Brandenburg committed May 13, 2019 577 End RelationToScheduled.  Sergey Bozhko committed Nov 19, 2019 578   Björn Brandenburg committed Nov 20, 2019 579 Require Import rt.restructuring.model.processor.ideal.  Sergey Bozhko committed Nov 19, 2019 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686  (** * Incremental Service in Ideal Schedule *) (** In the following section we prove a few facts about service in ideal schedeule. *) (* Note that these lemmas can be generalized to an arbitrary scheduler. *) Section IncrementalService. (** Consider any job type, ... *) Context {Job : JobType}. Context {JobArrival Job}. Context {JobCost Job}. (** ... any arrival sequence, ... *) Variable arr_seq : arrival_sequence Job. (** ... and any ideal uniprocessor schedule of this arrival sequence. *) Variable sched : schedule (ideal.processor_state Job). (** As a base case, we prove that if a job j receives service in some time interval [t1,t2), then there exists a time instant t ∈ [t1,t2) such that j is scheduled at time t and t is the first instant where j receives service. *) Lemma positive_service_during: forall j t1 t2, 0 < service_during sched j t1 t2 -> exists t : nat, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0. Proof. intros j t1 t2 SERV. have LE: t1 <= t2. { rewrite leqNgt; apply/negP; intros CONTR. by apply ltnW in CONTR; move: SERV; rewrite /service_during big_geq. } destruct (scheduled_at sched j t1) eqn:SCHED. { exists t1; repeat split; try done. - apply/andP; split; first by done. rewrite ltnNge; apply/negP; intros CONTR. by move: SERV; rewrite/service_during big_geq. - by rewrite /service_during big_geq. } { apply negbT in SCHED. move: SERV; rewrite /service /service_during; move => /sum_seq_gt0P [t [IN SCHEDt]]. rewrite lt0b in SCHEDt. rewrite mem_iota subnKC in IN; last by done. move: IN => /andP [IN1 IN2]. move: (exists_first_intermediate_point ((fun t => scheduled_at sched j t)) t1 t IN1 SCHED) => A. feed A; first by rewrite scheduled_at_def/=. move: A => [x [/andP [T1 T4] [T2 T3]]]. exists x; repeat split; try done. - apply/andP; split; first by apply ltnW. by apply leq_ltn_trans with t. - apply/eqP; rewrite big_nat_cond big1 //. move => y /andP [T5 _]. by apply/eqP; rewrite eqb0; specialize (T2 y); rewrite scheduled_at_def/= in T2; apply T2. } Qed. (** Next, we prove that if in some time interval [t1,t2) a job j receives k units of service, then there exists a time instant t ∈ [t1,t2) such that j is scheduled at time t and service of job j within interval [t1,t) is equal to k. *) Lemma incremental_service_during: forall j t1 t2 k, service_during sched j t1 t2 > k -> exists t, t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k. Proof. intros j t1 t2 k SERV. have LE: t1 <= t2. { rewrite leqNgt; apply/negP; intros CONTR. by apply ltnW in CONTR; move: SERV; rewrite /service_during big_geq. } induction k; first by apply positive_service_during in SERV. feed IHk; first by apply ltn_trans with k.+1. move: IHk => [t [/andP [NEQ1 NEQ2] [SCHEDt SERVk]]]. have SERVk1: service_during sched j t1 t.+1 = k.+1. { rewrite -(service_during_cat _ _ _ t); last by apply/andP; split. rewrite SERVk -[X in _ = X]addn1; apply/eqP; rewrite eqn_add2l. by rewrite /service_during big_nat1 /service_at eqb1 -scheduled_at_def/=. } move: SERV; rewrite -(service_during_cat _ _ _ t.+1); last first. { by apply/andP; split; first apply leq_trans with t. } rewrite SERVk1 -addn1 leq_add2l; move => SERV. destruct (scheduled_at sched j t.+1) eqn:SCHED. - exists t.+1; repeat split; try done. apply/andP; split. + apply leq_trans with t; by done. + rewrite ltnNge; apply/negP; intros CONTR. by move: SERV; rewrite /service_during big_geq. - apply negbT in SCHED. move: SERV; rewrite /service /service_during; move => /sum_seq_gt0P [x [INx SCHEDx]]. rewrite lt0b in SCHEDx. rewrite mem_iota subnKC in INx; last by done. move: INx => /andP [INx1 INx2]. move: (exists_first_intermediate_point _ _ _ INx1 SCHED) => A. feed A; first by rewrite scheduled_at_def/=. move: A => [y [/andP [T1 T4] [T2 T3]]]. exists y; repeat split; try done. + apply/andP; split. apply leq_trans with t; first by done. apply ltnW, ltn_trans with t.+1; by done. by apply leq_ltn_trans with x. + rewrite (@big_cat_nat _ _ _ t.+1) //=; [ | by apply leq_trans with t | by apply ltn_trans with t.+1]. unfold service_during in SERVk1; rewrite SERVk1; apply/eqP. rewrite -{2}[k.+1]addn0 eqn_add2l. rewrite big_nat_cond big1 //; move => z /andP [H5 _]. by apply/eqP; rewrite eqb0; specialize (T2 z); rewrite scheduled_at_def/= in T2; apply T2. Qed. End IncrementalService.`