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

Require Export prosa.model.job.properties.
Require Export prosa.model.schedule.nonpreemptive.
Require Export prosa.model.preemption.fully_nonpreemptive.
Require Export prosa.analysis.facts.behavior.all.

# 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}.
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.
Next, consider any non-preemptive unit-service schedule of the arrival sequence ...
Context {PState : ProcessorState Job}.
Hypothesis H_unit_service : unit_service_proc_model PState.
Variable sched : schedule PState.
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.
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.
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.
Section NoPreemptionsEquivalence.
Consider any type of jobs with preemption points.
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Consider any type of schedule.
Context {PState : ProcessorState Job}.
Variable sched : schedule PState.
We prove that no preemptions in a schedule is equivalent to a non-preemptive schedule.
Lemma no_preemptions_equiv_nonpreemptive :
(∀ j t, ~~preempted_at sched j t) ↔ nonpreemptive_schedule sched.
End NoPreemptionsEquivalence.