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.
Lemma zero_is_pt: preemption_time sched 0.
Proof.
unfold preemption_time.
case SCHED: (sched 0) ⇒ [j | ]; last by done.
move: (SCHED) ⇒ /eqP; rewrite -scheduled_at_def; move ⇒ ARR.
apply H_jobs_come_from_arrival_sequence in ARR.
rewrite /service /service_during big_geq; last by done.
by move: (H_valid_preemption_model j ARR) ⇒ [PP _].
Qed.
Proof.
unfold preemption_time.
case SCHED: (sched 0) ⇒ [j | ]; last by done.
move: (SCHED) ⇒ /eqP; rewrite -scheduled_at_def; move ⇒ ARR.
apply H_jobs_come_from_arrival_sequence in ARR.
rewrite /service /service_during big_geq; last by done.
by move: (H_valid_preemption_model j ARR) ⇒ [PP _].
Qed.
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.
Proof.
intros s pt ARR NSCHED SCHED.
unfold preemption_time.
move: (SCHED); rewrite scheduled_at_def; move ⇒ /eqP SCHED2; rewrite SCHED2; clear SCHED2.
by move: (H_valid_preemption_model s ARR) ⇒ [_ [_ [_ P]]]; apply P.
Qed.
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.
Proof.
intros s pt ARR NSCHED SCHED.
unfold preemption_time.
move: (SCHED); rewrite scheduled_at_def; move ⇒ /eqP SCHED2; rewrite SCHED2; clear SCHED2.
by move: (H_valid_preemption_model s ARR) ⇒ [_ [_ [_ P]]]; apply P.
Qed.
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.
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').
Proof.
intros s t SCHEDst.
have EX: ∃ t', (t' ≤ t) && (scheduled_at sched s t')
&& (all (fun t'' ⇒ scheduled_at sched s t'') (index_iota t' t.+1 )).
{ ∃ t. apply/andP; split; [ by apply/andP; split | ].
apply/allP; intros t'.
by rewrite mem_index_iota ltnS -eqn_leq; move ⇒ /eqP <-.
}
have MATE : jobs_must_arrive_to_execute sched by eauto with basic_facts.
move : (H_sched_valid) ⇒ [COME_ARR READY].
have MIN := ex_minnP EX.
move: MIN ⇒ [mpt /andP [/andP [LT1 SCHEDsmpt] /allP ALL] MIN]; clear EX.
destruct mpt.
- ∃ 0; repeat split.
+ by apply/andP; split ⇒ //; apply MATE.
+ eapply (zero_is_pt arr_seq); eauto 2.
+ by intros; apply ALL; rewrite mem_iota subn0 add0n ltnS.
- have NSCHED: ~~ scheduled_at sched s mpt.
{ apply/negP; intros SCHED.
enough (F : mpt < mpt); first by rewrite ltnn in F.
apply MIN.
apply/andP; split; [by apply/andP; split; [ apply ltnW | ] | ].
apply/allP; intros t'.
rewrite mem_index_iota; move ⇒ /andP [GE LE].
move: GE; rewrite leq_eqVlt; move ⇒ /orP [/eqP EQ| LT].
- by subst t'.
- by apply ALL; rewrite mem_index_iota; apply/andP; split.
}
have PP: preemption_time sched mpt.+1 by eapply (first_moment_is_pt arr_seq) with (j := s); eauto 2.
∃ mpt.+1; repeat split; try done.
+ apply/andP; split; last by done.
by apply MATE in SCHEDsmpt.
+ move ⇒ t' /andP [GE LE].
by apply ALL; rewrite mem_index_iota; apply/andP; split.
Qed.
End PreemptionFacts.
∀ 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').
Proof.
intros s t SCHEDst.
have EX: ∃ t', (t' ≤ t) && (scheduled_at sched s t')
&& (all (fun t'' ⇒ scheduled_at sched s t'') (index_iota t' t.+1 )).
{ ∃ t. apply/andP; split; [ by apply/andP; split | ].
apply/allP; intros t'.
by rewrite mem_index_iota ltnS -eqn_leq; move ⇒ /eqP <-.
}
have MATE : jobs_must_arrive_to_execute sched by eauto with basic_facts.
move : (H_sched_valid) ⇒ [COME_ARR READY].
have MIN := ex_minnP EX.
move: MIN ⇒ [mpt /andP [/andP [LT1 SCHEDsmpt] /allP ALL] MIN]; clear EX.
destruct mpt.
- ∃ 0; repeat split.
+ by apply/andP; split ⇒ //; apply MATE.
+ eapply (zero_is_pt arr_seq); eauto 2.
+ by intros; apply ALL; rewrite mem_iota subn0 add0n ltnS.
- have NSCHED: ~~ scheduled_at sched s mpt.
{ apply/negP; intros SCHED.
enough (F : mpt < mpt); first by rewrite ltnn in F.
apply MIN.
apply/andP; split; [by apply/andP; split; [ apply ltnW | ] | ].
apply/allP; intros t'.
rewrite mem_index_iota; move ⇒ /andP [GE LE].
move: GE; rewrite leq_eqVlt; move ⇒ /orP [/eqP EQ| LT].
- by subst t'.
- by apply ALL; rewrite mem_index_iota; apply/andP; split.
}
have PP: preemption_time sched mpt.+1 by eapply (first_moment_is_pt arr_seq) with (j := s); eauto 2.
∃ mpt.+1; repeat split; try done.
+ apply/andP; split; last by done.
by apply MATE in SCHEDsmpt.
+ move ⇒ t' /andP [GE LE].
by apply ALL; rewrite mem_index_iota; apply/andP; split.
Qed.
End PreemptionFacts.