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.analysis.facts.suspension.[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.suspension.dynamic.
Require Export prosa.analysis.facts.model.arrival_curves.
(** In this file, we prove some facts related to the dynamic self-suspension model. *)
Section TotalSuspensionBounded .
(** Consider any type of tasks each characterized by a WCET [task_cost],
an arrival curve [max_arrivals], and a bound on the maximum total
self-suspension duration exhibited by any job of the task
[task_total_suspension]. *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
Context `{MaxArrivals Task}.
Context `{TaskTotalSuspension Task}.
(** Consider any kind of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Here we consider that the jobs can exhibit self-suspensions. *)
Context `{JobSuspension Job}.
(** Assume that all jobs respect the bound on the maximum total self-suspension duration. *)
Hypothesis H_valid_dynamic_suspensions : valid_dynamic_suspensions.
(** Consider any valid arrival sequence of jobs ... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** ... and assume the notion of readiness for self-suspending jobs. *)
#[local] Existing Instance suspension_ready_instance .
(** Consider any kind of processor model. *)
Context `{PState : ProcessorState Job}.
(** Consider any valid schedule. *)
Variable sched : schedule PState.
Hypothesis H_valid_schedule : valid_schedule sched arr_seq.
(** Let [tsk] be any task. *)
Variable tsk : Task.
(** Consider any arbitrary time interval <<[t1, t1 + Δ)>>. *)
Variable t1 : instant.
Variable Δ : duration.
(** We first prove a bound on the total self-suspension duration of a job. *)
Section JobSuspensionBounded .
(** Consider any job [j] of [tsk]. *)
Variable j : Job.
Hypothesis H_job_tsk : job_of_task tsk j.
(** Now we prove an upper bound on the total duration a job remains suspended
in the interval <<[t1, t1 + Δ)>>. *)
Lemma job_suspension_bounded :
\sum_(t1 <= t < t1 + Δ) suspended sched j t <= task_total_suspension tsk.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j
\sum_(t1 <= t < t1 + Δ) suspended sched j t <=
task_total_suspension tsk
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j
\sum_(t1 <= t < t1 + Δ) suspended sched j t <=
task_total_suspension tsk
move : H_job_tsk; rewrite /job_of_task => /eqP <-.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j
\sum_(t1 <= t < t1 + Δ) suspended sched j t <=
task_total_suspension (job_task j)
apply : leq_trans; last by apply H_valid_dynamic_suspensions.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j
\sum_(t1 <= t < t1 + Δ) suspended sched j t <=
total_suspension j
rewrite /total_suspension.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j
\sum_(t1 <= t < t1 + Δ) suspended sched j t <=
\sum_(0 <= ρ < job_cost j) job_suspension j ρ
apply leq_trans with (n := \sum_(0 <= r < service sched j (t1 + Δ) + 1 )
\sum_(t1 <= t < (t1 + Δ) | service sched j t == r) suspended sched j t).Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j
\sum_(t1 <= t < t1 + Δ) suspended sched j t <=
\sum_(0 <= r < service sched j (t1 + Δ) + 1 )
\sum_(t1 <= t < t1 + Δ | service sched j t == r)
suspended sched j t
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j
\sum_(t1 <= t < t1 + Δ) suspended sched j t <=
\sum_(0 <= r < service sched j (t1 + Δ) + 1 )
\sum_(t1 <= t < t1 + Δ | service sched j t == r)
suspended sched j t
apply : sum_over_partitions_le => [t INt _].Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j t : Datatypes_nat__canonical__eqtype_Equality INt : t \in index_iota t1 (t1 + Δ)
service sched j t
\in index_iota 0 (service sched j (t1 + Δ) + 1 )
rewrite mem_index_iota in INt.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j t : Datatypes_nat__canonical__eqtype_Equality INt : t1 <= t < t1 + Δ
service sched j t
\in index_iota 0 (service sched j (t1 + Δ) + 1 )
rewrite mem_index_iota; apply /andP; split => //=.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j t : Datatypes_nat__canonical__eqtype_Equality INt : t1 <= t < t1 + Δ
service sched j t < service sched j (t1 + Δ) + 1
have ->: service sched j (t1 + Δ) = service sched j t + service_during sched j t (t1 + Δ)
by rewrite service_cat; lia .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j t : Datatypes_nat__canonical__eqtype_Equality INt : t1 <= t < t1 + Δ
service sched j t <
service sched j t + service_during sched j t (t1 + Δ) +
1
by lia . } Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j
\sum_(0 <= r < service sched j (t1 + Δ) + 1 )
\sum_(t1 <= t < t1 + Δ | service sched j t == r)
suspended sched j t <=
\sum_(0 <= ρ < job_cost j) job_suspension j ρ
have [GEQ | LT] := boolP(service sched j (t1 + Δ) + 1 >= job_cost j).Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j GEQ : job_cost j <= service sched j (t1 + Δ) + 1
\sum_(0 <= r < service sched j (t1 + Δ) + 1 )
\sum_(t1 <= t < t1 + Δ | service sched j t == r)
suspended sched j t <=
\sum_(0 <= ρ < job_cost j) job_suspension j ρ
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j GEQ : job_cost j <= service sched j (t1 + Δ) + 1
\sum_(0 <= r < service sched j (t1 + Δ) + 1 )
\sum_(t1 <= t < t1 + Δ | service sched j t == r)
suspended sched j t <=
\sum_(0 <= ρ < job_cost j) job_suspension j ρ
erewrite big_cat_nat with (n := job_cost j) => //=.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j GEQ : job_cost j <= service sched j (t1 + Δ) + 1
\sum_(0 <= i < job_cost j)
\sum_(t1 <= t < t1 + Δ | service sched j t == i)
suspended sched j t +
\sum_(job_cost j <= i < service sched j (t1 + Δ) + 1 )
\sum_(t1 <= t < t1 + Δ | service sched j t == i)
suspended sched j t <=
\sum_(0 <= ρ < job_cost j) job_suspension j ρ
have ->: \sum_(job_cost j <= r < service sched j (t1 + Δ) + 1 )
\sum_(t1 <= t < t1 + Δ | service sched j t == r) suspended sched j t = 0 .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j GEQ : job_cost j <= service sched j (t1 + Δ) + 1
\sum_(job_cost j <= r < service sched j (t1 + Δ) + 1 )
\sum_(t1 <= t < t1 + Δ | service sched j t == r)
suspended sched j t = 0
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j GEQ : job_cost j <= service sched j (t1 + Δ) + 1
\sum_(job_cost j <= r < service sched j (t1 + Δ) + 1 )
\sum_(t1 <= t < t1 + Δ | service sched j t == r)
suspended sched j t = 0
apply /eqP; rewrite sum_nat_eq0_nat.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j GEQ : job_cost j <= service sched j (t1 + Δ) + 1
all
(fun x : Datatypes_nat__canonical__eqtype_Equality
=>
\sum_(t1 <= t < t1 + Δ | service sched j t == x)
suspended sched j t == 0 )
[seq _ <- index_iota (job_cost j)
(service sched j (t1 + Δ) + 1 )
| true]
apply /allP => [r INr].Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j GEQ : job_cost j <= service sched j (t1 + Δ) + 1 r : Datatypes_nat__canonical__eqtype_Equality INr : r
\in [seq _ <- index_iota
(job_cost j)
(service sched j (t1 + Δ) + 1 )
| true]
\sum_(t1 <= t < t1 + Δ | service sched j t == r)
suspended sched j t == 0
move : INr; rewrite mem_filter andTb mem_index_iota => INr.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j GEQ : job_cost j <= service sched j (t1 + Δ) + 1 r : Datatypes_nat__canonical__eqtype_Equality INr : job_cost j <= r < service sched j (t1 + Δ) + 1
\sum_(t1 <= t < t1 + Δ | service sched j t == r)
suspended sched j t == 0
rewrite sum_nat_eq0_nat; apply /allP => [to INto].Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j GEQ : job_cost j <= service sched j (t1 + Δ) + 1 r : Datatypes_nat__canonical__eqtype_Equality INr : job_cost j <= r < service sched j (t1 + Δ) + 1 to : Datatypes_nat__canonical__eqtype_Equality INto : to
\in [seq x <- index_iota t1 (t1 + Δ)
| service sched j x == r]
suspended sched j to == 0
move : INto; rewrite mem_filter => /andP[/eqP SERVto INto].Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j GEQ : job_cost j <= service sched j (t1 + Δ) + 1 r : Datatypes_nat__canonical__eqtype_Equality INr : job_cost j <= r < service sched j (t1 + Δ) + 1 to : Datatypes_nat__canonical__eqtype_Equality SERVto : service sched j to = r INto : to \in index_iota t1 (t1 + Δ)
suspended sched j to == 0
rewrite /suspended.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j GEQ : job_cost j <= service sched j (t1 + Δ) + 1 r : Datatypes_nat__canonical__eqtype_Equality INr : job_cost j <= r < service sched j (t1 + Δ) + 1 to : Datatypes_nat__canonical__eqtype_Equality SERVto : service sched j to = r INto : to \in index_iota t1 (t1 + Δ)
~~ suspension_has_passed sched j to &&
pending sched j to == 0
have /negPf ->: ~~ pending sched j to; last by rewrite andbF.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j GEQ : job_cost j <= service sched j (t1 + Δ) + 1 r : Datatypes_nat__canonical__eqtype_Equality INr : job_cost j <= r < service sched j (t1 + Δ) + 1 to : Datatypes_nat__canonical__eqtype_Equality SERVto : service sched j to = r INto : to \in index_iota t1 (t1 + Δ)
~~ pending sched j to
rewrite /pending negb_and negbK; apply /orP; right .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j GEQ : job_cost j <= service sched j (t1 + Δ) + 1 r : Datatypes_nat__canonical__eqtype_Equality INr : job_cost j <= r < service sched j (t1 + Δ) + 1 to : Datatypes_nat__canonical__eqtype_Equality SERVto : service sched j to = r INto : to \in index_iota t1 (t1 + Δ)
completed_by sched j to
rewrite /completed_by; by lia . } Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j GEQ : job_cost j <= service sched j (t1 + Δ) + 1
\sum_(0 <= i < job_cost j)
\sum_(t1 <= t < t1 + Δ | service sched j t == i)
suspended sched j t + 0 <=
\sum_(0 <= ρ < job_cost j) job_suspension j ρ
rewrite addn0.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j GEQ : job_cost j <= service sched j (t1 + Δ) + 1
\sum_(0 <= i < job_cost j)
\sum_(t1 <= t < t1 + Δ | service sched j t == i)
suspended sched j t <=
\sum_(0 <= ρ < job_cost j) job_suspension j ρ
rewrite leq_sum_seq //= => r _ _.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j GEQ : job_cost j <= service sched j (t1 + Δ) + 1 r : nat
\sum_(t1 <= t < t1 + Δ | service sched j t == r)
suspended sched j t <= job_suspension j r
by apply : suspension_bounded_in_interval. } Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j LT : ~~ (job_cost j <= service sched j (t1 + Δ) + 1 )
\sum_(0 <= r < service sched j (t1 + Δ) + 1 )
\sum_(t1 <= t < t1 + Δ | service sched j t == r)
suspended sched j t <=
\sum_(0 <= ρ < job_cost j) job_suspension j ρ
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j LT : ~~ (job_cost j <= service sched j (t1 + Δ) + 1 )
\sum_(0 <= r < service sched j (t1 + Δ) + 1 )
\sum_(t1 <= t < t1 + Δ | service sched j t == r)
suspended sched j t <=
\sum_(0 <= ρ < job_cost j) job_suspension j ρ
apply leq_trans with (n := \sum_(0 <= r < job_cost j)
\sum_(t1 <= t < t1 + Δ | service sched j t == r) suspended sched j t).Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j LT : ~~ (job_cost j <= service sched j (t1 + Δ) + 1 )
\sum_(0 <= r < service sched j (t1 + Δ) + 1 )
\sum_(t1 <= t < t1 + Δ | service sched j t == r)
suspended sched j t <=
\sum_(0 <= r < job_cost j)
\sum_(t1 <= t < t1 + Δ | service sched j t == r)
suspended sched j t
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j LT : ~~ (job_cost j <= service sched j (t1 + Δ) + 1 )
\sum_(0 <= r < service sched j (t1 + Δ) + 1 )
\sum_(t1 <= t < t1 + Δ | service sched j t == r)
suspended sched j t <=
\sum_(0 <= r < job_cost j)
\sum_(t1 <= t < t1 + Δ | service sched j t == r)
suspended sched j t
rewrite -ltnNge in LT.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j LT : service sched j (t1 + Δ) + 1 < job_cost j
\sum_(0 <= r < service sched j (t1 + Δ) + 1 )
\sum_(t1 <= t < t1 + Δ | service sched j t == r)
suspended sched j t <=
\sum_(0 <= r < job_cost j)
\sum_(t1 <= t < t1 + Δ | service sched j t == r)
suspended sched j t
rewrite [in leqRHS](@big_cat_nat _ _ _ (service sched j (t1 + Δ) + 1 )) => //=.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j LT : service sched j (t1 + Δ) + 1 < job_cost j
\sum_(0 <= r < service sched j (t1 + Δ) + 1 )
\sum_(t1 <= t < t1 + Δ | service sched j t == r)
suspended sched j t <=
\sum_(0 <= i < service sched j (t1 + Δ) + 1 )
\sum_(t1 <= t < t1 + Δ | service sched j t == i)
suspended sched j t +
\sum_(service sched j (t1 + Δ) + 1 <= i < job_cost j)
\sum_(t1 <= t < t1 + Δ | service sched j t == i)
suspended sched j t
by lia . } Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j LT : ~~ (job_cost j <= service sched j (t1 + Δ) + 1 )
\sum_(0 <= r < job_cost j)
\sum_(t1 <= t < t1 + Δ | service sched j t == r)
suspended sched j t <=
\sum_(0 <= ρ < job_cost j) job_suspension j ρ
rewrite leq_sum_seq //= => r _ _.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration j : Job H_job_tsk : job_of_task tsk j LT : ~~ (job_cost j <= service sched j (t1 + Δ) + 1 ) r : nat
\sum_(t1 <= t < t1 + Δ | service sched j t == r)
suspended sched j t <= job_suspension j r
by apply : suspension_bounded_in_interval.
}
Qed .
End JobSuspensionBounded .
(* Next, assume that [tsk] respects the arrival curve defined by [max_arrivals]. *)
Hypothesis H_tsk_respects_max_arrivals : respects_max_arrivals arr_seq tsk (max_arrivals tsk).
(** Now we establish a bound on the total duration the jobs of task [tsk] remain suspended in the interval
<<[t1, t2)>>. *)
Lemma suspension_of_task_bounded :
\sum_(t1 <= t < t1 + Δ) \sum_(j <- task_arrivals_between arr_seq tsk t1 (t1 + Δ)) suspended sched j t
<= max_arrivals tsk Δ * task_total_suspension tsk.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration H_tsk_respects_max_arrivals : respects_max_arrivals
arr_seq tsk
(max_arrivals tsk)
\sum_(t1 <= t < t1 + Δ)
\sum_(j <- task_arrivals_between arr_seq tsk t1
(t1 + Δ)) suspended sched j t <=
max_arrivals tsk Δ * task_total_suspension tsk
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration H_tsk_respects_max_arrivals : respects_max_arrivals
arr_seq tsk
(max_arrivals tsk)
\sum_(t1 <= t < t1 + Δ)
\sum_(j <- task_arrivals_between arr_seq tsk t1
(t1 + Δ)) suspended sched j t <=
max_arrivals tsk Δ * task_total_suspension tsk
apply leq_trans with
(n := number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) * task_total_suspension tsk); last first .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration H_tsk_respects_max_arrivals : respects_max_arrivals
arr_seq tsk
(max_arrivals tsk)
number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) *
task_total_suspension tsk <=
max_arrivals tsk Δ * task_total_suspension tsk
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration H_tsk_respects_max_arrivals : respects_max_arrivals
arr_seq tsk
(max_arrivals tsk)
number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) *
task_total_suspension tsk <=
max_arrivals tsk Δ * task_total_suspension tsk
rewrite leq_mul2r; apply /orP; right .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration H_tsk_respects_max_arrivals : respects_max_arrivals
arr_seq tsk
(max_arrivals tsk)
number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) <=
max_arrivals tsk Δ
rewrite -{2 }[Δ](addKn t1).Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration H_tsk_respects_max_arrivals : respects_max_arrivals
arr_seq tsk
(max_arrivals tsk)
number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) <=
max_arrivals tsk (t1 + Δ - t1)
apply : H_tsk_respects_max_arrivals; by lia . } Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration H_tsk_respects_max_arrivals : respects_max_arrivals
arr_seq tsk
(max_arrivals tsk)
\sum_(t1 <= t < t1 + Δ)
\sum_(j <- task_arrivals_between arr_seq tsk t1
(t1 + Δ)) suspended sched j t <=
number_of_task_arrivals arr_seq tsk t1 (t1 + Δ) *
task_total_suspension tsk
rewrite /number_of_task_arrivals -sum1_size big_distrl //=.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration H_tsk_respects_max_arrivals : respects_max_arrivals
arr_seq tsk
(max_arrivals tsk)
\sum_(t1 <= t < t1 + Δ)
\sum_(j <- task_arrivals_between arr_seq tsk t1
(t1 + Δ)) suspended sched j t <=
\sum_(i <- task_arrivals_between arr_seq tsk t1
(t1 + Δ)) 1 * task_total_suspension tsk
rewrite exchange_big_idem //=.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration H_tsk_respects_max_arrivals : respects_max_arrivals
arr_seq tsk
(max_arrivals tsk)
\sum_(j <- task_arrivals_between arr_seq tsk t1
(t1 + Δ))
\sum_(t1 <= i < t1 + Δ) suspended sched j i <=
\sum_(i <- task_arrivals_between arr_seq tsk t1
(t1 + Δ)) 1 * task_total_suspension tsk
apply leq_sum_seq => jo INjo _; rewrite mul1n.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration H_tsk_respects_max_arrivals : respects_max_arrivals
arr_seq tsk
(max_arrivals tsk) jo : Job INjo : jo
\in task_arrivals_between arr_seq tsk t1
(t1 + Δ)
\sum_(t1 <= i < t1 + Δ) suspended sched jo i <=
task_total_suspension tsk
apply job_suspension_bounded.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskTotalSuspension Task Job : JobType H2 : JobTask Job Task H3 : JobArrival Job H4 : JobCost Job H5 : JobSuspension Job H_valid_dynamic_suspensions : valid_dynamic_suspensions arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq PState : ProcessorState Job sched : schedule PState H_valid_schedule : valid_schedule sched arr_seq tsk : Task t1 : instant Δ : duration H_tsk_respects_max_arrivals : respects_max_arrivals
arr_seq tsk
(max_arrivals tsk) jo : Job INjo : jo
\in task_arrivals_between arr_seq tsk t1
(t1 + Δ)
job_of_task tsk jo
by move : INjo; rewrite mem_filter => /andP[? ?].
Qed .
End TotalSuspensionBounded .