Library prosa.analysis.facts.preemption.task.floating
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.analysis.facts.preemption.job.limited.
Furthermore, we assume the task model with floating non-preemptive regions.
Require Import prosa.model.task.preemption.floating_nonpreemptive.
Require Import prosa.model.preemption.limited_preemptive.
Require Import prosa.model.preemption.limited_preemptive.
Platform for Floating Non-Preemptive 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 uni-processor preemption-aware schedule
of this arrival sequence ...
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_preemption_aware_schedule:
schedule_respects_preemption_model arr_seq sched.
Hypothesis H_preemption_aware_schedule:
schedule_respects_preemption_model arr_seq sched.
... where jobs do not execute before their arrival or after completion.
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
Next, we assume that preemption points are defined by the model
with floating non-preemptive regions.
Hypothesis H_valid_model_with_floating_nonpreemptive_regions:
valid_model_with_floating_nonpreemptive_regions arr_seq.
valid_model_with_floating_nonpreemptive_regions arr_seq.
Then, we prove that the [job_preemptable and
task_max_nonpreemptive_segment] functions define
a model with bounded non-preemptive regions.
Lemma floating_preemption_points_model_is_model_with_bounded_nonpreemptive_regions:
model_with_bounded_nonpreemptive_segments arr_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 658)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
============================
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
Proof.
intros j ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 661)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
============================
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
move: (H_valid_model_with_floating_nonpreemptive_regions) ⇒ LIM; move: LIM (LIM) ⇒ [LIM L] [[BEG [END NDEC]] MAX].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 708)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
============================
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
case: (posnP (job_cost j)) ⇒ [ZERO|POS].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 731)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
ZERO : job_cost j = 0
============================
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
subgoal 2 (ID 732) is:
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
- split.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 734)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
ZERO : job_cost j = 0
============================
job_respects_max_nonpreemptive_segment j
subgoal 2 (ID 735) is:
nonpreemptive_regions_have_bounded_length j
subgoal 3 (ID 732) is:
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
rewrite /job_respects_max_nonpreemptive_segment /job_max_nonpreemptive_segment
/lengths_of_segments /parameter.job_preemption_points; rewrite ZERO; simpl.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 783)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
ZERO : job_cost j = 0
============================
max0 (distances (if job_preemptable j 0 then [:: 0] else [::])) <=
task_max_nonpreemptive_segment (job_task j)
subgoal 2 (ID 735) is:
nonpreemptive_regions_have_bounded_length j
subgoal 3 (ID 732) is:
job_respects_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 735)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
ZERO : job_cost j = 0
============================
nonpreemptive_regions_have_bounded_length j
subgoal 2 (ID 732) is:
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
+ move ⇒ progr; rewrite ZERO leqn0; move ⇒ /andP [_ /eqP LE].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1062)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
ZERO : job_cost j = 0
progr : duration
LE : progr = 0
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
subgoal 2 (ID 732) is:
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
∃ 0; rewrite LE; split; first by apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1069)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
ZERO : job_cost j = 0
progr : duration
LE : progr = 0
============================
job_preemptable j 0
subgoal 2 (ID 732) is:
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
by eapply zero_in_preemption_points; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 732)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
============================
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
- split; last (move ⇒ progr /andP [_ LE]; destruct (progr \in job_preemption_points j) eqn:NotIN).
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1104)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
============================
job_respects_max_nonpreemptive_segment j
subgoal 2 (ID 1163) is:
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
subgoal 3 (ID 1164) is:
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
+ by apply MAX.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1163)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1164) 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 1164)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1271)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1296)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1358)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1363)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1368)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1373)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1372) is:
progr <= ptr <= progr + (job_max_nonpreemptive_segment j - ε)
----------------------------------------------------------------------------- *)
× by unfold job_preemptable, limited_preemptions_model; apply mem_nth.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1372)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1403)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1410)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1409) is:
ptr <= ptl + (job_max_nonpreemptive_segment j - ε) + 1
----------------------------------------------------------------------------- *)
-- rewrite addn1 ltn_add2r; apply N1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1409)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1420)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1436)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1452)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1470)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1471) is:
0 < max0 (lengths_of_segments j)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1470)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1475)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1482)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 (parameter.job_preemption_points j))
----------------------------------------------------------------------------- *)
erewrite job_parameters_max_np_to_job_limited; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1487)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1471)
subgoal 1 (ID 1471) is:
0 < max0 (lengths_of_segments j)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1471)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1471)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 3570)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 7919)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 7928)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 7932) is:
job_cost j \in job_preemption_points j
subgoal 3 (ID 7933) is:
0 <> job_cost j
----------------------------------------------------------------------------- *)
- by eapply zero_in_preemption_points; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 7932)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 7933) is:
0 <> job_cost j
----------------------------------------------------------------------------- *)
- by eapply job_cost_in_nonpreemptive_points; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 7933)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 658)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
============================
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
Proof.
intros j ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 661)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
============================
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
move: (H_valid_model_with_floating_nonpreemptive_regions) ⇒ LIM; move: LIM (LIM) ⇒ [LIM L] [[BEG [END NDEC]] MAX].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 708)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
============================
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
case: (posnP (job_cost j)) ⇒ [ZERO|POS].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 731)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
ZERO : job_cost j = 0
============================
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
subgoal 2 (ID 732) is:
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
- split.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 734)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
ZERO : job_cost j = 0
============================
job_respects_max_nonpreemptive_segment j
subgoal 2 (ID 735) is:
nonpreemptive_regions_have_bounded_length j
subgoal 3 (ID 732) is:
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
rewrite /job_respects_max_nonpreemptive_segment /job_max_nonpreemptive_segment
/lengths_of_segments /parameter.job_preemption_points; rewrite ZERO; simpl.
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 783)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
ZERO : job_cost j = 0
============================
max0 (distances (if job_preemptable j 0 then [:: 0] else [::])) <=
task_max_nonpreemptive_segment (job_task j)
subgoal 2 (ID 735) is:
nonpreemptive_regions_have_bounded_length j
subgoal 3 (ID 732) is:
job_respects_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 735)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
ZERO : job_cost j = 0
============================
nonpreemptive_regions_have_bounded_length j
subgoal 2 (ID 732) is:
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
+ move ⇒ progr; rewrite ZERO leqn0; move ⇒ /andP [_ /eqP LE].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1062)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
ZERO : job_cost j = 0
progr : duration
LE : progr = 0
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
subgoal 2 (ID 732) is:
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
∃ 0; rewrite LE; split; first by apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1069)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
ZERO : job_cost j = 0
progr : duration
LE : progr = 0
============================
job_preemptable j 0
subgoal 2 (ID 732) is:
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
by eapply zero_in_preemption_points; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 732)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
============================
job_respects_max_nonpreemptive_segment j /\
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
- split; last (move ⇒ progr /andP [_ LE]; destruct (progr \in job_preemption_points j) eqn:NotIN).
(* ----------------------------------[ coqtop ]---------------------------------
3 subgoals (ID 1104)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
============================
job_respects_max_nonpreemptive_segment j
subgoal 2 (ID 1163) is:
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
subgoal 3 (ID 1164) is:
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
+ by apply MAX.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1163)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1164) 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 1164)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1271)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1296)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1358)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1363)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1368)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1373)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1372) is:
progr <= ptr <= progr + (job_max_nonpreemptive_segment j - ε)
----------------------------------------------------------------------------- *)
× by unfold job_preemptable, limited_preemptions_model; apply mem_nth.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1372)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1403)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1410)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1409) is:
ptr <= ptl + (job_max_nonpreemptive_segment j - ε) + 1
----------------------------------------------------------------------------- *)
-- rewrite addn1 ltn_add2r; apply N1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1409)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1420)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1436)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1452)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1470)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1471) is:
0 < max0 (lengths_of_segments j)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1470)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1475)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1482)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 (parameter.job_preemption_points j))
----------------------------------------------------------------------------- *)
erewrite job_parameters_max_np_to_job_limited; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1487)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1471)
subgoal 1 (ID 1471) is:
0 < max0 (lengths_of_segments j)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1471)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 1471)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 3570)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 7919)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 7928)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 7932) is:
job_cost j \in job_preemption_points j
subgoal 3 (ID 7933) is:
0 <> job_cost j
----------------------------------------------------------------------------- *)
- by eapply zero_in_preemption_points; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 7932)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 7933) is:
0 <> job_cost j
----------------------------------------------------------------------------- *)
- by eapply job_cost_in_nonpreemptive_points; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 7933)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
j : Job
ARR : arrives_in arr_seq j
LIM : valid_limited_preemptions_job_model arr_seq
L : job_respects_task_max_np_segment arr_seq
BEG : beginning_of_execution_in_preemption_points arr_seq
END : end_of_execution_in_preemption_points arr_seq
NDEC : preemption_points_is_nondecreasing_sequence arr_seq
MAX : job_respects_task_max_np_segment arr_seq
POS : 0 < job_cost j
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 668)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
============================
valid_model_with_bounded_nonpreemptive_segments arr_seq sched
----------------------------------------------------------------------------- *)
Proof.
split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 670)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
============================
valid_preemption_model arr_seq sched
subgoal 2 (ID 671) is:
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
- apply valid_fixed_preemption_points_model_lemma; auto.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 676)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
============================
valid_limited_preemptions_job_model arr_seq
subgoal 2 (ID 671) is:
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
by apply H_valid_model_with_floating_nonpreemptive_regions.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 671)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
============================
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
- apply floating_preemption_points_model_is_model_with_bounded_nonpreemptive_regions.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End FloatingNonPreemptiveRegionsModel.
valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 668)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
============================
valid_model_with_bounded_nonpreemptive_segments arr_seq sched
----------------------------------------------------------------------------- *)
Proof.
split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 670)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
============================
valid_preemption_model arr_seq sched
subgoal 2 (ID 671) is:
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
- apply valid_fixed_preemption_points_model_lemma; auto.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 676)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
============================
valid_limited_preemptions_job_model arr_seq
subgoal 2 (ID 671) is:
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
by apply H_valid_model_with_floating_nonpreemptive_regions.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 671)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : TaskMaxNonpreemptiveSegment Task
H4 : JobPreemptionPoints Job
arr_seq : arrival_sequence Job
sched : schedule (ideal.processor_state Job)
H_preemption_aware_schedule : schedule_respects_preemption_model arr_seq
sched
H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq
============================
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
- apply floating_preemption_points_model_is_model_with_bounded_nonpreemptive_regions.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End FloatingNonPreemptiveRegionsModel.
We add the above lemma into a "Hint Database" basic_facts, so Coq will be able to apply them automatically.
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_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.