Library rt.model.schedule.global.jitter.constrained_deadlines
Require Import rt.util.all.
Require Import rt.model.arrival.basic.task rt.model.priority rt.model.arrival.basic.task_arrival.
Require Import rt.model.schedule.global.jitter.job rt.model.schedule.global.jitter.schedule
rt.model.schedule.global.jitter.interference rt.model.schedule.global.jitter.platform.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
Module ConstrainedDeadlines.
Import Job SporadicTaskset ScheduleOfSporadicTaskWithJitter SporadicTaskset
TaskArrival Interference Priority Platform.
Section Lemmas.
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_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → sporadic_task.
Variable job_jitter: Job → time.
(* Consider any job arrival sequence ... *)
Variable arr_seq: arrival_sequence Job.
(* ... and any schedule of this arrival sequence. *)
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
(* For simplicity, let's define some local names. *)
Let job_is_pending := pending job_arrival job_cost job_jitter sched.
Let job_is_backlogged := backlogged job_arrival job_cost job_jitter sched.
(* Next, assume all jobs have valid parameters. *)
Hypothesis H_valid_job_parameters:
∀ j,
arrives_in arr_seq j →
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
(* In this section we prove the absence of multiple jobs of the same
task when constrained deadlines are assumed. *)
Section NoMultipleJobs.
(* Assume any work-conserving priority-based scheduler. *)
Variable higher_eq_priority: JLDP_policy Job.
Hypothesis H_work_conserving:
work_conserving job_arrival job_cost job_jitter arr_seq sched.
Hypothesis H_respects_JLDP_policy:
respects_JLDP_policy job_arrival job_cost job_jitter arr_seq sched higher_eq_priority.
(* Consider task set ts. *)
Variable ts: taskset_of sporadic_task.
(* Assume that all jobs come from the taskset. *)
Hypothesis H_all_jobs_from_taskset:
∀ j,
arrives_in arr_seq j →
job_task j \in ts.
(* Suppose that jobs are sequential, ...*)
Hypothesis H_sequential_jobs: sequential_jobs sched.
(* ... jobs only execute after the jitter, ... *)
Hypothesis H_jobs_execute_after_jitter:
jobs_execute_after_jitter job_arrival job_jitter sched.
(* ... and jobs do not execute after completion. *)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Assume that the schedule satisfies the sporadic task model. *)
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period job_arrival job_task arr_seq.
(* Consider a valid task tsk, ...*)
Variable tsk: sporadic_task.
Hypothesis H_valid_task: is_valid_sporadic_task task_cost task_period task_deadline tsk.
(*... whose job j ... *)
Variable j: Job.
Hypothesis H_j_arrives: arrives_in arr_seq j.
Hypothesis H_job_of_tsk: job_task j = tsk.
(*... is backlogged at time t. *)
Variable t: time.
Hypothesis H_j_backlogged: job_is_backlogged j t.
(* Assume that any previous jobs of tsk have completed by the period. *)
Hypothesis H_all_previous_jobs_completed :
∀ j_other tsk_other,
arrives_in arr_seq j_other →
job_task j_other = tsk_other →
job_arrival j_other + task_period tsk_other ≤ t →
completed job_cost sched j_other (job_arrival j_other + task_period (job_task j_other)).
Let scheduled_task_other_than (tsk tsk_other: sporadic_task) :=
task_is_scheduled job_task sched tsk_other t && (tsk_other != tsk).
(* Then, there can be at most one pending job of each task at time t. *)
Lemma platform_at_most_one_pending_job_of_each_task :
∀ j1 j2,
arrives_in arr_seq j1 →
arrives_in arr_seq j2 →
job_is_pending j1 t →
job_is_pending j2 t →
job_task j1 = job_task j2 →
j1 = j2.
(* Therefore, all processors are busy with tasks other than tsk. *)
Lemma platform_cpus_busy_with_interfering_tasks :
count (scheduled_task_other_than tsk) ts = num_cpus.
End NoMultipleJobs.
(* In this section we also prove the absence of multiple jobs of the same
task when constrained deadlines are assumed, but in the specific case
of fixed-priority scheduling. *)
Section NoMultipleJobsFP.
(* Assume any work-conserving priority-based scheduler. *)
Variable higher_eq_priority: FP_policy sporadic_task.
Hypothesis H_work_conserving: work_conserving job_arrival job_cost job_jitter arr_seq sched.
Hypothesis H_respects_JLDP_policy:
respects_FP_policy job_arrival job_cost job_task job_jitter arr_seq sched higher_eq_priority.
(* Consider any task set ts. *)
Variable ts: taskset_of sporadic_task.
(* Assume that all jobs come from the taskset. *)
Hypothesis H_all_jobs_from_taskset:
∀ j,
arrives_in arr_seq j →
job_task j \in ts.
(* Suppose that jobs are sequential, ...*)
Hypothesis H_sequential_jobs: sequential_jobs sched.
(* ... jobs only execute after the jitter, ... *)
Hypothesis H_jobs_execute_after_jitter:
jobs_execute_after_jitter job_arrival job_jitter sched.
(* ... and jobs do not execute after completion. *)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Assume that the schedule satisfies the sporadic task model. *)
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period job_arrival job_task arr_seq.
(* Consider a valid task tsk, ...*)
Variable tsk: sporadic_task.
Hypothesis H_valid_task: is_valid_sporadic_task task_cost task_period task_deadline tsk.
(*... whose job j ... *)
Variable j: Job.
Hypothesis H_j_arrives: arrives_in arr_seq j.
Hypothesis H_job_of_tsk: job_task j = tsk.
(*... is backlogged at time t <= job_arrival j + task_period tsk. *)
Variable t: time.
Hypothesis H_j_backlogged: job_is_backlogged j t.
Hypothesis H_t_before_period: t < job_arrival j + task_period tsk.
(* Recall the definition of a higher-priority task (with respect to tsk). *)
Let is_hp_task := higher_priority_task higher_eq_priority tsk.
(* Assume that any jobs of higher-priority tasks complete by their period. *)
Hypothesis H_all_previous_jobs_completed :
∀ j_other tsk_other,
arrives_in arr_seq j_other →
job_task j_other = tsk_other →
is_hp_task tsk_other →
completed job_cost sched j_other (job_arrival j_other + task_period tsk_other).
(* Assume that any jobs of tsk prior to j complete by their period. *)
Hypothesis H_all_previous_jobs_of_tsk_completed :
∀ j0,
arrives_in arr_seq j0 →
job_task j0 = tsk →
job_arrival j0 < job_arrival j →
completed job_cost sched j0 (job_arrival j0 + task_period tsk).
Definition scheduled_task_with_higher_eq_priority (tsk_other: sporadic_task) :=
task_is_scheduled job_task sched tsk_other t &&
is_hp_task tsk_other.
(* Then, there can be at most one pending job of higher-priority tasks at time t. *)
Lemma platform_fp_no_multiple_jobs_of_interfering_tasks :
∀ j1 j2,
arrives_in arr_seq j1 →
arrives_in arr_seq j2 →
job_is_pending j1 t →
job_is_pending j2 t →
job_task j1 = job_task j2 →
is_hp_task (job_task j1) →
j1 = j2.
(* Also, there can be at most one pending job of tsk at time t. *)
Lemma platform_fp_no_multiple_jobs_of_tsk :
∀ j',
arrives_in arr_seq j' →
job_is_pending j' t →
job_task j' = tsk →
j' = j.
(* Therefore, all processors are busy with tasks other than tsk. *)
Lemma platform_fp_cpus_busy_with_interfering_tasks :
count scheduled_task_with_higher_eq_priority ts = num_cpus.
End NoMultipleJobsFP.
End Lemmas.
End ConstrainedDeadlines.
Require Import rt.model.arrival.basic.task rt.model.priority rt.model.arrival.basic.task_arrival.
Require Import rt.model.schedule.global.jitter.job rt.model.schedule.global.jitter.schedule
rt.model.schedule.global.jitter.interference rt.model.schedule.global.jitter.platform.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
Module ConstrainedDeadlines.
Import Job SporadicTaskset ScheduleOfSporadicTaskWithJitter SporadicTaskset
TaskArrival Interference Priority Platform.
Section Lemmas.
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_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → sporadic_task.
Variable job_jitter: Job → time.
(* Consider any job arrival sequence ... *)
Variable arr_seq: arrival_sequence Job.
(* ... and any schedule of this arrival sequence. *)
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
(* For simplicity, let's define some local names. *)
Let job_is_pending := pending job_arrival job_cost job_jitter sched.
Let job_is_backlogged := backlogged job_arrival job_cost job_jitter sched.
(* Next, assume all jobs have valid parameters. *)
Hypothesis H_valid_job_parameters:
∀ j,
arrives_in arr_seq j →
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
(* In this section we prove the absence of multiple jobs of the same
task when constrained deadlines are assumed. *)
Section NoMultipleJobs.
(* Assume any work-conserving priority-based scheduler. *)
Variable higher_eq_priority: JLDP_policy Job.
Hypothesis H_work_conserving:
work_conserving job_arrival job_cost job_jitter arr_seq sched.
Hypothesis H_respects_JLDP_policy:
respects_JLDP_policy job_arrival job_cost job_jitter arr_seq sched higher_eq_priority.
(* Consider task set ts. *)
Variable ts: taskset_of sporadic_task.
(* Assume that all jobs come from the taskset. *)
Hypothesis H_all_jobs_from_taskset:
∀ j,
arrives_in arr_seq j →
job_task j \in ts.
(* Suppose that jobs are sequential, ...*)
Hypothesis H_sequential_jobs: sequential_jobs sched.
(* ... jobs only execute after the jitter, ... *)
Hypothesis H_jobs_execute_after_jitter:
jobs_execute_after_jitter job_arrival job_jitter sched.
(* ... and jobs do not execute after completion. *)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Assume that the schedule satisfies the sporadic task model. *)
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period job_arrival job_task arr_seq.
(* Consider a valid task tsk, ...*)
Variable tsk: sporadic_task.
Hypothesis H_valid_task: is_valid_sporadic_task task_cost task_period task_deadline tsk.
(*... whose job j ... *)
Variable j: Job.
Hypothesis H_j_arrives: arrives_in arr_seq j.
Hypothesis H_job_of_tsk: job_task j = tsk.
(*... is backlogged at time t. *)
Variable t: time.
Hypothesis H_j_backlogged: job_is_backlogged j t.
(* Assume that any previous jobs of tsk have completed by the period. *)
Hypothesis H_all_previous_jobs_completed :
∀ j_other tsk_other,
arrives_in arr_seq j_other →
job_task j_other = tsk_other →
job_arrival j_other + task_period tsk_other ≤ t →
completed job_cost sched j_other (job_arrival j_other + task_period (job_task j_other)).
Let scheduled_task_other_than (tsk tsk_other: sporadic_task) :=
task_is_scheduled job_task sched tsk_other t && (tsk_other != tsk).
(* Then, there can be at most one pending job of each task at time t. *)
Lemma platform_at_most_one_pending_job_of_each_task :
∀ j1 j2,
arrives_in arr_seq j1 →
arrives_in arr_seq j2 →
job_is_pending j1 t →
job_is_pending j2 t →
job_task j1 = job_task j2 →
j1 = j2.
(* Therefore, all processors are busy with tasks other than tsk. *)
Lemma platform_cpus_busy_with_interfering_tasks :
count (scheduled_task_other_than tsk) ts = num_cpus.
End NoMultipleJobs.
(* In this section we also prove the absence of multiple jobs of the same
task when constrained deadlines are assumed, but in the specific case
of fixed-priority scheduling. *)
Section NoMultipleJobsFP.
(* Assume any work-conserving priority-based scheduler. *)
Variable higher_eq_priority: FP_policy sporadic_task.
Hypothesis H_work_conserving: work_conserving job_arrival job_cost job_jitter arr_seq sched.
Hypothesis H_respects_JLDP_policy:
respects_FP_policy job_arrival job_cost job_task job_jitter arr_seq sched higher_eq_priority.
(* Consider any task set ts. *)
Variable ts: taskset_of sporadic_task.
(* Assume that all jobs come from the taskset. *)
Hypothesis H_all_jobs_from_taskset:
∀ j,
arrives_in arr_seq j →
job_task j \in ts.
(* Suppose that jobs are sequential, ...*)
Hypothesis H_sequential_jobs: sequential_jobs sched.
(* ... jobs only execute after the jitter, ... *)
Hypothesis H_jobs_execute_after_jitter:
jobs_execute_after_jitter job_arrival job_jitter sched.
(* ... and jobs do not execute after completion. *)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Assume that the schedule satisfies the sporadic task model. *)
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period job_arrival job_task arr_seq.
(* Consider a valid task tsk, ...*)
Variable tsk: sporadic_task.
Hypothesis H_valid_task: is_valid_sporadic_task task_cost task_period task_deadline tsk.
(*... whose job j ... *)
Variable j: Job.
Hypothesis H_j_arrives: arrives_in arr_seq j.
Hypothesis H_job_of_tsk: job_task j = tsk.
(*... is backlogged at time t <= job_arrival j + task_period tsk. *)
Variable t: time.
Hypothesis H_j_backlogged: job_is_backlogged j t.
Hypothesis H_t_before_period: t < job_arrival j + task_period tsk.
(* Recall the definition of a higher-priority task (with respect to tsk). *)
Let is_hp_task := higher_priority_task higher_eq_priority tsk.
(* Assume that any jobs of higher-priority tasks complete by their period. *)
Hypothesis H_all_previous_jobs_completed :
∀ j_other tsk_other,
arrives_in arr_seq j_other →
job_task j_other = tsk_other →
is_hp_task tsk_other →
completed job_cost sched j_other (job_arrival j_other + task_period tsk_other).
(* Assume that any jobs of tsk prior to j complete by their period. *)
Hypothesis H_all_previous_jobs_of_tsk_completed :
∀ j0,
arrives_in arr_seq j0 →
job_task j0 = tsk →
job_arrival j0 < job_arrival j →
completed job_cost sched j0 (job_arrival j0 + task_period tsk).
Definition scheduled_task_with_higher_eq_priority (tsk_other: sporadic_task) :=
task_is_scheduled job_task sched tsk_other t &&
is_hp_task tsk_other.
(* Then, there can be at most one pending job of higher-priority tasks at time t. *)
Lemma platform_fp_no_multiple_jobs_of_interfering_tasks :
∀ j1 j2,
arrives_in arr_seq j1 →
arrives_in arr_seq j2 →
job_is_pending j1 t →
job_is_pending j2 t →
job_task j1 = job_task j2 →
is_hp_task (job_task j1) →
j1 = j2.
(* Also, there can be at most one pending job of tsk at time t. *)
Lemma platform_fp_no_multiple_jobs_of_tsk :
∀ j',
arrives_in arr_seq j' →
job_is_pending j' t →
job_task j' = tsk →
j' = j.
(* Therefore, all processors are busy with tasks other than tsk. *)
Lemma platform_fp_cpus_busy_with_interfering_tasks :
count scheduled_task_with_higher_eq_priority ts = num_cpus.
End NoMultipleJobsFP.
End Lemmas.
End ConstrainedDeadlines.