Built with
Alectryon , running Coq+SerAPI v8.19.0+0.19.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.definitions.blocking_bound.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 ] [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_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.analysis.facts.busy_interval.pi.
Require Export prosa.model.priority.edf.
Require Export prosa.model.task.absolute_deadline.
Require Export prosa.analysis.facts.model.arrival_curves.
(** * Lower-Priority Non-Preemptive Segment is Bounded *)
(** In this file, we prove that, under the EDF scheduling policy, the
length of the maximum non-preemptive segment of a lower-priority
job (w.r.t. a job of a task [tsk]) is bounded by
[blocking_bound]. *)
Section MaxNPSegmentIsBounded .
(** Consider any type of tasks, each characterized by a WCET
[task_cost], an arrival curve [max_arrivals], a relative
deadline [task_deadline], and a bound on the the task's longest
non-preemptive segment [task_max_nonpreemptive_segment] ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
Context `{MaxArrivals Task}.
Context `{TaskDeadline Task}.
Context `{TaskMaxNonpreemptiveSegment 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 `{JobCost Job}.
Context `{JobArrival Job}.
(** Consider any kind of processor state model. *)
Context `{PState : ProcessorState Job}.
(** Consider the EDF policy. *)
Let EDF := EDF Job.
(** Consider any valid arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** ... and any schedule of this arrival sequence. *)
Variable sched : schedule PState.
(** We further require that a job's cost cannot exceed its task's stated WCET ... *)
Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
(** ... and assume that jobs have bounded non-preemptive segments. *)
Context `{JobPreemptable Job}.
Hypothesis H_valid_model_with_bounded_nonpreemptive_segments :
valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
(** Consider an arbitrary task set [ts], ... *)
Variable ts : seq Task.
(** ... assume that all jobs come from the task set, ... *)
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
(** ... and let [tsk] be any task in [ts] that is to be analyzed. *)
Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.
(** Let [max_arrivals] be a family of arrival curves. *)
Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
(** Consider any job [j] of [tsk]. *)
Variable j : Job.
Hypothesis H_job_of_tsk : job_of_task tsk j.
(** Then, the maximum length of a nonpreemptive segment among all
lower-priority jobs (w.r.t. the given job [j]) arrived so far is
bounded by [blocking_bound]. *)
Lemma nonpreemptive_segments_bounded_by_blocking :
forall t1 t2 ,
busy_interval_prefix arr_seq sched j t1 t2 ->
max_lp_nonpreemptive_segment arr_seq j t1 <= blocking_bound ts tsk (job_arrival j - t1).Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskDeadline Task H2 : TaskMaxNonpreemptiveSegment Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job EDF := edf.EDF Job : JLFP_policy Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j
forall t1 t2 : instant,
busy_interval_prefix arr_seq sched j t1 t2 ->
max_lp_nonpreemptive_segment arr_seq j t1 <=
blocking_bound ts tsk (job_arrival j - t1)
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskDeadline Task H2 : TaskMaxNonpreemptiveSegment Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job EDF := edf.EDF Job : JLFP_policy Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j
forall t1 t2 : instant,
busy_interval_prefix arr_seq sched j t1 t2 ->
max_lp_nonpreemptive_segment arr_seq j t1 <=
blocking_bound ts tsk (job_arrival j - t1)
move => t1 t2 BUSY; rewrite /max_lp_nonpreemptive_segment /blocking_bound.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskDeadline Task H2 : TaskMaxNonpreemptiveSegment Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job EDF := edf.EDF Job : JLFP_policy Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2
\max_(j_lp <- arrivals_before arr_seq t1 | ~~
hep_job
j_lp j &&
(0 <
job_cost
j_lp))
(job_max_nonpreemptive_segment j_lp - 1 ) <=
\max_(tsk_o <- ts | blocking_relevant tsk_o &&
(task_deadline tsk +
(job_arrival j - t1) <
task_deadline tsk_o))
(task_max_nonpreemptive_segment tsk_o - 1 )
apply : leq_trans;first by exact : max_np_job_segment_bounded_by_max_np_task_segment.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskDeadline Task H2 : TaskMaxNonpreemptiveSegment Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job EDF := edf.EDF Job : JLFP_policy Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2
\max_(j_lp <- arrivals_between arr_seq 0 t1 | ~~
hep_job
j_lp j &&
(0 <
job_cost
j_lp))
(task_max_nonpreemptive_segment (job_task j_lp) - 1 ) <=
\max_(tsk_o <- ts | blocking_relevant tsk_o &&
(task_deadline tsk +
(job_arrival j - t1) <
task_deadline tsk_o))
(task_max_nonpreemptive_segment tsk_o - 1 )
apply /bigmax_leq_seqP => j' JINB NOTHEP.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskDeadline Task H2 : TaskMaxNonpreemptiveSegment Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job EDF := edf.EDF Job : JLFP_policy Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job JINB : j' \in arrivals_between arr_seq 0 t1 NOTHEP : ~~ hep_job j' j && (0 < job_cost j')
task_max_nonpreemptive_segment (job_task j') - 1 <=
\max_(tsk_o <- ts | blocking_relevant tsk_o &&
(task_deadline tsk +
(job_arrival j - t1) <
task_deadline tsk_o))
(task_max_nonpreemptive_segment tsk_o - 1 )
have ARR': arrives_in arr_seq j'
by apply : in_arrivals_implies_arrived; exact : JINB.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskDeadline Task H2 : TaskMaxNonpreemptiveSegment Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job EDF := edf.EDF Job : JLFP_policy Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job JINB : j' \in arrivals_between arr_seq 0 t1 NOTHEP : ~~ hep_job j' j && (0 < job_cost j') ARR' : arrives_in arr_seq j'
task_max_nonpreemptive_segment (job_task j') - 1 <=
\max_(tsk_o <- ts | blocking_relevant tsk_o &&
(task_deadline tsk +
(job_arrival j - t1) <
task_deadline tsk_o))
(task_max_nonpreemptive_segment tsk_o - 1 )
apply leq_bigmax_cond_seq with (x := (job_task j')) (F := fun tsk => task_max_nonpreemptive_segment tsk - 1 );
first by apply H_all_jobs_from_taskset.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskDeadline Task H2 : TaskMaxNonpreemptiveSegment Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job EDF := edf.EDF Job : JLFP_policy Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job JINB : j' \in arrivals_between arr_seq 0 t1 NOTHEP : ~~ hep_job j' j && (0 < job_cost j') ARR' : arrives_in arr_seq j'
blocking_relevant (job_task j') &&
(task_deadline tsk + (job_arrival j - t1) <
task_deadline (job_task j'))
apply in_arrivals_implies_arrived_between in JINB => [|//].Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskDeadline Task H2 : TaskMaxNonpreemptiveSegment Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job EDF := edf.EDF Job : JLFP_policy Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job JINB : arrived_between j' 0 t1 NOTHEP : ~~ hep_job j' j && (0 < job_cost j') ARR' : arrives_in arr_seq j'
blocking_relevant (job_task j') &&
(task_deadline tsk + (job_arrival j - t1) <
task_deadline (job_task j'))
move : JINB; move => /andP [_ TJ'].Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskDeadline Task H2 : TaskMaxNonpreemptiveSegment Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job EDF := edf.EDF Job : JLFP_policy Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job NOTHEP : ~~ hep_job j' j && (0 < job_cost j') ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1
blocking_relevant (job_task j') &&
(task_deadline tsk + (job_arrival j - t1) <
task_deadline (job_task j'))
repeat (apply /andP; split ); last first .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskDeadline Task H2 : TaskMaxNonpreemptiveSegment Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job EDF := edf.EDF Job : JLFP_policy Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job NOTHEP : ~~ hep_job j' j && (0 < job_cost j') ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1
task_deadline tsk + (job_arrival j - t1) <
task_deadline (job_task j')
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskDeadline Task H2 : TaskMaxNonpreemptiveSegment Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job EDF := edf.EDF Job : JLFP_policy Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job NOTHEP : ~~ hep_job j' j && (0 < job_cost j') ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1
task_deadline tsk + (job_arrival j - t1) <
task_deadline (job_task j')
rewrite /hep_job -ltnNge in NOTHEP.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskDeadline Task H2 : TaskMaxNonpreemptiveSegment Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job EDF := edf.EDF Job : JLFP_policy Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1 NOTHEP : (job_deadline j < job_deadline j') &&
(0 < job_cost j')
task_deadline tsk + (job_arrival j - t1) <
task_deadline (job_task j')
move : H_job_of_tsk => /eqP <-.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskDeadline Task H2 : TaskMaxNonpreemptiveSegment Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job EDF := edf.EDF Job : JLFP_policy Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1 NOTHEP : (job_deadline j < job_deadline j') &&
(0 < job_cost j')
task_deadline (job_task j) + (job_arrival j - t1) <
task_deadline (job_task j')
have ARRLE: job_arrival j' < job_arrival j.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskDeadline Task H2 : TaskMaxNonpreemptiveSegment Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job EDF := edf.EDF Job : JLFP_policy Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1 NOTHEP : (job_deadline j < job_deadline j') &&
(0 < job_cost j')
job_arrival j' < job_arrival j
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskDeadline Task H2 : TaskMaxNonpreemptiveSegment Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job EDF := edf.EDF Job : JLFP_policy Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1 NOTHEP : (job_deadline j < job_deadline j') &&
(0 < job_cost j')
job_arrival j' < job_arrival j
by apply : (@leq_trans t1) => //; move : BUSY => [ _ [ _ [ _ /andP [F G]]] ]. } Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskDeadline Task H2 : TaskMaxNonpreemptiveSegment Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job EDF := edf.EDF Job : JLFP_policy Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1 NOTHEP : (job_deadline j < job_deadline j') &&
(0 < job_cost j') ARRLE : job_arrival j' < job_arrival j
task_deadline (job_task j) + (job_arrival j - t1) <
task_deadline (job_task j')
move : NOTHEP; rewrite /job_deadline /absolute_deadline.job_deadline_from_task_deadline.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskDeadline Task H2 : TaskMaxNonpreemptiveSegment Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job EDF := edf.EDF Job : JLFP_policy Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1 ARRLE : job_arrival j' < job_arrival j
(job_arrival j + task_deadline (job_task j) <
job_arrival j' + task_deadline (job_task j')) &&
(0 < job_cost j') ->
task_deadline (job_task j) + (job_arrival j - t1) <
task_deadline (job_task j')
by lia . } Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskDeadline Task H2 : TaskMaxNonpreemptiveSegment Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job EDF := edf.EDF Job : JLFP_policy Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job NOTHEP : ~~ hep_job j' j && (0 < job_cost j') ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1
0 < task_cost (job_task j')
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskDeadline Task H2 : TaskMaxNonpreemptiveSegment Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job EDF := edf.EDF Job : JLFP_policy Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job NOTHEP : ~~ hep_job j' j && (0 < job_cost j') ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1
0 < task_cost (job_task j')
move : NOTHEP => /andP [_ NZ].Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskDeadline Task H2 : TaskMaxNonpreemptiveSegment Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job EDF := edf.EDF Job : JLFP_policy Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1 NZ : 0 < job_cost j'
0 < task_cost (job_task j')
move : (H_valid_job_cost j' ARR'); rewrite /valid_job_cost.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskDeadline Task H2 : TaskMaxNonpreemptiveSegment Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job EDF := edf.EDF Job : JLFP_policy Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1 NZ : 0 < job_cost j'
job_cost j' <= task_cost (job_task j') ->
0 < task_cost (job_task j')
by lia . } Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskDeadline Task H2 : TaskMaxNonpreemptiveSegment Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job EDF := edf.EDF Job : JLFP_policy Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job NOTHEP : ~~ hep_job j' j && (0 < job_cost j') ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1
0 < max_arrivals (job_task j') 1
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskDeadline Task H2 : TaskMaxNonpreemptiveSegment Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job EDF := edf.EDF Job : JLFP_policy Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job NOTHEP : ~~ hep_job j' j && (0 < job_cost j') ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1
0 < max_arrivals (job_task j') 1
apply : non_pathological_max_arrivals; last first .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskDeadline Task H2 : TaskMaxNonpreemptiveSegment Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job EDF := edf.EDF Job : JLFP_policy Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job NOTHEP : ~~ hep_job j' j && (0 < job_cost j') ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1
arrives_in ?Goal ?Goal1
- Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskDeadline Task H2 : TaskMaxNonpreemptiveSegment Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job EDF := edf.EDF Job : JLFP_policy Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job NOTHEP : ~~ hep_job j' j && (0 < job_cost j') ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1
arrives_in ?Goal ?Goal1
exact : ARR'.
- Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskDeadline Task H2 : TaskMaxNonpreemptiveSegment Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job EDF := edf.EDF Job : JLFP_policy Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job NOTHEP : ~~ hep_job j' j && (0 < job_cost j') ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1
job_of_task (job_task j') j'
by rewrite /job_of_task.
- Task : TaskType H : TaskCost Task H0 : MaxArrivals Task H1 : TaskDeadline Task H2 : TaskMaxNonpreemptiveSegment Task Job : JobType H3 : JobTask Job Task H4 : JobCost Job H5 : JobArrival Job PState : ProcessorState Job EDF := edf.EDF Job : JLFP_policy Job arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq sched : schedule PState H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq H6 : JobPreemptable Job H_valid_model_with_bounded_nonpreemptive_segments : valid_model_with_bounded_nonpreemptive_segments
arr_seq sched ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts tsk : Task H_tsk_in_ts : tsk \in ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts j : Job H_job_of_tsk : job_of_task tsk j t1, t2 : instant BUSY : busy_interval_prefix arr_seq sched j t1 t2 j' : Job NOTHEP : ~~ hep_job j' j && (0 < job_cost j') ARR' : arrives_in arr_seq j' TJ' : job_arrival j' < t1
respects_max_arrivals arr_seq (job_task j')
(max_arrivals (job_task j'))
by apply H_is_arrival_curve, H_all_jobs_from_taskset, ARR'. }
Qed .
End MaxNPSegmentIsBounded .