Library prosa.analysis.facts.model.ideal.service_of_jobs

Require Export prosa.model.priority.classes.
Require Export prosa.model.aggregate.service_of_jobs.
Require Export prosa.analysis.facts.behavior.service.

Service Received by Sets of Jobs in Uniprocessor Schedules

In this section, we establish a fact about the service received by sets of jobs in the presence of idle times on a fully-consuming uniprocessor model.
Section FullyConsumingModelLemmas.

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

Allow for any fully-consuming uniprocessor model.
  Context {PState : ProcessorState Job}.
  Hypothesis H_uniproc : uniprocessor_model PState.
  Hypothesis H_fully_consuming_proc_model : fully_consuming_proc_model PState.

Consider any arrival sequence with consistent arrivals.
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

Next, consider any schedule of this arrival sequence ...
  Variable sched : schedule PState.
  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.

Let P be any predicate over jobs.
  Variable P : pred Job.

We prove that, if the sum of the total blackout and the total service within some time interval [t1,t2) is smaller than t2 - t1, then there is an idle time instant t ∈ [t1,t2).
  Lemma low_service_implies_existence_of_idle_time_rs :
    ∀ t1 t2,
      blackout_during sched t1 t2
       + service_of_jobs sched predT (arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1 →
      ∃ t,
        t1 ≤ t < t2 ∧ is_idle arr_seq sched t.

End FullyConsumingModelLemmas.

Service Received by Sets of Jobs in Uniprocessor Ideal-Progress Schedules

Next, we establish a fact about the service received by sets of jobs in the presence of idle times on a uniprocessor under the ideal-progress assumption (i.e., that a scheduled job necessarily receives nonzero service).
Section IdealModelLemmas.

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 arrival sequence with consistent arrivals.
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

Allow for any uniprocessor model that ensures ideal progress.
  Context {PState : ProcessorState Job}.
  Hypothesis H_uniproc : uniprocessor_model PState.
  Hypothesis H_ideal_progress_proc_model : ideal_progress_proc_model PState.

Next, consider any ideal 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.

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

Let P be any predicate over jobs.
  Variable P : pred Job.

We prove that if the total service within some time interval [t1,t2) is smaller than [t2 - t1], then there is an idle time instant t ∈ [t1,t2)].
  Lemma low_service_implies_existence_of_idle_time :
    ∀ t1 t2,
      service_of_jobs sched predT (arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1 →
      ∃ t,
        t1 ≤ t < t2 ∧ is_idle arr_seq sched t.

End IdealModelLemmas.