Built with
Alectryon , running Coq+SerAPI v8.20.0+0.20.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.model.priority.edf.[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] [Loading ML file ring_plugin.cmxs (using legacy method) ... done ] Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted. [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ] Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.model.task.absolute_deadline.
Require Export prosa.analysis.definitions.workload.bounded.
Require Export prosa.analysis.facts.model.workload.
Require Export prosa.analysis.definitions.workload.edf_athep_bound.
(** * Bound on Higher-or-Equal Priority Workload under EDF Scheduling is Valid *)
(** In this file, we prove that the upper bound on interference
incurred by a job from jobs with higher-or-equal priority that
come from other tasks under EDF scheduling (defined in
[prosa.analysis.definitions.workload.edf_athep_bound]) is
valid. *)
Section ATHEPWorkloadBoundIsValidForEDF .
(** Consider any type of tasks, each characterized by a WCET
[task_cost], a relative deadline [task_deadline], and an arrival
curve [max_arrivals], ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
Context `{TaskDeadline Task}.
Context `{MaxArrivals Task}.
(** ... and any type of jobs associated with these tasks, where each
job has a task [job_task], a cost [job_cost], and an arrival
time [job_arrival]. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Consider any kind of processor model. *)
Context `{PState : ProcessorState Job}.
(** For brevity, let's denote the relative deadline of a task as [D]. *)
Let D tsk := task_deadline tsk.
(** Consider any valid arrival sequence [arr_seq] ... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** ... with valid job costs. *)
Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
(** We consider an arbitrary task set [ts] ... *)
Variable ts : seq Task.
(** ... and assume that all jobs stem from tasks in this task set. *)
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
(** We assume that [max_arrivals] is a family of valid arrival
curves that constrains the arrival sequence [arr_seq], i.e., for
any task [tsk] in [ts], [max_arrival tsk] is an arrival bound of
[tsk]. *)
Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
(** Let [tsk] be any task to be analyzed. *)
Variable tsk : Task.
(** Consider any schedule. *)
Variable sched : schedule PState.
(** Before we prove the main result, we establish some auxiliary lemmas. *)
Section HepWorkloadBound .
(** Consider an arbitrary job [j] of [tsk]. *)
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_of_task tsk j.
Hypothesis H_job_cost_positive : job_cost_positive j.
(** Consider the busy interval <<[t1, t2)>> of job [j]. *)
Variable t1 t2 : duration.
Hypothesis H_busy_interval : busy_interval arr_seq sched j t1 t2.
(** Let's define [A] as a relative arrival time of job [j] (with
respect to time [t1]). *)
Let A := job_arrival j - t1.
(** Consider an arbitrary shift [Δ] inside the busy interval ... *)
Variable Δ : duration.
Hypothesis H_Δ_in_busy : t1 + Δ < t2.
(** ... and the set of all arrivals between [t1] and [t1 + Δ]. *)
Let jobs := arrivals_between arr_seq t1 (t1 + Δ).
(** We define a predicate [EDF_from tsk]. Predicate [EDF_from tsk]
holds true for any job [jo] of task [tsk] such that
[job_deadline jo <= job_deadline j]. *)
Let EDF_from (tsk : Task) (jo : Job) := EDF Job jo j && (job_task jo == tsk).
(** Now, consider the case where [A + ε + D tsk - D tsk_o ≤ Δ]. *)
Section ShortenRange .
(** Consider an arbitrary task [tsk_o ≠ tsk] from [ts]. *)
Variable tsk_o : Task.
Hypothesis H_tsko_in_ts : tsk_o \in ts.
Hypothesis H_neq : tsk_o != tsk.
(** And assume that [A + ε + D tsk - D tsk_o ≤ Δ]. *)
Hypothesis H_Δ_ge : A + ε + D tsk - D tsk_o <= Δ.
(** Then we prove that the total workload of jobs with
higher-or-equal priority from task [tsk_o] over the interval
[[t1, t1 + Δ]] is bounded by workload over the interval
[[t1, t1 + A + ε + D tsk - D tsk_o]]. The intuition behind
this inequality is that jobs that arrive after time instant
[t1 + A + ε + D tsk - D tsk_o] have lower priority than job
[j] due to the term [D tsk - D tsk_o]. *)
Lemma total_workload_shorten_range :
workload_of_jobs (EDF_from tsk_o) (arrivals_between arr_seq t1 (t1 + Δ))
<= workload_of_jobs (EDF_from tsk_o) (arrivals_between arr_seq t1 (t1 + (A + ε + D tsk - D tsk_o))).Task : TaskType H : TaskCost Task H0 : TaskDeadline Task H1 : MaxArrivals Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job D := [eta task_deadline] : Task -> duration arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat Δ : duration H_Δ_in_busy : t1 + Δ < t2 jobs := arrivals_between arr_seq t1 (t1 + Δ) : seq Job EDF_from := fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool tsk_o : Task H_tsko_in_ts : tsk_o \in ts H_neq : tsk_o != tsk H_Δ_ge : A + 1 + D tsk - D tsk_o <= Δ
workload_of_jobs (EDF_from tsk_o)
(arrivals_between arr_seq t1 (t1 + Δ)) <=
workload_of_jobs (EDF_from tsk_o)
(arrivals_between arr_seq t1
(t1 + (A + 1 + D tsk - D tsk_o)))
Proof .Task : TaskType H : TaskCost Task H0 : TaskDeadline Task H1 : MaxArrivals Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job D := [eta task_deadline] : Task -> duration arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat Δ : duration H_Δ_in_busy : t1 + Δ < t2 jobs := arrivals_between arr_seq t1 (t1 + Δ) : seq Job EDF_from := fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool tsk_o : Task H_tsko_in_ts : tsk_o \in ts H_neq : tsk_o != tsk H_Δ_ge : A + 1 + D tsk - D tsk_o <= Δ
workload_of_jobs (EDF_from tsk_o)
(arrivals_between arr_seq t1 (t1 + Δ)) <=
workload_of_jobs (EDF_from tsk_o)
(arrivals_between arr_seq t1
(t1 + (A + 1 + D tsk - D tsk_o)))
have BOUNDED: t1 + (A + ε + D tsk - D tsk_o) <= t1 + Δ by lia .Task : TaskType H : TaskCost Task H0 : TaskDeadline Task H1 : MaxArrivals Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job D := [eta task_deadline] : Task -> duration arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat Δ : duration H_Δ_in_busy : t1 + Δ < t2 jobs := arrivals_between arr_seq t1 (t1 + Δ) : seq Job EDF_from := fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool tsk_o : Task H_tsko_in_ts : tsk_o \in ts H_neq : tsk_o != tsk H_Δ_ge : A + 1 + D tsk - D tsk_o <= Δ BOUNDED : t1 + (A + 1 + D tsk - D tsk_o) <= t1 + Δ
workload_of_jobs (EDF_from tsk_o)
(arrivals_between arr_seq t1 (t1 + Δ)) <=
workload_of_jobs (EDF_from tsk_o)
(arrivals_between arr_seq t1
(t1 + (A + 1 + D tsk - D tsk_o)))
rewrite (workload_of_jobs_nil_tail _ _ BOUNDED) // => j' IN'.Task : TaskType H : TaskCost Task H0 : TaskDeadline Task H1 : MaxArrivals Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job D := [eta task_deadline] : Task -> duration arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat Δ : duration H_Δ_in_busy : t1 + Δ < t2 jobs := arrivals_between arr_seq t1 (t1 + Δ) : seq Job EDF_from := fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool tsk_o : Task H_tsko_in_ts : tsk_o \in ts H_neq : tsk_o != tsk H_Δ_ge : A + 1 + D tsk - D tsk_o <= Δ BOUNDED : t1 + (A + 1 + D tsk - D tsk_o) <= t1 + Δ j' : Job IN' : j' \in arrivals_between arr_seq t1 (t1 + Δ)
t1 + (A + 1 + D tsk - D tsk_o) <= job_arrival j' ->
~~ EDF_from tsk_o j'
rewrite /EDF_from => ARR'.Task : TaskType H : TaskCost Task H0 : TaskDeadline Task H1 : MaxArrivals Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job D := [eta task_deadline] : Task -> duration arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat Δ : duration H_Δ_in_busy : t1 + Δ < t2 jobs := arrivals_between arr_seq t1 (t1 + Δ) : seq Job EDF_from := fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool tsk_o : Task H_tsko_in_ts : tsk_o \in ts H_neq : tsk_o != tsk H_Δ_ge : A + 1 + D tsk - D tsk_o <= Δ BOUNDED : t1 + (A + 1 + D tsk - D tsk_o) <= t1 + Δ j' : Job IN' : j' \in arrivals_between arr_seq t1 (t1 + Δ) ARR' : t1 + (A + 1 + D tsk - D tsk_o) <=
job_arrival j'
~~ (EDF Job j' j && (job_task j' == tsk_o))
case : (eqVneq (job_task j') tsk_o) => TSK';
last by rewrite andbF.Task : TaskType H : TaskCost Task H0 : TaskDeadline Task H1 : MaxArrivals Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job D := [eta task_deadline] : Task -> duration arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat Δ : duration H_Δ_in_busy : t1 + Δ < t2 jobs := arrivals_between arr_seq t1 (t1 + Δ) : seq Job EDF_from := fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool tsk_o : Task H_tsko_in_ts : tsk_o \in ts H_neq : tsk_o != tsk H_Δ_ge : A + 1 + D tsk - D tsk_o <= Δ BOUNDED : t1 + (A + 1 + D tsk - D tsk_o) <= t1 + Δ j' : Job IN' : j' \in arrivals_between arr_seq t1 (t1 + Δ) ARR' : t1 + (A + 1 + D tsk - D tsk_o) <=
job_arrival j' TSK' : job_task j' = tsk_o
~~ (EDF Job j' j && true)
rewrite andbT; apply : contraT => /negPn.Task : TaskType H : TaskCost Task H0 : TaskDeadline Task H1 : MaxArrivals Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job D := [eta task_deadline] : Task -> duration arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat Δ : duration H_Δ_in_busy : t1 + Δ < t2 jobs := arrivals_between arr_seq t1 (t1 + Δ) : seq Job EDF_from := fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool tsk_o : Task H_tsko_in_ts : tsk_o \in ts H_neq : tsk_o != tsk H_Δ_ge : A + 1 + D tsk - D tsk_o <= Δ BOUNDED : t1 + (A + 1 + D tsk - D tsk_o) <= t1 + Δ j' : Job IN' : j' \in arrivals_between arr_seq t1 (t1 + Δ) ARR' : t1 + (A + 1 + D tsk - D tsk_o) <=
job_arrival j' TSK' : job_task j' = tsk_o
EDF Job j' j -> false
rewrite /EDF/edf.EDF/job_deadline/job_deadline_from_task_deadline.Task : TaskType H : TaskCost Task H0 : TaskDeadline Task H1 : MaxArrivals Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job D := [eta task_deadline] : Task -> duration arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat Δ : duration H_Δ_in_busy : t1 + Δ < t2 jobs := arrivals_between arr_seq t1 (t1 + Δ) : seq Job EDF_from := fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool tsk_o : Task H_tsko_in_ts : tsk_o \in ts H_neq : tsk_o != tsk H_Δ_ge : A + 1 + D tsk - D tsk_o <= Δ BOUNDED : t1 + (A + 1 + D tsk - D tsk_o) <= t1 + Δ j' : Job IN' : j' \in arrivals_between arr_seq t1 (t1 + Δ) ARR' : t1 + (A + 1 + D tsk - D tsk_o) <=
job_arrival j' TSK' : job_task j' = tsk_o
job_arrival j' + task_deadline (job_task j') <=
job_arrival j + task_deadline (job_task j) -> false
move : H_job_of_tsk; rewrite TSK' /job_of_task => /eqP -> HEP.Task : TaskType H : TaskCost Task H0 : TaskDeadline Task H1 : MaxArrivals Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job D := [eta task_deadline] : Task -> duration arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat Δ : duration H_Δ_in_busy : t1 + Δ < t2 jobs := arrivals_between arr_seq t1 (t1 + Δ) : seq Job EDF_from := fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool tsk_o : Task H_tsko_in_ts : tsk_o \in ts H_neq : tsk_o != tsk H_Δ_ge : A + 1 + D tsk - D tsk_o <= Δ BOUNDED : t1 + (A + 1 + D tsk - D tsk_o) <= t1 + Δ j' : Job IN' : j' \in arrivals_between arr_seq t1 (t1 + Δ) ARR' : t1 + (A + 1 + D tsk - D tsk_o) <=
job_arrival j' TSK' : job_task j' = tsk_o HEP : job_arrival j' + task_deadline tsk_o <=
job_arrival j + task_deadline tsk
false
have LATEST: job_arrival j' <= t1 + A + D tsk - D tsk_o by rewrite /D/A; lia .Task : TaskType H : TaskCost Task H0 : TaskDeadline Task H1 : MaxArrivals Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job D := [eta task_deadline] : Task -> duration arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat Δ : duration H_Δ_in_busy : t1 + Δ < t2 jobs := arrivals_between arr_seq t1 (t1 + Δ) : seq Job EDF_from := fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool tsk_o : Task H_tsko_in_ts : tsk_o \in ts H_neq : tsk_o != tsk H_Δ_ge : A + 1 + D tsk - D tsk_o <= Δ BOUNDED : t1 + (A + 1 + D tsk - D tsk_o) <= t1 + Δ j' : Job IN' : j' \in arrivals_between arr_seq t1 (t1 + Δ) ARR' : t1 + (A + 1 + D tsk - D tsk_o) <=
job_arrival j' TSK' : job_task j' = tsk_o HEP : job_arrival j' + task_deadline tsk_o <=
job_arrival j + task_deadline tsk LATEST : job_arrival j' <= t1 + A + D tsk - D tsk_o
false
have EARLIEST: t1 <= job_arrival j' by apply : job_arrival_between_ge.Task : TaskType H : TaskCost Task H0 : TaskDeadline Task H1 : MaxArrivals Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job D := [eta task_deadline] : Task -> duration arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat Δ : duration H_Δ_in_busy : t1 + Δ < t2 jobs := arrivals_between arr_seq t1 (t1 + Δ) : seq Job EDF_from := fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool tsk_o : Task H_tsko_in_ts : tsk_o \in ts H_neq : tsk_o != tsk H_Δ_ge : A + 1 + D tsk - D tsk_o <= Δ BOUNDED : t1 + (A + 1 + D tsk - D tsk_o) <= t1 + Δ j' : Job IN' : j' \in arrivals_between arr_seq t1 (t1 + Δ) ARR' : t1 + (A + 1 + D tsk - D tsk_o) <=
job_arrival j' TSK' : job_task j' = tsk_o HEP : job_arrival j' + task_deadline tsk_o <=
job_arrival j + task_deadline tsk LATEST : job_arrival j' <= t1 + A + D tsk - D tsk_o EARLIEST : t1 <= job_arrival j'
false
by case : (leqP (A + 1 + D tsk) (D tsk_o)); [rewrite /D/A|]; lia .
Qed .
End ShortenRange .
(** Using the above lemma, we prove that the total workload of the
tasks is at most [bound_on_total_hep_workload(A, Δ)]. *)
Corollary sum_of_workloads_is_at_most_bound_on_total_hep_workload :
\sum_(tsk_o <- ts | tsk_o != tsk) workload_of_jobs (EDF_from tsk_o) jobs
<= bound_on_athep_workload ts tsk A Δ.Task : TaskType H : TaskCost Task H0 : TaskDeadline Task H1 : MaxArrivals Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job D := [eta task_deadline] : Task -> duration arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat Δ : duration H_Δ_in_busy : t1 + Δ < t2 jobs := arrivals_between arr_seq t1 (t1 + Δ) : seq Job EDF_from := fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool
\sum_(tsk_o <- ts | tsk_o != tsk)
workload_of_jobs (EDF_from tsk_o) jobs <=
bound_on_athep_workload ts tsk A Δ
Proof .Task : TaskType H : TaskCost Task H0 : TaskDeadline Task H1 : MaxArrivals Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job D := [eta task_deadline] : Task -> duration arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat Δ : duration H_Δ_in_busy : t1 + Δ < t2 jobs := arrivals_between arr_seq t1 (t1 + Δ) : seq Job EDF_from := fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool
\sum_(tsk_o <- ts | tsk_o != tsk)
workload_of_jobs (EDF_from tsk_o) jobs <=
bound_on_athep_workload ts tsk A Δ
apply leq_sum_seq => tsko INtsko NEQT; fold (D tsk) (D tsko).Task : TaskType H : TaskCost Task H0 : TaskDeadline Task H1 : MaxArrivals Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job D := [eta task_deadline] : Task -> duration arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat Δ : duration H_Δ_in_busy : t1 + Δ < t2 jobs := arrivals_between arr_seq t1 (t1 + Δ) : seq Job EDF_from := fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool tsko : Task INtsko : tsko \in ts NEQT : tsko != tsk
workload_of_jobs (EDF_from tsko) jobs <=
task_request_bound_function tsko
(minn (A + 1 + D tsk - D tsko) Δ)
edestruct (leqP Δ (A + ε + D tsk - D tsko)) as [NEQ|NEQ]; [ | apply ltnW in NEQ].Task : TaskType H : TaskCost Task H0 : TaskDeadline Task H1 : MaxArrivals Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job D := [eta task_deadline] : Task -> duration arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat Δ : duration H_Δ_in_busy : t1 + Δ < t2 jobs := arrivals_between arr_seq t1 (t1 + Δ) : seq Job EDF_from := fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool tsko : Task INtsko : tsko \in ts NEQT : tsko != tsk NEQ : Δ <= A + 1 + D tsk - D tsko
workload_of_jobs (EDF_from tsko) jobs <=
task_request_bound_function tsko Δ
- Task : TaskType H : TaskCost Task H0 : TaskDeadline Task H1 : MaxArrivals Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job D := [eta task_deadline] : Task -> duration arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat Δ : duration H_Δ_in_busy : t1 + Δ < t2 jobs := arrivals_between arr_seq t1 (t1 + Δ) : seq Job EDF_from := fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool tsko : Task INtsko : tsko \in ts NEQT : tsko != tsk NEQ : Δ <= A + 1 + D tsk - D tsko
workload_of_jobs (EDF_from tsko) jobs <=
task_request_bound_function tsko Δ
exact : (workload_le_rbf' arr_seq tsko).
- Task : TaskType H : TaskCost Task H0 : TaskDeadline Task H1 : MaxArrivals Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job D := [eta task_deadline] : Task -> duration arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat Δ : duration H_Δ_in_busy : t1 + Δ < t2 jobs := arrivals_between arr_seq t1 (t1 + Δ) : seq Job EDF_from := fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool tsko : Task INtsko : tsko \in ts NEQT : tsko != tsk NEQ : A + 1 + D tsk - D tsko <= Δ
workload_of_jobs (EDF_from tsko) jobs <=
task_request_bound_function tsko
(A + 1 + D tsk - D tsko)
eapply leq_trans; first by eapply total_workload_shorten_range; eauto 2 .Task : TaskType H : TaskCost Task H0 : TaskDeadline Task H1 : MaxArrivals Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job D := [eta task_deadline] : Task -> duration arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState j : Job H_j_arrives : arrives_in arr_seq j H_job_of_tsk : job_of_task tsk j H_job_cost_positive : job_cost_positive j t1, t2 : duration H_busy_interval : busy_interval arr_seq sched j t1 t2 A := job_arrival j - t1 : nat Δ : duration H_Δ_in_busy : t1 + Δ < t2 jobs := arrivals_between arr_seq t1 (t1 + Δ) : seq Job EDF_from := fun (tsk : Task) (jo : Job) =>
EDF Job jo j && (job_task jo == tsk): Task -> Job -> bool tsko : Task INtsko : tsko \in ts NEQT : tsko != tsk NEQ : A + 1 + D tsk - D tsko <= Δ
workload_of_jobs (EDF_from tsko)
(arrivals_between arr_seq t1
(t1 + (A + 1 + D tsk - D tsko))) <=
task_request_bound_function tsko
(A + 1 + D tsk - D tsko)
exact : workload_le_rbf'.
Qed .
End HepWorkloadBound .
(** The validity of [bound_on_athep_workload] then easily follows
from lemma [sum_of_workloads_is_at_most_bound_on_total_hep_workload]. *)
Corollary bound_on_athep_workload_is_valid :
athep_workload_is_bounded arr_seq sched tsk (bound_on_athep_workload ts tsk).Task : TaskType H : TaskCost Task H0 : TaskDeadline Task H1 : MaxArrivals Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job D := [eta task_deadline] : Task -> duration arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState
athep_workload_is_bounded arr_seq sched tsk
(bound_on_athep_workload ts tsk)
Proof .Task : TaskType H : TaskCost Task H0 : TaskDeadline Task H1 : MaxArrivals Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job D := [eta task_deadline] : Task -> duration arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState
athep_workload_is_bounded arr_seq sched tsk
(bound_on_athep_workload ts tsk)
move => j t1 Δ POS TSK QT.Task : TaskType H : TaskCost Task H0 : TaskDeadline Task H1 : MaxArrivals Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job D := [eta task_deadline] : Task -> duration arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState j : Job t1 : instant Δ : duration POS : job_cost_positive j TSK : job_of_task tsk j QT : quiet_time arr_seq sched j t1
workload_of_jobs (another_task_hep_job^~ j)
(arrivals_between arr_seq t1 (t1 + Δ)) <=
bound_on_athep_workload ts tsk (job_arrival j - t1) Δ
eapply leq_trans.Task : TaskType H : TaskCost Task H0 : TaskDeadline Task H1 : MaxArrivals Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job D := [eta task_deadline] : Task -> duration arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState j : Job t1 : instant Δ : duration POS : job_cost_positive j TSK : job_of_task tsk j QT : quiet_time arr_seq sched j t1
workload_of_jobs (another_task_hep_job^~ j)
(arrivals_between arr_seq t1 (t1 + Δ)) <= ?n
+ Task : TaskType H : TaskCost Task H0 : TaskDeadline Task H1 : MaxArrivals Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job D := [eta task_deadline] : Task -> duration arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState j : Job t1 : instant Δ : duration POS : job_cost_positive j TSK : job_of_task tsk j QT : quiet_time arr_seq sched j t1
workload_of_jobs (another_task_hep_job^~ j)
(arrivals_between arr_seq t1 (t1 + Δ)) <= ?n
eapply reorder_summation => j' IN _.Task : TaskType H : TaskCost Task H0 : TaskDeadline Task H1 : MaxArrivals Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job D := [eta task_deadline] : Task -> duration arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState j : Job t1 : instant Δ : duration POS : job_cost_positive j TSK : job_of_task tsk j QT : quiet_time arr_seq sched j t1 j' : Job IN : j' \in arrivals_between arr_seq t1 (t1 + Δ)
job_task j' \in ?ys
by apply H_all_jobs_from_taskset; eapply in_arrivals_implies_arrived; exact IN.
+ Task : TaskType H : TaskCost Task H0 : TaskDeadline Task H1 : MaxArrivals Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job D := [eta task_deadline] : Task -> duration arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState j : Job t1 : instant Δ : duration POS : job_cost_positive j TSK : job_of_task tsk j QT : quiet_time arr_seq sched j t1
\sum_(y <- ts | y != job_task j)
\sum_(x <- arrivals_between arr_seq t1 (t1 + Δ) |
(hep_job^~ j) x && (job_task x == y)) job_cost x <=
bound_on_athep_workload ts tsk (job_arrival j - t1) Δ
move : TSK => /eqP TSK; rewrite TSK.Task : TaskType H : TaskCost Task H0 : TaskDeadline Task H1 : MaxArrivals Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job PState : ProcessorState Job D := [eta task_deadline] : Task -> duration arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts tsk : Task sched : schedule PState j : Job t1 : instant Δ : duration POS : job_cost_positive j QT : quiet_time arr_seq sched j t1 TSK : job_task j = tsk
\sum_(y <- ts | y != tsk)
\sum_(x <- arrivals_between arr_seq t1 (t1 + Δ) |
hep_job x j && (job_task x == y)) job_cost x <=
bound_on_athep_workload ts tsk (job_arrival j - t1) Δ
by apply : sum_of_workloads_is_at_most_bound_on_total_hep_workload => //; apply /eqP.
Qed .
End ATHEPWorkloadBoundIsValidForEDF .