Library prosa.analysis.facts.model.service_of_jobs

Lemmas about Service Received by Sets of Jobs

In this file, we establish basic facts about the service received by sets of jobs.
To begin with, we provide some basic properties of service of a set of jobs in case of a generic scheduling model.
Consider any type of tasks ...
  Context {Task : TaskType}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

Consider any kind of processor state model, ...
  Context {PState : ProcessorState Job}.

... any job arrival sequence with consistent arrivals, ....
... and any schedule of this arrival sequence ...
  Variable sched : schedule PState.

... where jobs do not execute before their arrival or after completion.
Let P be any predicate over jobs.
  Variable P : pred Job.

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.

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.

In the following, we consider an arbitrary sequence of jobs jobs.
    Variable jobs : seq Job.

Also, consider an interval [t1, t2)...
    Variable t1 t2 : instant.

...and two additional predicates P1 and P2.
    Variable P1 P2 : pred Job.

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 jP1 j && P2 j) jobs t1 t2
        + service_of_jobs sched (fun jP1 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}.
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}.
Similarly, we show that if P1 is equivalent to P2, then the service of {jobs | P1} is equal to the service of {jobs | P2}.
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 [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.
In other words, we show that [∑_{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]>>.
We show that service of {jobs | false} is equal to 0.
    Lemma service_of_jobs_pred0 :
      service_of_jobs sched pred0 jobs t1 t2 = 0.

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.

In this section, we prove a lemma about the sum of service with different predicates over a fixed time interval.
Section HEPService.

Consider any type of jobs.
  Context {Job : JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

Consider any kind of processor state model, ...
  Context {PState : ProcessorState Job}.

... any valid arrival sequence, ....
... and any schedule of this arrival sequence ...
  Variable sched : schedule PState.

... where jobs do not execute before their arrival.
Consider a JLFP policy that indicates a higher-or-equal priority relation and assume that the relation is reflexive.
Consider an interval [t1, t2) ...
  Variables t1 t2 : instant.

... and a job j arriving no earlier than t1.
  Variable j : Job.
  Hypothesis H_arrives : arrives_in arr_seq j.
  Hypothesis H_t1_le_j_arr : t1 job_arrival j.

We prove that the sum of the service during [t1, t2) of job j and the service of higher-or-equal priority jobs distinct from j during [t1, t2) is equal to the service of higher-or-equal priority jobs in [t1, t2).
In this section, we prove some properties about service of sets of jobs for unit-service processor models.
Consider any type of tasks ...
  Context {Task : TaskType}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

Consider any kind of unit-service processor state model.
Consider any arrival sequence with consistent arrivals.
Next, consider any unit-service schedule of this arrival sequence ...
... where jobs do not execute before their arrival or after completion.
Let P be any predicate over jobs.
  Variable P : pred Job.

First, we prove that the service received by any set of jobs is upper-bounded by the corresponding workload.
In this section, we introduce a connection between the cumulative service, cumulative workload, and completion of jobs.
Consider an arbitrary time interval [t1, t2).
    Variables t1 t2 : instant.

Let jobs be a set of all jobs arrived during [t1, t2).
    Let jobs := arrivals_between arr_seq t1 t2.

Next, we consider some time instant t_compl.
    Variable t_compl : instant.

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.
    Let all_jobs_completed_by t_compl :=
       j, j \in jobs P j completed_by sched j t_compl.

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.
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.
Using the lemmas above, we prove the equivalence.
In this section, we prove some properties about service of sets of jobs for unit-service uniprocessor models.
Consider any type of tasks ...
  Context {Task : TaskType}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

Consider any kind of unit-service uniprocessor state model.
Consider any arrival sequence with consistent arrivals.
Next, consider any unit-service uni-processor schedule of this arrival sequence ...
... where jobs do not execute before their arrival or after completion.
Let P be any predicate over jobs.
  Variable P : pred Job.

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.
    Variable jobs : seq Job.
    Hypothesis H_no_duplicate_jobs : uniq jobs.

We prove that the overall service of jobs at a single time instant is at most 1.
    Lemma service_of_jobs_le_1:
       t, service_of_jobs_at sched P jobs t 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 + Δ) Δ.

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.

In this section, we prove a relation between a predicate defined on a set of jobs and the total service of these jobs.
  Section PredServedEqService.

Assume that the arrival sequence does not contain duplicate arrivals.
Consider a JLFP-policy that indicates a higher-or-equal priority relation.
    Context {JLFP : JLFP_policy Job}.

Consider a job j.
    Variable j : Job.
    Hypothesis H_j_arrives : arrives_in arr_seq j.

We consider an arbitrary time interval [t1, t) that starts with a quiet time.
    Variable t1 t : instant.
    Hypothesis H_quiet_time : quiet_time arr_seq sched j t1.

We prove that the number of points in the interval that satisfy the predicate j served jobs: P j is equal to the total service of all jobs that satisfy P.
Note that this lemma uses served_jobs_at instead of its uniprocessor variant served_job_at. This is done on purpose so that this lemma fits better with abstract functions and predicates defined in /analysis/abstract/... since such functions are usually defined on a general (not necessarily uniprocessor) class of processor models.