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

Require Export prosa.behavior.all.

Require Export prosa.model.processor.platform_properties.

Require Export prosa.analysis.definitions.schedule_prefix.

# Service

Consider any job type and any processor state.

For any given schedule...

...and any given 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.

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

Trivially, an interval consisting of one time unit is equivalent to
service_at.

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.

∀ t1 t2 t3,

t1 ≤ t2 ≤ t3 →

(service_during sched j t1 t2) + (service_during sched j t2 t3)

= service_during sched j t1 t3.

Lemma service_cat:

∀ t1 t2,

t1 ≤ t2 →

(service sched j t1) + (service_during sched j t1 t2)

= service sched j t2.

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

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

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

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

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

Consider any job type and any processor state.

Let's consider a unit-service model...

...and a given schedule.

Let j be any job that is to be scheduled.

First, we prove that the instantaneous service cannot be greater than 1, ...

... which implies that the instantaneous service always equals to 0 or 1.

Next we prove that the cumulative service received by job j in
any interval of length delta is at most delta.

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.

Section ServiceIsUnitGrowthFunction.

∀ t delta ρ,

ρ ≤ service_during sched j t (t + delta) →

ρ ≤ delta.

Section ServiceIsUnitGrowthFunction.

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

Next, consider any time t...

Corollary exists_intermediate_service:

∃ t',

t' < t ∧

service sched j t' = s.

End ServiceIsUnitGrowthFunction.

End UnitService.

∃ t',

t' < t ∧

service sched j t' = s.

End ServiceIsUnitGrowthFunction.

End UnitService.

We establish a basic fact about the monotonicity of service.

Consider any job type and any processor model.

Consider any given schedule...

...and a given job that is to be scheduled.

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.

∀ t1 t2,

t1 ≤ t2 →

service sched j t1 ≤ service sched j t2.

End Monotonicity.

Consider any job type and any processor model.

Consider any given schedule...

...and a given job that is to be scheduled.

We observe that a job that isn't scheduled in a given processor
state cannot possibly receive service in that state.

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.

∀ t,

~~ scheduled_at sched j t → service_at sched j t = 0.

Conversely, if a job receives service, then it must be scheduled.

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.

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

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

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

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

Assume j always receives some positive service.

In other words, not being scheduled is equivalent to receiving zero
service.

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.

∀ t1 t2,

service_during sched j t1 t2 = 0 →

∀ t,

t1 ≤ t < t2 → ~~ scheduled_at sched j t.

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.

∀ t1 t2,

(∀ t, t1 ≤ t < t2 → ~~ scheduled_at sched j t) →

service_during sched j t1 t2 = 0.

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.

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

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

Assume that jobs must arrive to execute.

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.

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

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.

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

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

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

...and where job j has received the same amount of service.

First, we observe that this means that the job receives no service
during

`[t1, t2)`

...
...which of course implies that it does not receive service at any
point, either.

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

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

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.

Section ServiceInTwoSchedules.

[∃ t: 'I_t1, scheduled_at sched j t] =

[∃ t': 'I_t2, scheduled_at sched j t'].

End TimesWithSameService.

End RelationToScheduled.

Section ServiceInTwoSchedules.

Consider any job type and any processor model.

Consider any two given schedules...

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

...and a given job that is to be scheduled.

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.

∀ t, t1 ≤ t < t2 →

service_at sched1 j t = service_at sched2 j t.

Lemma same_service_during:

service_during sched1 j t1 t2 = service_during sched2 j t1 t2.

End ServiceDuringEquivalentInterval.

service_during sched1 j t1 t2 = service_during sched2 j t1 t2.

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.

∀ t1 t2,

(∀ t, t1 ≤ t < t2 → sched1 t = sched2 t) →

∀ j, service_during sched1 j t1 t2 = service_during sched2 j t1 t2.

For convenience, we restate the corollary also at the level of
service for identical prefixes.