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.

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 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.
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 an ideal uniprocessor schedule.
  Variable sched : schedule (ideal.processor_state Job).

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.