Library rt.restructuring.analysis.basic_facts.preemption.task.floating
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.10.1 (October 2019)
----------------------------------------------------------------------------- *)
From rt.util Require Import all nondecreasing.
From rt.restructuring.behavior Require Import all.
From rt.restructuring Require Import job task.
From rt.restructuring.model.preemption Require Import
valid_model job.parameters task.parameters rtc_threshold.valid_rtct
job.instance.limited valid_schedule task.instance.floating.
From rt.restructuring.analysis.basic_facts.preemption Require Import job.limited.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
Platform for Floating Non-Premptive Regions Model
In this section, we prove that instantiation of functions [job_preemptable and task_max_nonpreemptive_segment] to the model with floating non-preemptive regions indeed defines a valid preemption model with bounded non-preemptive regions.
Consider any type of tasks ...
... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
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 ...
.. and the existence of functions mapping a
job to the sequence of its preemption points.
Consider any arrival sequence.
Next, consider any ideal uniprocessor preemption-aware schedule
of this arrival sequence ...
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_preemption_aware_schedule:
valid_schedule_with_limited_preemptions arr_seq sched.
Hypothesis H_preemption_aware_schedule:
valid_schedule_with_limited_preemptions 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.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
Next, we assume that preemption points are defined by the model
with floating nonpreemptive regions.
Hypothesis H_valid_model_with_floating_nonpreemptive_regions:
valid_model_with_floating_nonpreemptive_regions arr_seq.
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 nonpremtive regions.
Lemma floating_preemption_points_model_is_model_with_bounded_nonpreemptive_regions:
model_with_bounded_nonpreemptive_segments arr_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 192)
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 : valid_schedule_with_limited_preemptions
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.
intros j ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 195)
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 : valid_schedule_with_limited_preemptions
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_max_nonpreemptive_segment_le_task_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].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 242)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
============================
job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
case: (posnP (job_cost j)) ⇒ [ZERO|POS].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 265)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
ZERO : job_cost j = 0
============================
job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
subgoal 2 (ID 266) is:
job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
- split.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 268)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
ZERO : job_cost j = 0
============================
job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j
subgoal 2 (ID 269) is:
nonpreemptive_regions_have_bounded_length j
subgoal 3 (ID 266) is:
job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
rewrite /job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment /job_max_nonpreemptive_segment
/lengths_of_segments /parameters.job_preemption_points; rewrite ZERO; simpl.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 317)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_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)
subgoal 2 (ID 269) is:
nonpreemptive_regions_have_bounded_length j
subgoal 3 (ID 266) is:
job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
rewrite /job_preemptable /limited_preemptions_model; erewrite zero_in_preemption_points; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 269)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
ZERO : job_cost j = 0
============================
nonpreemptive_regions_have_bounded_length j
subgoal 2 (ID 266) is:
job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
+ move ⇒ progr; rewrite ZERO leqn0; move ⇒ /andP [_ /eqP LE].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 596)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_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
subgoal 2 (ID 266) is:
job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
∃ 0; rewrite LE; split; first by apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 603)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
ZERO : job_cost j = 0
progr : duration
LE : progr = 0
============================
job_preemptable j 0
subgoal 2 (ID 266) is:
job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
by eapply zero_in_preemption_points; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 266)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
============================
job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
- split; last (move ⇒ progr /andP [_ LE]; destruct (progr \in job_preemption_points j) eqn:NotIN).
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 638)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
============================
job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j
subgoal 2 (ID 697) is:
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
subgoal 3 (ID 698) is:
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
+ by apply MAX.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 697)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : (progr \in job_preemption_points j) = true
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
subgoal 2 (ID 698) is:
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
+ ∃ progr; split; first apply/andP; first split; rewrite ?leq_addr; by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 698)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : (progr \in job_preemption_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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 805)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 830)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N : nth 0 (job_preemption_points j) x < progr <
nth 0 (job_preemption_points j) (succn x)
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
move: N ⇒ /andP [N1 N2].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 892)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
set ptl := nth 0 (job_preemption_points j) x.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 897)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
set ptr := nth 0 (job_preemption_points j) x.+1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 902)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
∃ ptr; split; first last.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 907)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
job_preemptable j ptr
subgoal 2 (ID 906) is:
progr <= ptr <= progr + (job_max_nonpreemptive_segment j - ε)
----------------------------------------------------------------------------- *)
× by unfold job_preemptable, limited_preemptions_model; apply mem_nth.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 906)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
progr <= ptr <= progr + (job_max_nonpreemptive_segment j - ε)
----------------------------------------------------------------------------- *)
× apply/andP; split; first by apply ltnW.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 937)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
ptr <= progr + (job_max_nonpreemptive_segment j - ε)
----------------------------------------------------------------------------- *)
apply leq_trans with (ptl + (job_max_nonpreemptive_segment j - ε) + 1); first last.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 944)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
ptl + (job_max_nonpreemptive_segment j - ε) + 1 <=
progr + (job_max_nonpreemptive_segment j - ε)
subgoal 2 (ID 943) is:
ptr <= ptl + (job_max_nonpreemptive_segment j - ε) + 1
----------------------------------------------------------------------------- *)
-- rewrite addn1 ltn_add2r; apply N1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 943)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
ptr <= ptl + (job_max_nonpreemptive_segment j - ε) + 1
----------------------------------------------------------------------------- *)
-- unfold job_max_nonpreemptive_segment.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 954)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
ptr <= ptl + (max0 (lengths_of_segments j) - ε) + 1
----------------------------------------------------------------------------- *)
rewrite -addnA -leq_subLR -(leq_add2r 1).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 970)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
ptr - ptl + 1 <= max0 (lengths_of_segments j) - ε + 1 + 1
----------------------------------------------------------------------------- *)
rewrite [in X in _ ≤ X]addnC -leq_subLR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 986)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
ptr - ptl + 1 - 1 <= max0 (lengths_of_segments j) - ε + 1
----------------------------------------------------------------------------- *)
rewrite !subn1 !addn1 prednK.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1004)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
predn (succn (ptr - ptl)) <= max0 (lengths_of_segments j)
subgoal 2 (ID 1005) is:
0 < max0 (lengths_of_segments j)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1004)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
predn (succn (ptr - ptl)) <= max0 (lengths_of_segments j)
----------------------------------------------------------------------------- *)
rewrite -[_.+1.-1]pred_Sn.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1009)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
ptr - ptl <= max0 (lengths_of_segments j)
----------------------------------------------------------------------------- *)
rewrite /lengths_of_segments.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1016)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
ptr - ptl <= max0 (distances (parameters.job_preemption_points j))
----------------------------------------------------------------------------- *)
erewrite job_parameters_max_np_to_job_limited; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1021)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
ptr - ptl <= max0 (distances (job_preemption_points j))
----------------------------------------------------------------------------- *)
by apply distance_between_neighboring_elements_le_max_distance_in_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1005)
subgoal 1 (ID 1005) is:
0 < max0 (lengths_of_segments j)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1005)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
0 < max0 (lengths_of_segments j)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1005)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
0 < max0 (lengths_of_segments j)
----------------------------------------------------------------------------- *)
rewrite /lengths_of_segments; erewrite job_parameters_max_np_to_job_limited; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 3104)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
0 < max0 (distances (job_preemption_points j))
----------------------------------------------------------------------------- *)
apply max_distance_in_nontrivial_seq_is_positive; first by eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 7453)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
exists x0 y : nat_eqType,
x0 \in job_preemption_points j /\
y \in job_preemption_points j /\ x0 <> y
----------------------------------------------------------------------------- *)
∃ 0, (job_cost j); repeat split.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 7462)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
0 \in job_preemption_points j
subgoal 2 (ID 7466) is:
job_cost j \in job_preemption_points j
subgoal 3 (ID 7467) is:
0 <> job_cost j
----------------------------------------------------------------------------- *)
- by eapply zero_in_preemption_points; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 7466)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
job_cost j \in job_preemption_points j
subgoal 2 (ID 7467) is:
0 <> job_cost j
----------------------------------------------------------------------------- *)
- by eapply job_cost_in_nonpreemptive_points; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 7467)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
0 <> job_cost j
----------------------------------------------------------------------------- *)
- by apply/eqP; rewrite eq_sym -lt0n; apply POS.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
model_with_bounded_nonpreemptive_segments arr_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 192)
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 : valid_schedule_with_limited_preemptions
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.
intros j ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 195)
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 : valid_schedule_with_limited_preemptions
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_max_nonpreemptive_segment_le_task_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].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 242)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
============================
job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
case: (posnP (job_cost j)) ⇒ [ZERO|POS].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 265)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
ZERO : job_cost j = 0
============================
job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
subgoal 2 (ID 266) is:
job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
- split.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 268)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
ZERO : job_cost j = 0
============================
job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j
subgoal 2 (ID 269) is:
nonpreemptive_regions_have_bounded_length j
subgoal 3 (ID 266) is:
job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
rewrite /job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment /job_max_nonpreemptive_segment
/lengths_of_segments /parameters.job_preemption_points; rewrite ZERO; simpl.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 317)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_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)
subgoal 2 (ID 269) is:
nonpreemptive_regions_have_bounded_length j
subgoal 3 (ID 266) is:
job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
rewrite /job_preemptable /limited_preemptions_model; erewrite zero_in_preemption_points; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 269)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
ZERO : job_cost j = 0
============================
nonpreemptive_regions_have_bounded_length j
subgoal 2 (ID 266) is:
job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
+ move ⇒ progr; rewrite ZERO leqn0; move ⇒ /andP [_ /eqP LE].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 596)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_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
subgoal 2 (ID 266) is:
job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
∃ 0; rewrite LE; split; first by apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 603)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
ZERO : job_cost j = 0
progr : duration
LE : progr = 0
============================
job_preemptable j 0
subgoal 2 (ID 266) is:
job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
by eapply zero_in_preemption_points; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 266)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
============================
job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
- split; last (move ⇒ progr /andP [_ LE]; destruct (progr \in job_preemption_points j) eqn:NotIN).
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 638)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
============================
job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j
subgoal 2 (ID 697) is:
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
subgoal 3 (ID 698) is:
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
+ by apply MAX.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 697)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : (progr \in job_preemption_points j) = true
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
subgoal 2 (ID 698) is:
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
+ ∃ progr; split; first apply/andP; first split; rewrite ?leq_addr; by done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 698)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : (progr \in job_preemption_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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 805)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 830)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N : nth 0 (job_preemption_points j) x < progr <
nth 0 (job_preemption_points j) (succn x)
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
move: N ⇒ /andP [N1 N2].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 892)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
set ptl := nth 0 (job_preemption_points j) x.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 897)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
set ptr := nth 0 (job_preemption_points j) x.+1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 902)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
∃ ptr; split; first last.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 907)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
job_preemptable j ptr
subgoal 2 (ID 906) is:
progr <= ptr <= progr + (job_max_nonpreemptive_segment j - ε)
----------------------------------------------------------------------------- *)
× by unfold job_preemptable, limited_preemptions_model; apply mem_nth.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 906)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
progr <= ptr <= progr + (job_max_nonpreemptive_segment j - ε)
----------------------------------------------------------------------------- *)
× apply/andP; split; first by apply ltnW.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 937)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
ptr <= progr + (job_max_nonpreemptive_segment j - ε)
----------------------------------------------------------------------------- *)
apply leq_trans with (ptl + (job_max_nonpreemptive_segment j - ε) + 1); first last.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 944)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
ptl + (job_max_nonpreemptive_segment j - ε) + 1 <=
progr + (job_max_nonpreemptive_segment j - ε)
subgoal 2 (ID 943) is:
ptr <= ptl + (job_max_nonpreemptive_segment j - ε) + 1
----------------------------------------------------------------------------- *)
-- rewrite addn1 ltn_add2r; apply N1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 943)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
ptr <= ptl + (job_max_nonpreemptive_segment j - ε) + 1
----------------------------------------------------------------------------- *)
-- unfold job_max_nonpreemptive_segment.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 954)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
ptr <= ptl + (max0 (lengths_of_segments j) - ε) + 1
----------------------------------------------------------------------------- *)
rewrite -addnA -leq_subLR -(leq_add2r 1).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 970)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
ptr - ptl + 1 <= max0 (lengths_of_segments j) - ε + 1 + 1
----------------------------------------------------------------------------- *)
rewrite [in X in _ ≤ X]addnC -leq_subLR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 986)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
ptr - ptl + 1 - 1 <= max0 (lengths_of_segments j) - ε + 1
----------------------------------------------------------------------------- *)
rewrite !subn1 !addn1 prednK.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1004)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
predn (succn (ptr - ptl)) <= max0 (lengths_of_segments j)
subgoal 2 (ID 1005) is:
0 < max0 (lengths_of_segments j)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1004)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
predn (succn (ptr - ptl)) <= max0 (lengths_of_segments j)
----------------------------------------------------------------------------- *)
rewrite -[_.+1.-1]pred_Sn.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1009)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
ptr - ptl <= max0 (lengths_of_segments j)
----------------------------------------------------------------------------- *)
rewrite /lengths_of_segments.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1016)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
ptr - ptl <= max0 (distances (parameters.job_preemption_points j))
----------------------------------------------------------------------------- *)
erewrite job_parameters_max_np_to_job_limited; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1021)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
ptr - ptl <= max0 (distances (job_preemption_points j))
----------------------------------------------------------------------------- *)
by apply distance_between_neighboring_elements_le_max_distance_in_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1005)
subgoal 1 (ID 1005) is:
0 < max0 (lengths_of_segments j)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1005)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
0 < max0 (lengths_of_segments j)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1005)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
0 < max0 (lengths_of_segments j)
----------------------------------------------------------------------------- *)
rewrite /lengths_of_segments; erewrite job_parameters_max_np_to_job_limited; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 3104)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
0 < max0 (distances (job_preemption_points j))
----------------------------------------------------------------------------- *)
apply max_distance_in_nontrivial_seq_is_positive; first by eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 7453)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
exists x0 y : nat_eqType,
x0 \in job_preemption_points j /\
y \in job_preemption_points j /\ x0 <> y
----------------------------------------------------------------------------- *)
∃ 0, (job_cost j); repeat split.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 7462)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
0 \in job_preemption_points j
subgoal 2 (ID 7466) is:
job_cost j \in job_preemption_points j
subgoal 3 (ID 7467) is:
0 <> job_cost j
----------------------------------------------------------------------------- *)
- by eapply zero_in_preemption_points; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 7466)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
job_cost j \in job_preemption_points j
subgoal 2 (ID 7467) is:
0 <> job_cost j
----------------------------------------------------------------------------- *)
- by eapply job_cost_in_nonpreemptive_points; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 7467)
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 : valid_schedule_with_limited_preemptions
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_max_np_segment_le_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_max_np_segment_le_task_max_np_segment arr_seq
POS : 0 < job_cost j
progr : duration
LE : progr <= job_cost j
NotIN : progr \notin job_preemption_points j
x : nat
SIZE2 : succn x < size (job_preemption_points j)
N1 : nth 0 (job_preemption_points j) x < progr
N2 : progr < nth 0 (job_preemption_points j) (succn x)
ptl := nth 0 (job_preemption_points j) x : nat
ptr := nth 0 (job_preemption_points j) (succn x) : nat
============================
0 <> job_cost j
----------------------------------------------------------------------------- *)
- by apply/eqP; rewrite eq_sym -lt0n; apply POS.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 202)
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 : valid_schedule_with_limited_preemptions
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.
split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 204)
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 : valid_schedule_with_limited_preemptions
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
subgoal 2 (ID 205) is:
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
- apply valid_fixed_preemption_points_model_lemma; auto.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 210)
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 : valid_schedule_with_limited_preemptions
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
subgoal 2 (ID 205) is:
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
by apply H_valid_model_with_floating_nonpreemptive_regions.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 205)
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 : valid_schedule_with_limited_preemptions
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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End FloatingNonPremptiveRegionsModel.
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_facts.
valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 202)
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 : valid_schedule_with_limited_preemptions
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.
split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 204)
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 : valid_schedule_with_limited_preemptions
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
subgoal 2 (ID 205) is:
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
- apply valid_fixed_preemption_points_model_lemma; auto.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 210)
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 : valid_schedule_with_limited_preemptions
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
subgoal 2 (ID 205) is:
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
by apply H_valid_model_with_floating_nonpreemptive_regions.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 205)
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 : valid_schedule_with_limited_preemptions
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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End FloatingNonPremptiveRegionsModel.
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_facts.