Library prosa.classic.model.schedule.uni.limited.platform.definitions
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.job
prosa.classic.model.arrival.basic.task
prosa.classic.model.priority
prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.schedule.uni.schedule
prosa.classic.model.schedule.uni.service
prosa.classic.model.schedule.uni.basic.platform.
Require Import prosa.classic.model.schedule.uni.nonpreemptive.schedule.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
Require Import prosa.classic.model.arrival.basic.job
prosa.classic.model.arrival.basic.task
prosa.classic.model.priority
prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.schedule.uni.schedule
prosa.classic.model.schedule.uni.service
prosa.classic.model.schedule.uni.basic.platform.
Require Import prosa.classic.model.schedule.uni.nonpreemptive.schedule.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
Platform with limited preemptions
In this module we introduce the notion of whether a job can be preempted at a given time (using a predicate can_be_preempted). In addition, we provide instantiations of the predicate for various preemption models.
Module LimitedPreemptionPlatform.
Import Job SporadicTaskset UniprocessorSchedule Priority Service.
Section Properties.
Context {Task: eqType}.
Variable task_cost: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → Task.
Variable arr_seq: arrival_sequence Job.
Variable sched: schedule Job.
Let job_pending := pending job_arrival job_cost sched.
Let job_completed_by := completed_by job_cost sched.
Let job_scheduled_at := scheduled_at sched.
Section PreemptionTime.
Variable can_be_preempted: Job → time → bool.
Definition preemption_time (t: time) :=
if sched t is Some j then
can_be_preempted j (service sched j t)
else true.
Section CorrectPreemptionModel.
Definition not_preemptive_implies_scheduled (j: Job) :=
∀ t,
~~ can_be_preempted j (service sched j t) →
job_scheduled_at j t.
Definition execution_starts_with_preemption_point (j: Job) :=
∀ prt,
~~ job_scheduled_at j prt →
job_scheduled_at j prt.+1 →
can_be_preempted j (service sched j prt.+1).
Definition correct_preemption_model :=
∀ j,
arrives_in arr_seq j →
not_preemptive_implies_scheduled j
∧ execution_starts_with_preemption_point j.
End CorrectPreemptionModel.
Section ModelWithBoundedNonpreemptiveRegions.
Definition job_cannot_become_nonpreemptive_before_execution (j: Job) :=
can_be_preempted j 0.
Definition job_cannot_be_nonpreemptive_after_completion (j: Job) :=
can_be_preempted j (job_cost j).
Variable job_max_nps: Job → time.
Variable task_max_nps: Task → time.
Definition job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment (j: Job) :=
arrives_in arr_seq j →
job_max_nps j ≤ task_max_nps (job_task j).
Definition nonpreemptive_regions_have_bounded_length (j: Job) :=
∀ progr,
0 ≤ progr ≤ job_cost j →
∃ preemption_point,
progr ≤ preemption_point ≤ progr + (job_max_nps j - ε) ∧
can_be_preempted j preemption_point.
Definition model_with_bounded_nonpreemptive_segments :=
∀ j,
arrives_in arr_seq j →
job_cannot_become_nonpreemptive_before_execution j
∧ job_cannot_be_nonpreemptive_after_completion j
∧ job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j
∧ nonpreemptive_regions_have_bounded_length j.
End ModelWithBoundedNonpreemptiveRegions.
Section Lemmas.
Variable job_max_nps: Job → time.
Variable task_max_nps: Task → time.
Hypothesis H_correct_preemption_model: correct_preemption_model.
Hypothesis H_model_with_bounded_np_segments:
model_with_bounded_nonpreemptive_segments job_max_nps task_max_nps.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
Lemma zero_is_pt: preemption_time 0.
Proof.
unfold preemption_time.
case SCHED: (sched 0) ⇒ [j | ]; last by done.
move: (SCHED) ⇒ /eqP ARR.
apply H_jobs_come_from_arrival_sequence in ARR.
rewrite /service /service_during big_geq; last by done.
by move: (H_model_with_bounded_np_segments j ARR) ⇒ [PP _]; apply PP.
Qed.
Lemma first_moment_is_pt:
∀ j prt,
arrives_in arr_seq j →
~~ job_scheduled_at j prt →
job_scheduled_at j prt.+1 →
preemption_time prt.+1.
Proof.
intros s pt ARR NSCHED SCHED.
unfold preemption_time.
move: (SCHED) ⇒ /eqP SCHED2; rewrite SCHED2; clear SCHED2.
by move: (H_correct_preemption_model s ARR) ⇒ [_ FHF]; auto.
Qed.
End Lemmas.
End PreemptionTime.
Section Execution.
Definition work_conserving := Platform.work_conserving job_cost.
End Execution.
Section FP.
Variable preemption_model: Job → time → bool.
Variable higher_eq_priority: FP_policy Task.
Definition respects_FP_policy_at_preemption_point :=
∀ j j_hp t,
preemption_time preemption_model t →
arrives_in arr_seq j →
backlogged job_arrival job_cost sched j t →
scheduled_at sched j_hp t →
higher_eq_priority (job_task j_hp) (job_task j).
End FP.
Section JLFP.
Variable preemption_model: Job → time → bool.
Variable higher_eq_priority: JLFP_policy Job.
Definition respects_JLFP_policy_at_preemption_point :=
∀ j j_hp t,
preemption_time preemption_model t →
arrives_in arr_seq j →
backlogged job_arrival job_cost sched j t →
scheduled_at sched j_hp t →
higher_eq_priority j_hp j.
End JLFP.
End Properties.
End LimitedPreemptionPlatform.
Import Job SporadicTaskset UniprocessorSchedule Priority Service.
Section Properties.
Context {Task: eqType}.
Variable task_cost: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → Task.
Variable arr_seq: arrival_sequence Job.
Variable sched: schedule Job.
Let job_pending := pending job_arrival job_cost sched.
Let job_completed_by := completed_by job_cost sched.
Let job_scheduled_at := scheduled_at sched.
Section PreemptionTime.
Variable can_be_preempted: Job → time → bool.
Definition preemption_time (t: time) :=
if sched t is Some j then
can_be_preempted j (service sched j t)
else true.
Section CorrectPreemptionModel.
Definition not_preemptive_implies_scheduled (j: Job) :=
∀ t,
~~ can_be_preempted j (service sched j t) →
job_scheduled_at j t.
Definition execution_starts_with_preemption_point (j: Job) :=
∀ prt,
~~ job_scheduled_at j prt →
job_scheduled_at j prt.+1 →
can_be_preempted j (service sched j prt.+1).
Definition correct_preemption_model :=
∀ j,
arrives_in arr_seq j →
not_preemptive_implies_scheduled j
∧ execution_starts_with_preemption_point j.
End CorrectPreemptionModel.
Section ModelWithBoundedNonpreemptiveRegions.
Definition job_cannot_become_nonpreemptive_before_execution (j: Job) :=
can_be_preempted j 0.
Definition job_cannot_be_nonpreemptive_after_completion (j: Job) :=
can_be_preempted j (job_cost j).
Variable job_max_nps: Job → time.
Variable task_max_nps: Task → time.
Definition job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment (j: Job) :=
arrives_in arr_seq j →
job_max_nps j ≤ task_max_nps (job_task j).
Definition nonpreemptive_regions_have_bounded_length (j: Job) :=
∀ progr,
0 ≤ progr ≤ job_cost j →
∃ preemption_point,
progr ≤ preemption_point ≤ progr + (job_max_nps j - ε) ∧
can_be_preempted j preemption_point.
Definition model_with_bounded_nonpreemptive_segments :=
∀ j,
arrives_in arr_seq j →
job_cannot_become_nonpreemptive_before_execution j
∧ job_cannot_be_nonpreemptive_after_completion j
∧ job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j
∧ nonpreemptive_regions_have_bounded_length j.
End ModelWithBoundedNonpreemptiveRegions.
Section Lemmas.
Variable job_max_nps: Job → time.
Variable task_max_nps: Task → time.
Hypothesis H_correct_preemption_model: correct_preemption_model.
Hypothesis H_model_with_bounded_np_segments:
model_with_bounded_nonpreemptive_segments job_max_nps task_max_nps.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
Lemma zero_is_pt: preemption_time 0.
Proof.
unfold preemption_time.
case SCHED: (sched 0) ⇒ [j | ]; last by done.
move: (SCHED) ⇒ /eqP ARR.
apply H_jobs_come_from_arrival_sequence in ARR.
rewrite /service /service_during big_geq; last by done.
by move: (H_model_with_bounded_np_segments j ARR) ⇒ [PP _]; apply PP.
Qed.
Lemma first_moment_is_pt:
∀ j prt,
arrives_in arr_seq j →
~~ job_scheduled_at j prt →
job_scheduled_at j prt.+1 →
preemption_time prt.+1.
Proof.
intros s pt ARR NSCHED SCHED.
unfold preemption_time.
move: (SCHED) ⇒ /eqP SCHED2; rewrite SCHED2; clear SCHED2.
by move: (H_correct_preemption_model s ARR) ⇒ [_ FHF]; auto.
Qed.
End Lemmas.
End PreemptionTime.
Section Execution.
Definition work_conserving := Platform.work_conserving job_cost.
End Execution.
Section FP.
Variable preemption_model: Job → time → bool.
Variable higher_eq_priority: FP_policy Task.
Definition respects_FP_policy_at_preemption_point :=
∀ j j_hp t,
preemption_time preemption_model t →
arrives_in arr_seq j →
backlogged job_arrival job_cost sched j t →
scheduled_at sched j_hp t →
higher_eq_priority (job_task j_hp) (job_task j).
End FP.
Section JLFP.
Variable preemption_model: Job → time → bool.
Variable higher_eq_priority: JLFP_policy Job.
Definition respects_JLFP_policy_at_preemption_point :=
∀ j j_hp t,
preemption_time preemption_model t →
arrives_in arr_seq j →
backlogged job_arrival job_cost sched j t →
scheduled_at sched j_hp t →
higher_eq_priority j_hp j.
End JLFP.
End Properties.
End LimitedPreemptionPlatform.