Library prosa.analysis.facts.preemption.job.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.
Consider any type of jobs.
  Context {Job : JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

We assume that jobs are fully non-preemptive.
  #[local] Existing Instance fully_nonpreemptive_job_model.

Consider any arrival sequence with consistent arrivals.
Next, consider any non-preemptive ideal uniprocessor schedule of this arrival sequence ...
... where jobs do not execute before their arrival or after completion.
For simplicity, let's define some local names.
Then, we prove that fully_nonpreemptive_model is a valid preemption model.
We also prove that under the fully non-preemptive model job_max_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.
Global Hint Resolve valid_fully_nonpreemptive_model : basic_rt_facts.

In this section, we prove the equivalence between no preemptions and a non-preemptive schedule.
Consider any type of jobs with preemption points.
  Context {Job : JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

Consider an ideal uniprocessor schedule.
We prove that no preemptions in a schedule is equivalent to a non-preemptive schedule.