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.model.schedule.limited_preemptive.[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.analysis.definitions.job_properties.
Require Export prosa.analysis.facts.behavior.all .
Require Export prosa.analysis.facts.model.sequential.
Require Export prosa.model.preemption.limited_preemptive.
(** * Platform for Models with Limited Preemptions *)
(** In this section, we prove that instantiation of predicate
[job_preemptable] to the model with limited preemptions
indeed defines a valid preemption model. *)
Section ModelWithLimitedPreemptions .
(** 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}.
(** In addition, assume the existence of a function that maps a job
to the sequence of its preemption points... *)
Context `{JobPreemptionPoints Job}.
(** ..., i.e., we assume limited-preemptive jobs. *)
#[local] Existing Instance limited_preemptive_job_model .
(** Consider any arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
(** Next, consider any limited-preemptive schedule of this arrival sequence ... *)
Context {PState : ProcessorState Job}.
Variable sched : schedule PState.
Hypothesis H_schedule_respects_preemption_model :
schedule_respects_preemption_model arr_seq sched.
(** ...where jobs do not execute after their completion. *)
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
(** Next, we assume that preemption points are defined by the
job-level model with limited preemptions. *)
Hypothesis H_valid_limited_preemptions_job_model :
valid_limited_preemptions_job_model arr_seq.
(** First, we prove a few auxiliary lemmas. *)
Section AuxiliaryLemmas .
(** Consider a job j. *)
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
(** Recall that 0 is a preemption point. *)
Remark zero_in_preemption_points : 0 \in job_preemptive_points j.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j
0 \in job_preemptive_points j
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j
0 \in job_preemptive_points j
by apply H_valid_limited_preemptions_job_model. Qed .
(** Using the fact that [job_preemptive_points] is a
non-decreasing sequence, we prove that the first element of
[job_preemptive_points] is 0. *)
Lemma zero_is_first_element : first0 (job_preemptive_points j) = 0 .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j
first0 (job_preemptive_points j) = 0
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j
first0 (job_preemptive_points j) = 0
have F := zero_in_preemption_points.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j F : 0 \in job_preemptive_points j
first0 (job_preemptive_points j) = 0
destruct H_valid_limited_preemptions_job_model as [_ [_ C]]; specialize (C j H_j_arrives).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j F : 0 \in job_preemptive_points jC : nondecreasing_sequence (job_preemptive_points j)
first0 (job_preemptive_points j) = 0
by apply nondec_seq_zero_first.
Qed .
(** We prove that the list of preemption points is not empty. *)
Lemma list_of_preemption_point_is_not_empty :
0 < size (job_preemptive_points j).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j
0 < size (job_preemptive_points j)
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j
0 < size (job_preemptive_points j)
move : H_valid_limited_preemptions_job_model => [BEG [END _]].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq
0 < size (job_preemptive_points j)
apply /negPn/negP; rewrite -eqn0Ngt; intros CONTR; rewrite size_eq0 in CONTR.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq CONTR : job_preemptive_points j == [::]
False
specialize (BEG j H_j_arrives).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j BEG : 0 \in job_preemptive_points jEND : end_of_execution_in_preemption_points arr_seq CONTR : job_preemptive_points j == [::]
False
by move : CONTR BEG => /eqP; rewrite /beginning_of_execution_in_preemption_points => ->.
Qed .
(** Next, we prove that the cost of a job is a preemption point. *)
Lemma job_cost_in_nonpreemptive_points : job_cost j \in job_preemptive_points j.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j
job_cost j \in job_preemptive_points j
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j
job_cost j \in job_preemptive_points j
move : H_valid_limited_preemptions_job_model => [BEG [END _]].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq
job_cost j \in job_preemptive_points j
move : (END _ H_j_arrives) => EQ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq EQ : last0 (job_preemptive_points j) = job_cost j
job_cost j \in job_preemptive_points j
rewrite -EQ; clear EQ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq
last0 (job_preemptive_points j)
\in job_preemptive_points j
rewrite /last0 -nth_last.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq
nth 0 (job_preemptive_points j)
(size (job_preemptive_points j)).-1
\in job_preemptive_points j
apply /(nthP 0 ).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq
exists2 i : nat,
i < size (job_preemptive_points j) &
nth 0 (job_preemptive_points j) i =
nth 0 (job_preemptive_points j)
(size (job_preemptive_points j)).-1
exists ((size (job_preemptive_points j)).-1 ) => [|//].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq
(size (job_preemptive_points j)).-1 <
size (job_preemptive_points j)
rewrite -(leq_add2r 1 ) !addn1 prednK //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq
0 < size (job_preemptive_points j)
exact : list_of_preemption_point_is_not_empty.
Qed .
(** As a corollary, we prove that the sequence of non-preemptive
points of a job with positive cost contains at least 2
points. *)
Corollary number_of_preemption_points_at_least_two :
job_cost_positive j ->
2 <= size (job_preemptive_points j).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j
job_cost_positive j ->
1 < size (job_preemptive_points j)
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j
job_cost_positive j ->
1 < size (job_preemptive_points j)
intros POS.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j POS : job_cost_positive j
1 < size (job_preemptive_points j)
move : H_valid_limited_preemptions_job_model => [BEG [END _]].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j POS : job_cost_positive j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq
1 < size (job_preemptive_points j)
have EQ: 2 = size [::0 ; job_cost j] => [//|].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j POS : job_cost_positive j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq EQ : 2 = size [:: 0 ; job_cost j]
1 < size (job_preemptive_points j)
rewrite EQ; clear EQ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j POS : job_cost_positive j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq
size [:: 0 ; job_cost j] <=
size (job_preemptive_points j)
apply subseq_leq_size.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j POS : job_cost_positive j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq
uniq [:: 0 ; job_cost j]
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j POS : job_cost_positive j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq
uniq [:: 0 ; job_cost j]
rewrite !cons_uniq.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j POS : job_cost_positive j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq
[&& 0 \notin [:: job_cost j], job_cost j \notin [::]
& uniq [::]]
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j POS : job_cost_positive j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq
[&& 0 \notin [:: job_cost j], job_cost j \notin [::]
& uniq [::]]
apply /andP; split .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j POS : job_cost_positive j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq
0 \notin [:: job_cost j]
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j POS : job_cost_positive j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq
0 \notin [:: job_cost j]
rewrite in_cons negb_or; apply /andP; split => [|//].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j POS : job_cost_positive j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq
0 != job_cost j
rewrite neq_ltn; apply /orP; left ; eauto 2 .
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j POS : job_cost_positive j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq
(job_cost j \notin [::]) && uniq [::]
by apply /andP. }
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j POS : job_cost_positive j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq
forall x : Datatypes_nat__canonical__eqtype_Equality,
x \in [:: 0 ; job_cost j] ->
x \in job_preemptive_points j
intros t EQ; move : EQ; rewrite !in_cons.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j POS : job_cost_positive j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq t : Datatypes_nat__canonical__eqtype_Equality
[|| t == 0 , t == job_cost j | t \in [::]] ->
t \in job_preemptive_points j
move => /orP [/eqP EQ| /orP [/eqP EQ|EQ]] //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j POS : job_cost_positive j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq t : Datatypes_nat__canonical__eqtype_Equality EQ : t = 0
t \in job_preemptive_points j
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j POS : job_cost_positive j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq t : Datatypes_nat__canonical__eqtype_Equality EQ : t = 0
t \in job_preemptive_points j
by rewrite EQ; apply zero_in_preemption_points.
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j POS : job_cost_positive j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq t : Datatypes_nat__canonical__eqtype_Equality EQ : t = job_cost j
t \in job_preemptive_points j
by rewrite EQ; apply job_cost_in_nonpreemptive_points.
Qed .
(** Next we prove that "anti-density" property (from
[preemption.util] file) holds for [job_preemption_point j]. *)
Lemma antidensity_of_preemption_points :
forall (ρ : work),
ρ <= job_cost j ->
~~ (ρ \in job_preemptive_points j) ->
first0 (job_preemptive_points j) <= ρ < last0 (job_preemptive_points j).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j
forall ρ : work,
ρ <= job_cost j ->
ρ \notin job_preemptive_points j ->
first0 (job_preemptive_points j) <= ρ <
last0 (job_preemptive_points j)
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j
forall ρ : work,
ρ <= job_cost j ->
ρ \notin job_preemptive_points j ->
first0 (job_preemptive_points j) <= ρ <
last0 (job_preemptive_points j)
intros ρ LE NotIN.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j ρ : work LE : ρ <= job_cost j NotIN : ρ \notin job_preemptive_points j
first0 (job_preemptive_points j) <= ρ <
last0 (job_preemptive_points j)
move : H_valid_limited_preemptions_job_model => [BEG [END NDEC]].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j ρ : work LE : ρ <= job_cost j NotIN : ρ \notin job_preemptive_points j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq
first0 (job_preemptive_points j) <= ρ <
last0 (job_preemptive_points j)
apply /andP; split .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j ρ : work LE : ρ <= job_cost j NotIN : ρ \notin job_preemptive_points j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq
first0 (job_preemptive_points j) <= ρ
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j ρ : work LE : ρ <= job_cost j NotIN : ρ \notin job_preemptive_points j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq
first0 (job_preemptive_points j) <= ρ
by rewrite zero_is_first_element.
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j ρ : work LE : ρ <= job_cost j NotIN : ρ \notin job_preemptive_points j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq
ρ < last0 (job_preemptive_points j)
rewrite END//.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j ρ : work LE : ρ <= job_cost j NotIN : ρ \notin job_preemptive_points j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq
ρ < job_cost j
rewrite ltn_neqAle; apply /andP; split => [|//].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j ρ : work LE : ρ <= job_cost j NotIN : ρ \notin job_preemptive_points j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq
ρ != job_cost j
apply /negP; intros CONTR; move : CONTR => /eqP CONTR.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j ρ : work LE : ρ <= job_cost j NotIN : ρ \notin job_preemptive_points j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq CONTR : ρ = job_cost j
False
rewrite CONTR in NotIN.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j ρ : work LE : ρ <= job_cost j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq CONTR : ρ = job_cost j NotIN : job_cost j \notin job_preemptive_points j
False
move : NotIN => /negP NIN; apply : NIN.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j ρ : work LE : ρ <= job_cost j BEG : beginning_of_execution_in_preemption_points
arr_seq END : end_of_execution_in_preemption_points arr_seq NDEC : preemption_points_is_nondecreasing_sequence
arr_seq CONTR : ρ = job_cost j
job_cost j \in job_preemptive_points j
by apply job_cost_in_nonpreemptive_points.
Qed .
(** We also prove that any work that doesn't belong to
preemption points of job j is placed strictly between two
neighboring preemption points. *)
Lemma work_belongs_to_some_nonpreemptive_segment :
forall (ρ : work),
ρ <= job_cost j ->
~~ (ρ \in job_preemptive_points j) ->
exists n ,
n.+1 < size (job_preemptive_points j) /\
nth 0 (job_preemptive_points j) n < ρ < nth 0 (job_preemptive_points j) n.+1 .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j
forall ρ : work,
ρ <= job_cost j ->
ρ \notin job_preemptive_points j ->
exists n : nat,
n.+1 < size (job_preemptive_points j) /\
nth 0 (job_preemptive_points j) n < ρ <
nth 0 (job_preemptive_points j) n.+1
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j
forall ρ : work,
ρ <= job_cost j ->
ρ \notin job_preemptive_points j ->
exists n : nat,
n.+1 < size (job_preemptive_points j) /\
nth 0 (job_preemptive_points j) n < ρ <
nth 0 (job_preemptive_points j) n.+1
intros ρ LE NotIN.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j ρ : work LE : ρ <= job_cost j NotIN : ρ \notin job_preemptive_points j
exists n : nat,
n.+1 < size (job_preemptive_points j) /\
nth 0 (job_preemptive_points j) n < ρ <
nth 0 (job_preemptive_points j) n.+1
case : (posnP (job_cost j)) => [ZERO|POS].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j ρ : work LE : ρ <= job_cost j NotIN : ρ \notin job_preemptive_points j ZERO : job_cost j = 0
exists n : nat,
n.+1 < size (job_preemptive_points j) /\
nth 0 (job_preemptive_points j) n < ρ <
nth 0 (job_preemptive_points j) n.+1
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j ρ : work LE : ρ <= job_cost j NotIN : ρ \notin job_preemptive_points j ZERO : job_cost j = 0
exists n : nat,
n.+1 < size (job_preemptive_points j) /\
nth 0 (job_preemptive_points j) n < ρ <
nth 0 (job_preemptive_points j) n.+1
exfalso ; move : NotIN => /negP NIN; apply : NIN.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j ρ : work LE : ρ <= job_cost j ZERO : job_cost j = 0
ρ \in job_preemptive_points j
move : LE.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j ρ : work ZERO : job_cost j = 0
ρ <= job_cost j -> ρ \in job_preemptive_points j
rewrite ZERO leqn0; move => /eqP ->.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j ρ : work ZERO : job_cost j = 0
0 \in job_preemptive_points j
by apply zero_in_preemption_points. } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j ρ : work LE : ρ <= job_cost j NotIN : ρ \notin job_preemptive_points j POS : 0 < job_cost j
exists n : nat,
n.+1 < size (job_preemptive_points j) /\
nth 0 (job_preemptive_points j) n < ρ <
nth 0 (job_preemptive_points j) n.+1
move : (belonging_to_segment_of_seq_is_total
(job_preemptive_points j) ρ (number_of_preemption_points_at_least_two POS)
(antidensity_of_preemption_points _ LE NotIN)) => [n [SIZE2 /andP [N1 N2]]].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j ρ : work LE : ρ <= job_cost j NotIN : ρ \notin job_preemptive_points j POS : 0 < job_cost jn : nat SIZE2 : n.+1 < size (job_preemptive_points j) N1 : nth 0 (job_preemptive_points j) n <= ρ N2 : ρ < nth 0 (job_preemptive_points j) n.+1
exists n : nat,
n.+1 < size (job_preemptive_points j) /\
nth 0 (job_preemptive_points j) n < ρ <
nth 0 (job_preemptive_points j) n.+1
exists n ; split => [//|].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j ρ : work LE : ρ <= job_cost j NotIN : ρ \notin job_preemptive_points j POS : 0 < job_cost jn : nat SIZE2 : n.+1 < size (job_preemptive_points j) N1 : nth 0 (job_preemptive_points j) n <= ρ N2 : ρ < nth 0 (job_preemptive_points j) n.+1
nth 0 (job_preemptive_points j) n < ρ <
nth 0 (job_preemptive_points j) n.+1
apply /andP; split => [|//].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j ρ : work LE : ρ <= job_cost j NotIN : ρ \notin job_preemptive_points j POS : 0 < job_cost jn : nat SIZE2 : n.+1 < size (job_preemptive_points j) N1 : nth 0 (job_preemptive_points j) n <= ρ N2 : ρ < nth 0 (job_preemptive_points j) n.+1
nth 0 (job_preemptive_points j) n < ρ
move : N1; rewrite leq_eqVlt; move => /orP [/eqP EQ | //].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j ρ : work LE : ρ <= job_cost j NotIN : ρ \notin job_preemptive_points j POS : 0 < job_cost jn : nat SIZE2 : n.+1 < size (job_preemptive_points j) N2 : ρ < nth 0 (job_preemptive_points j) n.+1 EQ : nth 0 (job_preemptive_points j) n = ρ
nth 0 (job_preemptive_points j) n < ρ
exfalso .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j ρ : work LE : ρ <= job_cost j NotIN : ρ \notin job_preemptive_points j POS : 0 < job_cost jn : nat SIZE2 : n.+1 < size (job_preemptive_points j) N2 : ρ < nth 0 (job_preemptive_points j) n.+1 EQ : nth 0 (job_preemptive_points j) n = ρ
False
move : NotIN => /negP CONTR; apply : CONTR.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j ρ : work LE : ρ <= job_cost j POS : 0 < job_cost jn : nat SIZE2 : n.+1 < size (job_preemptive_points j) N2 : ρ < nth 0 (job_preemptive_points j) n.+1 EQ : nth 0 (job_preemptive_points j) n = ρ
ρ \in job_preemptive_points j
rewrite -EQ; clear EQ.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j ρ : work LE : ρ <= job_cost j POS : 0 < job_cost jn : nat SIZE2 : n.+1 < size (job_preemptive_points j) N2 : ρ < nth 0 (job_preemptive_points j) n.+1
nth 0 (job_preemptive_points j) n
\in job_preemptive_points j
by rewrite mem_nth.
Qed .
(** Recall that the module [prosa.model.preemption.parameters] also defines
a notion of preemption points, namely [job_preemption_points], which
cannot have duplicated preemption points. Therefore, we need additional
lemmas to relate [job_preemption_points] and [job_preemptive_points]. *)
(** First we show that the length of the last non-preemptive segment in
[job_preemption_points] is equal to the length of the last non-empty
non-preemptive segment of [job_preemptive_points]. *)
Lemma job_parameters_last_np_to_job_limited :
last0 (distances (job_preemption_points j)) =
last0 (filter (fun x => 0 < x) (distances (job_preemptive_points j))).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j
last0 (distances (job_preemption_points j)) =
last0
[seq x <- distances (job_preemptive_points j)
| 0 < x]
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j
last0 (distances (job_preemption_points j)) =
last0
[seq x <- distances (job_preemptive_points j)
| 0 < x]
destruct H_valid_limited_preemptions_job_model as [A1 [A2 A3]].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j A1 : beginning_of_execution_in_preemption_points
arr_seq A2 : end_of_execution_in_preemption_points arr_seq A3 : preemption_points_is_nondecreasing_sequence
arr_seq
last0 (distances (job_preemption_points j)) =
last0
[seq x <- distances (job_preemptive_points j)
| 0 < x]
unfold job_preemption_points, job_preemptable, limited_preemptive_job_model.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j A1 : beginning_of_execution_in_preemption_points
arr_seq A2 : end_of_execution_in_preemption_points arr_seq A3 : preemption_points_is_nondecreasing_sequence
arr_seq
last0
(distances
[seq ρ <- range 0 (job_cost j)
| ρ \in job_preemptive_points j]) =
last0
[seq x <- distances (job_preemptive_points j)
| 0 < x]
intros ; rewrite distances_iota_filtered; eauto .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j A1 : beginning_of_execution_in_preemption_points
arr_seq A2 : end_of_execution_in_preemption_points arr_seq A3 : preemption_points_is_nondecreasing_sequence
arr_seq
forall x : nat,
x \in job_preemptive_points j -> x <= job_cost j
rewrite -A2 //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j A1 : beginning_of_execution_in_preemption_points
arr_seq A2 : end_of_execution_in_preemption_points arr_seq A3 : preemption_points_is_nondecreasing_sequence
arr_seq
forall x : nat,
x \in job_preemptive_points j ->
x <= last0 (job_preemptive_points j)
by intros ; apply last_is_max_in_nondecreasing_seq; eauto 2 .
Qed .
(** Next we show that the length of the max non-preemptive segment of
[job_preemption_points] is equal to the length of the max non-preemptive
segment of [job_preemptive_points]. *)
Lemma job_parameters_max_np_to_job_limited :
max0 (distances (job_preemption_points j)) =
max0 (distances (job_preemptive_points j)).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j
max0 (distances (job_preemption_points j)) =
max0 (distances (job_preemptive_points j))
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j
max0 (distances (job_preemption_points j)) =
max0 (distances (job_preemptive_points j))
destruct H_valid_limited_preemptions_job_model as [A1 [A2 A3]].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j A1 : beginning_of_execution_in_preemption_points
arr_seq A2 : end_of_execution_in_preemption_points arr_seq A3 : preemption_points_is_nondecreasing_sequence
arr_seq
max0 (distances (job_preemption_points j)) =
max0 (distances (job_preemptive_points j))
unfold job_preemption_points, job_preemptable, limited_preemptive_job_model.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j A1 : beginning_of_execution_in_preemption_points
arr_seq A2 : end_of_execution_in_preemption_points arr_seq A3 : preemption_points_is_nondecreasing_sequence
arr_seq
max0
(distances
[seq ρ <- range 0 (job_cost j)
| ρ \in job_preemptive_points j]) =
max0 (distances (job_preemptive_points j))
intros ; rewrite distances_iota_filtered; eauto 2 .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j A1 : beginning_of_execution_in_preemption_points
arr_seq A2 : end_of_execution_in_preemption_points arr_seq A3 : preemption_points_is_nondecreasing_sequence
arr_seq
max0
[seq x <- distances (job_preemptive_points j)
| 0 < x] =
max0 (distances (job_preemptive_points j))
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j A1 : beginning_of_execution_in_preemption_points
arr_seq A2 : end_of_execution_in_preemption_points arr_seq A3 : preemption_points_is_nondecreasing_sequence
arr_seq
max0
[seq x <- distances (job_preemptive_points j)
| 0 < x] =
max0 (distances (job_preemptive_points j))
by rewrite max0_rem0 //.
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j A1 : beginning_of_execution_in_preemption_points
arr_seq A2 : end_of_execution_in_preemption_points arr_seq A3 : preemption_points_is_nondecreasing_sequence
arr_seq
forall x : nat,
x \in job_preemptive_points j -> x <= job_cost j
rewrite -A2 //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job H_j_arrives : arrives_in arr_seq j A1 : beginning_of_execution_in_preemption_points
arr_seq A2 : end_of_execution_in_preemption_points arr_seq A3 : preemption_points_is_nondecreasing_sequence
arr_seq
forall x : nat,
x \in job_preemptive_points j ->
x <= last0 (job_preemptive_points j)
by intros ; apply last_is_max_in_nondecreasing_seq; eauto 2 .
Qed .
End AuxiliaryLemmas .
(** We prove that the [fixed_preemption_point_model] function
defines a valid preemption model. *)
Lemma valid_fixed_preemption_points_model_lemma :
valid_preemption_model arr_seq sched.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
valid_preemption_model arr_seq sched
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq
valid_preemption_model arr_seq sched
intros j ARR; repeat split .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job ARR : arrives_in arr_seq j
job_cannot_become_nonpreemptive_before_execution j
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job ARR : arrives_in arr_seq j
job_cannot_become_nonpreemptive_before_execution j
by apply zero_in_preemption_points. } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job ARR : arrives_in arr_seq j
job_cannot_be_nonpreemptive_after_completion j
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job ARR : arrives_in arr_seq j
job_cannot_be_nonpreemptive_after_completion j
by apply job_cost_in_nonpreemptive_points. } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job ARR : arrives_in arr_seq j
not_preemptive_implies_scheduled sched j
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job ARR : arrives_in arr_seq j
not_preemptive_implies_scheduled sched j
by move => t NPP; apply H_schedule_respects_preemption_model. } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job ARR : arrives_in arr_seq j
execution_starts_with_preemption_point sched j
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job ARR : arrives_in arr_seq j
execution_starts_with_preemption_point sched j
intros t NSCHED SCHED.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job ARR : arrives_in arr_seq j t : instant NSCHED : ~~ scheduled_at sched j t SCHED : scheduled_at sched j t.+1
job_preemptable j (service sched j t.+1 )
have ->: service sched j t.+1 = service sched j t
by rewrite -service_last_plus_before not_scheduled_implies_no_service // addn0.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job ARR : arrives_in arr_seq j t : instant NSCHED : ~~ scheduled_at sched j t SCHED : scheduled_at sched j t.+1
job_preemptable j (service sched j t)
apply : contraT => NP.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job ARR : arrives_in arr_seq j t : instant NSCHED : ~~ scheduled_at sched j t SCHED : scheduled_at sched j t.+1 NP : ~~ job_preemptable j (service sched j t)
false
have : scheduled_at sched j t by apply : H_schedule_respects_preemption_model.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job H3 : JobPreemptionPoints Job arr_seq : arrival_sequence Job PState : ProcessorState Job sched : schedule PState H_schedule_respects_preemption_model : schedule_respects_preemption_model
arr_seq sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_limited_preemptions_job_model : valid_limited_preemptions_job_model
arr_seq j : Job ARR : arrives_in arr_seq j t : instant NSCHED : ~~ scheduled_at sched j t SCHED : scheduled_at sched j t.+1 NP : ~~ job_preemptable j (service sched j t)
scheduled_at sched j t -> false
by move : NSCHED => /negP. }
Qed .
End ModelWithLimitedPreemptions .
Global Hint Resolve valid_fixed_preemption_points_model_lemma : basic_rt_facts.