Built with
Alectryon , running Coq+SerAPI v8.20.0+0.20.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.analysis.facts.preemption.job.nonpreemptive.[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] [Loading ML file ring_plugin.cmxs (using legacy method) ... done ] Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted. [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ] Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export 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. *)
Section FullyNonPreemptiveModel .
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Assume a fully non-preemptive task model. *)
#[local] Existing Instance fully_nonpreemptive_job_model .
#[local] Existing Instance fully_nonpreemptive_task_model .
#[local] Existing Instance fully_nonpreemptive_rtc_threshold .
(** Consider any arrival sequence with consistent arrivals. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
(** Next, consider any non-preemptive unit-service schedule of the arrival sequence ... *)
Context {PState : ProcessorState Job}.
Hypothesis H_unit_service : unit_service_proc_model PState.
Variable sched : schedule PState.
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.
(** Assume that a job cost cannot be larger than a task cost. *)
Hypothesis H_valid_job_cost :
arrivals_have_valid_job_costs arr_seq.
(** Then we prove that the [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.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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 .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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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
have F: forall n , n = 0 \/ n > 0 by intros n; destruct n; [left | right ].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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 .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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 < nj : Job H3 : arrives_in arr_seq j
job_respects_max_nonpreemptive_segment j
{ 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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 < nj : Job H3 : arrives_in arr_seq j
job_respects_max_nonpreemptive_segment j
rewrite /job_respects_max_nonpreemptive_segment; eauto 2 .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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 < nj : 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 .
} 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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 < nj : Job H3 : arrives_in arr_seq j
nonpreemptive_regions_have_bounded_length j
move => progr /andP [_ GE].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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 < nj : 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 - 1 ) /\
job_preemptable j pp
move : (F (progr)) => [EQ | GT].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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 < nj : 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 - 1 ) /\
job_preemptable j pp
{ 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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 < nj : 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 - 1 ) /\
job_preemptable j pp
exists progr ; split .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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 < nj : 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 - 1 )
- 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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 < nj : 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 - 1 )
by apply /andP; split ; [|rewrite leq_addr].
- 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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 < nj : 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_job_model.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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 < nj : Job H3 : arrives_in arr_seq j progr : duration GE : progr <= job_cost j EQ : progr = 0
(progr == 0 ) || (progr == job_cost j)
by apply /orP; left ; rewrite EQ.
} 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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 < nj : 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 - 1 ) /\
job_preemptable j pp
{ 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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 < nj : 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 - 1 ) /\
job_preemptable j pp
exists (maxn progr (job_cost j)).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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 < nj : 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 - 1 ) /\
job_preemptable j (maxn progr (job_cost j))
have POS: 0 < job_cost j by apply leq_trans with progr.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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 < nj : Job H3 : arrives_in arr_seq j progr : duration GE : progr <= job_cost j GT : 0 < progrPOS : 0 < job_cost j
progr <= maxn progr (job_cost j) <=
progr + (job_max_nonpreemptive_segment j - 1 ) /\
job_preemptable j (maxn progr (job_cost j))
split .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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 < nj : Job H3 : arrives_in arr_seq j progr : duration GE : progr <= job_cost j GT : 0 < progrPOS : 0 < job_cost j
progr <= maxn progr (job_cost j) <=
progr + (job_max_nonpreemptive_segment j - 1 )
{ 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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 < nj : Job H3 : arrives_in arr_seq j progr : duration GE : progr <= job_cost j GT : 0 < progrPOS : 0 < job_cost j
progr <= maxn progr (job_cost j) <=
progr + (job_max_nonpreemptive_segment j - 1 )
apply /andP; split ; first by rewrite leq_maxl.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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 < nj : Job H3 : arrives_in arr_seq j progr : duration GE : progr <= job_cost j GT : 0 < progrPOS : 0 < job_cost j
maxn progr (job_cost j) <=
progr + (job_max_nonpreemptive_segment j - 1 )
erewrite job_max_nps_is_job_cost; eauto 2 ; rewrite addnBA; last eauto 2 .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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 < nj : Job H3 : arrives_in arr_seq j progr : duration GE : progr <= job_cost j GT : 0 < progrPOS : 0 < job_cost j
maxn progr (job_cost j) <= progr + job_cost j - 1
rewrite geq_max; apply /andP; split .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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 < nj : Job H3 : arrives_in arr_seq j progr : duration GE : progr <= job_cost j GT : 0 < progrPOS : 0 < job_cost j
progr <= progr + job_cost j - 1
- 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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 < nj : Job H3 : arrives_in arr_seq j progr : duration GE : progr <= job_cost j GT : 0 < progrPOS : 0 < job_cost j
progr <= progr + job_cost j - 1
rewrite -addnBA; last by eauto 2 .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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 < nj : Job H3 : arrives_in arr_seq j progr : duration GE : progr <= job_cost j GT : 0 < progrPOS : 0 < job_cost j
progr <= progr + (job_cost j - 1 )
by rewrite leq_addr.
- 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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 < nj : Job H3 : arrives_in arr_seq j progr : duration GE : progr <= job_cost j GT : 0 < progrPOS : 0 < job_cost j
job_cost j <= progr + job_cost j - 1
by rewrite addnC -addnBA // leq_addr.
} 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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 < nj : Job H3 : arrives_in arr_seq j progr : duration GE : progr <= job_cost j GT : 0 < progrPOS : 0 < job_cost j
job_preemptable j (maxn progr (job_cost j))
{ 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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 < nj : Job H3 : arrives_in arr_seq j progr : duration GE : progr <= job_cost j GT : 0 < progrPOS : 0 < job_cost j
job_preemptable j (maxn progr (job_cost j))
apply /orP; right .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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 < nj : Job H3 : arrives_in arr_seq j progr : duration GE : progr <= job_cost j GT : 0 < progrPOS : 0 < job_cost j
maxn progr (job_cost j) == job_cost j
rewrite eqn_leq; apply /andP; split .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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 < nj : Job H3 : arrives_in arr_seq j progr : duration GE : progr <= job_cost j GT : 0 < progrPOS : 0 < job_cost j
maxn progr (job_cost j) <= job_cost j
- 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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 < nj : Job H3 : arrives_in arr_seq j progr : duration GE : progr <= job_cost j GT : 0 < progrPOS : 0 < job_cost j
maxn progr (job_cost j) <= job_cost j
by rewrite geq_max; apply /andP; split .
- 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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 < nj : Job H3 : arrives_in arr_seq j progr : duration GE : progr <= job_cost j GT : 0 < progrPOS : 0 < job_cost j
job_cost j <= maxn progr (job_cost j)
by rewrite leq_max; apply /orP; right .
}
}
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.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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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 .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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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
split .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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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
- 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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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
by apply valid_fully_nonpreemptive_model.
- 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 PState : ProcessorState Job H_unit_service : unit_service_proc_model PState sched : schedule PState 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.
Qed .
End FullyNonPreemptiveModel .
(** We add the above lemma into a "Hint Database" basic_rt_facts, so Coq will be able to apply them automatically. *)
Global Hint Resolve
valid_fully_nonpreemptive_model
fully_nonpreemptive_model_is_model_with_bounded_nonpreemptive_regions
fully_nonpreemptive_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_rt_facts.