Library prosa.analysis.facts.preemption.job.nonpreemptive

Require Export prosa.analysis.facts.behavior.all.
Require Export prosa.analysis.facts.model.ideal_schedule.
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.model.schedule.nonpreemptive.

Furthermore, we assume the fully non-preemptive job model.
Require Import prosa.model.preemption.fully_nonpreemptive.

Platform for Fully Non-Preemptive model

In this section, we prove that instantiation of predicate job_preemptable to the fully non-preemptive model indeed defines a valid preemption model.
Section FullyNonPreemptiveModel.

Consider any type of jobs.
  Context {Job : JobType}.
  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 non-preemptive ideal uniprocessor schedule of this arrival sequence ...
  Variable sched : schedule (ideal.processor_state Job).
  Hypothesis H_nonpreemptive_sched : nonpreemptive_schedule sched.

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

For simplicity, let's define some local names.
  Let job_pending := pending sched.
  Let job_completed_by := completed_by sched.
  Let job_scheduled_at := scheduled_at sched.

Then, we prove that fully_nonpreemptive_model is a valid preemption model.
  Lemma valid_fully_nonpreemptive_model:
    valid_preemption_model arr_seq sched.

We also prove that under the fully non-preemptive model job_max_nonpreemptive_segment j is equal to job_cost j ...
  Lemma job_max_nps_is_job_cost:
    ∀ j, job_max_nonpreemptive_segment j = job_cost j.

... and job_last_nonpreemptive_segment j is equal to job_cost j.
  Lemma job_last_nps_is_job_cost:
    ∀ j, job_last_nonpreemptive_segment j = job_cost j.

End FullyNonPreemptiveModel.
Hint Resolve valid_fully_nonpreemptive_model : basic_facts.