Library prosa.analysis.facts.behavior.service

Require Export prosa.util.all.
Require Export prosa.behavior.all.
Require Export prosa.model.processor.platform_properties.
Require Export prosa.analysis.definitions.schedule_prefix.

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.
    move⇒ t1 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.
    move ⇒ t1 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...
  Hypothesis H_unit_service: unit_service_proc_model PState.

...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.
    move⇒ t.
    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.
    move⇒ t delta; rewrite -[X in _ ≤ X](sum_of_ones t).
    apply: leq_sum ⇒ t' _; 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.
      move⇒ t; 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 move⇒ t1 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.
    move⇒ s.
    move⇒ /existsP Hsched; apply/eqP; rewrite sum_nat_eq0; apply/forallP ⇒ c.
    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.
    move⇒ t; 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.
    move⇒ t; 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.
    move⇒ t1 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.
    move⇒ t1 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 move⇒ t /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.
    Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model PState.

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.
      move⇒ t.
      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.
      move⇒ t1 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.
      move⇒ t1 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.
      move⇒ t1 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.
      move⇒ t.
      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.
      move⇒ t /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 move⇒ t ?; 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.
      move⇒ t 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.
      move⇒ t1 t2 early; rewrite big_nat_eq0 ⇒ t /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.
      move⇒ t1 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.
      move⇒ t 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.
    Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model PState.

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.
  Section ServiceDuringEquivalentInterval.

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.
    Lemma same_service_during:
      service_during sched1 j t1 t2 = service_during sched2 j t1 t2.
    Proof. exact/eq_big_nat/H_sched1_sched2_same_service_at. Qed.

  End ServiceDuringEquivalentInterval.

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.
    move⇒ t1 t2 sch j; apply: same_service_during ⇒ t' 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.