behavior/schedule/completion_facts.v

+From rt.behavior.schedule Require Export schedule service_facts.
+
+(** In this file, we establish basic facts about job completions. *)
+
+
+Section CompletionFacts.
+  (* Consider any job type,...*)
+  Context {Job: JobType}.
+  Context `{JobCost Job}.
+
+  (* ...any kind of processor model,... *)
+  Context {PState: Type}.
+  Context `{ProcessorState Job PState}.
+
+  (* ...and a given schedule. *)
+  Variable sched: schedule PState.
+
+  (* Let j be any job that is to be scheduled. *)
+  Variable j: Job.
+
+  (* We prove that after job j completes, it remains completed. *)
+  Lemma completion_monotonic:
+    forall t t',
+      t <= t' ->
+      completed_by sched j t ->
+      completed_by sched j t'.
+  Proof.
+    move => t t' LE. rewrite /completed_by /service => COMP.
+    apply leq_trans with (n := service_during sched j 0 t); auto.
+    by apply service_monotonic.
+  Qed.
+
+  (* We observe that being incomplete is the same as not having received
+     sufficient service yet... *)
+  Lemma less_service_than_cost_is_incomplete:
+    forall t,
+      service sched j t < job_cost j
+      <->
+      ~~ completed_by sched j t.
+  Proof.
+    move=> t. by split; rewrite /completed_by; [rewrite -ltnNge // | rewrite ltnNge //].
+  Qed.
+
+  (* ...which is also the same as having positive remaining cost. *)
+  Lemma incomplete_is_positive_remaining_cost:
+    forall t,
+      ~~ completed_by sched j t
+      <->
+      remaining_cost sched j t > 0.
+  Proof.
+    move=> t. by split; rewrite /remaining_cost -less_service_than_cost_is_incomplete subn_gt0 //.
+  Qed.
+
+  (* Assume that completed jobs do not execute. *)
+  Hypothesis H_completed_jobs:
+    completed_jobs_dont_execute sched.
+
+  (* Further, we note that if a job receives service at some time t, then its
+     remaining cost at this time is positive. *)
+  Lemma serviced_implies_positive_remaining_cost:
+    forall t,
+      service_at sched j t > 0 ->
+      remaining_cost sched j t > 0.
+  Proof.
+    move=> t SERVICE.
+    rewrite subn_gt0 /service /service_during.
+    apply leq_trans with (\sum_(0 <= t0 < t.+1) service_at sched j t0);
+      last by rewrite H_completed_jobs.
+      by rewrite big_nat_recr //= -addn1 leq_add2l.
+  Qed.
+
+  (* Consequently, if we have a have processor model where scheduled jobs
+   * necessarily receive service, we can conclude that scheduled jobs have
+   * remaining positive cost. *)
+
+  (* Assume a scheduled job always receives some positive service. *)
+  Hypothesis H_scheduled_implies_serviced:
+    forall j s, scheduled_in j s -> service_in j s > 0.
+
+  (* Then a scheduled job has positive remaining cost. *)
+  Corollary scheduled_implies_positive_remaining_cost:
+    forall t,
+      scheduled_at sched j t ->
+      remaining_cost sched j t > 0.
+  Proof.
+    rewrite /scheduled_at => t SCHEDULED.
+      by apply: serviced_implies_positive_remaining_cost; rewrite /service_at; apply: H_scheduled_implies_serviced.
+  Qed.
+
+  (* We also prove that a completed job cannot be scheduled... *)
+  Lemma completed_implies_not_scheduled:
+    forall t,
+      completed_by sched j t ->
+      ~~ scheduled_at 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.
+    rewrite /service /service_during big_nat_recr // /= -addn1.
+    apply leq_add.
+    * by rewrite -/(service_during sched j 0 t) -/(completed_by sched j t).
+    * by rewrite /service_at; apply: H_scheduled_implies_serviced; rewrite -/(scheduled_at _ _ _).
+  Qed.
+
+  (* ... and that a scheduled job cannot be completed. *)
+  Lemma scheduled_implies_not_completed:
+    forall t,
+      scheduled_at sched j t ->
+      ~~ completed_by sched j t.
+  Proof.
+    move=> t SCHED.
+    have REMPOS := scheduled_implies_positive_remaining_cost t SCHED.
+    rewrite /remaining_cost subn_gt0 in REMPOS.
+      by rewrite -less_service_than_cost_is_incomplete.
+  Qed.
+
+  (* We further observe that [service] and [remaining_cost] are complements of
+     one another. *)
+  Lemma service_cost_invariant:
+    forall t,
+      (service sched j t) + (remaining_cost sched j t) = job_cost j.
+  Proof.
+    move=> t. rewrite /remaining_cost subnKC //.
+  Qed.
+
+End CompletionFacts.
+
+
+Section ServiceAndCompletionFacts.
+  (** In this section, we establish some facts that are really about service,
+      but are also related to completion and rely on some of the above lemmas.
+      Hence they are in this file, rather than service_facts.v. *)
+
+  (* Consider any job type,...*)
+  Context {Job: JobType}.
+  Context `{JobCost Job}.
+
+  (* ...any kind of processor model,... *)
+  Context {PState: Type}.
+  Context `{ProcessorState Job PState}.
+
+  (* ...and a given schedule. *)
+  Variable sched: schedule PState.
+
+  (* Assume that completed jobs do not execute. *)
+  Hypothesis H_completed_jobs:
+    completed_jobs_dont_execute sched.
+
+  (* Let j be any job that is to be scheduled. *)
+  Variable j: Job.
+
+  (* Assume that a scheduled job receives exactly one time unit of service. *)
+  Hypothesis H_unit_service: unit_service_proc_model.
+
+  Section GuaranteedService.
+
+    (* Assume a scheduled job always receives some positive service. *)
+    Hypothesis H_scheduled_implies_serviced:
+      forall j s, scheduled_in j s -> service_in j s > 0.
+
+    (* Then we can easily show that the service never exceeds the total cost of
+       the job. *)
+    Lemma service_le_cost:
+      forall t,
+        service sched j t <= job_cost j.
+    Proof.
+      elim => [| n IH]; first by rewrite service0 //.
+      rewrite leq_eqVlt in IH.
+      case/orP: IH => [EQ | LT]; rewrite -service_last_plus_before.
+      * rewrite not_scheduled_implies_no_service; first by rewrite addn0 //.
+        apply: completed_implies_not_scheduled; auto. unfold unit_service_proc_model in H_unit_service.
+        move /eqP in EQ.
+        rewrite /completed_by EQ //.
+      * apply leq_trans with (n := service sched j n + 1).
+        - rewrite leq_add2l /service_at //.
+        - rewrite -(ltnS (service sched j n + 1) _) -(addn1 (job_cost j)) ltn_add2r //.
+    Qed.
+
+    (* We show that the service received by job j in any interval is no larger
+       than its cost. *)
+    Lemma cumulative_service_le_job_cost:
+      forall t t',
+        service_during sched j t t' <= job_cost j.
+    Proof.
+      move=> t t'.
+      case/orP: (leq_total t t') => [tt'|tt']; last by rewrite service_during_geq //.
+      apply leq_trans with (n := service sched j t'); last by apply: service_le_cost.
+      rewrite /service. rewrite -(service_during_cat sched j 0 t t') // leq_addl //.
+    Qed.
+
+  End GuaranteedService.
+
+  (* If a job isn't complete at time t, it can't be completed at time (t +
+     remaining_cost j t - 1). *)
+  Lemma job_doesnt_complete_before_remaining_cost:
+    forall t,
+      ~~ completed_by sched j t ->
+      ~~ completed_by sched j (t + remaining_cost sched j t - 1).
+  Proof.
+    move=> t.
+    rewrite incomplete_is_positive_remaining_cost => REMCOST.
+    rewrite -less_service_than_cost_is_incomplete -(service_cat sched j t);
+      last by rewrite -addnBA //; apply: leq_addr.
+    apply leq_ltn_trans with (n := service sched j t + remaining_cost sched j t - 1).
+    - by rewrite -!addnBA //; rewrite leq_add2l; apply cumulative_service_le_delta; exact.
+    - rewrite service_cost_invariant // -subn_gt0 subKn //.
+      move: REMCOST. rewrite /remaining_cost subn_gt0 => SERVICE.
+      by apply leq_ltn_trans with (n := service sched j t).
+ Qed.
+
+End ServiceAndCompletionFacts.

behavior/schedule/service_facts.v

+From rt.behavior.schedule Require Export schedule.
+From rt Require Import util.tactics.
+
+(** In this file, we establish basic facts about the service received by
+    jobs. *)
+
+
+Section UnitService.
+  (** To begin with, we establish facts about schedules in which a job receives
+      either 1 or 0 service units at all times. *)
+
+  (* Consider any job type and any processor state. *)
+  Context {Job: JobType}.
+  Context {PState: Type}.
+  Context `{ProcessorState Job PState}.
+
+  (* We say that a kind processor state provides unit service if no
+     job ever receives more than one unit of service at any time. *)
+  Definition unit_service_proc_model := forall j s, service_in j s <= 1.
+
+  (* Let's consider a unit-service model... *)
+  Hypothesis H_unit_service: unit_service_proc_model.
+
+  (* ...and a given schedule. *)
+  Variable sched: schedule PState.
+
+  (* Let j be any job that is to be scheduled. *)
+  Variable j: Job.
+
+  (* First, we prove that the instantaneous service cannot be greater than 1, ... *)
+  Lemma service_at_most_one:
+    forall t, service_at sched j t <= 1.
+  Proof.
+      by move=> t; rewrite /service_at.
+  Qed.
+
+  (* ...which implies that the cumulative service received by job j in any
+     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);
+      last by simpl_sum_const; rewrite addKn leqnn.
+      by apply: leq_sum => t' _; apply: service_at_most_one.
+  Qed.
+
+End UnitService.
+
+Section Composition.
+
+  (* Consider any job type and any processor state. *)
+  Context {Job: eqType}.
+  Context {PState: Type}.
+  Context `{ProcessorState Job PState}.
+
+  (* For any given schedule... *)
+  Variable sched: schedule PState.
+
+  (* ...and any given job... *)
+  Variable j: Job.
+
+  (* ...we establish a number of useful rewriting rules that decompose
+     the service received during an interval into smaller intervals. *)
+
+  (* As a trivial base case, no job receives any service during an empty
+     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.
+
+  (* Equally trivially, no job has received service prior to time zero. *)
+  Corollary service0:
+    service sched j 0 = 0.
+  Proof.
+    rewrite /service service_during_geq //.
+  Qed.
+
+  (* Trivially, an interval consiting of one time unit is equivalent to
+     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.
+
+  (* Next, we observe that we can look at the service received during an
+     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.
+
+  (* Since [service] is just a special case of [service_during], the same holds
+     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.
+
+  (* As a special case, we observe that the service during an interval can be
+     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.
+
+  (* Symmetrically, we have the same for the end of the interval. *)
+  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.
+    Proof.
+      move=> t1 t2 t1t2.
+      rewrite -(service_during_cat t1 t2 t2.+1); last by rewrite /(_ && _) ifT //.
+      rewrite service_during_instant //.
+    Qed.
+
+    (* And hence also for [service]. *)
+    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.
+
+  (* Finally, we deconstruct the service received during an interval [t1, t3)
+     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.
+
+Section Monotonicity.
+  (** We establish a basic fact about the monotonicity of service. *)
+
+  (* Consider any job type and any processor model. *)
+  Context {Job: JobType}.
+  Context {PState: Type}.
+  Context `{ProcessorState Job PState}.
+
+  (* Consider any given schedule... *)
+  Variable sched: schedule PState.
+
+  (* ...and a given job that is to be scheduled. *)
+  Variable j: Job.
+
+  (* We observe that the amount of service received is monotonic by definition. *)
+  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.
+  (* Consider any job type and any processor model. *)
+  Context {Job: JobType}.
+  Context {PState: Type}.
+  Context `{ProcessorState Job PState}.
+
+  (* Consider any given schedule... *)
+  Variable sched: schedule PState.
+
+  (* ...and a given job that is to be scheduled. *)
+  Variable j: Job.
+
+  (* We observe that a job that isn't scheduled cannot possibly receive service. *)
+  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 //.
+      by apply: negbTE.
+  Qed.
+
+End RelationToScheduled.

model/schedule/uni/service.v

@@ -310,9 +310,9 @@ Module Service.
       } 
     Qed.
     
-    (* Last, we prove that overall service of jobs at each time instant is at most 1. *)
+    (* We prove that the overall service of jobs at each time instant is at most 1. *)
     Lemma service_of_jobs_le_1:
-      forall t1 t2 t P,
+      forall (t1 t2 t: time) (P: Job -> bool),
         \sum_(j <- arrivals_between t1 t2 | P j) service_at sched j t <= 1.
     Proof.
       intros t1 t2 t P.
@@ -348,6 +348,23 @@ Module Service.
           by rewrite /service_at /scheduled_at SCHED.
       }
     Qed.
+
+    (* We prove that the overall service of jobs within 
+       some time interval [t, t + Δ) is at most Δ. *)
+    Lemma total_service_of_jobs_le_delta:  
+      forall (t Δ: time) (P: Job -> bool),
+        \sum_(j <- arrivals_between t (t + Δ) | P j)
+         service_during sched j t (t + Δ) <= Δ.
+    Proof.
+      intros.
+      have EQ: \sum_(t <= x < t + Δ) 1 = Δ.
+      { by rewrite big_const_nat iter_addn mul1n addn0 -{2}[t]addn0 subnDl subn0. } 
+      rewrite -{3}EQ; clear EQ.
+      rewrite exchange_big //=.
+      rewrite leq_sum //.
+      move => t' _.
+        by apply service_of_jobs_le_1.
+    Qed.
     
     (* In this section, we introduce a connection between the cumulative 
        service, cumulative workload, and completion of jobs. *)

util/sum.v

@@ -246,14 +246,14 @@ End ExtraLemmas.
 Section SumArithmetic.
 
   Lemma sum_seq_diff:
-    forall (T:eqType) (r: seq T) (F G : T -> nat),
-      (forall i : T, i \in r -> G i <= F i) ->
-      \sum_(i <- r) (F i - G i) = \sum_(i <- r) F i - \sum_(i <- r) G i.
+    forall (T:eqType) (rs: seq T) (F G : T -> nat),
+      (forall i : T, i \in rs -> G i <= F i) ->
+      \sum_(i <- rs) (F i - G i) = \sum_(i <- rs) F i - \sum_(i <- rs) G i.
   Proof.
     intros.
-    induction r; first by rewrite !big_nil subn0. 
+    induction rs; first by rewrite !big_nil subn0. 
     rewrite !big_cons subh2.
-    - apply/eqP; rewrite eqn_add2l; apply/eqP; apply IHr.
+    - apply/eqP; rewrite eqn_add2l; apply/eqP; apply IHrs.
         by intros; apply H; rewrite in_cons; apply/orP; right.
     - by apply H; rewrite in_cons; apply/orP; left.
     - rewrite big_seq_cond [in X in _ <= X]big_seq_cond.
@@ -272,6 +272,21 @@ Section SumArithmetic.
     move => i; rewrite mem_index_iota; move => /andP [_ LT].
       by apply ALL.
   Qed.
+
+  Lemma sum_pred_diff:
+    forall (T: eqType) (rs: seq T) (P: T -> bool) (F: T -> nat),
+      \sum_(r <- rs | P r) F r =
+      \sum_(r <- rs) F r - \sum_(r <- rs | ~~ P r) F r.
+  Proof.
+    clear; intros.
+    induction rs; first by rewrite !big_nil subn0.
+    rewrite !big_cons !IHrs; clear IHrs.
+    case (P a); simpl; last by rewrite subnDl.
+    rewrite addnBA; first by done.
+    rewrite big_mkcond leq_sum //.
+    intros t _.
+      by case (P t).
+  Qed.
   
   Lemma telescoping_sum :
     forall (T: Type) (F: T->nat) r (x0: T),