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

Require Export prosa.model.preemption.fully_nonpreemptive.

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

Require Export prosa.analysis.definitions.job_properties.

Require Export prosa.model.schedule.nonpreemptive.

Require Export prosa.model.preemption.fully_nonpreemptive.

# Platform for Fully Non-Preemptive model

Consider any type of jobs.

We assume that jobs are fully non-preemptive.

#[local] Existing Instance fully_nonpreemptive_job_model.

Consider any arrival sequence with consistent arrivals.

Variable arr_seq : arrival_sequence Job.

Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.

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.

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.

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.

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.

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.

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

Consider an ideal uniprocessor schedule.

We prove that no preemptions in a schedule is equivalent to a non-preemptive schedule.