Library rt.model.jitter.platform
Require Import rt.util.all.
Require Import rt.model.jitter.task rt.model.jitter.job rt.model.jitter.schedule
rt.model.jitter.priority rt.model.jitter.task_arrival rt.model.jitter.interference.
Module Platform.
Import Job SporadicTaskset ScheduleOfSporadicTaskWithJitter SporadicTaskset SporadicTaskArrival Interference Priority.
Section Properties.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Context {Job: eqType}.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → sporadic_task.
Variable job_jitter: Job → time.
(* Assume any job arrival sequence... *)
Context {arr_seq: arrival_sequence Job}.
(* Consider any schedule. *)
Context {num_cpus: nat}.
Variable sched: schedule num_cpus arr_seq.
Section Execution.
(* A scheduler is work-conserving iff when a job j is backlogged,
all processors are busy with other jobs.
Note: backlogged means that jitter has already passed. *)
Definition work_conserving :=
∀ j t,
backlogged job_cost job_jitter sched j t →
∀ cpu, ∃ j_other,
scheduled_on sched j_other cpu t.
(* We also provide an alternative, equivalent definition of work-conserving
based on counting the number of scheduled jobs. *)
Definition work_conserving_count :=
∀ j t,
backlogged job_cost job_jitter sched j t →
size (jobs_scheduled_at sched t) = num_cpus.
End Execution.
Section JLDP.
(* A JLFP/JLDP policy ...*)
Variable higher_eq_priority: JLDP_policy arr_seq.
(* ... is enforced by the scheduler iff at any time t,
a scheduled job has higher (or same) priority than (as)
a backlogged job. *)
Definition enforces_JLDP_policy :=
∀ (j j_hp: JobIn arr_seq) t,
backlogged job_cost job_jitter sched j t →
scheduled sched j_hp t →
higher_eq_priority t j_hp j.
End JLDP.
Section FP.
(* Given an FP policy, ...*)
Variable higher_eq_priority: FP_policy sporadic_task.
(* ... this policy is enforced by the scheduler iff
a corresponding JLDP policy is enforced by the scheduler. *)
Definition enforces_FP_policy :=
enforces_JLDP_policy (FP_to_JLDP job_task higher_eq_priority).
End FP.
Section Lemmas.
(* Assume all jobs have valid parameters, ...*)
Hypothesis H_valid_job_parameters:
∀ (j: JobIn arr_seq),
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
(* In this section, we prove that the two definitions of work-conserving are equivalent. *)
Section EquivalentDefinitions.
Lemma work_conserving_eq_work_conserving_count :
work_conserving ↔ work_conserving_count.
End EquivalentDefinitions.
End Lemmas.
End Properties.
End Platform.
Require Import rt.model.jitter.task rt.model.jitter.job rt.model.jitter.schedule
rt.model.jitter.priority rt.model.jitter.task_arrival rt.model.jitter.interference.
Module Platform.
Import Job SporadicTaskset ScheduleOfSporadicTaskWithJitter SporadicTaskset SporadicTaskArrival Interference Priority.
Section Properties.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Context {Job: eqType}.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → sporadic_task.
Variable job_jitter: Job → time.
(* Assume any job arrival sequence... *)
Context {arr_seq: arrival_sequence Job}.
(* Consider any schedule. *)
Context {num_cpus: nat}.
Variable sched: schedule num_cpus arr_seq.
Section Execution.
(* A scheduler is work-conserving iff when a job j is backlogged,
all processors are busy with other jobs.
Note: backlogged means that jitter has already passed. *)
Definition work_conserving :=
∀ j t,
backlogged job_cost job_jitter sched j t →
∀ cpu, ∃ j_other,
scheduled_on sched j_other cpu t.
(* We also provide an alternative, equivalent definition of work-conserving
based on counting the number of scheduled jobs. *)
Definition work_conserving_count :=
∀ j t,
backlogged job_cost job_jitter sched j t →
size (jobs_scheduled_at sched t) = num_cpus.
End Execution.
Section JLDP.
(* A JLFP/JLDP policy ...*)
Variable higher_eq_priority: JLDP_policy arr_seq.
(* ... is enforced by the scheduler iff at any time t,
a scheduled job has higher (or same) priority than (as)
a backlogged job. *)
Definition enforces_JLDP_policy :=
∀ (j j_hp: JobIn arr_seq) t,
backlogged job_cost job_jitter sched j t →
scheduled sched j_hp t →
higher_eq_priority t j_hp j.
End JLDP.
Section FP.
(* Given an FP policy, ...*)
Variable higher_eq_priority: FP_policy sporadic_task.
(* ... this policy is enforced by the scheduler iff
a corresponding JLDP policy is enforced by the scheduler. *)
Definition enforces_FP_policy :=
enforces_JLDP_policy (FP_to_JLDP job_task higher_eq_priority).
End FP.
Section Lemmas.
(* Assume all jobs have valid parameters, ...*)
Hypothesis H_valid_job_parameters:
∀ (j: JobIn arr_seq),
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
(* In this section, we prove that the two definitions of work-conserving are equivalent. *)
Section EquivalentDefinitions.
Lemma work_conserving_eq_work_conserving_count :
work_conserving ↔ work_conserving_count.
End EquivalentDefinitions.
End Lemmas.
End Properties.
End Platform.