Library prosa.analysis.facts.preemption.task.nonpreemptive
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.13.0 (January 2021)
----------------------------------------------------------------------------- *)
Require Export prosa.analysis.facts.preemption.job.nonpreemptive.
Furthermore, we assume the fully non-preemptive task model.
Require Import prosa.model.preemption.fully_nonpreemptive.
Require Import prosa.model.task.preemption.fully_nonpreemptive.
Require Import prosa.model.task.preemption.fully_nonpreemptive.
Platform for Fully Non-Preemptive Model
In this section, we prove that instantiation of functions [job_preemptable and task_max_nonpreemptive_segment] to the fully non-preemptive model 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}.
Consider any arrival sequence with consistent arrivals.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
Next, consider any ideal non-preemptive uni-processor schedule of this arrival sequence...
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_nonpreemptive_sched : nonpreemptive_schedule sched.
Hypothesis H_nonpreemptive_sched : nonpreemptive_schedule 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.
Assume that a job cost cannot be larger than a task cost.
Then we prove that [fully_nonpreemptive_model] function
defines a model with bounded non-preemptive regions.
Lemma fully_nonpreemptive_model_is_model_with_bounded_nonpreemptive_regions:
model_with_bounded_nonpreemptive_segments arr_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 45)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
============================
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
Proof.
have F: ∀ n, n = 0 ∨ n > 0 by intros n; destruct n; [left | right].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 62)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
============================
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
intros j; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 67)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
============================
job_respects_max_nonpreemptive_segment j
subgoal 2 (ID 68) is:
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 67)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
============================
job_respects_max_nonpreemptive_segment j
----------------------------------------------------------------------------- *)
rewrite /job_respects_max_nonpreemptive_segment; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 81)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
============================
job_max_nonpreemptive_segment j <=
task_max_nonpreemptive_segment (job_task j)
----------------------------------------------------------------------------- *)
erewrite job_max_nps_is_job_cost; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 68) is:
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 68)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
============================
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
move ⇒ progr /andP [_ GE].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 139)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
move: (F (progr)) ⇒ [EQ | GT].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 153)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
EQ : progr = 0
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
subgoal 2 (ID 154) is:
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 153)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
EQ : progr = 0
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
∃ progr; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 158)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
EQ : progr = 0
============================
progr <= progr <= progr + (job_max_nonpreemptive_segment j - ε)
subgoal 2 (ID 159) is:
job_preemptable j progr
----------------------------------------------------------------------------- *)
- by apply/andP; split; [done | rewrite leq_addr].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 159)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
EQ : progr = 0
============================
job_preemptable j progr
----------------------------------------------------------------------------- *)
- rewrite /job_preemptable /fully_nonpreemptive_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 200)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
EQ : progr = 0
============================
model.preemption.fully_nonpreemptive.fully_nonpreemptive_model j progr
----------------------------------------------------------------------------- *)
by apply/orP; left; rewrite EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 154) is:
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 154)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
GT : 0 < progr
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 154)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
GT : 0 < progr
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
∃ (maxn progr (job_cost j)).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 232)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
GT : 0 < progr
============================
progr <= maxn progr (job_cost j) <=
progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j (maxn progr (job_cost j))
----------------------------------------------------------------------------- *)
have POS: 0 < job_cost j by apply leq_trans with progr.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 239)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
GT : 0 < progr
POS : 0 < job_cost j
============================
progr <= maxn progr (job_cost j) <=
progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j (maxn progr (job_cost j))
----------------------------------------------------------------------------- *)
split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 241)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
GT : 0 < progr
POS : 0 < job_cost j
============================
progr <= maxn progr (job_cost j) <=
progr + (job_max_nonpreemptive_segment j - ε)
subgoal 2 (ID 242) is:
job_preemptable j (maxn progr (job_cost j))
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 241)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
GT : 0 < progr
POS : 0 < job_cost j
============================
progr <= maxn progr (job_cost j) <=
progr + (job_max_nonpreemptive_segment j - ε)
----------------------------------------------------------------------------- *)
apply/andP; split; first by rewrite leq_maxl.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 269)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
GT : 0 < progr
POS : 0 < job_cost j
============================
maxn progr (job_cost j) <= progr + (job_max_nonpreemptive_segment j - ε)
----------------------------------------------------------------------------- *)
erewrite job_max_nps_is_job_cost; eauto 2; rewrite addnBA; last eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 293)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
GT : 0 < progr
POS : 0 < job_cost j
============================
maxn progr (job_cost j) <= progr + job_cost j - ε
----------------------------------------------------------------------------- *)
rewrite geq_max; apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 329)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
GT : 0 < progr
POS : 0 < job_cost j
============================
progr <= progr + job_cost j - ε
subgoal 2 (ID 330) is:
job_cost j <= progr + job_cost j - ε
----------------------------------------------------------------------------- *)
- rewrite -addnBA; last by eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 336)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
GT : 0 < progr
POS : 0 < job_cost j
============================
progr <= progr + (job_cost j - ε)
subgoal 2 (ID 330) is:
job_cost j <= progr + job_cost j - ε
----------------------------------------------------------------------------- *)
by rewrite leq_addr.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 330)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
GT : 0 < progr
POS : 0 < job_cost j
============================
job_cost j <= progr + job_cost j - ε
----------------------------------------------------------------------------- *)
- by rewrite addnC -addnBA // leq_addr.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 242) is:
job_preemptable j (maxn progr (job_cost j))
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 242)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
GT : 0 < progr
POS : 0 < job_cost j
============================
job_preemptable j (maxn progr (job_cost j))
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 242)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
GT : 0 < progr
POS : 0 < job_cost j
============================
job_preemptable j (maxn progr (job_cost j))
----------------------------------------------------------------------------- *)
apply/orP; right.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 409)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
GT : 0 < progr
POS : 0 < job_cost j
============================
maxn progr (job_cost j) == job_cost j
----------------------------------------------------------------------------- *)
rewrite eqn_leq; apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 439)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
GT : 0 < progr
POS : 0 < job_cost j
============================
maxn progr (job_cost j) <= job_cost j
subgoal 2 (ID 440) is:
job_cost j <= maxn progr (job_cost j)
----------------------------------------------------------------------------- *)
- by rewrite geq_max; apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 440)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
GT : 0 < progr
POS : 0 < job_cost j
============================
job_cost j <= maxn progr (job_cost j)
----------------------------------------------------------------------------- *)
- by rewrite leq_max; apply/orP; right.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
model_with_bounded_nonpreemptive_segments arr_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 45)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
============================
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
Proof.
have F: ∀ n, n = 0 ∨ n > 0 by intros n; destruct n; [left | right].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 62)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
============================
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
intros j; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 67)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
============================
job_respects_max_nonpreemptive_segment j
subgoal 2 (ID 68) is:
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 67)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
============================
job_respects_max_nonpreemptive_segment j
----------------------------------------------------------------------------- *)
rewrite /job_respects_max_nonpreemptive_segment; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 81)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
============================
job_max_nonpreemptive_segment j <=
task_max_nonpreemptive_segment (job_task j)
----------------------------------------------------------------------------- *)
erewrite job_max_nps_is_job_cost; eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 68) is:
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 68)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
============================
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
move ⇒ progr /andP [_ GE].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 139)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
move: (F (progr)) ⇒ [EQ | GT].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 153)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
EQ : progr = 0
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
subgoal 2 (ID 154) is:
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 153)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
EQ : progr = 0
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
∃ progr; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 158)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
EQ : progr = 0
============================
progr <= progr <= progr + (job_max_nonpreemptive_segment j - ε)
subgoal 2 (ID 159) is:
job_preemptable j progr
----------------------------------------------------------------------------- *)
- by apply/andP; split; [done | rewrite leq_addr].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 159)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
EQ : progr = 0
============================
job_preemptable j progr
----------------------------------------------------------------------------- *)
- rewrite /job_preemptable /fully_nonpreemptive_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 200)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
EQ : progr = 0
============================
model.preemption.fully_nonpreemptive.fully_nonpreemptive_model j progr
----------------------------------------------------------------------------- *)
by apply/orP; left; rewrite EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 154) is:
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 154)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
GT : 0 < progr
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 154)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
GT : 0 < progr
============================
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
∃ (maxn progr (job_cost j)).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 232)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
GT : 0 < progr
============================
progr <= maxn progr (job_cost j) <=
progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j (maxn progr (job_cost j))
----------------------------------------------------------------------------- *)
have POS: 0 < job_cost j by apply leq_trans with progr.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 239)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
GT : 0 < progr
POS : 0 < job_cost j
============================
progr <= maxn progr (job_cost j) <=
progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j (maxn progr (job_cost j))
----------------------------------------------------------------------------- *)
split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 241)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
GT : 0 < progr
POS : 0 < job_cost j
============================
progr <= maxn progr (job_cost j) <=
progr + (job_max_nonpreemptive_segment j - ε)
subgoal 2 (ID 242) is:
job_preemptable j (maxn progr (job_cost j))
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 241)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
GT : 0 < progr
POS : 0 < job_cost j
============================
progr <= maxn progr (job_cost j) <=
progr + (job_max_nonpreemptive_segment j - ε)
----------------------------------------------------------------------------- *)
apply/andP; split; first by rewrite leq_maxl.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 269)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
GT : 0 < progr
POS : 0 < job_cost j
============================
maxn progr (job_cost j) <= progr + (job_max_nonpreemptive_segment j - ε)
----------------------------------------------------------------------------- *)
erewrite job_max_nps_is_job_cost; eauto 2; rewrite addnBA; last eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 293)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
GT : 0 < progr
POS : 0 < job_cost j
============================
maxn progr (job_cost j) <= progr + job_cost j - ε
----------------------------------------------------------------------------- *)
rewrite geq_max; apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 329)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
GT : 0 < progr
POS : 0 < job_cost j
============================
progr <= progr + job_cost j - ε
subgoal 2 (ID 330) is:
job_cost j <= progr + job_cost j - ε
----------------------------------------------------------------------------- *)
- rewrite -addnBA; last by eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 336)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
GT : 0 < progr
POS : 0 < job_cost j
============================
progr <= progr + (job_cost j - ε)
subgoal 2 (ID 330) is:
job_cost j <= progr + job_cost j - ε
----------------------------------------------------------------------------- *)
by rewrite leq_addr.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 330)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
GT : 0 < progr
POS : 0 < job_cost j
============================
job_cost j <= progr + job_cost j - ε
----------------------------------------------------------------------------- *)
- by rewrite addnC -addnBA // leq_addr.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal
subgoal 1 (ID 242) is:
job_preemptable j (maxn progr (job_cost j))
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 242)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
GT : 0 < progr
POS : 0 < job_cost j
============================
job_preemptable j (maxn progr (job_cost j))
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 242)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
GT : 0 < progr
POS : 0 < job_cost j
============================
job_preemptable j (maxn progr (job_cost j))
----------------------------------------------------------------------------- *)
apply/orP; right.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 409)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
GT : 0 < progr
POS : 0 < job_cost j
============================
maxn progr (job_cost j) == job_cost j
----------------------------------------------------------------------------- *)
rewrite eqn_leq; apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 439)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
GT : 0 < progr
POS : 0 < job_cost j
============================
maxn progr (job_cost j) <= job_cost j
subgoal 2 (ID 440) is:
job_cost j <= maxn progr (job_cost j)
----------------------------------------------------------------------------- *)
- by rewrite geq_max; apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 440)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
progr : duration
GE : progr <= job_cost j
GT : 0 < progr
POS : 0 < job_cost j
============================
job_cost j <= maxn progr (job_cost j)
----------------------------------------------------------------------------- *)
- by rewrite leq_max; apply/orP; right.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
Which together with lemma [valid_fully_nonpreemptive_model]
gives us the fact that [fully_nonpreemptive_model] defined a valid
preemption model with bounded non-preemptive regions.
Corollary fully_nonpreemptive_model_is_valid_model_with_bounded_nonpreemptive_regions:
valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 56)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
============================
valid_model_with_bounded_nonpreemptive_segments arr_seq sched
----------------------------------------------------------------------------- *)
Proof.
split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 58)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
============================
valid_preemption_model arr_seq sched
subgoal 2 (ID 59) is:
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
- by apply valid_fully_nonpreemptive_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 59)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
============================
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
- by apply fully_nonpreemptive_model_is_model_with_bounded_nonpreemptive_regions.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End FullyNonPreemptiveModel.
valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 56)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
============================
valid_model_with_bounded_nonpreemptive_segments arr_seq sched
----------------------------------------------------------------------------- *)
Proof.
split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 58)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
============================
valid_preemption_model arr_seq sched
subgoal 2 (ID 59) is:
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
- by apply valid_fully_nonpreemptive_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 59)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
H_arrival_times_are_consistent : consistent_arrival_times arr_seq
sched : schedule (ideal.processor_state Job)
H_nonpreemptive_sched : nonpreemptive_schedule 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_job_cost : arrivals_have_valid_job_costs arr_seq
============================
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
- by apply fully_nonpreemptive_model_is_model_with_bounded_nonpreemptive_regions.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End FullyNonPreemptiveModel.
We add the above lemma into a "Hint Database" basic_facts, so Coq will be able to apply them automatically.
Global Hint Resolve
valid_fully_nonpreemptive_model
fully_nonpreemptive_model_is_model_with_bounded_nonpreemptive_regions
fully_nonpreemptive_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_facts.
valid_fully_nonpreemptive_model
fully_nonpreemptive_model_is_model_with_bounded_nonpreemptive_regions
fully_nonpreemptive_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_facts.