Library prosa.analysis.facts.preemption.task.nonpreemptive
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
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 659)
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 677)
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 682)
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 683) is:
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 682)
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 696)
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 (ID 683)
subgoal 1 (ID 683) is:
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 683)
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 758)
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 772)
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 773) is:
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 772)
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 777)
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 778) is:
job_preemptable j progr
----------------------------------------------------------------------------- *)
- by apply/andP; split; [done | rewrite leq_addr].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 778)
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 819)
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 (ID 773)
subgoal 1 (ID 773) is:
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 773)
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 773)
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 851)
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 858)
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 860)
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 861) is:
job_preemptable j (maxn progr (job_cost j))
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 860)
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 888)
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 914)
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 951)
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 952) is:
job_cost j <= progr + job_cost j - ε
----------------------------------------------------------------------------- *)
- rewrite -addnBA; last by eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 958)
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 952) is:
job_cost j <= progr + job_cost j - ε
----------------------------------------------------------------------------- *)
by rewrite leq_addr.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 952)
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 (ID 861)
subgoal 1 (ID 861) is:
job_preemptable j (maxn progr (job_cost j))
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 861)
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 861)
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 1033)
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 1063)
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 1064) is:
job_cost j <= maxn progr (job_cost j)
----------------------------------------------------------------------------- *)
- by rewrite geq_max; apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1064)
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 659)
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 677)
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 682)
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 683) is:
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 682)
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 696)
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 (ID 683)
subgoal 1 (ID 683) is:
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 683)
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 758)
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 772)
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 773) is:
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 772)
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 777)
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 778) is:
job_preemptable j progr
----------------------------------------------------------------------------- *)
- by apply/andP; split; [done | rewrite leq_addr].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 778)
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 819)
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 (ID 773)
subgoal 1 (ID 773) is:
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 773)
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 773)
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 851)
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 858)
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 860)
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 861) is:
job_preemptable j (maxn progr (job_cost j))
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 860)
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 888)
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 914)
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 951)
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 952) is:
job_cost j <= progr + job_cost j - ε
----------------------------------------------------------------------------- *)
- rewrite -addnBA; last by eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 958)
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 952) is:
job_cost j <= progr + job_cost j - ε
----------------------------------------------------------------------------- *)
by rewrite leq_addr.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 952)
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 (ID 861)
subgoal 1 (ID 861) is:
job_preemptable j (maxn progr (job_cost j))
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 861)
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 861)
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 1033)
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 1063)
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 1064) is:
job_cost j <= maxn progr (job_cost j)
----------------------------------------------------------------------------- *)
- by rewrite geq_max; apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1064)
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 670)
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 672)
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 673) is:
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
- by apply valid_fully_nonpreemptive_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 673)
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 670)
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 672)
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 673) is:
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
- by apply valid_fully_nonpreemptive_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 673)
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.
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.