Library rt.restructuring.analysis.basic_facts.preemption.task.nonpreemptive
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.10.1 (October 2019)
----------------------------------------------------------------------------- *)
From rt.util Require Import all.
From rt.restructuring.behavior Require Import all.
From rt.restructuring.analysis.basic_facts Require Import all.
From rt.restructuring.model Require Import job task.
From rt.restructuring.model.schedule Require Import nonpreemptive.
From rt.restructuring.model.preemption Require Import
job.instance.nonpreemptive task.instance.nonpreemptive.
From rt.restructuring.analysis.basic_facts.preemption Require Import
job.nonpreemptive.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
Platform for Fully Non-Premptive 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 uniprocessor schedule of this arrival sequence...
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_nonpreemptive_sched : is_nonpreemptive_schedule sched.
Hypothesis H_nonpreemptive_sched : is_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 nonpremtive regions.
Lemma fully_nonpreemptive_model_is_model_with_bounded_nonpreemptive_regions:
model_with_bounded_nonpreemptive_segments arr_seq.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 195)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 213)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
arr_seq
F : forall n : nat, n = 0 \/ 0 < n
============================
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
intros j; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 218)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
============================
job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j
subgoal 2 (ID 219) is:
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 218)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
============================
job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j
----------------------------------------------------------------------------- *)
rewrite /job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment; eauto 2.
(* ----------------------------------[ 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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 219)
subgoal 1 (ID 219) is:
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 219)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 294)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 308)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 309) is:
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 308)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 313)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 314) is:
job_preemptable j progr
----------------------------------------------------------------------------- *)
- by apply/andP; split; [done | rewrite leq_addr].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 314)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 355)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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.instance.nonpreemptive.fully_nonpreemptive_model j progr
----------------------------------------------------------------------------- *)
by apply/orP; left; rewrite EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 309)
subgoal 1 (ID 309) is:
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 309)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 309)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 387)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 394)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 396)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 397) is:
job_preemptable j (maxn progr (job_cost j))
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 396)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 424)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 450)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 487)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 488) is:
job_cost j <= progr + job_cost j - ε
----------------------------------------------------------------------------- *)
- rewrite -addnBA; last by eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 494)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 488) is:
job_cost j <= progr + job_cost j - ε
----------------------------------------------------------------------------- *)
by rewrite leq_addr.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 488)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 397)
subgoal 1 (ID 397) is:
job_preemptable j (maxn progr (job_cost j))
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 397)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 397)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 569)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 599)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 600) is:
job_cost j <= maxn progr (job_cost j)
----------------------------------------------------------------------------- *)
- by rewrite geq_max; apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 600)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 195)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 213)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
arr_seq
F : forall n : nat, n = 0 \/ 0 < n
============================
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
intros j; split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 218)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
============================
job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j
subgoal 2 (ID 219) is:
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 218)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
arr_seq
F : forall n : nat, n = 0 \/ 0 < n
j : Job
H3 : arrives_in arr_seq j
============================
job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j
----------------------------------------------------------------------------- *)
rewrite /job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment; eauto 2.
(* ----------------------------------[ 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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 219)
subgoal 1 (ID 219) is:
nonpreemptive_regions_have_bounded_length j
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 219)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 294)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 308)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 309) is:
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 308)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 313)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 314) is:
job_preemptable j progr
----------------------------------------------------------------------------- *)
- by apply/andP; split; [done | rewrite leq_addr].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 314)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 355)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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.instance.nonpreemptive.fully_nonpreemptive_model j progr
----------------------------------------------------------------------------- *)
by apply/orP; left; rewrite EQ.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 309)
subgoal 1 (ID 309) is:
exists pp : duration,
progr <= pp <= progr + (job_max_nonpreemptive_segment j - ε) /\
job_preemptable j pp
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 309)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 309)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 387)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 394)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 396)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 397) is:
job_preemptable j (maxn progr (job_cost j))
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 396)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 424)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 450)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 487)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 488) is:
job_cost j <= progr + job_cost j - ε
----------------------------------------------------------------------------- *)
- rewrite -addnBA; last by eauto 2.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 494)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 488) is:
job_cost j <= progr + job_cost j - ε
----------------------------------------------------------------------------- *)
by rewrite leq_addr.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 488)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 397)
subgoal 1 (ID 397) is:
job_preemptable j (maxn progr (job_cost j))
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 397)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 397)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 569)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 599)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 600) is:
job_cost j <= maxn progr (job_cost j)
----------------------------------------------------------------------------- *)
- by rewrite geq_max; apply/andP; split.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 600)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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 206)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
arr_seq
============================
valid_model_with_bounded_nonpreemptive_segments arr_seq sched
----------------------------------------------------------------------------- *)
Proof.
split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 208)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
arr_seq
============================
valid_preemption_model arr_seq sched
subgoal 2 (ID 209) is:
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
- by apply valid_fully_nonpreemptive_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 209)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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.
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_model_with_bounded_nonpreemptive_segments arr_seq sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 206)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
arr_seq
============================
valid_model_with_bounded_nonpreemptive_segments arr_seq sched
----------------------------------------------------------------------------- *)
Proof.
split.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 208)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
arr_seq
============================
valid_preemption_model arr_seq sched
subgoal 2 (ID 209) is:
model_with_bounded_nonpreemptive_segments arr_seq
----------------------------------------------------------------------------- *)
- by apply valid_fully_nonpreemptive_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 209)
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 (processor_state Job)
H_nonpreemptive_sched : is_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_job_cost_le_task_cost : cost_of_jobs_from_arrival_sequence_le_task_cost
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.
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.