Library prosa.classic.model.schedule.uni.nonpreemptive.platform
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job prosa.classic.model.priority prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.schedule.uni.schedule
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.
Module NonpreemptivePlatform.
Import Job SporadicTaskset UniprocessorSchedule Priority.
(* In this section, we define properties of the processor platform. *)
Section Properties.
Context {sporadic_task: eqType}.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → sporadic_task.
(* Consider any job arrival sequence ...*)
Variable arr_seq: arrival_sequence Job.
(* ...and any uniprocessor schedule of these jobs. *)
Variable sched: schedule Job.
(* For simplicity, let's define some local names. *)
Let job_completed_by := completed_by job_cost sched.
Let job_scheduled_at := scheduled_at sched.
(* First, we define the notion of a preemption point. *)
Section PreemptionPoint.
(* We say that t is a preemption point iff (a) t is equal to 0
or (b) there is no scheduling job at time t or
(c) a job that was scheduled at time (t - 1) and
has completed by t exists. *)
Definition is_preemption_point' (t: time) :=
t = 0
∨ sched (t-1) = None
∨ ∃ j, scheduled_at sched j (t - 1) ∧ job_completed_by j t.
(* Moreover, we provide a shorter definition, more convenient for the proofs. *)
Definition is_preemption_point (t: time) :=
t = 0 ∨ ∀ j, job_scheduled_at j (t - 1) → job_completed_by j t.
(* Let's prove that the definitions above are equal. *)
Lemma defitions_of_preemption_point_are_equal:
∀ t, is_preemption_point t ↔ is_preemption_point' t.
Proof.
unfold is_preemption_point, is_preemption_point'.
intros; split; intros.
{
destruct H as [H | H]; [by left | right].
destruct (sched (t-1)) eqn:SCHED; [right; ∃ s | by left].
move: SCHED ⇒ /eqP SCHED.
by split; last by apply H in SCHED.
}
{
destruct H as [H | [H | H]]; [by left| | ]; right; intros.
unfold job_scheduled_at, scheduled_at in H0. rewrite H in H0. inversion H0.
inversion H as [j' [H1 H2]]. unfold job_scheduled_at in H0.
have EQ: j = j'. by apply (only_one_job_scheduled sched) with (t := t-1).
by subst j'.
}
Qed.
End PreemptionPoint.
(* Next, we define properties related to execution. *)
Section Execution.
(* We say that a scheduler is work-conserving iff whenever a job j
is backlogged, the processor is always busy with another job. *)
(* Imported from the preemptive schedule. *)
Definition work_conserving := Platform.work_conserving job_cost.
End Execution.
(* Next, we define properties related to FP scheduling. *)
Section FP.
(* We say that an FP policy...*)
Variable higher_eq_priority: FP_policy sporadic_task.
(* ...is respected by the schedule iff a scheduled task has
higher (or same) priority than (as) any backlogged task at
every preemption point. *)
Definition respects_FP_policy_at_preemption_point :=
∀ j j_hp t,
arrives_in arr_seq j →
backlogged job_arrival job_cost sched j t →
scheduled_at sched j_hp t →
is_preemption_point t →
higher_eq_priority (job_task j_hp) (job_task j).
End FP.
(* Next, we define properties related to JLFP policies. *)
Section JLFP.
(* We say that a JLFP policy ...*)
Variable higher_eq_priority: JLFP_policy Job.
(* ... is respected by the scheduler iff a scheduled job has
higher (or same) priority than (as) any backlogged job at
every preemption point. *)
Definition respects_JLFP_policy_at_preemption_point :=
∀ j j_hp t,
arrives_in arr_seq j →
backlogged job_arrival job_cost sched j t →
scheduled_at sched j_hp t →
is_preemption_point t →
higher_eq_priority j_hp j.
End JLFP.
End Properties.
End NonpreemptivePlatform.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job prosa.classic.model.priority prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.schedule.uni.schedule
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.
Module NonpreemptivePlatform.
Import Job SporadicTaskset UniprocessorSchedule Priority.
(* In this section, we define properties of the processor platform. *)
Section Properties.
Context {sporadic_task: eqType}.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → sporadic_task.
(* Consider any job arrival sequence ...*)
Variable arr_seq: arrival_sequence Job.
(* ...and any uniprocessor schedule of these jobs. *)
Variable sched: schedule Job.
(* For simplicity, let's define some local names. *)
Let job_completed_by := completed_by job_cost sched.
Let job_scheduled_at := scheduled_at sched.
(* First, we define the notion of a preemption point. *)
Section PreemptionPoint.
(* We say that t is a preemption point iff (a) t is equal to 0
or (b) there is no scheduling job at time t or
(c) a job that was scheduled at time (t - 1) and
has completed by t exists. *)
Definition is_preemption_point' (t: time) :=
t = 0
∨ sched (t-1) = None
∨ ∃ j, scheduled_at sched j (t - 1) ∧ job_completed_by j t.
(* Moreover, we provide a shorter definition, more convenient for the proofs. *)
Definition is_preemption_point (t: time) :=
t = 0 ∨ ∀ j, job_scheduled_at j (t - 1) → job_completed_by j t.
(* Let's prove that the definitions above are equal. *)
Lemma defitions_of_preemption_point_are_equal:
∀ t, is_preemption_point t ↔ is_preemption_point' t.
Proof.
unfold is_preemption_point, is_preemption_point'.
intros; split; intros.
{
destruct H as [H | H]; [by left | right].
destruct (sched (t-1)) eqn:SCHED; [right; ∃ s | by left].
move: SCHED ⇒ /eqP SCHED.
by split; last by apply H in SCHED.
}
{
destruct H as [H | [H | H]]; [by left| | ]; right; intros.
unfold job_scheduled_at, scheduled_at in H0. rewrite H in H0. inversion H0.
inversion H as [j' [H1 H2]]. unfold job_scheduled_at in H0.
have EQ: j = j'. by apply (only_one_job_scheduled sched) with (t := t-1).
by subst j'.
}
Qed.
End PreemptionPoint.
(* Next, we define properties related to execution. *)
Section Execution.
(* We say that a scheduler is work-conserving iff whenever a job j
is backlogged, the processor is always busy with another job. *)
(* Imported from the preemptive schedule. *)
Definition work_conserving := Platform.work_conserving job_cost.
End Execution.
(* Next, we define properties related to FP scheduling. *)
Section FP.
(* We say that an FP policy...*)
Variable higher_eq_priority: FP_policy sporadic_task.
(* ...is respected by the schedule iff a scheduled task has
higher (or same) priority than (as) any backlogged task at
every preemption point. *)
Definition respects_FP_policy_at_preemption_point :=
∀ j j_hp t,
arrives_in arr_seq j →
backlogged job_arrival job_cost sched j t →
scheduled_at sched j_hp t →
is_preemption_point t →
higher_eq_priority (job_task j_hp) (job_task j).
End FP.
(* Next, we define properties related to JLFP policies. *)
Section JLFP.
(* We say that a JLFP policy ...*)
Variable higher_eq_priority: JLFP_policy Job.
(* ... is respected by the scheduler iff a scheduled job has
higher (or same) priority than (as) any backlogged job at
every preemption point. *)
Definition respects_JLFP_policy_at_preemption_point :=
∀ j j_hp t,
arrives_in arr_seq j →
backlogged job_arrival job_cost sched j t →
scheduled_at sched j_hp t →
is_preemption_point t →
higher_eq_priority j_hp j.
End JLFP.
End Properties.
End NonpreemptivePlatform.