Library probsa.rt.analysis.scheduler_properties
From prosa Require Export model.preemption.fully_preemptive.
From prosa.implementation Require Import facts.ideal_uni.prio_aware.
From probsa.util Require Export seq prosa.prio_aware.
From probsa.rt.model Require Export scheduler abort_readiness.
From probsa.rt.model.assumptions
Require Export basic pr_respects_policy pr_must_be_ready pr_work_conserving.
Local Open Scope nat_scope.
From prosa.implementation Require Import facts.ideal_uni.prio_aware.
From probsa.util Require Export seq prosa.prio_aware.
From probsa.rt.model Require Export scheduler abort_readiness.
From probsa.rt.model.assumptions
Require Export basic pr_respects_policy pr_must_be_ready pr_work_conserving.
Local Open Scope nat_scope.
Sustainability and Properties of Fixed-Priority Fully-Preemptive Scheduling
Section SustainableUniFPFP.
Context {Job : finType}
{job_arrival : JobArrival Job}
{job_deadline : JobDeadline Job}
{JLDP : JLDP_policy Job}.
Context {Job : finType}
{job_arrival : JobArrival Job}
{job_deadline : JobDeadline Job}
{JLDP : JLDP_policy Job}.
Consider two job cost functions where job_cost2 is pointwise smaller
than job_cost1 (i.e., costs have been reduced).
Context {job_cost1 : JobCost Job}
{job_cost2 : JobCost Job}.
Hypothesis H_cost_monotone : ∀ j, job_cost1 j ≥ job_cost2 j.
Let job_ready1 := @abort_ready_instance Job _ job_arrival job_cost1 job_deadline.
Let job_ready2 := @abort_ready_instance Job _ job_arrival job_cost2 job_deadline.
Variable arr_seq : arrival_sequence Job.
{job_cost2 : JobCost Job}.
Hypothesis H_cost_monotone : ∀ j, job_cost1 j ≥ job_cost2 j.
Let job_ready1 := @abort_ready_instance Job _ job_arrival job_cost1 job_deadline.
Let job_ready2 := @abort_ready_instance Job _ job_arrival job_cost2 job_deadline.
Variable arr_seq : arrival_sequence Job.
Let sched1 := @uni_schedule Job job_cost1 job_arrival arr_seq job_ready1 fully_preemptive_model JLDP.
Let sched2 := @uni_schedule Job job_cost2 job_arrival arr_seq job_ready2 fully_preemptive_model JLDP.
Hypothesis H_consistent_arrival_times : consistent_arrival_times arr_seq.
Hypothesis H_arrival_sequence_uniq : arrival_sequence_uniq arr_seq.
Hypothesis H_total : total_priorities.
Hypothesis H_reflexive : reflexive_priorities.
Hypothesis H_transitive : transitive_priorities.
Section ScheduledAtMonotone.
Variables j : Job.
Variables t : instant.
Hypothesis H_j_sched1 : scheduled_at sched1 j t.
Hypothesis H_j_not_completed_sched2 : ~~ completed_by sched2 j t.
Hypothesis H_service_monotone_wrt_schedules :
∀ (j : Job),
~~ completed_by sched2 j t →
service sched1 j t ≤ service sched2 j t.
Let sched2 := @uni_schedule Job job_cost2 job_arrival arr_seq job_ready2 fully_preemptive_model JLDP.
Hypothesis H_consistent_arrival_times : consistent_arrival_times arr_seq.
Hypothesis H_arrival_sequence_uniq : arrival_sequence_uniq arr_seq.
Hypothesis H_total : total_priorities.
Hypothesis H_reflexive : reflexive_priorities.
Hypothesis H_transitive : transitive_priorities.
Section ScheduledAtMonotone.
Variables j : Job.
Variables t : instant.
Hypothesis H_j_sched1 : scheduled_at sched1 j t.
Hypothesis H_j_not_completed_sched2 : ~~ completed_by sched2 j t.
Hypothesis H_service_monotone_wrt_schedules :
∀ (j : Job),
~~ completed_by sched2 j t →
service sched1 j t ≤ service sched2 j t.
If job j is scheduled at time t in sched1 (with higher costs) and
hasn't completed by t in sched2 (with lower costs), then j must
also be scheduled at t in sched2. Intuition: With lower costs, other
jobs complete faster, freeing the processor for j at least as early as
before.
Local Lemma j_scheduled_at_t_in_sched2 :
scheduled_at sched2 j t.
Proof.
move: (H_j_sched1) ⇒ SUPR; apply scheduled_job_is_supremum in SUPR; last first.
{ by rewrite /preemption_time; destruct (uni_schedule _ _). }
apply supremum_monotone_wrt_subset
with (xs := @jobs_backlogged_at
_ _ _ _ _ arr_seq
match t return _ with
| O ⇒ @empty_schedule _ (ideal.processor_state _) None
| S t' ⇒ @schedule_up_to
_ _ (@allocation_at
_ _ _ arr_seq _ _ (@choose_highest_prio_job _ JLDP))
None t'
end t
) in SUPR; try done.
{ apply scheduled_job_is_supremum_new in SUPR.
{ by apply SUPR. }
{ by rewrite /preemption_time; destruct (uni_schedule _ _). }
}
{ by rewrite filter_uniq //; apply arrivals_uniq ⇒ //. }
{ apply seq.subseq_filter ⇒ s IN.
destruct t.
{ rewrite /backlogged !scheduled_at_def //=.
destruct (0 < _); last first.
{ by rewrite !andbT andbF. }
{ rewrite !andbT /pending.
destruct has_arrived; last by rewrite andFb.
rewrite !andTb /completed_by -!ltnNge ⇒ SERV.
apply: leq_trans; first apply: SERV.
by apply H_cost_monotone.
}
}
{ clear SUPR H_j_sched1.
rewrite /backlogged !scheduled_at_def !schedule_up_to_empty //= !andbT.
destruct (_ < _ ); last by rewrite andbF.
rewrite !andbT /pending; destruct has_arrived; last by rewrite andFb.
rewrite !andTb; apply contra ⇒ COMPI.
have [COMP2 | NCOMP2] := boolP (@completed_by _ _ (sched2) job_cost2 s i.+1).
{ apply: leq_trans; first by apply: COMP2.
rewrite /sched1 /service /service_during big_nat_cond [X in _ ≤ X]big_nat_cond.
apply leq_sum ⇒ k /andP [/andP [_ L] _].
by rewrite !service_at_def; erewrite schedule_up_to_identical_prefix; [ | | apply L].
}
feed (H_service_monotone_wrt_schedules s); [ by eassumption | clear NCOMP2].
apply: leq_trans; [apply: leq_trans; last by apply COMPI | ]; first by apply H_cost_monotone.
apply: leq_trans; [apply: leq_trans; last by apply H_service_monotone_wrt_schedules | ].
{ rewrite /sched1 /service /service_during big_nat_cond [X in _ ≤ X]big_nat_cond.
apply leq_sum ⇒ k /andP [/andP [_ L] _].
rewrite !service_at_def.
by erewrite schedule_up_to_identical_prefix; [ | | apply L] ⇒ //.
}
{ rewrite /sched1 /service /service_during big_nat_cond [X in _ ≤ X]big_nat_cond.
apply leq_sum ⇒ k /andP [/andP [_ L] _].
rewrite !service_at_def.
by erewrite schedule_up_to_identical_prefix; [ | | apply L] ⇒ //.
}
}
}
{ have VNPR : valid_nonpreemptive_readiness job_ready1 by intros ?.
have NCR : nonclairvoyant_readiness job_ready1
by intros ? ? ? ? ? ? ? ⇒ //=; f_equal; apply: identical_prefix_pending; eauto 1.
have USV := @uni_schedule_valid Job _ _ arr_seq job_ready1 NCR fully_preemptive_model VNPR JLDP.
destruct USV as [JFAS MBR].
have HA : has_arrived j t by apply jobs_must_arrive_to_be_ready in MBR; apply MBR.
have GED : t < prosa.behavior.job.job_deadline j
by apply MBR in H_j_sched1; move: H_j_sched1 ⇒ /andP [_ DEAD].
rewrite mem_filter; apply/andP; split; last first.
{ by apply arrived_between_implies_in_arrivals; [ | eapply JFAS, H_j_sched1 | apply HA ]. }
{ apply/andP; split; last first.
{ by destruct t; rewrite scheduled_at_def // schedule_up_to_empty. }
{ apply/andP; split ⇒ //; apply/andP; split ⇒ //.
move: H_j_not_completed_sched2; apply contra ⇒ NCOMP2.
apply: leq_trans; first by apply: NCOMP2.
rewrite /sched1 /service /service_during big_nat_cond [X in _ ≤ X]big_nat_cond.
apply leq_sum ⇒ i /andP [/andP [_ L] _].
destruct t; first by done.
rewrite !service_at_def.
by erewrite schedule_up_to_identical_prefix; [ | | apply L] ⇒ //.
}
}
}
Qed.
End ScheduledAtMonotone.
scheduled_at sched2 j t.
Proof.
move: (H_j_sched1) ⇒ SUPR; apply scheduled_job_is_supremum in SUPR; last first.
{ by rewrite /preemption_time; destruct (uni_schedule _ _). }
apply supremum_monotone_wrt_subset
with (xs := @jobs_backlogged_at
_ _ _ _ _ arr_seq
match t return _ with
| O ⇒ @empty_schedule _ (ideal.processor_state _) None
| S t' ⇒ @schedule_up_to
_ _ (@allocation_at
_ _ _ arr_seq _ _ (@choose_highest_prio_job _ JLDP))
None t'
end t
) in SUPR; try done.
{ apply scheduled_job_is_supremum_new in SUPR.
{ by apply SUPR. }
{ by rewrite /preemption_time; destruct (uni_schedule _ _). }
}
{ by rewrite filter_uniq //; apply arrivals_uniq ⇒ //. }
{ apply seq.subseq_filter ⇒ s IN.
destruct t.
{ rewrite /backlogged !scheduled_at_def //=.
destruct (0 < _); last first.
{ by rewrite !andbT andbF. }
{ rewrite !andbT /pending.
destruct has_arrived; last by rewrite andFb.
rewrite !andTb /completed_by -!ltnNge ⇒ SERV.
apply: leq_trans; first apply: SERV.
by apply H_cost_monotone.
}
}
{ clear SUPR H_j_sched1.
rewrite /backlogged !scheduled_at_def !schedule_up_to_empty //= !andbT.
destruct (_ < _ ); last by rewrite andbF.
rewrite !andbT /pending; destruct has_arrived; last by rewrite andFb.
rewrite !andTb; apply contra ⇒ COMPI.
have [COMP2 | NCOMP2] := boolP (@completed_by _ _ (sched2) job_cost2 s i.+1).
{ apply: leq_trans; first by apply: COMP2.
rewrite /sched1 /service /service_during big_nat_cond [X in _ ≤ X]big_nat_cond.
apply leq_sum ⇒ k /andP [/andP [_ L] _].
by rewrite !service_at_def; erewrite schedule_up_to_identical_prefix; [ | | apply L].
}
feed (H_service_monotone_wrt_schedules s); [ by eassumption | clear NCOMP2].
apply: leq_trans; [apply: leq_trans; last by apply COMPI | ]; first by apply H_cost_monotone.
apply: leq_trans; [apply: leq_trans; last by apply H_service_monotone_wrt_schedules | ].
{ rewrite /sched1 /service /service_during big_nat_cond [X in _ ≤ X]big_nat_cond.
apply leq_sum ⇒ k /andP [/andP [_ L] _].
rewrite !service_at_def.
by erewrite schedule_up_to_identical_prefix; [ | | apply L] ⇒ //.
}
{ rewrite /sched1 /service /service_during big_nat_cond [X in _ ≤ X]big_nat_cond.
apply leq_sum ⇒ k /andP [/andP [_ L] _].
rewrite !service_at_def.
by erewrite schedule_up_to_identical_prefix; [ | | apply L] ⇒ //.
}
}
}
{ have VNPR : valid_nonpreemptive_readiness job_ready1 by intros ?.
have NCR : nonclairvoyant_readiness job_ready1
by intros ? ? ? ? ? ? ? ⇒ //=; f_equal; apply: identical_prefix_pending; eauto 1.
have USV := @uni_schedule_valid Job _ _ arr_seq job_ready1 NCR fully_preemptive_model VNPR JLDP.
destruct USV as [JFAS MBR].
have HA : has_arrived j t by apply jobs_must_arrive_to_be_ready in MBR; apply MBR.
have GED : t < prosa.behavior.job.job_deadline j
by apply MBR in H_j_sched1; move: H_j_sched1 ⇒ /andP [_ DEAD].
rewrite mem_filter; apply/andP; split; last first.
{ by apply arrived_between_implies_in_arrivals; [ | eapply JFAS, H_j_sched1 | apply HA ]. }
{ apply/andP; split; last first.
{ by destruct t; rewrite scheduled_at_def // schedule_up_to_empty. }
{ apply/andP; split ⇒ //; apply/andP; split ⇒ //.
move: H_j_not_completed_sched2; apply contra ⇒ NCOMP2.
apply: leq_trans; first by apply: NCOMP2.
rewrite /sched1 /service /service_during big_nat_cond [X in _ ≤ X]big_nat_cond.
apply leq_sum ⇒ i /andP [/andP [_ L] _].
destruct t; first by done.
rewrite !service_at_def.
by erewrite schedule_up_to_identical_prefix; [ | | apply L] ⇒ //.
}
}
}
Qed.
End ScheduledAtMonotone.
Jobs receive at least as much service with lower costs, since other jobs
finish faster and consume less processor time.
Local Lemma service_monotone_wrt_sched :
∀ (j : Job) (t : instant),
~~ completed_by sched2 j t →
service sched1 j t ≤ service sched2 j t.
Proof.
intros; move: j H.
induction t; intros s.
{ by rewrite /service /service_during /service_at !big_geq //=. }
{ intros NCOMP.
have [COMPt | NCOMPs] := boolP (@completed_by _ _ sched2 job_cost2 s t).
{ exfalso; move: NCOMP ⇒ /negP NCOMP; apply: NCOMP.
by eapply completion_monotonic; last by eassumption.
}
{ have SERV := IHt _ NCOMPs.
have [SCHED1 | NSCHED1] := boolP (scheduled_at sched1 s t); last first.
{ rewrite -!service_last_plus_before.
apply: leq_add; first by done.
apply leq_trans with 0; last by done.
rewrite leqn0 service_at_def eqb0.
by move: NSCHED1; rewrite scheduled_at_def.
}
{ have SCHED2 : scheduled_at sched2 s t
by apply j_scheduled_at_t_in_sched2 ⇒ //.
rewrite -!service_last_plus_before.
apply: leq_add; first by done.
by move: SCHED1 SCHED2; rewrite !scheduled_at_def !service_at_def ⇒ /eqP → /eqP →.
}
}
}
Qed.
∀ (j : Job) (t : instant),
~~ completed_by sched2 j t →
service sched1 j t ≤ service sched2 j t.
Proof.
intros; move: j H.
induction t; intros s.
{ by rewrite /service /service_during /service_at !big_geq //=. }
{ intros NCOMP.
have [COMPt | NCOMPs] := boolP (@completed_by _ _ sched2 job_cost2 s t).
{ exfalso; move: NCOMP ⇒ /negP NCOMP; apply: NCOMP.
by eapply completion_monotonic; last by eassumption.
}
{ have SERV := IHt _ NCOMPs.
have [SCHED1 | NSCHED1] := boolP (scheduled_at sched1 s t); last first.
{ rewrite -!service_last_plus_before.
apply: leq_add; first by done.
apply leq_trans with 0; last by done.
rewrite leqn0 service_at_def eqb0.
by move: NSCHED1; rewrite scheduled_at_def.
}
{ have SCHED2 : scheduled_at sched2 s t
by apply j_scheduled_at_t_in_sched2 ⇒ //.
rewrite -!service_last_plus_before.
apply: leq_add; first by done.
by move: SCHED1 SCHED2; rewrite !scheduled_at_def !service_at_def ⇒ /eqP → /eqP →.
}
}
}
Qed.
Main sustainability result: Reducing job costs cannot delay completion.
If a job completes by time t in a schedule with larger costs
job_cost1, it will also complete by t in a schedule with smaller costs
job_cost2.
Lemma sustainable_uni_fp_fp :
∀ t j,
completed_by (H := job_cost1) sched1 j t →
completed_by (H := job_cost2) sched2 j t.
Proof.
intros.
have [COMP2 | NCOMP2] := boolP (@completed_by _ _ sched2 job_cost2 j t) ⇒ //.
move: (NCOMP2) ⇒ /negP NCOM; exfalso; apply: NCOM.
apply: leq_trans; last by apply service_monotone_wrt_sched.
apply: leq_trans; last by apply H.
by apply H_cost_monotone.
Qed.
End SustainableUniFPFP.
∀ t j,
completed_by (H := job_cost1) sched1 j t →
completed_by (H := job_cost2) sched2 j t.
Proof.
intros.
have [COMP2 | NCOMP2] := boolP (@completed_by _ _ sched2 job_cost2 j t) ⇒ //.
move: (NCOMP2) ⇒ /negP NCOM; exfalso; apply: NCOM.
apply: leq_trans; last by apply service_monotone_wrt_sched.
apply: leq_trans; last by apply H.
by apply H_cost_monotone.
Qed.
End SustainableUniFPFP.
Scheduler Definition and Properties
Section UniScheduleAsSchedulerAC.
Context {Task : TaskType}
{FP : FP_policy Task}
{D : TaskDeadline Task}.
Context {Job : finType}
{job_task : JobTask Job Task}.
Let arr_seq (A : Job → option instant) : arrival_sequence Job :=
fun t ⇒
[seq j <- index_enum Job |
if A j is Some ta
then t == ta
else false
].
Let job_deadline (A : Job → option nat) : JobDeadline Job :=
fun (j : Job) ⇒
odflt 0 (match A j with Some a ⇒ Some (a + D (job_task j)) | None ⇒ None end).
Let readiness (A C : Job → option nat) :=
@abort_ready_instance
_ _ (fun j ⇒ odflt 0 (A j)) (fun j ⇒ odflt 0 (C j)) (job_deadline A).
Let JLDP : JLDP_policy Job :=
@JLFP_to_JLDP _ (@FP_to_JLFP Job Task _ FP).
Context {Task : TaskType}
{FP : FP_policy Task}
{D : TaskDeadline Task}.
Context {Job : finType}
{job_task : JobTask Job Task}.
Let arr_seq (A : Job → option instant) : arrival_sequence Job :=
fun t ⇒
[seq j <- index_enum Job |
if A j is Some ta
then t == ta
else false
].
Let job_deadline (A : Job → option nat) : JobDeadline Job :=
fun (j : Job) ⇒
odflt 0 (match A j with Some a ⇒ Some (a + D (job_task j)) | None ⇒ None end).
Let readiness (A C : Job → option nat) :=
@abort_ready_instance
_ _ (fun j ⇒ odflt 0 (A j)) (fun j ⇒ odflt 0 (C j)) (job_deadline A).
Let JLDP : JLDP_policy Job :=
@JLFP_to_JLDP _ (@FP_to_JLFP Job Task _ FP).
Given vectors A and C describing job arrivals and job costs
respectively, the scheduler FP_FP_sched defined below implements
fully-preemptive fixed-priority scheduling using uni_schedule.
Definition FP_FP_sched : @scheduler𝗔𝗖 Job :=
fun (A C : Job → option nat) t ⇒
@uni_schedule
Job
(fun j ⇒ odflt 0 (C j)) (fun j ⇒ odflt 0 (A j))
(arr_seq A)
(readiness A C)
fully_preemptive_model
JLDP
t.
End UniScheduleAsSchedulerAC.
fun (A C : Job → option nat) t ⇒
@uni_schedule
Job
(fun j ⇒ odflt 0 (C j)) (fun j ⇒ odflt 0 (A j))
(arr_seq A)
(readiness A C)
fully_preemptive_model
JLDP
t.
End UniScheduleAsSchedulerAC.
Verification of Scheduler Properties
Section SchedulerProperties.
Context {Task : TaskType}
{FP : FP_policy Task}
{D : TaskDeadline Task}.
Context {Ω} {μ : measure Ω}.
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}
{job_arrival : JobArrivalRV Job Ω μ}
{job_task : JobTask Job Task}.
Hypothesis H_total : total_priorities.
Hypothesis H_reflexive : reflexive_priorities.
Hypothesis H_transitive : transitive_priorities.
Let pr_sched := @compute_pr_schedule Ω μ Job job_arrival job_cost FP_FP_sched.
Lemma abortion_readiness_is_nonclairvoyant :
∀ ω, @nonclairvoyant_readiness _ _ _ _ (pr_abort_ready_instance ω).
Proof.
intros ? ? ? ? ? ? ? ?.
simpl; f_equal.
by apply: identical_prefix_pending; eauto 1.
Qed.
Lemma FP_FP_sched_respects_completed_jobs_dont_execute :
pr_completed_jobs_dont_execute pr_sched.
Proof.
intros ω.
apply: valid_schedule_implies_completed_jobs_dont_execute; eauto 1.
apply: np_schedule_valid.
{ by apply abortion_readiness_is_nonclairvoyant. }
{ by intros *; apply: supremum_in. }
{ by unfold job_preemptable, fully_preemptive_model. }
Qed.
Lemma FP_FP_sched_respects_jobs_must_arrive_to_execute :
pr_jobs_must_arrive_to_execute pr_sched.
Proof.
intros ω.
apply: valid_schedule_implies_jobs_must_arrive_to_execute; eauto 1.
apply: np_schedule_valid.
{ by apply abortion_readiness_is_nonclairvoyant. }
{ by intros *; apply: supremum_in. }
{ by unfold job_preemptable, fully_preemptive_model. }
Qed.
Lemma FP_FP_sched_respects_jobs_come_from_arrival_sequence :
pr_jobs_come_from_arrival_sequence pr_sched.
Proof.
intros ω.
apply np_schedule_valid.
{ by apply abortion_readiness_is_nonclairvoyant. }
{ by intros *; apply: supremum_in. }
{ by unfold job_preemptable, fully_preemptive_model. }
Qed.
Lemma FP_FP_sched_is_work_conserving :
pr_work_conserving pr_sched pr_abort_ready_instance.
Proof.
intros ω.
apply: uni_schedule_work_conserving.
{ by apply pr_consistent_arrival_times. }
{ by apply abortion_readiness_is_nonclairvoyant. }
Qed.
Lemma FP_FP_sched_respects_policy_at_preemption_point :
pr_respects_policy_at_preemption_point
pr_sched pr_abort_ready_instance fully_preemptive_model.
Proof.
intros ω; apply schedule_respects_policy ⇒ //.
{ by apply pr_consistent_arrival_times. }
{ by apply abortion_readiness_is_nonclairvoyant. }
Qed.
Lemma FP_FP_sched_respects_jobs_must_be_ready_to_execute :
pr_jobs_must_be_ready_to_execute pr_sched pr_abort_ready_instance.
Proof.
intros ?.
apply np_schedule_valid.
{ by apply abortion_readiness_is_nonclairvoyant. }
{ by intros *; apply: supremum_in. }
{ by unfold job_preemptable, fully_preemptive_model. }
Qed.
Context {Task : TaskType}
{FP : FP_policy Task}
{D : TaskDeadline Task}.
Context {Ω} {μ : measure Ω}.
Context {Job : finType}
{job_cost : JobCostRV Job Ω μ}
{job_arrival : JobArrivalRV Job Ω μ}
{job_task : JobTask Job Task}.
Hypothesis H_total : total_priorities.
Hypothesis H_reflexive : reflexive_priorities.
Hypothesis H_transitive : transitive_priorities.
Let pr_sched := @compute_pr_schedule Ω μ Job job_arrival job_cost FP_FP_sched.
Lemma abortion_readiness_is_nonclairvoyant :
∀ ω, @nonclairvoyant_readiness _ _ _ _ (pr_abort_ready_instance ω).
Proof.
intros ? ? ? ? ? ? ? ?.
simpl; f_equal.
by apply: identical_prefix_pending; eauto 1.
Qed.
Lemma FP_FP_sched_respects_completed_jobs_dont_execute :
pr_completed_jobs_dont_execute pr_sched.
Proof.
intros ω.
apply: valid_schedule_implies_completed_jobs_dont_execute; eauto 1.
apply: np_schedule_valid.
{ by apply abortion_readiness_is_nonclairvoyant. }
{ by intros *; apply: supremum_in. }
{ by unfold job_preemptable, fully_preemptive_model. }
Qed.
Lemma FP_FP_sched_respects_jobs_must_arrive_to_execute :
pr_jobs_must_arrive_to_execute pr_sched.
Proof.
intros ω.
apply: valid_schedule_implies_jobs_must_arrive_to_execute; eauto 1.
apply: np_schedule_valid.
{ by apply abortion_readiness_is_nonclairvoyant. }
{ by intros *; apply: supremum_in. }
{ by unfold job_preemptable, fully_preemptive_model. }
Qed.
Lemma FP_FP_sched_respects_jobs_come_from_arrival_sequence :
pr_jobs_come_from_arrival_sequence pr_sched.
Proof.
intros ω.
apply np_schedule_valid.
{ by apply abortion_readiness_is_nonclairvoyant. }
{ by intros *; apply: supremum_in. }
{ by unfold job_preemptable, fully_preemptive_model. }
Qed.
Lemma FP_FP_sched_is_work_conserving :
pr_work_conserving pr_sched pr_abort_ready_instance.
Proof.
intros ω.
apply: uni_schedule_work_conserving.
{ by apply pr_consistent_arrival_times. }
{ by apply abortion_readiness_is_nonclairvoyant. }
Qed.
Lemma FP_FP_sched_respects_policy_at_preemption_point :
pr_respects_policy_at_preemption_point
pr_sched pr_abort_ready_instance fully_preemptive_model.
Proof.
intros ω; apply schedule_respects_policy ⇒ //.
{ by apply pr_consistent_arrival_times. }
{ by apply abortion_readiness_is_nonclairvoyant. }
Qed.
Lemma FP_FP_sched_respects_jobs_must_be_ready_to_execute :
pr_jobs_must_be_ready_to_execute pr_sched pr_abort_ready_instance.
Proof.
intros ?.
apply np_schedule_valid.
{ by apply abortion_readiness_is_nonclairvoyant. }
{ by intros *; apply: supremum_in. }
{ by unfold job_preemptable, fully_preemptive_model. }
Qed.
We prove that the scheduler is RT-monotonic. That is, reducing a job's
cost can only improve (or maintain) its completion time.
Lemma FP_FP_sched_is_rt_monotonic :
∀ horizon,
rt_monotonic_scheduler (Some horizon) FP_FP_sched.
Proof.
intros × A C ju j r c1 c2 LE.
set (Cs := update C ju c1); set (Cl := update C ju c2).
have UNI :
∀ t j,
@completed_by _ _ (FP_FP_sched A Cl) (fun j ⇒ odflt 0 (Cl j)) j t →
@completed_by _ _ (FP_FP_sched A Cs) (fun j ⇒ odflt 0 (Cs j)) j t.
{ apply sustainable_uni_fp_fp; eauto 1; last first.
{ by intros ?; rewrite filter_uniq // index_enum_uniq. }
{ intros s t; rewrite /arrives_at /arrivals_at mem_filter.
destruct (A s) eqn:EQ; last by done.
rewrite /prosa.behavior.job.job_arrival EQ //=.
by move⇒ /andP [/eqP → _].
}
{ by intros ?; rewrite /Cs /Cl /update; destruct (j0 == ju); [apply LE | done]. }
}
unfold FP_FP_sched, scheduler𝗔𝗖_to_rt𝗔𝗖 in *; simpl in ×.
destruct (scheduler.min_completion_time).
{ destruct (A j) as [aj | ] eqn:Aj; last by done.
destruct s as [rt1 [COMP1 MIN1]].
have [LErt1|GTrt1] := leqP horizon rt1.
{ intros _.
destruct (scheduler.min_completion_time); last by done.
destruct s as [rt2 [COMP2 MIN2]].
destruct (horizon ≤ rt2) eqn:GTrt2 ⇒ //.
move: GTrt2 ⇒ /negP/negP; rewrite -ltnNge ⇒ GTrt2.
exfalso; unfold FP_FP_sched, scheduler𝗔𝗖_to_completed𝗔𝗖 in ×.
apply (MIN1 rt2); first by apply/leP; apply: leq_trans; [apply GTrt2 | apply LErt1].
by apply UNI; apply COMP2. }
{ rewrite //= ltn_subRL ⇒ LTrt1.
destruct (scheduler.min_completion_time); last by done.
destruct s as [rt2 [COMP2 MIN2]].
destruct (horizon ≤ rt2) eqn:GTrt2 ⇒ //.
rewrite //= ltn_subRL; move_neq_up GErt2; unfold FP_FP_sched, scheduler𝗔𝗖_to_completed𝗔𝗖 in ×.
apply (MIN1 rt2); first by apply/leP; apply: leq_ltn_trans; [apply GErt2 | apply LTrt1].
by apply UNI; apply COMP2. }
}
{ destruct (A j) as [aj | ] eqn:Aj; last by done.
intros _; destruct (scheduler.min_completion_time); last by done.
destruct s as [rt2 [COMP2 MIN2]].
exfalso; apply: (n rt2); unfold scheduler𝗔𝗖_to_completed𝗔𝗖 in ×.
by apply UNI, COMP2.
}
Qed.
End SchedulerProperties.
∀ horizon,
rt_monotonic_scheduler (Some horizon) FP_FP_sched.
Proof.
intros × A C ju j r c1 c2 LE.
set (Cs := update C ju c1); set (Cl := update C ju c2).
have UNI :
∀ t j,
@completed_by _ _ (FP_FP_sched A Cl) (fun j ⇒ odflt 0 (Cl j)) j t →
@completed_by _ _ (FP_FP_sched A Cs) (fun j ⇒ odflt 0 (Cs j)) j t.
{ apply sustainable_uni_fp_fp; eauto 1; last first.
{ by intros ?; rewrite filter_uniq // index_enum_uniq. }
{ intros s t; rewrite /arrives_at /arrivals_at mem_filter.
destruct (A s) eqn:EQ; last by done.
rewrite /prosa.behavior.job.job_arrival EQ //=.
by move⇒ /andP [/eqP → _].
}
{ by intros ?; rewrite /Cs /Cl /update; destruct (j0 == ju); [apply LE | done]. }
}
unfold FP_FP_sched, scheduler𝗔𝗖_to_rt𝗔𝗖 in *; simpl in ×.
destruct (scheduler.min_completion_time).
{ destruct (A j) as [aj | ] eqn:Aj; last by done.
destruct s as [rt1 [COMP1 MIN1]].
have [LErt1|GTrt1] := leqP horizon rt1.
{ intros _.
destruct (scheduler.min_completion_time); last by done.
destruct s as [rt2 [COMP2 MIN2]].
destruct (horizon ≤ rt2) eqn:GTrt2 ⇒ //.
move: GTrt2 ⇒ /negP/negP; rewrite -ltnNge ⇒ GTrt2.
exfalso; unfold FP_FP_sched, scheduler𝗔𝗖_to_completed𝗔𝗖 in ×.
apply (MIN1 rt2); first by apply/leP; apply: leq_trans; [apply GTrt2 | apply LErt1].
by apply UNI; apply COMP2. }
{ rewrite //= ltn_subRL ⇒ LTrt1.
destruct (scheduler.min_completion_time); last by done.
destruct s as [rt2 [COMP2 MIN2]].
destruct (horizon ≤ rt2) eqn:GTrt2 ⇒ //.
rewrite //= ltn_subRL; move_neq_up GErt2; unfold FP_FP_sched, scheduler𝗔𝗖_to_completed𝗔𝗖 in ×.
apply (MIN1 rt2); first by apply/leP; apply: leq_ltn_trans; [apply GErt2 | apply LTrt1].
by apply UNI; apply COMP2. }
}
{ destruct (A j) as [aj | ] eqn:Aj; last by done.
intros _; destruct (scheduler.min_completion_time); last by done.
destruct s as [rt2 [COMP2 MIN2]].
exfalso; apply: (n rt2); unfold scheduler𝗔𝗖_to_completed𝗔𝗖 in ×.
by apply UNI, COMP2.
}
Qed.
End SchedulerProperties.