Library prosa.analysis.facts.behavior.service

Service

In this file, we establish basic facts about the service received by jobs.
To begin with, we provide some simple but handy rewriting rules for service and service_during.
Section Composition.

Consider any job type and any processor state.
  Context {Job: JobType}.
  Context {PState: ProcessorState Job}.

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:
     t1 t2,
      t1 t2 service_during sched j t1 t2 = 0.
  Proof. by move⇒ ? ? ?; 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. by rewrite /service service_during_geq. Qed.

Trivially, an interval consisting of one time unit is equivalent to service_at.
  Lemma service_during_instant:
     t,
      service_during sched j t t.+1 = service_at sched j t.
  Proof. by move⇒ ?; 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:
     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. by move ⇒ ? ? ? /andP[? ?]; rewrite -big_cat_nat. Qed.

Since service is just a special case of service_during, the same holds for service.
  Lemma service_cat:
     t1 t2,
      t1 t2
      (service sched j t1) + (service_during sched j t1 t2)
      = service sched j t2.
  Proof. move⇒ ? ? ?; exact: 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:
     t1 t2,
      t1 < t2
      (service_at sched j t1) + (service_during sched j t1.+1 t2)
      = service_during sched j t1 t2.
  Proof.
    by move⇒ ? ? ?; rewrite -service_during_instant service_during_cat// leqnSn.
  Qed.

Symmetrically, we have the same for the end of the interval.
  Lemma service_during_last_plus_before:
     t1 t2,
      t1 t2
      (service_during sched j t1 t2) + (service_at sched j t2)
      = service_during sched j t1 t2.+1.
  Proof.
    movet1 t2 ?; rewrite -(service_during_cat t1 t2 t2.+1) ?leqnSn ?andbT//.
    by rewrite service_during_instant.
  Qed.

And hence also for service.
  Corollary service_last_plus_before:
     t,
      (service sched j t) + (service_at sched j t)
      = service sched j t.+1.
  Proof. move⇒ ?; exact: 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:
     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.
    movet1 t2 t3 /andP[t1t2 t2t3].
    rewrite -addnA service_during_first_plus_later// service_during_cat//.
    by rewrite t1t2 ltnW.
  Qed.

End Composition.

As a common special case, we establish facts about schedules in which a job receives either 1 or 0 service units at all times.
Section UnitService.

Consider any job type and any processor state.
  Context {Job : JobType}.
  Context {PState : ProcessorState Job}.

Let's consider a unit-service 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:
     t, service_at sched j t 1.
  Proof. by rewrite /service_at. Qed.

... which implies that the instantaneous service always equals to 0 or 1.
  Corollary service_is_zero_or_one:
     t, service_at sched j t = 0 service_at sched j t = 1.
  Proof.
    movet.
    by case: service_at (service_at_most_one t) ⇒ [|[|//]] _; [left|right].
  Qed.

Next we prove that the cumulative service received by job j in any interval of length delta is at most delta.
  Lemma cumulative_service_le_delta:
     t delta, service_during sched j t (t + delta) delta.
  Proof.
    movet delta; rewrite -[X in _ X](sum_of_ones t).
    apply: leq_sumt' _; exact: service_at_most_one.
  Qed.

Conversely, we prove that if the cumulative service received by job j in an interval of length delta is greater than or equal to ρ, then ρ delta.
  Lemma cumulative_service_ge_delta :
     t delta ρ,
      ρ service_during sched j t (t + delta)
      ρ delta.
  Proof. move⇒ ??? /leq_trans; apply; exact: cumulative_service_le_delta. Qed.

  Section ServiceIsUnitGrowthFunction.

We show that the service received by any job j is a unit growth function.
    Lemma service_is_unit_growth_function :
      unit_growth_function (service sched j).
    Proof.
      movet; rewrite addn1 -service_last_plus_before leq_add2l.
      exact: service_at_most_one.
    Qed.

Next, consider any time t...
    Variable t : instant.

...and let s be any value less than the service received by job j by time t.
    Variable s : duration.
    Hypothesis H_less_than_s: s < service sched j t.

Then, we show that there exists an earlier time t' where job j had s units of service.
    Corollary exists_intermediate_service:
       t',
        t' < t
        service sched j t' = s.
    Proof.
      apply: (exists_intermediate_point _ service_is_unit_growth_function 0) ⇒ //.
      by rewrite service0.
    Qed.

  End ServiceIsUnitGrowthFunction.

End UnitService.

We establish a basic fact about the monotonicity of service.
Section Monotonicity.

Consider any job type and any processor model.
  Context {Job: JobType}.
  Context {PState: ProcessorState Job}.

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:
     t1 t2,
      t1 t2
      service sched j t1 service sched j t2.
  Proof. by movet1 t2 ?; rewrite -(service_cat _ _ t1 t2)// leq_addr. Qed.

End Monotonicity.

Consider any job type and any processor model.
Section RelationToScheduled.

  Context {Job: JobType}.
  Context {PState: ProcessorState Job}.

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 in a given processor state cannot possibly receive service in that state.
  Lemma service_in_implies_scheduled_in :
     s,
      ~~ scheduled_in j s service_in j s = 0.
  Proof.
    moves.
    move⇒ /existsP Hsched; apply/eqP; rewrite sum_nat_eq0; apply/forallPc.
    rewrite service_on_implies_scheduled_on//.
    by apply/negP ⇒ ?; apply: Hsched; c.
  Qed.

In particular, it cannot receive service at any given time.
  Corollary not_scheduled_implies_no_service:
     t,
      ~~ scheduled_at sched j t service_at sched j t = 0.
  Proof. move⇒ ?; exact: service_in_implies_scheduled_in. Qed.

Conversely, if a job receives service, then it must be scheduled.
  Lemma service_at_implies_scheduled_at :
     t,
      service_at sched j t > 0 scheduled_at sched j t.
  Proof.
    movet; case SCHEDULED: scheduled_at ⇒ //.
    by rewrite not_scheduled_implies_no_service// negbT.
  Qed.

Thus, if the cumulative amount of service changes, then it must be scheduled, too.
  Lemma service_delta_implies_scheduled:
     t,
      service sched j t < service sched j t.+1 scheduled_at sched j t.
  Proof.
    movet; rewrite -service_last_plus_before -ltn_subLR// subnn.
    exact: service_at_implies_scheduled_at.
  Qed.

We observe that a job receives cumulative service during some interval iff it receives services at some specific time in the interval.
  Lemma service_during_service_at:
     t1 t2,
      service_during sched j t1 t2 > 0
      
       t,
        t1 t < t2
        service_at sched j t > 0.
  Proof.
    movet1 t2.
    split⇒ [|[t [titv nz_serv]]].
    - rewrite sum_nat_gt0 filter_predT ⇒ /hasP [t IN GT0].
      by t; split; [rewrite -mem_index_iota|].
    - rewrite sum_nat_gt0; apply/hasP.
      by t; [rewrite filter_predT mem_index_iota|].
  Qed.

Thus, any job that receives some service during an interval must be scheduled at some point during the interval...
  Corollary cumulative_service_implies_scheduled:
     t1 t2,
      service_during sched j t1 t2 > 0
       t,
        t1 t < t2
        scheduled_at sched j t.
  Proof.
    movet1 t2; rewrite service_during_service_at ⇒ -[t' [TIMES SERVICED]].
     t'; split⇒ //; exact: service_at_implies_scheduled_at.
  Qed.

...which implies that any job with positive cumulative service must have been scheduled at some point.
  Corollary positive_service_implies_scheduled_before:
     t,
      service sched j t > 0 t', (t' < t scheduled_at sched j t').
  Proof.
    by movet /cumulative_service_implies_scheduled[t' ?]; t'.
  Qed.

If we can assume that a scheduled job always receives service, we can further prove the converse.
  Section GuaranteedService.

Assume j always receives some positive service.
In other words, not being scheduled is equivalent to receiving zero service.
    Lemma no_service_not_scheduled:
       t,
        ~~ scheduled_at sched j t service_at sched j t = 0.
    Proof.
      movet.
      split ⇒ [|NO_SERVICE]; first exact: service_in_implies_scheduled_in.
      apply: (contra (H_scheduled_implies_serviced j (sched t))).
      by rewrite -eqn0Ngt -NO_SERVICE.
    Qed.

Then, if a job does not receive any service during an interval, it is not scheduled.
    Lemma no_service_during_implies_not_scheduled:
       t1 t2,
        service_during sched j t1 t2 = 0
         t,
          t1 t < t2 ~~ scheduled_at sched j t.
    Proof.
      movet1 t2.
      by move⇒ + t titv; rewrite no_service_not_scheduled big_nat_eq0; apply.
    Qed.

Conversely, if a job is not scheduled during an interval, then it does not receive any service in that interval
    Lemma not_scheduled_during_implies_zero_service:
       t1 t2,
        ( t, t1 t < t2 ~~ scheduled_at sched j t)
        service_during sched j t1 t2 = 0.
    Proof.
      movet1 t2; rewrite big_nat_eq0 ⇒ + t titv ⇒ /(_ t titv).
      by rewrite no_service_not_scheduled.
    Qed.

If a job is scheduled at some point in an interval, it receives positive cumulative service during the interval...
    Lemma scheduled_implies_cumulative_service:
       t1 t2,
        ( t,
            t1 t < t2
            scheduled_at sched j t)
        service_during sched j t1 t2 > 0.
    Proof.
      movet1 t2 [t [titv sch]]; rewrite service_during_service_at.
       t; split⇒ //; exact: H_scheduled_implies_serviced.
    Qed.

...which again applies to total service, too.
    Corollary scheduled_implies_nonzero_service:
       t,
        ( t',
            t' < t
            scheduled_at sched j t')
        service sched j t > 0.
    Proof.
      movet.
      by move⇒ [t' ?]; apply: scheduled_implies_cumulative_service; t'.
    Qed.

  End GuaranteedService.

Furthermore, if we know that jobs are not released early, then we can narrow the interval during which they must have been scheduled.
  Section AfterArrival.

    Context `{JobArrival Job}.

Assume that jobs must arrive to execute.
    Hypothesis H_jobs_must_arrive:
      jobs_must_arrive_to_execute sched.

We prove that any job with positive cumulative service at time t must have been scheduled some time since its arrival and before time t.
    Lemma positive_service_implies_scheduled_since_arrival:
       t,
        service sched j t > 0
         t', (job_arrival j t' < t scheduled_at sched j t').
    Proof.
      movet /positive_service_implies_scheduled_before[t' [t't sch]].
       t'; split⇒ //; rewrite t't andbT; exact: H_jobs_must_arrive.
    Qed.

    Lemma not_scheduled_before_arrival:
       t, t < job_arrival j ~~ scheduled_at sched j t.
    Proof.
      by movet ?; apply: (contra (H_jobs_must_arrive j t)); rewrite -ltnNge.
    Qed.

We show that job j does not receive service at any time t prior to its arrival.
    Lemma service_before_job_arrival_zero:
       t,
        t < job_arrival j
        service_at sched j t = 0.
    Proof.
      movet NOT_ARR; rewrite not_scheduled_implies_no_service//.
      exact: not_scheduled_before_arrival.
    Qed.

Note that the same property applies to the cumulative service.
    Lemma cumulative_service_before_job_arrival_zero :
       t1 t2 : instant,
        t2 job_arrival j
        service_during sched j t1 t2 = 0.
    Proof.
      movet1 t2 early; rewrite big_nat_eq0t /andP[_ t_lt_t2].
      apply: service_before_job_arrival_zero; exact: leq_trans early.
    Qed.

Hence, one can ignore the service received by a job before its arrival time...
    Lemma ignore_service_before_arrival:
       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.
      movet1 t2 t1_le t2_ge.
      rewrite -(service_during_cat sched _ _ (job_arrival j)); last exact/andP.
      by rewrite cumulative_service_before_job_arrival_zero.
    Qed.

... which we can also state in terms of cumulative service.
    Corollary no_service_before_arrival:
       t,
        t job_arrival j service sched j t = 0.
    Proof. exact: cumulative_service_before_job_arrival_zero. Qed.

  End AfterArrival.

In this section, we prove some lemmas about time instants with same service.
  Section TimesWithSameService.

Consider any time instants t1 and t2...
    Variable t1 t2: instant.

...where t1 is no later than t2...
    Hypothesis H_t1_le_t2: t1 t2.

...and where job j has received the same amount of service.
    Hypothesis H_same_service: service sched j t1 = service sched j t2.

First, we observe that this means that the job receives no service 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 _ _ t1 t2)// ⇒ /eqP.
      by rewrite -[X in X == _]addn0 eqn_add2l ⇒ /eqP.
    Qed.

...which of course implies that it does not receive service at any point, either.
    Lemma constant_service_implies_not_scheduled:
       t,
        t1 t < t2 service_at sched j t = 0.
    Proof.
      movet titv.
      have := constant_service_implies_no_service_during.
      rewrite big_nat_eq0; exact.
    Qed.

We show that job j receives service at some point t < t1 iff j receives service at some point t' < t2.
    Lemma same_service_implies_serviced_at_earlier_times:
      [ t: 'I_t1, service_at sched j t > 0] =
      [ t': 'I_t2, service_at sched j t' > 0].
    Proof.
      apply/idP/idP ⇒ /existsP[t serv].
      { by apply/existsP; (widen_ord H_t1_le_t2 t). }
      have [t_lt_t1|t1_le_t] := ltnP t t1.
      { by apply/existsP; (Ordinal t_lt_t1). }
      exfalso; move: serv; apply/negP; rewrite -eqn0Ngt.
      by apply/eqP/constant_service_implies_not_scheduled; rewrite t1_le_t /=.
    Qed.

Then, under the assumption that scheduled jobs receives service, we can translate this into a claim about scheduled_at.
Assume j always receives some positive service.
We show that job j is scheduled at some point t < t1 iff j is scheduled at some point t' < t2.
    Lemma same_service_implies_scheduled_at_earlier_times:
      [ t: 'I_t1, scheduled_at sched j t] =
      [ t': 'I_t2, scheduled_at sched j t'].
    Proof.
      have CONV B : [ b: 'I_B, scheduled_at sched j b]
                    = [ b: 'I_B, service_at sched j b > 0].
      { apply/idP/idP ⇒ /existsP[b P]; apply/existsP; b.
        - exact: H_scheduled_implies_serviced.
        - exact: service_at_implies_scheduled_at. }
      by rewrite !CONV same_service_implies_serviced_at_earlier_times.
    Qed.

  End TimesWithSameService.

End RelationToScheduled.

Section ServiceInTwoSchedules.

Consider any job type and any processor model.
  Context {Job: JobType}.
  Context {PState: ProcessorState Job}.

Consider any two given schedules...
  Variable sched1 sched2: schedule PState.

Given an interval in which the schedules provide the same service to a job at each instant, we can prove that the cumulative service received during the interval has to be the same.
Consider two time instants...
    Variable t1 t2 : instant.

...and a given job that is to be scheduled.
    Variable j: Job.

Assume that, in any instant between t1 and t2 the service provided to j from the two schedules is the same.
    Hypothesis H_sched1_sched2_same_service_at:
       t, t1 t < t2
           service_at sched1 j t = service_at sched2 j t.

It follows that the service provided during t1 and t2 is also the same.
We can leverage the previous lemma to conclude that two schedules that match in a given interval will also have the same cumulative service across the interval.
  Corollary equal_prefix_implies_same_service_during:
     t1 t2,
      ( t, t1 t < t2 sched1 t = sched2 t)
       j, service_during sched1 j t1 t2 = service_during sched2 j t1 t2.
  Proof.
    movet1 t2 sch j; apply: same_service_duringt' t'itv.
    by rewrite /service_at sch.
  Qed.

For convenience, we restate the corollary also at the level of service for identical prefixes.
  Corollary identical_prefix_service:
     h,
      identical_prefix sched1 sched2 h
       j, service sched1 j h = service sched2 j h.
  Proof. move⇒ ? ? ?; exact: equal_prefix_implies_same_service_during. Qed.

End ServiceInTwoSchedules.