Library rt.model.basic.constrained_deadlines
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
rt.model.basic.priority rt.model.basic.task_arrival
rt.model.basic.interference rt.model.basic.platform.
Module ConstrainedDeadlines.
Import Job SporadicTaskset ScheduleOfSporadicTask SporadicTaskset
SporadicTaskArrival 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_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → sporadic_task.
(* Assume any job arrival sequence ... *)
Context {arr_seq: arrival_sequence Job}.
(* ... and any schedule of this arrival sequence. *)
Context {num_cpus: nat}.
Variable sched: schedule num_cpus arr_seq.
(* 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 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 arr_seq.
Hypothesis H_work_conserving: work_conserving job_cost sched.
Hypothesis H_enforces_JLDP_policy:
enforces_JLDP_policy job_cost 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: JobIn arr_seq), job_task j ∈ ts.
(* Suppose that jobs are sequential, ...*)
Hypothesis H_sequential_jobs: sequential_jobs sched.
(* ... jobs must arrive to execute, ... *)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* ... and jobs do not execute after completion. *)
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute sched.
(* Assume that the schedule satisfies the sporadic task model ...*)
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period arr_seq job_task.
(* 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: JobIn arr_seq.
Variable H_job_of_tsk: job_task j = tsk.
(*... is backlogged at time t. *)
Variable t: time.
Hypothesis H_j_backlogged: backlogged job_cost sched j t.
(* Assume that any previous jobs of tsk have completed by the period. *)
Hypothesis H_all_previous_jobs_completed :
∀ (j_other: JobIn arr_seq) tsk_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,
pending job_cost sched j1 t →
pending job_cost sched 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_cost sched.
Hypothesis H_enforces_JLDP_policy:
enforces_FP_policy job_cost job_task 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: JobIn arr_seq), job_task j ∈ ts.
(* Suppose that jobs are sequential, ...*)
Hypothesis H_sequential_jobs: sequential_jobs sched.
(* ... jobs must arrive to execute, ... *)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* ... and jobs do not execute after completion. *)
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute sched.
(* Assume that jobs arrive sporadically. *)
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period arr_seq job_task.
(* 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: JobIn arr_seq.
Variable 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: backlogged job_cost sched 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: JobIn arr_seq) tsk_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 : JobIn arr_seq,
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 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,
pending job_cost sched j1 t →
pending job_cost sched 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',
pending job_cost sched 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 tsk) ts = num_cpus.
End NoMultipleJobsFP.
End Lemmas.
End ConstrainedDeadlines.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
rt.model.basic.priority rt.model.basic.task_arrival
rt.model.basic.interference rt.model.basic.platform.
Module ConstrainedDeadlines.
Import Job SporadicTaskset ScheduleOfSporadicTask SporadicTaskset
SporadicTaskArrival 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_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → sporadic_task.
(* Assume any job arrival sequence ... *)
Context {arr_seq: arrival_sequence Job}.
(* ... and any schedule of this arrival sequence. *)
Context {num_cpus: nat}.
Variable sched: schedule num_cpus arr_seq.
(* 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 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 arr_seq.
Hypothesis H_work_conserving: work_conserving job_cost sched.
Hypothesis H_enforces_JLDP_policy:
enforces_JLDP_policy job_cost 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: JobIn arr_seq), job_task j ∈ ts.
(* Suppose that jobs are sequential, ...*)
Hypothesis H_sequential_jobs: sequential_jobs sched.
(* ... jobs must arrive to execute, ... *)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* ... and jobs do not execute after completion. *)
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute sched.
(* Assume that the schedule satisfies the sporadic task model ...*)
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period arr_seq job_task.
(* 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: JobIn arr_seq.
Variable H_job_of_tsk: job_task j = tsk.
(*... is backlogged at time t. *)
Variable t: time.
Hypothesis H_j_backlogged: backlogged job_cost sched j t.
(* Assume that any previous jobs of tsk have completed by the period. *)
Hypothesis H_all_previous_jobs_completed :
∀ (j_other: JobIn arr_seq) tsk_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,
pending job_cost sched j1 t →
pending job_cost sched 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_cost sched.
Hypothesis H_enforces_JLDP_policy:
enforces_FP_policy job_cost job_task 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: JobIn arr_seq), job_task j ∈ ts.
(* Suppose that jobs are sequential, ...*)
Hypothesis H_sequential_jobs: sequential_jobs sched.
(* ... jobs must arrive to execute, ... *)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* ... and jobs do not execute after completion. *)
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute sched.
(* Assume that jobs arrive sporadically. *)
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period arr_seq job_task.
(* 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: JobIn arr_seq.
Variable 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: backlogged job_cost sched 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: JobIn arr_seq) tsk_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 : JobIn arr_seq,
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 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,
pending job_cost sched j1 t →
pending job_cost sched 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',
pending job_cost sched 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 tsk) ts = num_cpus.
End NoMultipleJobsFP.
End Lemmas.
End ConstrainedDeadlines.