Library prosa.analysis.facts.preemption.job.preemptive

Preemptions in Fully Preemptive Model

In this section, we prove that instantiation of predicate job_preemptable to the fully preemptive model indeed defines a valid preemption model.
We assume that jobs are fully preemptive.
  #[local] Existing Instance fully_preemptive_job_model.

Consider any type of jobs.
  Context {Job : JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

Consider any kind of processor state model, ...
  Context {PState : ProcessorState Job}.

... any job arrival sequence, ...
  Variable arr_seq : arrival_sequence Job.

... and any given schedule.
  Variable sched : schedule PState.

Then, we prove that fully_preemptive_model is a valid preemption model.
We also prove that under the fully preemptive model job_max_nonpreemptive_segment j is equal to 0, when job_cost j = 0 ...
  Lemma job_max_nps_is_0:
      job_cost j = 0
      job_max_nonpreemptive_segment j = 0.

... or ε when job_cost j > 0.
  Lemma job_max_nps_is_ε:
      job_cost j > 0
      job_max_nonpreemptive_segment j = ε.

End FullyPreemptiveModel.
Global Hint Resolve valid_fully_preemptive_model : basic_rt_facts.