Library prosa.analysis.facts.model.preemption

Require Export prosa.model.schedule.priority_driven.
Require Export prosa.analysis.facts.model.ideal.schedule.
Require Export prosa.analysis.facts.behavior.completion.

In this section, we establish two basic facts about preemption times.

Section PreemptionTimes.

Consider any type of jobs.

  Context {Job : JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

In addition, we assume the existence of a function mapping a job and its progress to a boolean value saying whether this job is preemptable at its current point of execution.

Context `{JobPreemptable Job}.

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 ideal uniprocessor schedule of this arrival sequence...

Variable sched : schedule (ideal.processor_state Job).

...where, jobs come from the arrival sequence.

Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.

Consider a valid preemption model.

Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.

We show that time 0 is a preemption time.

Lemma zero_is_pt: preemption_time sched 0.

Also, we show that the first instant of execution is a preemption time.

  Lemma first_moment_is_pt:
    ∀ j prt,
      arrives_in arr_seq j →
      ~~ scheduled_at sched j prt →
      scheduled_at sched j prt .+1 →
      preemption_time sched prt .+1.

End PreemptionTimes.

In this section, we prove a lemma relating scheduling and preemption times.

Section PreemptionFacts.

Consider any type of jobs.

  Context {Job : JobType}.
  Context `{Arrival : JobArrival Job}.
  Context `{Cost : JobCost Job}.
  Context `{@JobReady Job (ideal.processor_state Job ) Cost Arrival}.

Consider any arrival sequence.

Variable arr_seq : arrival_sequence Job.

Next, consider any ideal uni-processor schedule of this arrival sequence, ...

Variable sched : schedule (ideal.processor_state Job).

...and, assume that the schedule is valid.

Hypothesis H_sched_valid : valid_schedule sched arr_seq.

In addition, we assume the existence of a function mapping jobs to their preemption points ...

Context `{JobPreemptable Job}.

... and assume that it defines a valid preemption model.

Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.

We prove that every nonpreemptive segment always begins with a preemption time.

  Lemma scheduling_of_any_segment_starts_with_preemption_time:
    ∀ j t,
      scheduled_at sched j t →
      ∃ pt ,
        job_arrival j ≤ pt ≤ t ∧
          preemption_time sched pt ∧
          (∀ t', pt ≤ t' ≤ t → scheduled_at sched j t').

End PreemptionFacts.