Library prosa.analysis.facts.preemption.job.preemptive
Require Export prosa.model.task.preemption.parameters.
Require Export prosa.model.preemption.fully_preemptive.
Require Export prosa.model.preemption.fully_preemptive.
Preemptions in Fully Preemptive Model
In this section, we prove that instantiation of predicate job_preemptable to the fully preemptive model indeed defines a valid preemption model.
We assume that jobs are fully preemptive.
Consider any type of jobs.
Consider any kind of processor state model, ...
... any job arrival sequence, ...
... and any given schedule.
Then, we prove that fully_preemptive_model is a valid preemption model.
Lemma valid_fully_preemptive_model:
valid_preemption_model arr_seq sched.
Proof.
by intros j ARR; repeat split; intros t CONTR.
Qed.
valid_preemption_model arr_seq sched.
Proof.
by intros j ARR; repeat split; intros t CONTR.
Qed.
We also prove that under the fully preemptive model
job_max_nonpreemptive_segment j is equal to 0, when job_cost
j = 0 ...
Lemma job_max_nps_is_0:
∀ j,
job_cost j = 0 →
job_max_nonpreemptive_segment j = 0.
Proof.
move⇒ j H1.
rewrite /job_max_nonpreemptive_segment /lengths_of_segments
/job_preemption_points.
by rewrite H1.
Qed.
∀ j,
job_cost j = 0 →
job_max_nonpreemptive_segment j = 0.
Proof.
move⇒ j H1.
rewrite /job_max_nonpreemptive_segment /lengths_of_segments
/job_preemption_points.
by rewrite H1.
Qed.
Lemma job_max_nps_is_ε:
∀ j,
job_cost j > 0 →
job_max_nonpreemptive_segment j = ε.
Proof.
intros ? POS.
rewrite /job_max_nonpreemptive_segment /lengths_of_segments
/job_preemption_points.
rewrite /job_preemptable /fully_preemptive_job_model.
rewrite filter_predT.
apply max0_of_uniform_set.
- rewrite /range /index_iota subn0.
rewrite [size _]pred_Sn -[in X in _ ≤ X]addn1 -size_of_seq_of_distances size_iota.
+ by rewrite -pred_Sn.
+ by rewrite ltnS.
- by apply distances_of_iota_ε.
Qed.
End FullyPreemptiveModel.
Global Hint Resolve valid_fully_preemptive_model : basic_rt_facts.
∀ j,
job_cost j > 0 →
job_max_nonpreemptive_segment j = ε.
Proof.
intros ? POS.
rewrite /job_max_nonpreemptive_segment /lengths_of_segments
/job_preemption_points.
rewrite /job_preemptable /fully_preemptive_job_model.
rewrite filter_predT.
apply max0_of_uniform_set.
- rewrite /range /index_iota subn0.
rewrite [size _]pred_Sn -[in X in _ ≤ X]addn1 -size_of_seq_of_distances size_iota.
+ by rewrite -pred_Sn.
+ by rewrite ltnS.
- by apply distances_of_iota_ε.
Qed.
End FullyPreemptiveModel.
Global Hint Resolve valid_fully_preemptive_model : basic_rt_facts.