Library prosa.classic.model.schedule.global.jitter.constrained_deadlines
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.priority prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.schedule.global.jitter.job prosa.classic.model.schedule.global.jitter.schedule
prosa.classic.model.schedule.global.jitter.interference prosa.classic.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.
Variable arr_seq: arrival_sequence Job.
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.
Let job_is_pending := pending job_arrival job_cost job_jitter sched.
Let job_is_backlogged := backlogged job_arrival job_cost job_jitter sched.
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.
Section NoMultipleJobs.
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.
Variable ts: taskset_of sporadic_task.
Hypothesis H_all_jobs_from_taskset:
∀ j,
arrives_in arr_seq j →
job_task j \in ts.
Hypothesis H_sequential_jobs: sequential_jobs sched.
Hypothesis H_jobs_execute_after_jitter:
jobs_execute_after_jitter job_arrival job_jitter sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period job_arrival job_task arr_seq.
Variable tsk: sporadic_task.
Hypothesis H_valid_task: is_valid_sporadic_task task_cost task_period task_deadline tsk.
Variable j: Job.
Hypothesis H_j_arrives: arrives_in arr_seq j.
Hypothesis H_job_of_tsk: job_task j = tsk.
Variable t: time.
Hypothesis H_j_backlogged: job_is_backlogged j t.
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).
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.
Lemma platform_cpus_busy_with_interfering_tasks :
count (scheduled_task_other_than tsk) ts = num_cpus.
End NoMultipleJobs.
Section NoMultipleJobsFP.
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.
Variable ts: taskset_of sporadic_task.
Hypothesis H_all_jobs_from_taskset:
∀ j,
arrives_in arr_seq j →
job_task j \in ts.
Hypothesis H_sequential_jobs: sequential_jobs sched.
Hypothesis H_jobs_execute_after_jitter:
jobs_execute_after_jitter job_arrival job_jitter sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period job_arrival job_task arr_seq.
Variable tsk: sporadic_task.
Hypothesis H_valid_task: is_valid_sporadic_task task_cost task_period task_deadline tsk.
Variable j: Job.
Hypothesis H_j_arrives: arrives_in arr_seq j.
Hypothesis H_job_of_tsk: job_task j = 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.
Let is_hp_task := higher_priority_task higher_eq_priority tsk.
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).
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.
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.
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.
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 prosa.classic.model.arrival.basic.task prosa.classic.model.priority prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.schedule.global.jitter.job prosa.classic.model.schedule.global.jitter.schedule
prosa.classic.model.schedule.global.jitter.interference prosa.classic.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.
Variable arr_seq: arrival_sequence Job.
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.
Let job_is_pending := pending job_arrival job_cost job_jitter sched.
Let job_is_backlogged := backlogged job_arrival job_cost job_jitter sched.
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.
Section NoMultipleJobs.
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.
Variable ts: taskset_of sporadic_task.
Hypothesis H_all_jobs_from_taskset:
∀ j,
arrives_in arr_seq j →
job_task j \in ts.
Hypothesis H_sequential_jobs: sequential_jobs sched.
Hypothesis H_jobs_execute_after_jitter:
jobs_execute_after_jitter job_arrival job_jitter sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period job_arrival job_task arr_seq.
Variable tsk: sporadic_task.
Hypothesis H_valid_task: is_valid_sporadic_task task_cost task_period task_deadline tsk.
Variable j: Job.
Hypothesis H_j_arrives: arrives_in arr_seq j.
Hypothesis H_job_of_tsk: job_task j = tsk.
Variable t: time.
Hypothesis H_j_backlogged: job_is_backlogged j t.
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).
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.
Lemma platform_cpus_busy_with_interfering_tasks :
count (scheduled_task_other_than tsk) ts = num_cpus.
End NoMultipleJobs.
Section NoMultipleJobsFP.
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.
Variable ts: taskset_of sporadic_task.
Hypothesis H_all_jobs_from_taskset:
∀ j,
arrives_in arr_seq j →
job_task j \in ts.
Hypothesis H_sequential_jobs: sequential_jobs sched.
Hypothesis H_jobs_execute_after_jitter:
jobs_execute_after_jitter job_arrival job_jitter sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period job_arrival job_task arr_seq.
Variable tsk: sporadic_task.
Hypothesis H_valid_task: is_valid_sporadic_task task_cost task_period task_deadline tsk.
Variable j: Job.
Hypothesis H_j_arrives: arrives_in arr_seq j.
Hypothesis H_job_of_tsk: job_task j = 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.
Let is_hp_task := higher_priority_task higher_eq_priority tsk.
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).
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.
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.
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.
Lemma platform_fp_cpus_busy_with_interfering_tasks :
count scheduled_task_with_higher_eq_priority ts = num_cpus.
End NoMultipleJobsFP.
End Lemmas.
End ConstrainedDeadlines.