Library prosa.analysis.facts.model.ideal.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.model.service_of_jobs.
Require Export prosa.analysis.facts.behavior.completion.

Throughout this file, we assume ideal uni-processor schedules.

Require Import prosa.model.processor.ideal.
Require Export prosa.analysis.facts.model.ideal.schedule.

Service Received by Sets of Jobs in Ideal Uni-Processor Schedules

In this file, we establish a fact about the service received by sets of jobs under ideal uni-processor schedule and the presence of idle times. The lemma is currently specific to ideal uniprocessors only because of the lack of a general notion of idle time, which should be added in the near future. Conceptually, the fact holds for any ideal_progress_proc_model. Once a general notion of idle time has been defined, this file should be generalized.

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_arrival_times_are_consistent : consistent_arrival_times arr_seq.

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

  Variable sched : schedule (ideal.processor_state Job).
  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 sched t.

End IdealModelLemmas.