Library prosa.analysis.facts.preemption.rtc_threshold.job_preemptable
Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.analysis.facts.behavior.all.
Require Export prosa.model.task.preemption.parameters.
Require Export prosa.analysis.facts.behavior.all.
Require Export prosa.model.task.preemption.parameters.
Run-to-Completion Threshold
In this section, we provide a few basic properties of run-to-completion-threshold-compliant schedules.
Consider any type of jobs.
In addition, we assume existence of a function
mapping jobs to their preemption points.
Consider any kind of processor state model, ...
... any job arrival sequence, ...
... and any given schedule.
Assume that the preemption model is valid.
Consider an arbitrary job j from the arrival sequence.
First we prove a few auxiliary lemmas about
job_preemption_points.
We prove that the sequence of preemption points of a zero-cost
job consists of one element -- 0.
Lemma preemption_points_of_zero_cost_job:
job_cost j = 0 →
job_preemption_points j = [::0].
Proof.
intros ZERO.
destruct (H_valid_preemption_model j) as [A1 [A2 [A3 A4]]]; auto.
unfold job_preemption_points; rewrite ZERO; simpl.
simpl; unfold job_cannot_become_nonpreemptive_before_execution in ×.
by rewrite A1.
Qed.
job_cost j = 0 →
job_preemption_points j = [::0].
Proof.
intros ZERO.
destruct (H_valid_preemption_model j) as [A1 [A2 [A3 A4]]]; auto.
unfold job_preemption_points; rewrite ZERO; simpl.
simpl; unfold job_cannot_become_nonpreemptive_before_execution in ×.
by rewrite A1.
Qed.
For a positive-cost job, 0 ...
Lemma zero_in_preemption_points:
0 < job_cost j →
0 \in job_preemption_points j.
Proof.
intros POS.
unfold job_preemption_points, range.
destruct (H_valid_preemption_model j) as [A1 [A2 [A3 A4]]]; auto.
unfold job_cannot_become_nonpreemptive_before_execution in ×.
by rewrite index_iota_lt_step//= A1 in_cons eq_refl.
Qed.
0 < job_cost j →
0 \in job_preemption_points j.
Proof.
intros POS.
unfold job_preemption_points, range.
destruct (H_valid_preemption_model j) as [A1 [A2 [A3 A4]]]; auto.
unfold job_cannot_become_nonpreemptive_before_execution in ×.
by rewrite index_iota_lt_step//= A1 in_cons eq_refl.
Qed.
... and job_cost are in preemption points.
Lemma job_cost_in_preemption_points:
0 < job_cost j →
job_cost j \in job_preemption_points j.
Proof.
intros POS.
unfold job_preemption_points, range, index_iota; rewrite subn0 -addn1.
rewrite iotaD add0n filter_cat mem_cat.
apply/orP; right; simpl.
destruct (H_valid_preemption_model j) as [A1 [A2 [A3 A4]]]; auto.
unfold job_cannot_be_nonpreemptive_after_completion in ×.
by rewrite A2 in_cons eq_refl.
Qed.
0 < job_cost j →
job_cost j \in job_preemption_points j.
Proof.
intros POS.
unfold job_preemption_points, range, index_iota; rewrite subn0 -addn1.
rewrite iotaD add0n filter_cat mem_cat.
apply/orP; right; simpl.
destruct (H_valid_preemption_model j) as [A1 [A2 [A3 A4]]]; auto.
unfold job_cannot_be_nonpreemptive_after_completion in ×.
by rewrite A2 in_cons eq_refl.
Qed.
Therefore, for a positive-cost job size of the sequence of
preemption points is at least two.
Lemma size_of_preemption_points:
0 < job_cost j →
2 ≤ size (job_preemption_points j).
Proof.
intros POS.
replace 2 with (size [::0; job_cost j]) ⇒ [|//].
apply subseq_leq_size.
- apply/andP; split.
+ rewrite !in_cons Bool.negb_orb.
by apply/andP; split; [rewrite neq_ltn POS|].
+ by [].
- intros ρ; rewrite !in_cons; move ⇒ /orP [/eqP EQ| /orP [/eqP Cost | C]].
+ by subst; apply zero_in_preemption_points.
+ by subst; apply job_cost_in_preemption_points.
+ by [].
Qed.
0 < job_cost j →
2 ≤ size (job_preemption_points j).
Proof.
intros POS.
replace 2 with (size [::0; job_cost j]) ⇒ [|//].
apply subseq_leq_size.
- apply/andP; split.
+ rewrite !in_cons Bool.negb_orb.
by apply/andP; split; [rewrite neq_ltn POS|].
+ by [].
- intros ρ; rewrite !in_cons; move ⇒ /orP [/eqP EQ| /orP [/eqP Cost | C]].
+ by subst; apply zero_in_preemption_points.
+ by subst; apply job_cost_in_preemption_points.
+ by [].
Qed.
Next we show that the sequence of preemption points is a non-decreasing sequence.
Lemma preemption_points_nondecreasing:
nondecreasing_sequence (job_preemption_points j).
Proof. by apply increasing_implies_nondecreasing, iota_is_increasing_sequence. Qed.
nondecreasing_sequence (job_preemption_points j).
Proof. by apply increasing_implies_nondecreasing, iota_is_increasing_sequence. Qed.
Next, we prove that the last element of the sequence of
preemption points is job_cost.
Lemma job_cost_is_last_element_of_preemption_points:
job_cost j = last0 (job_preemption_points j).
Proof.
unfold job_preemption_points.
edestruct H_valid_preemption_model as [A1 [A2 [A3 A4]]]; eauto 2.
erewrite last0_filter.
+ by apply/eqP; apply eq_refl.
+ unfold range, index_iota; rewrite subn0 -addn1.
by rewrite iotaD; destruct (iota 0 (job_cost j)).
+ unfold range, index_iota; rewrite subn0 -addn1.
by rewrite iotaD last0_cat //.
+ by apply A2.
Qed.
job_cost j = last0 (job_preemption_points j).
Proof.
unfold job_preemption_points.
edestruct H_valid_preemption_model as [A1 [A2 [A3 A4]]]; eauto 2.
erewrite last0_filter.
+ by apply/eqP; apply eq_refl.
+ unfold range, index_iota; rewrite subn0 -addn1.
by rewrite iotaD; destruct (iota 0 (job_cost j)).
+ unfold range, index_iota; rewrite subn0 -addn1.
by rewrite iotaD last0_cat //.
+ by apply A2.
Qed.
Last non-preemptive segment of a positive-cost job has positive length.
Lemma job_last_nonpreemptive_segment_positive:
job_cost_positive j →
0 < job_last_nonpreemptive_segment j.
Proof.
intros COST. unfold job_last_nonpreemptive_segment.
rewrite last0_nth function_of_distances_is_correct subn_gt0.
rewrite [size _]pred_Sn -addn1-addn1.
rewrite -size_of_seq_of_distances ?addn1; last by apply size_of_preemption_points.
rewrite prednK; last first.
{ rewrite -(leq_add2r 1) !addn1 prednK.
- apply size_of_preemption_points; eauto.
- rewrite ltnW //; apply size_of_preemption_points; eauto.
}
apply iota_is_increasing_sequence; apply/andP; split.
- rewrite -(leq_add2r 2) !addn2.
rewrite prednK//.
rewrite -(leq_add2r 1) !addn1.
rewrite prednK.
+ by apply size_of_preemption_points.
+ by rewrite ltnW //; apply size_of_preemption_points.
- rewrite -(leq_add2r 1) !addn1.
unfold job_preemption_points, range.
by rewrite prednK ?ltnS// ltnW// size_of_preemption_points.
Qed.
job_cost_positive j →
0 < job_last_nonpreemptive_segment j.
Proof.
intros COST. unfold job_last_nonpreemptive_segment.
rewrite last0_nth function_of_distances_is_correct subn_gt0.
rewrite [size _]pred_Sn -addn1-addn1.
rewrite -size_of_seq_of_distances ?addn1; last by apply size_of_preemption_points.
rewrite prednK; last first.
{ rewrite -(leq_add2r 1) !addn1 prednK.
- apply size_of_preemption_points; eauto.
- rewrite ltnW //; apply size_of_preemption_points; eauto.
}
apply iota_is_increasing_sequence; apply/andP; split.
- rewrite -(leq_add2r 2) !addn2.
rewrite prednK//.
rewrite -(leq_add2r 1) !addn1.
rewrite prednK.
+ by apply size_of_preemption_points.
+ by rewrite ltnW //; apply size_of_preemption_points.
- rewrite -(leq_add2r 1) !addn1.
unfold job_preemption_points, range.
by rewrite prednK ?ltnS// ltnW// size_of_preemption_points.
Qed.
Max nonpreemptive segment of a positive-cost job has positive length.
Lemma job_max_nonpreemptive_segment_positive:
job_cost_positive j →
0 < job_max_nonpreemptive_segment j.
Proof.
intros COST.
eapply leq_trans.
- by apply job_last_nonpreemptive_segment_positive.
- by apply last_of_seq_le_max_of_seq.
Qed.
job_cost_positive j →
0 < job_max_nonpreemptive_segment j.
Proof.
intros COST.
eapply leq_trans.
- by apply job_last_nonpreemptive_segment_positive.
- by apply last_of_seq_le_max_of_seq.
Qed.
Next we show that max nonpreemptive segment is at most the
cost of a job.
Lemma job_max_nonpreemptive_segment_le_job_cost:
job_max_nonpreemptive_segment j ≤ job_cost j.
Proof.
eapply leq_trans.
- apply max_distance_in_seq_le_last_element_of_seq; apply preemption_points_nondecreasing.
- destruct (H_valid_preemption_model j) as [A1 [A2 [A3 A4]]]; auto.
case: (posnP (job_cost j)) ⇒ [ZERO|POSt].
{ unfold job_preemption_points; rewrite ZERO.
simpl; unfold job_cannot_become_nonpreemptive_before_execution in ×.
by rewrite A1.
}
{ eapply leq_trans; first apply last_of_seq_le_max_of_seq.
rewrite job_cost_is_last_element_of_preemption_points.
apply last_is_max_in_nondecreasing_seq; first by apply preemption_points_nondecreasing.
apply max0_in_seq.
have LL := size_of_preemption_points POSt.
by destruct (job_preemption_points j).
}
Qed.
job_max_nonpreemptive_segment j ≤ job_cost j.
Proof.
eapply leq_trans.
- apply max_distance_in_seq_le_last_element_of_seq; apply preemption_points_nondecreasing.
- destruct (H_valid_preemption_model j) as [A1 [A2 [A3 A4]]]; auto.
case: (posnP (job_cost j)) ⇒ [ZERO|POSt].
{ unfold job_preemption_points; rewrite ZERO.
simpl; unfold job_cannot_become_nonpreemptive_before_execution in ×.
by rewrite A1.
}
{ eapply leq_trans; first apply last_of_seq_le_max_of_seq.
rewrite job_cost_is_last_element_of_preemption_points.
apply last_is_max_in_nondecreasing_seq; first by apply preemption_points_nondecreasing.
apply max0_in_seq.
have LL := size_of_preemption_points POSt.
by destruct (job_preemption_points j).
}
Qed.
We also show that last nonpreemptive segment is at most the
cost of a job.
Lemma job_last_nonpreemptive_segment_le_job_cost:
job_last_nonpreemptive_segment j ≤ job_cost j.
Proof.
eapply leq_trans.
- apply last_of_seq_le_max_of_seq.
- apply job_max_nonpreemptive_segment_le_job_cost.
Qed.
End AuxiliaryLemmas.
job_last_nonpreemptive_segment j ≤ job_cost j.
Proof.
eapply leq_trans.
- apply last_of_seq_le_max_of_seq.
- apply job_max_nonpreemptive_segment_le_job_cost.
Qed.
End AuxiliaryLemmas.
We prove that the run-to-completion threshold is positive for
any job with positive cost. I.e., in order to become
non-preemptive a job must receive at least one unit of
service.
Lemma job_run_to_completion_threshold_positive:
job_cost_positive j →
0 < job_rtct j.
Proof.
intros COST; unfold job_rtct.
have N1 := job_last_nonpreemptive_segment_positive COST.
have N2 := job_last_nonpreemptive_segment_le_job_cost.
lia.
Qed.
job_cost_positive j →
0 < job_rtct j.
Proof.
intros COST; unfold job_rtct.
have N1 := job_last_nonpreemptive_segment_positive COST.
have N2 := job_last_nonpreemptive_segment_le_job_cost.
lia.
Qed.
Next we show that the run-to-completion threshold is at most
the cost of a job.
Lemma job_run_to_completion_threshold_le_job_cost:
job_rtct j ≤ job_cost j.
Proof. by apply leq_subr. Qed.
job_rtct j ≤ job_cost j.
Proof. by apply leq_subr. Qed.
We prove that a job cannot be preempted
during execution of the last segment.
Lemma job_cannot_be_preempted_within_last_segment:
∀ (ρ : duration),
job_rtct j ≤ ρ < job_cost j →
~~ job_preemptable j ρ.
Proof.
move ⇒ ρ /andP [GE LT].
apply/negP; intros C.
have POS : 0 < job_cost j; first by lia.
rewrite /job_rtct subnBA in GE; last by apply job_last_nonpreemptive_segment_positive.
rewrite -addnBAC in GE; [rewrite addn1 in GE | by apply job_last_nonpreemptive_segment_le_job_cost].
rewrite job_cost_is_last_element_of_preemption_points in LT, GE.
rewrite last_seq_minus_last_distance_seq in GE; last by apply preemption_points_nondecreasing.
have EQ := antidensity_of_nondecreasing_seq.
specialize (EQ (job_preemption_points j) ρ (size (job_preemption_points j)).-2 ).
feed_n 2 EQ; first by apply preemption_points_nondecreasing.
{ apply/andP; split⇒ [//|].
rewrite prednK; first by rewrite -last0_nth.
rewrite -(leq_add2r 1) !addn1 prednK.
- exact: size_of_preemption_points.
- by eapply leq_trans; last apply size_of_preemption_points.
}
move: EQ ⇒ /negP EQ; apply: EQ.
apply conversion_preserves_equivalence ⇒ //.
eapply leq_trans; first by apply ltnW; exact LT.
by rewrite job_cost_is_last_element_of_preemption_points.
Qed.
∀ (ρ : duration),
job_rtct j ≤ ρ < job_cost j →
~~ job_preemptable j ρ.
Proof.
move ⇒ ρ /andP [GE LT].
apply/negP; intros C.
have POS : 0 < job_cost j; first by lia.
rewrite /job_rtct subnBA in GE; last by apply job_last_nonpreemptive_segment_positive.
rewrite -addnBAC in GE; [rewrite addn1 in GE | by apply job_last_nonpreemptive_segment_le_job_cost].
rewrite job_cost_is_last_element_of_preemption_points in LT, GE.
rewrite last_seq_minus_last_distance_seq in GE; last by apply preemption_points_nondecreasing.
have EQ := antidensity_of_nondecreasing_seq.
specialize (EQ (job_preemption_points j) ρ (size (job_preemption_points j)).-2 ).
feed_n 2 EQ; first by apply preemption_points_nondecreasing.
{ apply/andP; split⇒ [//|].
rewrite prednK; first by rewrite -last0_nth.
rewrite -(leq_add2r 1) !addn1 prednK.
- exact: size_of_preemption_points.
- by eapply leq_trans; last apply size_of_preemption_points.
}
move: EQ ⇒ /negP EQ; apply: EQ.
apply conversion_preserves_equivalence ⇒ //.
eapply leq_trans; first by apply ltnW; exact LT.
by rewrite job_cost_is_last_element_of_preemption_points.
Qed.
In order to get a consistent schedule, the scheduler should respect
the notion of run-to-completion threshold. We assume that, after
a job reaches its run-to-completion threshold, it cannot be preempted
until its completion.
Lemma job_nonpreemptive_after_run_to_completion_threshold:
∀ t t',
t ≤ t' →
job_rtct j ≤ service sched j t →
~~ completed_by sched j t' →
scheduled_at sched j t'.
Proof.
move⇒ t t' LE TH COM.
apply H_valid_preemption_model ⇒ [//|].
apply job_cannot_be_preempted_within_last_segment; apply/andP; split.
- by apply leq_trans with (service sched j t); last apply service_monotonic.
- by rewrite ltnNge.
Qed.
End RunToCompletionThreshold.
∀ t t',
t ≤ t' →
job_rtct j ≤ service sched j t →
~~ completed_by sched j t' →
scheduled_at sched j t'.
Proof.
move⇒ t t' LE TH COM.
apply H_valid_preemption_model ⇒ [//|].
apply job_cannot_be_preempted_within_last_segment; apply/andP; split.
- by apply leq_trans with (service sched j t); last apply service_monotonic.
- by rewrite ltnNge.
Qed.
End RunToCompletionThreshold.
We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq
will be able to apply them automatically.
Global Hint Resolve job_run_to_completion_threshold_le_job_cost : basic_rt_facts.