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.
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.
Consider any type of jobs.
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.
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 ideal uniprocessor schedule of this arrival sequence...
...where, jobs come from the arrival sequence.
Consider a valid preemption model.
We show that time 0 is a preemption time.
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.
∀ 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.
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}.
Context `{Arrival : JobArrival Job}.
Context `{Cost : JobCost Job}.
Context `{@JobReady Job (ideal.processor_state Job) _ Cost Arrival}.
Consider any arrival sequence.
Next, consider any ideal uni-processor schedule of this arrival sequence, ...
...and, assume that the schedule is valid.
In addition, we assume the existence of a function mapping jobs to their preemption points ...
... and assume that it defines a valid preemption model.
We prove that every nonpreemptive segment always begins with a preemption time.