Library rt.restructuring.behavior.facts.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].
(* 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 consiting 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.
Section UnitService.
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. *)
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.
(* ...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.
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:
∀ t1 t2,
t1 ≤ t2 →
service sched j t1 ≤ service sched j t2.
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:
∀ 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').
Section GuaranteedService.
(* If we can assume that a scheduled job always receives service, we can
further prove the converse. *)
(* Assume j always receives some positive service. *)
Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model.
(* 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 receivees
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.
Section AfterArrival.
(* Futhermore, if we know that jobs are not released early, then we can
narrow the interval during which they must have been scheduled. *)
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.
Section TimesWithSameService.
In this section, we prove some lemmas about time instants with same
service.
(* 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.
(* 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.