# Library prosa.analysis.facts.model.service_of_jobs

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

Require Export prosa.model.aggregate.workload.

Require Export prosa.model.aggregate.service_of_jobs.

Require Export prosa.analysis.facts.behavior.completion.

Require Export prosa.model.aggregate.workload.

Require Export prosa.model.aggregate.service_of_jobs.

Require Export prosa.analysis.facts.behavior.completion.

# Lemmas about Service Received by Sets of Jobs

In this file, we establish basic facts about the service received by*sets*of jobs.

Consider any type of tasks ...

... and any type of jobs associated with these tasks.

Context {Job : JobType}.

Context `{JobTask Job Task}.

Context `{JobArrival Job}.

Context `{JobCost Job}.

Context `{JobTask Job Task}.

Context `{JobArrival Job}.

Context `{JobCost Job}.

Consider any kind of processor state model, ...

... any job arrival sequence with consistent arrivals, ....

Variable arr_seq : arrival_sequence Job.

Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.

Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.

... and any schedule of this arrival sequence ...

... where jobs do not execute before their arrival or after completion.

Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.

Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.

Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.

Let P be any predicate over jobs.

We show that the total service of jobs released in a time interval

`[t1,t2)`

during `[t1,t2)`

is equal to the sum of:
(1) the total service of jobs released in time interval `[t1, t)`

during time `[t1, t)`

(2) the total service of jobs released in time interval `[t1, t)`

during time `[t, t2)`

and (3) the total service of jobs released in time interval `[t, t2)`

during time `[t, t2)`

.
Lemma service_of_jobs_cat_scheduling_interval :

∀ t1 t2 t,

t1 ≤ t ≤ t2 →

service_of_jobs sched P (arrivals_between arr_seq t1 t2) t1 t2

= service_of_jobs sched P (arrivals_between arr_seq t1 t) t1 t

+ service_of_jobs sched P (arrivals_between arr_seq t1 t) t t2

+ service_of_jobs sched P (arrivals_between arr_seq t t2) t t2.

∀ t1 t2 t,

t1 ≤ t ≤ t2 →

service_of_jobs sched P (arrivals_between arr_seq t1 t2) t1 t2

= service_of_jobs sched P (arrivals_between arr_seq t1 t) t1 t

+ service_of_jobs sched P (arrivals_between arr_seq t1 t) t t2

+ service_of_jobs sched P (arrivals_between arr_seq t t2) t t2.

We show that the total service of jobs released in a time interval

`[t1, t2)`

during `[t, t2)`

is equal to the sum of:
(1) the total service of jobs released in a time interval `[t1, t)`

during `[t, t2)`

and (2) the total service of jobs released in a time interval `[t, t2)`

during `[t, t2)`

.
Lemma service_of_jobs_cat_arrival_interval :

∀ t1 t2 t,

t1 ≤ t ≤ t2 →

service_of_jobs sched P (arrivals_between arr_seq t1 t2) t t2 =

service_of_jobs sched P (arrivals_between arr_seq t1 t) t t2 +

service_of_jobs sched P (arrivals_between arr_seq t t2) t t2.

∀ t1 t2 t,

t1 ≤ t ≤ t2 →

service_of_jobs sched P (arrivals_between arr_seq t1 t2) t t2 =

service_of_jobs sched P (arrivals_between arr_seq t1 t) t t2 +

service_of_jobs sched P (arrivals_between arr_seq t t2) t t2.

In the following, we consider an arbitrary sequence of jobs jobs.

Also, consider an interval

`[t1, t2)`

...
For brevity, in the following comments we denote a subset of jobs
satisfying a predicate P by {jobs | P}.
First, we prove that the service received by {jobs | P1} can be split
into: (1) the service received by {jobs | P1 ∧ P2} and (2) the service
received by the a subset {jobs | P1 ∧ ¬ P2}.

Lemma service_of_jobs_case_on_pred :

service_of_jobs sched P1 jobs t1 t2 =

service_of_jobs sched (fun j ⇒ P1 j && P2 j) jobs t1 t2

+ service_of_jobs sched (fun j ⇒ P1 j && ~~ P2 j) jobs t1 t2.

service_of_jobs sched P1 jobs t1 t2 =

service_of_jobs sched (fun j ⇒ P1 j && P2 j) jobs t1 t2

+ service_of_jobs sched (fun j ⇒ P1 j && ~~ P2 j) jobs t1 t2.

We show that the service received by {jobs | P} is equal to the
difference between the total service received by jobs and the service
of {jobs | ¬ P}.

Lemma service_of_jobs_negate_pred :

service_of_jobs sched P jobs t1 t2 =

total_service_of_jobs_in sched jobs t1 t2 - service_of_jobs sched (fun j ⇒ ~~ P j) jobs t1 t2.

service_of_jobs sched P jobs t1 t2 =

total_service_of_jobs_in sched jobs t1 t2 - service_of_jobs sched (fun j ⇒ ~~ P j) jobs t1 t2.

We show that service_of_jobs is monotone with respect to the
predicate. That is, given the fact ∀ j ∈ jobs: P1 j ==> P2 j, we show
that the service of {jobs | P1} is bounded by the service of {jobs | P2}.

Lemma service_of_jobs_pred_impl :

(∀ j : Job, j \in jobs → P1 j → P2 j) →

service_of_jobs sched P1 jobs t1 t2 ≤ service_of_jobs sched P2 jobs t1 t2.

(∀ j : Job, j \in jobs → P1 j → P2 j) →

service_of_jobs sched P1 jobs t1 t2 ≤ service_of_jobs sched P2 jobs t1 t2.

Similarly, we show that if P1 is equivalent to P2, then the service
of {jobs | P1} is equal to the service of {jobs | P2}.

Lemma service_of_jobs_equiv_pred :

{in jobs, P1 =1 P2} →

service_of_jobs sched P1 jobs t1 t2 = service_of_jobs sched P2 jobs t1 t2.

{in jobs, P1 =1 P2} →

service_of_jobs sched P1 jobs t1 t2 = service_of_jobs sched P2 jobs t1 t2.

Next, we show an auxiliary lemma that allows us to change the order of
summation.
Recall that service_of_jobs is defined as a sum over all jobs in
jobs of
In other words, we show that

`[service_during j [t1,t2)]`

. We show that service_of_jobs
over an interval `[t1,t2)`

is equal to the sum over individual time
instances (in `[t1,t2)`

) of service_of_jobs_at.
```
[∑_{j ∈ jobs} ∑_{t \in [t1,t2)} service
```

of j at t]>> is equal to ```
[∑_{t \in [t1,t2)} ∑_{j ∈ jobs} service of j
```

at t]>>.
Lemma service_of_jobs_sum_over_time_interval :

service_of_jobs sched P jobs t1 t2

= \sum_(t1 ≤ t < t2) service_of_jobs_at sched P jobs t.

service_of_jobs sched P jobs t1 t2

= \sum_(t1 ≤ t < t2) service_of_jobs_at sched P jobs t.

More generally, if none of the jobs inside jobs is scheduled
at time t or satisfies P, then total service of jobs at
time t is equal to 0.

Lemma service_of_jobs_nsched_or_unsat :

∀ (t : instant),

(∀ j, j \in jobs → ~~ (P j && scheduled_at sched j t)) →

service_of_jobs_at sched P jobs t = 0.

End GenericModelLemmas.

∀ (t : instant),

(∀ j, j \in jobs → ~~ (P j && scheduled_at sched j t)) →

service_of_jobs_at sched P jobs t = 0.

End GenericModelLemmas.

In this section, we prove some properties about service
of sets of jobs for unit-service processor models.

Consider any type of tasks ...

... and any type of jobs associated with these tasks.

Context {Job : JobType}.

Context `{JobTask Job Task}.

Context `{JobArrival Job}.

Context `{JobCost Job}.

Context `{JobTask Job Task}.

Context `{JobArrival Job}.

Context `{JobCost Job}.

Consider any kind of unit-service processor state model.

Context {PState : ProcessorState Job}.

Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.

Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.

Consider any arrival sequence with consistent arrivals.

Variable arr_seq : arrival_sequence Job.

Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.

Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.

Next, consider any unit-service schedule of this arrival sequence ...

Variable sched : schedule PState.

Hypothesis H_jobs_come_from_arrival_sequence:

jobs_come_from_arrival_sequence sched arr_seq.

Hypothesis H_jobs_come_from_arrival_sequence:

jobs_come_from_arrival_sequence sched arr_seq.

... where jobs do not execute before their arrival or after completion.

Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.

Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.

Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.

Let P be any predicate over jobs.

First, we prove that the service received by any set of jobs is
upper-bounded by the corresponding workload.

Lemma service_of_jobs_le_workload:

∀ (jobs : seq Job) (t1 t2 : instant),

service_of_jobs sched P jobs t1 t2 ≤ workload_of_jobs P jobs.

∀ (jobs : seq Job) (t1 t2 : instant),

service_of_jobs sched P jobs t1 t2 ≤ workload_of_jobs P jobs.

In this section, we introduce a connection between the cumulative
service, cumulative workload, and completion of jobs.

Consider an arbitrary time interval

`[t1, t2)`

.
Let jobs be a set of all jobs arrived during

`[t1, t2)`

.
Next, we consider some time instant t_compl.

And state the proposition that all jobs are completed by time
t_compl. Next we show that this proposition is equivalent to
the fact that workload of jobs = service of jobs.

First, we prove that if the workload of jobs is equal to the
service of jobs, then any job in jobs is completed by time
t_compl.

Lemma workload_eq_service_impl_all_jobs_have_completed :

workload_of_jobs P jobs = service_of_jobs sched P jobs t1 t_compl →

all_jobs_completed_by t_compl.

workload_of_jobs P jobs = service_of_jobs sched P jobs t1 t_compl →

all_jobs_completed_by t_compl.

And vice versa, the fact that any job in jobs is completed by time t_compl
implies that the workload of jobs is equal to the service of jobs.

Lemma all_jobs_have_completed_impl_workload_eq_service :

all_jobs_completed_by t_compl →

workload_of_jobs P jobs =

service_of_jobs sched P jobs t1 t_compl.

all_jobs_completed_by t_compl →

workload_of_jobs P jobs =

service_of_jobs sched P jobs t1 t_compl.

Using the lemmas above, we prove the equivalence.

Corollary all_jobs_have_completed_equiv_workload_eq_service :

all_jobs_completed_by t_compl ↔

workload_of_jobs P jobs = service_of_jobs sched P jobs t1 t_compl.

End WorkloadServiceAndCompletion.

End UnitServiceModelLemmas.

all_jobs_completed_by t_compl ↔

workload_of_jobs P jobs = service_of_jobs sched P jobs t1 t_compl.

End WorkloadServiceAndCompletion.

End UnitServiceModelLemmas.

In this section, we prove some properties about service
of sets of jobs for unit-service uniprocessor models.

Consider any type of tasks ...

... and any type of jobs associated with these tasks.

Context {Job : JobType}.

Context `{JobTask Job Task}.

Context `{JobArrival Job}.

Context `{JobCost Job}.

Context `{JobTask Job Task}.

Context `{JobArrival Job}.

Context `{JobCost Job}.

Consider any kind of unit-service uniprocessor state model.

Context {PState : ProcessorState Job}.

Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.

Hypothesis H_uniprocessor_model : uniprocessor_model PState.

Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.

Hypothesis H_uniprocessor_model : uniprocessor_model PState.

Consider any arrival sequence with consistent arrivals.

Variable arr_seq : arrival_sequence Job.

Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.

Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.

Next, consider any unit-service uni-processor schedule of this arrival sequence ...

Variable sched : schedule PState.

Hypothesis H_jobs_come_from_arrival_sequence :

jobs_come_from_arrival_sequence sched arr_seq.

Hypothesis H_jobs_come_from_arrival_sequence :

jobs_come_from_arrival_sequence sched arr_seq.

... where jobs do not execute before their arrival or after completion.

Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.

Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.

Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.

Let P be any predicate over jobs.

In this section, we prove that the service received by any set of jobs
is upper-bounded by the corresponding interval length.

Let jobs denote any set of jobs.

We prove that the overall service of jobs at a single time instant is at most 1.

Next, we prove that the service received by those jobs is no larger
than their workload.

Corollary service_of_jobs_le_length_of_interval:

∀ (t : instant) (Δ : duration),

service_of_jobs sched P jobs t (t + Δ) ≤ Δ.

∀ (t : instant) (Δ : duration),

service_of_jobs sched P jobs t (t + Δ) ≤ Δ.

The same holds for two time instants.

Corollary service_of_jobs_le_length_of_interval':

∀ (t1 t2 : instant),

service_of_jobs sched P jobs t1 t2 ≤ t2 - t1.

End ServiceOfJobsIsBoundedByLength.

End UnitServiceUniProcessorModelLemmas.

∀ (t1 t2 : instant),

service_of_jobs sched P jobs t1 t2 ≤ t2 - t1.

End ServiceOfJobsIsBoundedByLength.

End UnitServiceUniProcessorModelLemmas.