Library prosa.analysis.facts.model.preemption
Require Export prosa.model.schedule.priority_driven.
Require Export prosa.analysis.facts.behavior.completion.
Require Export prosa.analysis.facts.model.scheduled.
Require Export prosa.analysis.facts.behavior.completion.
Require Export prosa.analysis.facts.model.scheduled.
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 valid arrival sequence
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
Allow for any uniprocessor model.
Next, consider any schedule of the arrival sequence...
... where jobs come from the arrival sequence and don't execute before
their arrival time.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
Hypothesis H_must_arrive: jobs_must_arrive_to_execute sched.
jobs_come_from_arrival_sequence sched arr_seq.
Hypothesis H_must_arrive: jobs_must_arrive_to_execute sched.
Consider a valid preemption model.
We start with a trivial fact that, given a time interval
[t1,
t2)>>, the interval either contains a preemption time t or it
does not.
Lemma preemption_time_interval_case :
∀ t1 t2,
(∀ t, t1 ≤ t < t2 → ~~ preemption_time arr_seq sched t)
∨ (∃ t,
t1 ≤ t < t2
∧ preemption_time arr_seq sched t
∧ ∀ t', t1 ≤ t' → preemption_time arr_seq sched t' → t ≤ t').
∀ t1 t2,
(∀ t, t1 ≤ t < t2 → ~~ preemption_time arr_seq sched t)
∨ (∃ t,
t1 ≤ t < t2
∧ preemption_time arr_seq sched t
∧ ∀ t', t1 ≤ t' → preemption_time arr_seq sched t' → t ≤ t').
An idle instant is a preemption time.
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 arr_seq sched prt.+1.
∀ j prt,
arrives_in arr_seq j →
~~ scheduled_at sched j prt →
scheduled_at sched j prt.+1 →
preemption_time arr_seq sched prt.+1.
If a job is scheduled at a point in time that is not a preemption time,
then it was previously scheduled.
Lemma neg_pt_scheduled_at :
∀ j t,
scheduled_at sched j t.+1 →
~~ preemption_time arr_seq sched t.+1 →
scheduled_at sched j t.
∀ j t,
scheduled_at sched j t.+1 →
~~ preemption_time arr_seq sched t.+1 →
scheduled_at sched j t.
If a job is scheduled at time t-1 and time t is not a
preemption time, then the job is scheduled at time t as
well.
Lemma neg_pt_scheduled_before :
∀ j t,
~~ preemption_time arr_seq sched t →
scheduled_at sched j t.-1 →
scheduled_at sched j t.
∀ j t,
~~ preemption_time arr_seq sched t →
scheduled_at sched j t.-1 →
scheduled_at sched j t.
Next we extend the above lemma to an interval. That is, as long as there
is no preemption time, a job will remain scheduled.
Lemma neg_pt_scheduled_continuously_before :
∀ j t1 t2,
scheduled_at sched j t1 →
t1 ≤ t2 →
(∀ t, t1 < t ≤ t2 → ~~ preemption_time arr_seq sched t) →
scheduled_at sched j t2.
∀ j t1 t2,
scheduled_at sched j t1 →
t1 ≤ t2 →
(∀ t, t1 < t ≤ t2 → ~~ preemption_time arr_seq sched t) →
scheduled_at sched j t2.
Conversely if a job is scheduled at some time t2 and
we know that there is no preemption time between t1
and t2 then the job must have been scheduled at t1
too.
Lemma neg_pt_scheduled_continuously_after :
∀ j t1 t2,
scheduled_at sched j t2 →
t1 ≤ t2 →
(∀ t, t1 ≤ t ≤ t2 → ~~ preemption_time arr_seq sched t) →
scheduled_at sched j t1.
∀ j t1 t2,
scheduled_at sched j t2 →
t1 ≤ t2 →
(∀ t, t1 ≤ t ≤ t2 → ~~ preemption_time arr_seq sched t) →
scheduled_at sched j t1.
Finally, using the above two lemmas we can prove that, if there is no
preemption time in an interval
[t1, t2)
, then if a job is scheduled
at time t ∈ [t1, t2)
, then the same job is also scheduled at
another time t' ∈ [t1, t2)
.
Lemma neg_pt_scheduled_continuous :
∀ j t1 t2 t t',
t1 ≤ t < t2 →
t1 ≤ t' < t2 →
(∀ t, t1 ≤ t < t2 → ~~ preemption_time arr_seq sched t) →
scheduled_at sched j t →
scheduled_at sched j t'.
∀ j t1 t2 t t',
t1 ≤ t < t2 →
t1 ≤ t' < t2 →
(∀ t, t1 ≤ t < t2 → ~~ preemption_time arr_seq sched t) →
scheduled_at sched j t →
scheduled_at sched j t'.
If we observe two different jobs scheduled at two points in time, then
there necessarily is a preemption time in between.
Lemma neq_scheduled_at_pt :
∀ j t,
scheduled_at sched j t →
∀ j' t',
scheduled_at sched j' t' →
j != j' →
t ≤ t' →
exists2 pt, preemption_time arr_seq sched pt & t < pt ≤ t'.
∀ j t,
scheduled_at sched j t →
∀ j' t',
scheduled_at sched j' t' →
j != j' →
t ≤ t' →
exists2 pt, preemption_time arr_seq sched pt & t < pt ≤ t'.
We can strengthen the above lemma to say that there exists a preemption
time such that, after the preemption point, the next job to be scheduled
is scheduled continuously.
Lemma neq_scheduled_at_pt_continuous_sched :
∀ j t,
scheduled_at sched j t →
∀ j' t',
scheduled_at sched j' t' →
j != j' →
t ≤ t' →
∃ pt,
preemption_time arr_seq sched pt
∧ t < pt ≤ t'
∧ scheduled_at sched j' pt.
End PreemptionTimes.
∀ j t,
scheduled_at sched j t →
∀ j' t',
scheduled_at sched j' t' →
j != j' →
t ≤ t' →
∃ pt,
preemption_time arr_seq sched pt
∧ t < pt ≤ t'
∧ scheduled_at sched j' pt.
End PreemptionTimes.
In this section, we prove a lemma relating scheduling and preemption times.
Consider any type of jobs.
Allow for any uniprocessor model.
Context {PState : ProcessorState Job}.
Hypothesis H_uniproc : uniprocessor_model PState.
Context `{@JobReady Job PState Cost Arrival}.
Hypothesis H_uniproc : uniprocessor_model PState.
Context `{@JobReady Job PState Cost Arrival}.
Consider any valid arrival sequence.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
Next, consider any valid schedule of this arrival sequence.
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.
Lemma scheduling_of_any_segment_starts_with_preemption_time:
∀ j t,
scheduled_at sched j t →
∃ pt,
job_arrival j ≤ pt ≤ t ∧
preemption_time arr_seq sched pt ∧
(∀ t', pt ≤ t' ≤ t → scheduled_at sched j t').
∀ j t,
scheduled_at sched j t →
∃ pt,
job_arrival j ≤ pt ≤ t ∧
preemption_time arr_seq sched pt ∧
(∀ t', pt ≤ t' ≤ t → scheduled_at sched j t').
We strengthen the above lemma to say that the preemption time that a segment
starts with must lie between the last preemption time and the instant we
know the job is scheduled at.