Library prosa.analysis.facts.behavior.service

Require Export prosa.util.all.
Require Export prosa.behavior.all.
Require Export prosa.model.processor.platform_properties.

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: 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:
    ∀ t1 t2,
      t1 ≥ t2 → service_during sched j t1 t2 = 0.

Equally trivially, no job has received service prior to time zero.

Corollary service0:
service sched j 0 = 0.

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.

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.

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.

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.

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.

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.

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.

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: Type}.
  Context `{ProcessorState Job PState}.

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.

...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:
    ∀ t delta,
      service_during sched j t (t + delta) ≤ delta.

  Section ServiceIsAStepFunction.

We show that the service received by any job j is a step function.

Lemma service_is_a_step_function:
is_step_function (service sched j).

Next, consider any time t...

Variable t: instant.

...and let s0 be any value less than the service received by job j by time t.

Variable s0: duration.
Hypothesis H_less_than_s: s0 < service sched j t.

Then, we show that there exists an earlier time t0 where job j had s0 units of service.

    Corollary exists_intermediate_service:
      ∃ t0,
        t0 < t ∧
        service sched j t0 = s0.
  End ServiceIsAStepFunction.

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: 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:
    ∀ t1 t2,
      t1 ≤ t2 →
      service sched j t1 ≤ service sched j t2.

End Monotonicity.

Consider any job type and any processor model.

Section RelationToScheduled.

  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:
    ∀ t,
      ~~ scheduled_at sched j t → service_at sched j t = 0.

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.

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.

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.

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.

...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').

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.

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.

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.

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

  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').

    Lemma not_scheduled_before_arrival:
      ∀ t, t < job_arrival j → ~~ scheduled_at sched j t.

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.

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.

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.

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

  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.

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

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].

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'].
  End TimesWithSameService.

End RelationToScheduled.