Built with
Alectryon , running Coq+SerAPI v8.15.0+0.15.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.model.preemption.limited_preemptive.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Require Export prosa.model.task.preemption.floating_nonpreemptive.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Export prosa.analysis.facts.preemption.job.limited.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
(** * Platform for Floating Non-Preemptive Regions Model *)
(** In this section, we prove that instantiation of functions
[job_preemptable] and [task_max_nonpreemptive_segment] for the model
with floating non-preemptive regions indeed defines a valid
preemption model with bounded non-preemptive regions. *)
Section FloatingNonPreemptiveRegionsModel .
(** 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}.
(** In addition, we assume the existence of a function mapping a
task to its maximal non-preemptive segment ... *)
Context `{TaskMaxNonpreemptiveSegment Task}.
(** .. and the existence of functions mapping a
job to the sequence of its preemption points, ... *)
Context `{JobPreemptionPoints Job}.
(** ... 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 ideal uni-processor preemption-aware schedule
of this arrival sequence ... *)
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_preemption_aware_schedule :
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.
(** Next, we assume that preemption points are defined by the model
with floating non-preemptive regions. *)
Hypothesis H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq.
(** Then, we prove that the [job_preemptable and
task_max_nonpreemptive_segment] functions define
a model with bounded non-preemptive regions. *)
Lemma floating_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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq
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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq
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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
move : (H_valid_model_with_floating_nonpreemptive_regions) => LIM; move : LIM (LIM) => [LIM L] [[BEG [END NDEC]] MAX].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq
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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq ZERO : job_cost j = 0
max0
(distances
(if job_preemptable j 0 then [:: 0 ] else [::])) <=
task_max_nonpreemptive_segment (job_task j)
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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq ZERO : job_cost j = 0
nonpreemptive_regions_have_bounded_length j
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq ZERO : job_cost j = 0 progr : duration LE : progr = 0
exists pp : duration,
progr <= pp <=
progr + (job_max_nonpreemptive_segment j - ε) /\
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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq POS : 0 < job_cost j
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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq POS : 0 < job_cost j
job_respects_max_nonpreemptive_segment j
by apply MAX.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 - ε) /\
job_preemptable j pp
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 - ε) /\
job_preemptable j pp
by exists progr ; split ; first apply /andP; first split ; rewrite ?leq_addr // conversion_preserves_equivalence.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 - ε) /\
job_preemptable j pp
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 - ε) /\
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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 - ε) /\
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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 - ε) /\
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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 - ε) /\
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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 - ε) /\
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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 - ε) /\
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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 - ε)
* Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 - ε)
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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 - ε)
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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 <=
progr + (job_max_nonpreemptive_segment j - ε)
-- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 <=
progr + (job_max_nonpreemptive_segment j - ε)
rewrite addn1 ltn_add2r; apply N1.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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
-- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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
unfold job_max_nonpreemptive_segment.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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
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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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
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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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
rewrite !subn1 !addn1 prednK.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 : nat_eqType,
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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq j : Job ARR : arrives_in arr_seq j LIM : valid_limited_preemptions_job_model arr_seq L : job_respects_task_max_np_segment arr_seq 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 MAX : job_respects_task_max_np_segment arr_seq 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_max_nonpreemptive_segment] define a valid preemption model
with bounded non-preemptive regions. *)
Corollary floating_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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq
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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq
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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq
valid_preemption_model arr_seq sched
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq
valid_preemption_model arr_seq sched
apply valid_fixed_preemption_points_model_lemma; auto .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq
valid_limited_preemptions_job_model arr_seq
by apply H_valid_model_with_floating_nonpreemptive_regions.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq
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 : TaskMaxNonpreemptiveSegment Task H4 : JobPreemptionPoints Job arr_seq : arrival_sequence Job sched : schedule (ideal.processor_state Job) H_preemption_aware_schedule : 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 H_valid_model_with_floating_nonpreemptive_regions : valid_model_with_floating_nonpreemptive_regions
arr_seq
model_with_bounded_nonpreemptive_segments arr_seq
apply floating_preemption_points_model_is_model_with_bounded_nonpreemptive_regions.
Qed .
End FloatingNonPreemptiveRegionsModel .
(** 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
floating_preemption_points_model_is_model_with_bounded_nonpreemptive_regions
floating_preemption_points_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_rt_facts.