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.preemption.job.limited.[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.preemption.limited_preemptive.
(** * Platform for Models with Limited Preemptions *)
(** In this section, we prove that instantiation of functions
[job_preemptable and task_preemption_points] to the
limited preemptions model indeed defines a valid preemption model
with bounded non-preemptive regions. *)
Section LimitedPreemptionsModel .
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** We assume that jobs are preemptable only at specific points during their
execution, ... *)
Context `{JobPreemptionPoints Job}.
Context `{TaskPreemptionPoints Task}.
(** ... i.e., we assume limited-preemptive jobs. *)
#[local] Existing Instance limited_preemptive_job_model .
(** Consider any arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
(** Next, consider any preemption-aware schedule of this arrival sequence... *)
Context {PState : ProcessorState Job}.
Variable sched : schedule PState.
Hypothesis H_schedule_respects_preemption_model :
schedule_respects_preemption_model arr_seq sched.
(** ... where jobs do not execute before their arrival or after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
(** Consider an arbitrary task set ts. *)
Variable ts : list Task.
(** Next, we assume that preemption points are defined by the model
with fixed preemption points. *)
Hypothesis H_valid_fixed_preemption_points_model :
valid_fixed_preemption_points_model arr_seq ts.
(** Then we prove that functions [job_preemptable and
task_preemption_points] define a model with bounded non-preemptive
regions. *)
Lemma fixed_preemption_points_model_is_model_with_bounded_nonpreemptive_regions :
model_with_bounded_nonpreemptive_segments arr_seq .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
model_with_bounded_nonpreemptive_segments arr_seq
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
model_with_bounded_nonpreemptive_segments arr_seq
intros j ARR.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
move : H_valid_fixed_preemption_points_model => [LIM FIX].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
move : (LIM) => [BEG [END NDEC]]; move : (FIX) => [A1 [A2 [A3 [A4 A5]]]].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
case : (posnP (job_cost j)) => [ZERO|POS].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts ZERO : job_cost j = 0
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts ZERO : job_cost j = 0
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
split .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts ZERO : job_cost j = 0
job_respects_max_nonpreemptive_segment j
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts ZERO : job_cost j = 0
job_respects_max_nonpreemptive_segment j
rewrite /job_respects_max_nonpreemptive_segment /job_max_nonpreemptive_segment
/lengths_of_segments /job_preemption_points; rewrite ZERO; simpl .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts ZERO : job_cost j = 0
max0
(distances
(if job_preemptable j 0 then [:: 0 ] else [::])) <=
task_max_nonpreemptive_segment (job_task j)
by rewrite /job_preemptable /limited_preemptive_job_model; erewrite zero_in_preemption_points; eauto 2 .
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts ZERO : job_cost j = 0
nonpreemptive_regions_have_bounded_length j
move => progr; rewrite ZERO leqn0; move => /andP [_ /eqP LE].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts ZERO : job_cost j = 0 progr : duration LE : progr = 0
exists pp : duration,
progr <= pp <=
progr + (job_max_nonpreemptive_segment j - 1 ) /\
job_preemptable j pp
exists 0 ; rewrite LE; split ; first by apply /andP; split .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts ZERO : job_cost j = 0 progr : duration LE : progr = 0
job_preemptable j 0
by eapply zero_in_preemption_points; eauto 2 .
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost j
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
split ; last (move => progr /andP [_ LE]; destruct (progr \in job_preemptive_points j) eqn :NotIN).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost j
job_respects_max_nonpreemptive_segment j
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost j
job_respects_max_nonpreemptive_segment j
rewrite /job_respects_max_nonpreemptive_segment
/job_max_nonpreemptive_segment /lengths_of_segments; erewrite job_parameters_max_np_to_job_limited; eauto .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost j
max0 (distances (job_preemptive_points j)) <=
task_max_nonpreemptive_segment (job_task j)
by apply max_of_dominating_seq; intros ; apply A5.
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost jprogr : duration LE : progr <= job_cost j NotIN : (progr \in job_preemptive_points j) = true
exists pp : duration,
progr <= pp <=
progr + (job_max_nonpreemptive_segment j - 1 ) /\
job_preemptable j pp
by exists progr ; split ; first apply /andP; first split ; rewrite ?leq_addr .
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost jprogr : duration LE : progr <= job_cost j NotIN : (progr \in job_preemptive_points j) = false
exists pp : duration,
progr <= pp <=
progr + (job_max_nonpreemptive_segment j - 1 ) /\
job_preemptable j pp
move : NotIN => /eqP; rewrite eqbF_neg; move => NotIN.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost jprogr : duration LE : progr <= job_cost j NotIN : progr \notin job_preemptive_points j
exists pp : duration,
progr <= pp <=
progr + (job_max_nonpreemptive_segment j - 1 ) /\
job_preemptable j pp
edestruct (work_belongs_to_some_nonpreemptive_segment arr_seq) as [x [SIZE2 N]]; eauto 2 .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost jprogr : duration LE : progr <= job_cost j NotIN : progr \notin job_preemptive_points j x : nat SIZE2 : x.+1 < size (job_preemptive_points j) N : nth 0 (job_preemptive_points j) x < progr <
nth 0 (job_preemptive_points j) x.+1
exists pp : duration,
progr <= pp <=
progr + (job_max_nonpreemptive_segment j - 1 ) /\
job_preemptable j pp
move : N => /andP [N1 N2].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost jprogr : duration LE : progr <= job_cost j NotIN : progr \notin job_preemptive_points j x : nat SIZE2 : x.+1 < size (job_preemptive_points j) N1 : nth 0 (job_preemptive_points j) x < progr N2 : progr < nth 0 (job_preemptive_points j) x.+1
exists pp : duration,
progr <= pp <=
progr + (job_max_nonpreemptive_segment j - 1 ) /\
job_preemptable j pp
set ptl := nth 0 (job_preemptive_points j) x.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost jprogr : duration LE : progr <= job_cost j NotIN : progr \notin job_preemptive_points j x : nat SIZE2 : x.+1 < size (job_preemptive_points j) N1 : nth 0 (job_preemptive_points j) x < progr N2 : progr < nth 0 (job_preemptive_points j) x.+1 ptl := nth 0 (job_preemptive_points j) x : nat
exists pp : duration,
progr <= pp <=
progr + (job_max_nonpreemptive_segment j - 1 ) /\
job_preemptable j pp
set ptr := nth 0 (job_preemptive_points j) x.+1 .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost jprogr : duration LE : progr <= job_cost j NotIN : progr \notin job_preemptive_points j x : nat SIZE2 : x.+1 < size (job_preemptive_points j) N1 : nth 0 (job_preemptive_points j) x < progr N2 : progr < nth 0 (job_preemptive_points j) x.+1 ptl := nth 0 (job_preemptive_points j) x : nat ptr := nth 0 (job_preemptive_points j) x.+1 : nat
exists pp : duration,
progr <= pp <=
progr + (job_max_nonpreemptive_segment j - 1 ) /\
job_preemptable j pp
exists ptr ; split ; first last .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost jprogr : duration LE : progr <= job_cost j NotIN : progr \notin job_preemptive_points j x : nat SIZE2 : x.+1 < size (job_preemptive_points j) N1 : nth 0 (job_preemptive_points j) x < progr N2 : progr < nth 0 (job_preemptive_points j) x.+1 ptl := nth 0 (job_preemptive_points j) x : nat ptr := nth 0 (job_preemptive_points j) x.+1 : nat
job_preemptable j ptr
* Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost jprogr : duration LE : progr <= job_cost j NotIN : progr \notin job_preemptive_points j x : nat SIZE2 : x.+1 < size (job_preemptive_points j) N1 : nth 0 (job_preemptive_points j) x < progr N2 : progr < nth 0 (job_preemptive_points j) x.+1 ptl := nth 0 (job_preemptive_points j) x : nat ptr := nth 0 (job_preemptive_points j) x.+1 : nat
job_preemptable j ptr
by unfold job_preemptable, limited_preemptive_job_model; apply mem_nth.
* Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost jprogr : duration LE : progr <= job_cost j NotIN : progr \notin job_preemptive_points j x : nat SIZE2 : x.+1 < size (job_preemptive_points j) N1 : nth 0 (job_preemptive_points j) x < progr N2 : progr < nth 0 (job_preemptive_points j) x.+1 ptl := nth 0 (job_preemptive_points j) x : nat ptr := nth 0 (job_preemptive_points j) x.+1 : nat
progr <= ptr <=
progr + (job_max_nonpreemptive_segment j - 1 )
apply /andP; split ; first by apply ltnW.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost jprogr : duration LE : progr <= job_cost j NotIN : progr \notin job_preemptive_points j x : nat SIZE2 : x.+1 < size (job_preemptive_points j) N1 : nth 0 (job_preemptive_points j) x < progr N2 : progr < nth 0 (job_preemptive_points j) x.+1 ptl := nth 0 (job_preemptive_points j) x : nat ptr := nth 0 (job_preemptive_points j) x.+1 : nat
ptr <= progr + (job_max_nonpreemptive_segment j - 1 )
apply leq_trans with (ptl + (job_max_nonpreemptive_segment j - ε) + 1 ); first last .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost jprogr : duration LE : progr <= job_cost j NotIN : progr \notin job_preemptive_points j x : nat SIZE2 : x.+1 < size (job_preemptive_points j) N1 : nth 0 (job_preemptive_points j) x < progr N2 : progr < nth 0 (job_preemptive_points j) x.+1 ptl := nth 0 (job_preemptive_points j) x : nat ptr := nth 0 (job_preemptive_points j) x.+1 : nat
ptl + (job_max_nonpreemptive_segment j - 1 ) + 1 <=
progr + (job_max_nonpreemptive_segment j - 1 )
-- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost jprogr : duration LE : progr <= job_cost j NotIN : progr \notin job_preemptive_points j x : nat SIZE2 : x.+1 < size (job_preemptive_points j) N1 : nth 0 (job_preemptive_points j) x < progr N2 : progr < nth 0 (job_preemptive_points j) x.+1 ptl := nth 0 (job_preemptive_points j) x : nat ptr := nth 0 (job_preemptive_points j) x.+1 : nat
ptl + (job_max_nonpreemptive_segment j - 1 ) + 1 <=
progr + (job_max_nonpreemptive_segment j - 1 )
rewrite addn1 ltn_add2r; apply N1.
-- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost jprogr : duration LE : progr <= job_cost j NotIN : progr \notin job_preemptive_points j x : nat SIZE2 : x.+1 < size (job_preemptive_points j) N1 : nth 0 (job_preemptive_points j) x < progr N2 : progr < nth 0 (job_preemptive_points j) x.+1 ptl := nth 0 (job_preemptive_points j) x : nat ptr := nth 0 (job_preemptive_points j) x.+1 : nat
ptr <= ptl + (job_max_nonpreemptive_segment j - 1 ) + 1
unfold job_max_nonpreemptive_segment.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost jprogr : duration LE : progr <= job_cost j NotIN : progr \notin job_preemptive_points j x : nat SIZE2 : x.+1 < size (job_preemptive_points j) N1 : nth 0 (job_preemptive_points j) x < progr N2 : progr < nth 0 (job_preemptive_points j) x.+1 ptl := nth 0 (job_preemptive_points j) x : nat ptr := nth 0 (job_preemptive_points j) x.+1 : nat
ptr <= ptl + (max0 (lengths_of_segments j) - 1 ) + 1
rewrite -addnA -leq_subLR -(leq_add2r 1 ).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost jprogr : duration LE : progr <= job_cost j NotIN : progr \notin job_preemptive_points j x : nat SIZE2 : x.+1 < size (job_preemptive_points j) N1 : nth 0 (job_preemptive_points j) x < progr N2 : progr < nth 0 (job_preemptive_points j) x.+1 ptl := nth 0 (job_preemptive_points j) x : nat ptr := nth 0 (job_preemptive_points j) x.+1 : nat
ptr - ptl + 1 <=
max0 (lengths_of_segments j) - 1 + 1 + 1
rewrite [in X in _ <= X]addnC -leq_subLR.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost jprogr : duration LE : progr <= job_cost j NotIN : progr \notin job_preemptive_points j x : nat SIZE2 : x.+1 < size (job_preemptive_points j) N1 : nth 0 (job_preemptive_points j) x < progr N2 : progr < nth 0 (job_preemptive_points j) x.+1 ptl := nth 0 (job_preemptive_points j) x : nat ptr := nth 0 (job_preemptive_points j) x.+1 : nat
ptr - ptl + 1 - 1 <=
max0 (lengths_of_segments j) - 1 + 1
rewrite !subn1 !addn1 prednK.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost jprogr : duration LE : progr <= job_cost j NotIN : progr \notin job_preemptive_points j x : nat SIZE2 : x.+1 < size (job_preemptive_points j) N1 : nth 0 (job_preemptive_points j) x < progr N2 : progr < nth 0 (job_preemptive_points j) x.+1 ptl := nth 0 (job_preemptive_points j) x : nat ptr := nth 0 (job_preemptive_points j) x.+1 : nat
(ptr - ptl).+1 .-1 <= max0 (lengths_of_segments j)
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost jprogr : duration LE : progr <= job_cost j NotIN : progr \notin job_preemptive_points j x : nat SIZE2 : x.+1 < size (job_preemptive_points j) N1 : nth 0 (job_preemptive_points j) x < progr N2 : progr < nth 0 (job_preemptive_points j) x.+1 ptl := nth 0 (job_preemptive_points j) x : nat ptr := nth 0 (job_preemptive_points j) x.+1 : nat
(ptr - ptl).+1 .-1 <= max0 (lengths_of_segments j)
rewrite -[_.+1 .-1 ]pred_Sn.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost jprogr : duration LE : progr <= job_cost j NotIN : progr \notin job_preemptive_points j x : nat SIZE2 : x.+1 < size (job_preemptive_points j) N1 : nth 0 (job_preemptive_points j) x < progr N2 : progr < nth 0 (job_preemptive_points j) x.+1 ptl := nth 0 (job_preemptive_points j) x : nat ptr := nth 0 (job_preemptive_points j) x.+1 : nat
ptr - ptl <= max0 (lengths_of_segments j)
rewrite /lengths_of_segments.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost jprogr : duration LE : progr <= job_cost j NotIN : progr \notin job_preemptive_points j x : nat SIZE2 : x.+1 < size (job_preemptive_points j) N1 : nth 0 (job_preemptive_points j) x < progr N2 : progr < nth 0 (job_preemptive_points j) x.+1 ptl := nth 0 (job_preemptive_points j) x : nat ptr := nth 0 (job_preemptive_points j) x.+1 : nat
ptr - ptl <=
max0 (distances (job_preemption_points j))
erewrite job_parameters_max_np_to_job_limited; eauto .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost jprogr : duration LE : progr <= job_cost j NotIN : progr \notin job_preemptive_points j x : nat SIZE2 : x.+1 < size (job_preemptive_points j) N1 : nth 0 (job_preemptive_points j) x < progr N2 : progr < nth 0 (job_preemptive_points j) x.+1 ptl := nth 0 (job_preemptive_points j) x : nat ptr := nth 0 (job_preemptive_points j) x.+1 : nat
ptr - ptl <=
max0 (distances (job_preemptive_points j))
by apply distance_between_neighboring_elements_le_max_distance_in_seq. } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost jprogr : duration LE : progr <= job_cost j NotIN : progr \notin job_preemptive_points j x : nat SIZE2 : x.+1 < size (job_preemptive_points j) N1 : nth 0 (job_preemptive_points j) x < progr N2 : progr < nth 0 (job_preemptive_points j) x.+1 ptl := nth 0 (job_preemptive_points j) x : nat ptr := nth 0 (job_preemptive_points j) x.+1 : nat
0 < max0 (lengths_of_segments j)
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost jprogr : duration LE : progr <= job_cost j NotIN : progr \notin job_preemptive_points j x : nat SIZE2 : x.+1 < size (job_preemptive_points j) N1 : nth 0 (job_preemptive_points j) x < progr N2 : progr < nth 0 (job_preemptive_points j) x.+1 ptl := nth 0 (job_preemptive_points j) x : nat ptr := nth 0 (job_preemptive_points j) x.+1 : nat
0 < max0 (lengths_of_segments j)
rewrite /lengths_of_segments; erewrite job_parameters_max_np_to_job_limited; eauto .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost jprogr : duration LE : progr <= job_cost j NotIN : progr \notin job_preemptive_points j x : nat SIZE2 : x.+1 < size (job_preemptive_points j) N1 : nth 0 (job_preemptive_points j) x < progr N2 : progr < nth 0 (job_preemptive_points j) x.+1 ptl := nth 0 (job_preemptive_points j) x : nat ptr := nth 0 (job_preemptive_points j) x.+1 : nat
0 < max0 (distances (job_preemptive_points j))
apply max_distance_in_nontrivial_seq_is_positive; first by eauto 2 .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost jprogr : duration LE : progr <= job_cost j NotIN : progr \notin job_preemptive_points j x : nat SIZE2 : x.+1 < size (job_preemptive_points j) N1 : nth 0 (job_preemptive_points j) x < progr N2 : progr < nth 0 (job_preemptive_points j) x.+1 ptl := nth 0 (job_preemptive_points j) x : nat ptr := nth 0 (job_preemptive_points j) x.+1 : nat
exists
x y : Datatypes_nat__canonical__eqtype_Equality,
x \in job_preemptive_points j /\
y \in job_preemptive_points j /\ x <> y
exists 0 , (job_cost j); repeat split .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost jprogr : duration LE : progr <= job_cost j NotIN : progr \notin job_preemptive_points j x : nat SIZE2 : x.+1 < size (job_preemptive_points j) N1 : nth 0 (job_preemptive_points j) x < progr N2 : progr < nth 0 (job_preemptive_points j) x.+1 ptl := nth 0 (job_preemptive_points j) x : nat ptr := nth 0 (job_preemptive_points j) x.+1 : nat
0 \in job_preemptive_points j
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost jprogr : duration LE : progr <= job_cost j NotIN : progr \notin job_preemptive_points j x : nat SIZE2 : x.+1 < size (job_preemptive_points j) N1 : nth 0 (job_preemptive_points j) x < progr N2 : progr < nth 0 (job_preemptive_points j) x.+1 ptl := nth 0 (job_preemptive_points j) x : nat ptr := nth 0 (job_preemptive_points j) x.+1 : nat
0 \in job_preemptive_points j
by eapply zero_in_preemption_points; eauto .
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost jprogr : duration LE : progr <= job_cost j NotIN : progr \notin job_preemptive_points j x : nat SIZE2 : x.+1 < size (job_preemptive_points j) N1 : nth 0 (job_preemptive_points j) x < progr N2 : progr < nth 0 (job_preemptive_points j) x.+1 ptl := nth 0 (job_preemptive_points j) x : nat ptr := nth 0 (job_preemptive_points j) x.+1 : nat
job_cost j \in job_preemptive_points j
by eapply job_cost_in_nonpreemptive_points; eauto .
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq FIX : valid_fixed_preemption_points_task_model arr_seq
ts BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq A1 : task_beginning_of_execution_in_preemption_points
ts A2 : task_end_of_execution_in_preemption_points ts A3 : nondecreasing_task_preemption_points ts A4 : consistent_job_segment_count arr_seq A5 : job_respects_segment_lengths arr_seq /\
task_segments_are_nonempty ts POS : 0 < job_cost jprogr : duration LE : progr <= job_cost j NotIN : progr \notin job_preemptive_points j x : nat SIZE2 : x.+1 < size (job_preemptive_points j) N1 : nth 0 (job_preemptive_points j) x < progr N2 : progr < nth 0 (job_preemptive_points j) x.+1 ptl := nth 0 (job_preemptive_points j) x : nat ptr := nth 0 (job_preemptive_points j) x.+1 : nat
0 <> job_cost j
by apply /eqP; rewrite eq_sym -lt0n; apply POS.
}
Qed .
(** Which together with lemma [valid_fixed_preemption_points_model]
gives us the fact that functions [job_preemptable and
task_preemption_points] defines a valid preemption model with
bounded non-preemptive regions. *)
Corollary fixed_preemption_points_model_is_valid_model_with_bounded_nonpreemptive_regions :
valid_model_with_bounded_nonpreemptive_segments arr_seq sched.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
valid_model_with_bounded_nonpreemptive_segments
arr_seq sched
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
valid_model_with_bounded_nonpreemptive_segments
arr_seq sched
split .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
valid_preemption_model arr_seq sched
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
valid_preemption_model arr_seq sched
by apply valid_fixed_preemption_points_model_lemma; destruct H_valid_fixed_preemption_points_model.
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job H4 : TaskPreemptionPoints Task arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched ts : seq Task H_valid_fixed_preemption_points_model : valid_fixed_preemption_points_model
arr_seq ts
model_with_bounded_nonpreemptive_segments arr_seq
by apply fixed_preemption_points_model_is_model_with_bounded_nonpreemptive_regions.
Qed .
End LimitedPreemptionsModel .
(** We add the above lemma into a "Hint Database" basic_rt_facts, so Coq will be able to apply them automatically. *)
Global Hint Resolve
valid_fixed_preemption_points_model_lemma
fixed_preemption_points_model_is_model_with_bounded_nonpreemptive_regions
fixed_preemption_points_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_rt_facts.