Built with
Alectryon , running Coq+SerAPI v8.15.0+0.15.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.definitions.job_properties.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Require Export prosa.analysis.facts.behavior.all .Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Export prosa.model.task.preemption.parameters.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
(** * Run-to-Completion Threshold *)
(** In this section, we provide a few basic properties
of run-to-completion-threshold-compliant schedules. *)
Section RunToCompletionThreshold .
(** Consider any type of jobs. *)
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** In addition, we assume existence of a function
mapping jobs to their preemption points. *)
Context `{JobPreemptable Job}.
(** Consider any kind of processor state model, ... *)
Context {PState : ProcessorState Job}.
(** ... any job arrival sequence, ... *)
Variable arr_seq : arrival_sequence Job.
(** ... and any given schedule. *)
Variable sched : schedule PState.
(** Assume that the preemption model is valid. *)
Hypothesis H_valid_preemption_model :
valid_preemption_model arr_seq sched.
(** Consider an arbitrary job j from the arrival sequence. *)
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
(** First we prove a few auxiliary lemmas about
[job_preemption_points]. *)
Section AuxiliaryLemmas .
(** We prove that the sequence of preemption points of a zero-cost
job consists of one element -- 0. *)
Lemma preemption_points_of_zero_cost_job :
job_cost j = 0 ->
job_preemption_points j = [::0 ].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
job_cost j = 0 -> job_preemption_points j = [:: 0 ]
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
job_cost j = 0 -> job_preemption_points j = [:: 0 ]
intros ZERO.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j ZERO : job_cost j = 0
job_preemption_points j = [:: 0 ]
destruct (H_valid_preemption_model j) as [A1 [A2 [A3 A4]]]; auto .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j ZERO : job_cost j = 0 A1 : job_cannot_become_nonpreemptive_before_execution
j A2 : job_cannot_be_nonpreemptive_after_completion j A3 : not_preemptive_implies_scheduled sched j A4 : execution_starts_with_preemption_point sched j
job_preemption_points j = [:: 0 ]
unfold job_preemption_points; rewrite ZERO; simpl .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j ZERO : job_cost j = 0 A1 : job_cannot_become_nonpreemptive_before_execution
j A2 : job_cannot_be_nonpreemptive_after_completion j A3 : not_preemptive_implies_scheduled sched j A4 : execution_starts_with_preemption_point sched j
(if job_preemptable j 0 then [:: 0 ] else [::]) =
[:: 0 ]
simpl ; unfold job_cannot_become_nonpreemptive_before_execution in *.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j ZERO : job_cost j = 0 A1 : job_preemptable j 0 A2 : job_cannot_be_nonpreemptive_after_completion j A3 : not_preemptive_implies_scheduled sched j A4 : execution_starts_with_preemption_point sched j
(if job_preemptable j 0 then [:: 0 ] else [::]) =
[:: 0 ]
by rewrite A1.
Qed .
(** For a positive-cost job, 0 ... *)
Lemma zero_in_preemption_points :
0 < job_cost j ->
0 \in job_preemption_points j.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
0 < job_cost j -> 0 \in job_preemption_points j
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
0 < job_cost j -> 0 \in job_preemption_points j
intros POS.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j POS : 0 < job_cost j
0 \in job_preemption_points j
unfold job_preemption_points, range.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j POS : 0 < job_cost j
0
\in [seq ρ <- index_iota 0 (job_cost j).+1
| job_preemptable j ρ]
destruct (H_valid_preemption_model j) as [A1 [A2 [A3 A4]]]; auto .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j POS : 0 < job_cost jA1 : job_cannot_become_nonpreemptive_before_execution
j A2 : job_cannot_be_nonpreemptive_after_completion j A3 : not_preemptive_implies_scheduled sched j A4 : execution_starts_with_preemption_point sched j
0
\in [seq ρ <- index_iota 0 (job_cost j).+1
| job_preemptable j ρ]
unfold job_cannot_become_nonpreemptive_before_execution in *.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j POS : 0 < job_cost jA1 : job_preemptable j 0 A2 : job_cannot_be_nonpreemptive_after_completion j A3 : not_preemptive_implies_scheduled sched j A4 : execution_starts_with_preemption_point sched j
0
\in [seq ρ <- index_iota 0 (job_cost j).+1
| job_preemptable j ρ]
rewrite index_iota_lt_step; last by done .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j POS : 0 < job_cost jA1 : job_preemptable j 0 A2 : job_cannot_be_nonpreemptive_after_completion j A3 : not_preemptive_implies_scheduled sched j A4 : execution_starts_with_preemption_point sched j
0
\in [seq ρ <- 0 :: index_iota 1 (job_cost j).+1
| job_preemptable j ρ]
by simpl ; rewrite A1 in_cons eq_refl.
Qed .
(** ... and [job_cost] are in preemption points. *)
Lemma job_cost_in_preemption_points :
0 < job_cost j ->
job_cost j \in job_preemption_points j.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
0 < job_cost j ->
job_cost j \in job_preemption_points j
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
0 < job_cost j ->
job_cost j \in job_preemption_points j
intros POS.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j POS : 0 < job_cost j
job_cost j \in job_preemption_points j
unfold job_preemption_points, range, index_iota; rewrite subn0 -addn1.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j POS : 0 < job_cost j
job_cost j
\in [seq ρ <- iota 0 (job_cost j + 1 )
| job_preemptable j ρ]
rewrite iotaD add0n filter_cat mem_cat.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j POS : 0 < job_cost j
(job_cost j
\in [seq ρ <- iota 0 (job_cost j)
| job_preemptable j ρ])
|| (job_cost j
\in [seq ρ <- iota (job_cost j) 1
| job_preemptable j ρ])
apply /orP; right ; simpl .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j POS : 0 < job_cost j
job_cost j
\in (if job_preemptable j (job_cost j)
then [:: job_cost j]
else [::])
destruct (H_valid_preemption_model j) as [A1 [A2 [A3 A4]]]; auto .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j POS : 0 < job_cost jA1 : job_cannot_become_nonpreemptive_before_execution
j A2 : job_cannot_be_nonpreemptive_after_completion j A3 : not_preemptive_implies_scheduled sched j A4 : execution_starts_with_preemption_point sched j
job_cost j
\in (if job_preemptable j (job_cost j)
then [:: job_cost j]
else [::])
unfold job_cannot_be_nonpreemptive_after_completion in *.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j POS : 0 < job_cost jA1 : job_cannot_become_nonpreemptive_before_execution
j A2 : job_preemptable j (job_cost j) A3 : not_preemptive_implies_scheduled sched j A4 : execution_starts_with_preemption_point sched j
job_cost j
\in (if job_preemptable j (job_cost j)
then [:: job_cost j]
else [::])
by rewrite A2 in_cons eq_refl.
Qed .
(** Therefore, for a positive-cost job size of the sequence of
preemption points is at least two. *)
Lemma size_of_preemption_points :
0 < job_cost j ->
2 <= size (job_preemption_points j).Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
0 < job_cost j -> 1 < size (job_preemption_points j)
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
0 < job_cost j -> 1 < size (job_preemption_points j)
intros POS.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j POS : 0 < job_cost j
1 < size (job_preemption_points j)
replace 2 with (size [::0 ; job_cost j]); last by done .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j POS : 0 < job_cost j
size [:: 0 ; job_cost j] <=
size (job_preemption_points j)
apply subseq_leq_size.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j POS : 0 < job_cost j
uniq [:: 0 ; job_cost j]
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j POS : 0 < job_cost j
uniq [:: 0 ; job_cost j]
apply /andP; split .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j POS : 0 < job_cost j
0 \notin [:: job_cost j]
rewrite !in_cons Bool.negb_orb.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j POS : 0 < job_cost j
(0 != job_cost j) && (0 \notin [::])
+ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j POS : 0 < job_cost j
(0 != job_cost j) && (0 \notin [::])
apply /andP; split .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j POS : 0 < job_cost j
0 != job_cost j
by rewrite neq_ltn POS.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j POS : 0 < job_cost j
0 \notin [::]
by done .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j POS : 0 < job_cost j
(job_cost j \notin [::]) && true
+ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j POS : 0 < job_cost j
(job_cost j \notin [::]) && true
apply /andP; split ; by done .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j POS : 0 < job_cost j
forall x : nat_eqType,
x \in [:: 0 ; job_cost j] ->
x \in job_preemption_points j
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j POS : 0 < job_cost j
forall x : nat_eqType,
x \in [:: 0 ; job_cost j] ->
x \in job_preemption_points j
intros ρ; rewrite !in_cons; move => /orP [/eqP EQ| /orP [/eqP Cost | C]].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j POS : 0 < job_cost jρ : nat_eqType EQ : ρ = 0
ρ \in job_preemption_points j
+ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j POS : 0 < job_cost jρ : nat_eqType EQ : ρ = 0
ρ \in job_preemption_points j
by subst ; apply zero_in_preemption_points.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j POS : 0 < job_cost jρ : nat_eqType Cost : ρ = job_cost j
ρ \in job_preemption_points j
+ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j POS : 0 < job_cost jρ : nat_eqType Cost : ρ = job_cost j
ρ \in job_preemption_points j
by subst ; apply job_cost_in_preemption_points.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j POS : 0 < job_cost jρ : nat_eqType C : ρ \in [::]
ρ \in job_preemption_points j
+ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j POS : 0 < job_cost jρ : nat_eqType C : ρ \in [::]
ρ \in job_preemption_points j
by done .
Qed .
(** Next we show that the sequence of preemption points is a non-decreasing sequence. *)
Lemma preemption_points_nondecreasing :
nondecreasing_sequence (job_preemption_points j).Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
nondecreasing_sequence (job_preemption_points j)
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
nondecreasing_sequence (job_preemption_points j)
by apply increasing_implies_nondecreasing, iota_is_increasing_sequence. Qed .
(** Next, we prove that the last element of the sequence of
preemption points is [job_cost]. *)
Lemma job_cost_is_last_element_of_preemption_points :
job_cost j = last0 (job_preemption_points j).Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
job_cost j = last0 (job_preemption_points j)
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
job_cost j = last0 (job_preemption_points j)
unfold job_preemption_points.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
job_cost j =
last0
[seq ρ <- range 0 (job_cost j)
| job_preemptable j ρ]
edestruct H_valid_preemption_model as [A1 [A2 [A3 A4]]]; eauto 2 .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j A1 : job_cannot_become_nonpreemptive_before_execution
j A2 : job_cannot_be_nonpreemptive_after_completion j A3 : not_preemptive_implies_scheduled sched j A4 : execution_starts_with_preemption_point sched j
job_cost j =
last0
[seq ρ <- range 0 (job_cost j)
| job_preemptable j ρ]
erewrite last0_filter.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j A1 : job_cannot_become_nonpreemptive_before_execution
j A2 : job_cannot_be_nonpreemptive_after_completion j A3 : not_preemptive_implies_scheduled sched j A4 : execution_starts_with_preemption_point sched j
job_cost j = ?x
+ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j A1 : job_cannot_become_nonpreemptive_before_execution
j A2 : job_cannot_be_nonpreemptive_after_completion j A3 : not_preemptive_implies_scheduled sched j A4 : execution_starts_with_preemption_point sched j
job_cost j = ?x
by apply /eqP; apply eq_refl.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j A1 : job_cannot_become_nonpreemptive_before_execution
j A2 : job_cannot_be_nonpreemptive_after_completion j A3 : not_preemptive_implies_scheduled sched j A4 : execution_starts_with_preemption_point sched j
range 0 (job_cost j) <> [::]
+ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j A1 : job_cannot_become_nonpreemptive_before_execution
j A2 : job_cannot_be_nonpreemptive_after_completion j A3 : not_preemptive_implies_scheduled sched j A4 : execution_starts_with_preemption_point sched j
range 0 (job_cost j) <> [::]
unfold range, index_iota; rewrite subn0 -addn1.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j A1 : job_cannot_become_nonpreemptive_before_execution
j A2 : job_cannot_be_nonpreemptive_after_completion j A3 : not_preemptive_implies_scheduled sched j A4 : execution_starts_with_preemption_point sched j
iota 0 (job_cost j + 1 ) <> [::]
by rewrite iotaD; destruct (iota 0 (job_cost j)).Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j A1 : job_cannot_become_nonpreemptive_before_execution
j A2 : job_cannot_be_nonpreemptive_after_completion j A3 : not_preemptive_implies_scheduled sched j A4 : execution_starts_with_preemption_point sched j
last0 (range 0 (job_cost j)) = job_cost j
+ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j A1 : job_cannot_become_nonpreemptive_before_execution
j A2 : job_cannot_be_nonpreemptive_after_completion j A3 : not_preemptive_implies_scheduled sched j A4 : execution_starts_with_preemption_point sched j
last0 (range 0 (job_cost j)) = job_cost j
unfold range, index_iota; rewrite subn0 -addn1.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j A1 : job_cannot_become_nonpreemptive_before_execution
j A2 : job_cannot_be_nonpreemptive_after_completion j A3 : not_preemptive_implies_scheduled sched j A4 : execution_starts_with_preemption_point sched j
last0 (iota 0 (job_cost j + 1 )) = job_cost j
by rewrite iotaD last0_cat //.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j A1 : job_cannot_become_nonpreemptive_before_execution
j A2 : job_cannot_be_nonpreemptive_after_completion j A3 : not_preemptive_implies_scheduled sched j A4 : execution_starts_with_preemption_point sched j
job_preemptable j (job_cost j)
+ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j A1 : job_cannot_become_nonpreemptive_before_execution
j A2 : job_cannot_be_nonpreemptive_after_completion j A3 : not_preemptive_implies_scheduled sched j A4 : execution_starts_with_preemption_point sched j
job_preemptable j (job_cost j)
by apply A2.
Qed .
(** Last non-preemptive segment of a positive-cost job has positive length. *)
Lemma job_last_nonpreemptive_segment_positive :
job_cost_positive j ->
0 < job_last_nonpreemptive_segment j.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
job_cost_positive j ->
0 < job_last_nonpreemptive_segment j
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
job_cost_positive j ->
0 < job_last_nonpreemptive_segment j
intros COST.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j
0 < job_last_nonpreemptive_segment j
unfold job_last_nonpreemptive_segment.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j
0 < last0 (lengths_of_segments j)
rewrite last0_nth function_of_distances_is_correct subn_gt0.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j
nth 0 (job_preemption_points j)
(size (lengths_of_segments j)).-1 <
nth 0 (job_preemption_points j)
(size (lengths_of_segments j)).-1 .+1
rewrite [size _]pred_Sn -addn1-addn1.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j
nth 0 (job_preemption_points j)
(size (lengths_of_segments j) + 1 ).-2 + 1 <=
nth 0 (job_preemption_points j)
(size (lengths_of_segments j) + 1 ).-2 .+1
rewrite -size_of_seq_of_distances ?addn1 ; last by apply size_of_preemption_points.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j
nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 <
nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 .+1
rewrite prednK; last first .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j
0 < (size (job_preemption_points j)).-1
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j
0 < (size (job_preemption_points j)).-1
rewrite -(leq_add2r 1 ) !addn1 prednK.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j
1 < size (job_preemption_points j)
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j
1 < size (job_preemption_points j)
apply size_of_preemption_points; eauto .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j
0 < size (job_preemption_points j)
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j
0 < size (job_preemption_points j)
rewrite ltnW //; apply size_of_preemption_points; eauto .
} Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j
nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 <
nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-1
apply iota_is_increasing_sequence; apply /andP; split .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j
(size (job_preemption_points j)).-2 <
(size (job_preemption_points j)).-1
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j
(size (job_preemption_points j)).-2 <
(size (job_preemption_points j)).-1
rewrite -(leq_add2r 2 ) !addn2.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j
(size (job_preemption_points j)).-2 .+2 <
(size (job_preemption_points j)).-1 .+2
rewrite prednK; first by done .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j
0 < (size (job_preemption_points j)).-1
rewrite -(leq_add2r 1 ) !addn1.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j
1 < (size (job_preemption_points j)).-1 .+1
rewrite prednK.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j
1 < size (job_preemption_points j)
+ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j
1 < size (job_preemption_points j)
by apply size_of_preemption_points.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j
0 < size (job_preemption_points j)
+ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j
0 < size (job_preemption_points j)
by rewrite ltnW //; apply size_of_preemption_points.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j
(size (job_preemption_points j)).-1 <
size
[seq x <- index_iota 0 (job_cost j).+1
| job_preemptable j x]
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j
(size (job_preemption_points j)).-1 <
size
[seq x <- index_iota 0 (job_cost j).+1
| job_preemptable j x]
rewrite -(leq_add2r 1 ) !addn1.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j
(size (job_preemption_points j)).-1 .+1 <
(size
[seq x <- index_iota 0 (job_cost j).+1
| job_preemptable j x]).+1
unfold job_preemption_points, range.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j
(size
[seq ρ <- index_iota 0 (job_cost j).+1
| job_preemptable j ρ]).-1 .+1 <
(size
[seq x <- index_iota 0 (job_cost j).+1
| job_preemptable j x]).+1
rewrite prednK ?ltnS ; first by done .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j
0 <
size
[seq ρ <- index_iota 0 (job_cost j).+1
| job_preemptable j ρ]
by rewrite ltnW //; apply size_of_preemption_points.
Qed .
(** Max nonpreemptive segment of a positive-cost job has positive length. *)
Lemma job_max_nonpreemptive_segment_positive :
job_cost_positive j ->
0 < job_max_nonpreemptive_segment j.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
job_cost_positive j ->
0 < job_max_nonpreemptive_segment j
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
job_cost_positive j ->
0 < job_max_nonpreemptive_segment j
intros COST.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j
0 < job_max_nonpreemptive_segment j
eapply leq_trans.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j
0 < ?n
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j
0 < ?n
by apply job_last_nonpreemptive_segment_positive.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j
job_last_nonpreemptive_segment j <=
job_max_nonpreemptive_segment j
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j
job_last_nonpreemptive_segment j <=
job_max_nonpreemptive_segment j
by apply last_of_seq_le_max_of_seq.
Qed .
(** Next we show that max nonpreemptive segment is at most the
cost of a job. *)
Lemma job_max_nonpreemptive_segment_le_job_cost :
job_max_nonpreemptive_segment j <= job_cost j.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
job_max_nonpreemptive_segment j <= job_cost j
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
job_max_nonpreemptive_segment j <= job_cost j
eapply leq_trans.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
job_max_nonpreemptive_segment j <= ?n
apply max_distance_in_seq_le_last_element_of_seq; apply preemption_points_nondecreasing.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
last0 (job_preemption_points j) <= job_cost j
destruct (H_valid_preemption_model j) as [A1 [A2 [A3 A4]]]; auto .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j A1 : job_cannot_become_nonpreemptive_before_execution
j A2 : job_cannot_be_nonpreemptive_after_completion j A3 : not_preemptive_implies_scheduled sched j A4 : execution_starts_with_preemption_point sched j
last0 (job_preemption_points j) <= job_cost j
case : (posnP (job_cost j)) => [ZERO|POSt].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j A1 : job_cannot_become_nonpreemptive_before_execution
j A2 : job_cannot_be_nonpreemptive_after_completion j A3 : not_preemptive_implies_scheduled sched j A4 : execution_starts_with_preemption_point sched j ZERO : job_cost j = 0
last0 (job_preemption_points j) <= job_cost j
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j A1 : job_cannot_become_nonpreemptive_before_execution
j A2 : job_cannot_be_nonpreemptive_after_completion j A3 : not_preemptive_implies_scheduled sched j A4 : execution_starts_with_preemption_point sched j ZERO : job_cost j = 0
last0 (job_preemption_points j) <= job_cost j
unfold job_preemption_points; rewrite ZERO.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j A1 : job_cannot_become_nonpreemptive_before_execution
j A2 : job_cannot_be_nonpreemptive_after_completion j A3 : not_preemptive_implies_scheduled sched j A4 : execution_starts_with_preemption_point sched j ZERO : job_cost j = 0
last0 [seq ρ <- range 0 0 | job_preemptable j ρ] <= 0
simpl ; unfold job_cannot_become_nonpreemptive_before_execution in *.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j A1 : job_preemptable j 0 A2 : job_cannot_be_nonpreemptive_after_completion j A3 : not_preemptive_implies_scheduled sched j A4 : execution_starts_with_preemption_point sched j ZERO : job_cost j = 0
last0 (if job_preemptable j 0 then [:: 0 ] else [::]) <=
0
by rewrite A1.
} Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j A1 : job_cannot_become_nonpreemptive_before_execution
j A2 : job_cannot_be_nonpreemptive_after_completion j A3 : not_preemptive_implies_scheduled sched j A4 : execution_starts_with_preemption_point sched j POSt : 0 < job_cost j
last0 (job_preemption_points j) <= job_cost j
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j A1 : job_cannot_become_nonpreemptive_before_execution
j A2 : job_cannot_be_nonpreemptive_after_completion j A3 : not_preemptive_implies_scheduled sched j A4 : execution_starts_with_preemption_point sched j POSt : 0 < job_cost j
last0 (job_preemption_points j) <= job_cost j
eapply leq_trans; first apply last_of_seq_le_max_of_seq.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j A1 : job_cannot_become_nonpreemptive_before_execution
j A2 : job_cannot_be_nonpreemptive_after_completion j A3 : not_preemptive_implies_scheduled sched j A4 : execution_starts_with_preemption_point sched j POSt : 0 < job_cost j
max0 (job_preemption_points j) <= job_cost j
rewrite job_cost_is_last_element_of_preemption_points.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j A1 : job_cannot_become_nonpreemptive_before_execution
j A2 : job_cannot_be_nonpreemptive_after_completion j A3 : not_preemptive_implies_scheduled sched j A4 : execution_starts_with_preemption_point sched j POSt : 0 < job_cost j
max0 (job_preemption_points j) <=
last0 (job_preemption_points j)
apply last_is_max_in_nondecreasing_seq; first by apply preemption_points_nondecreasing.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j A1 : job_cannot_become_nonpreemptive_before_execution
j A2 : job_cannot_be_nonpreemptive_after_completion j A3 : not_preemptive_implies_scheduled sched j A4 : execution_starts_with_preemption_point sched j POSt : 0 < job_cost j
max0 (job_preemption_points j)
\in job_preemption_points j
apply max0_in_seq.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j A1 : job_cannot_become_nonpreemptive_before_execution
j A2 : job_cannot_be_nonpreemptive_after_completion j A3 : not_preemptive_implies_scheduled sched j A4 : execution_starts_with_preemption_point sched j POSt : 0 < job_cost j
job_preemption_points j <> [::]
have LL := size_of_preemption_points POSt.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j A1 : job_cannot_become_nonpreemptive_before_execution
j A2 : job_cannot_be_nonpreemptive_after_completion j A3 : not_preemptive_implies_scheduled sched j A4 : execution_starts_with_preemption_point sched j POSt : 0 < job_cost jLL : 1 < size (job_preemption_points j)
job_preemption_points j <> [::]
by destruct (job_preemption_points j).
}
Qed .
(** We also show that last nonpreemptive segment is at most the
cost of a job. *)
Lemma job_last_nonpreemptive_segment_le_job_cost :
job_last_nonpreemptive_segment j <= job_cost j.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
job_last_nonpreemptive_segment j <= job_cost j
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
job_last_nonpreemptive_segment j <= job_cost j
eapply leq_trans.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
job_last_nonpreemptive_segment j <= ?n
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
job_last_nonpreemptive_segment j <= ?n
apply last_of_seq_le_max_of_seq.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
max0 (lengths_of_segments j) <= job_cost j
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
max0 (lengths_of_segments j) <= job_cost j
apply job_max_nonpreemptive_segment_le_job_cost.
Qed .
End AuxiliaryLemmas .
(** We prove that the run-to-completion threshold is positive for
any job with positive cost. I.e., in order to become
non-preemptive a job must receive at least one unit of
service. *)
Lemma job_run_to_completion_threshold_positive :
job_cost_positive j ->
0 < job_rtct j.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
job_cost_positive j -> 0 < job_rtct j
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
job_cost_positive j -> 0 < job_rtct j
intros COST; unfold job_rtct, ε.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j
0 <
job_cost j - (job_last_nonpreemptive_segment j - 1 )
have N1 := job_last_nonpreemptive_segment_positive COST.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j N1 : 0 < job_last_nonpreemptive_segment j
0 <
job_cost j - (job_last_nonpreemptive_segment j - 1 )
have N2 := job_last_nonpreemptive_segment_le_job_cost.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j COST : job_cost_positive j N1 : 0 < job_last_nonpreemptive_segment jN2 : job_last_nonpreemptive_segment j <= job_cost j
0 <
job_cost j - (job_last_nonpreemptive_segment j - 1 )
lia .
Qed .
(** Next we show that the run-to-completion threshold is at most
the cost of a job. *)
Lemma job_run_to_completion_threshold_le_job_cost :
job_rtct j <= job_cost j.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
job_rtct j <= job_cost j
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
job_rtct j <= job_cost j
by apply leq_subr. Qed .
(** We prove that a job cannot be preempted
during execution of the last segment. *)
Lemma job_cannot_be_preempted_within_last_segment :
forall (ρ : duration),
job_rtct j <= ρ < job_cost j ->
~~ job_preemptable j ρ.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
forall ρ : duration,
job_rtct j <= ρ < job_cost j -> ~~ job_preemptable j ρ
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
forall ρ : duration,
job_rtct j <= ρ < job_cost j -> ~~ job_preemptable j ρ
move => ρ /andP [GE LT].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j ρ : duration GE : job_rtct j <= ρ LT : ρ < job_cost j
~~ job_preemptable j ρ
apply /negP; intros C.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j ρ : duration GE : job_rtct j <= ρ LT : ρ < job_cost j C : job_preemptable j ρ
False
have POS : 0 < job_cost j; first by lia .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j ρ : duration GE : job_rtct j <= ρ LT : ρ < job_cost j C : job_preemptable j ρ POS : 0 < job_cost j
False
rewrite /job_rtct subnBA in GE; last by apply job_last_nonpreemptive_segment_positive.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j ρ : duration LT : ρ < job_cost j C : job_preemptable j ρ POS : 0 < job_cost jGE : job_cost j + ε - job_last_nonpreemptive_segment j <=
ρ
False
rewrite -addnBAC in GE; [rewrite addn1 in GE | by apply job_last_nonpreemptive_segment_le_job_cost].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j ρ : duration LT : ρ < job_cost j C : job_preemptable j ρ POS : 0 < job_cost jGE : job_cost j - job_last_nonpreemptive_segment j < ρ
False
rewrite job_cost_is_last_element_of_preemption_points in LT, GE.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j ρ : duration C : job_preemptable j ρ POS : 0 < job_cost jLT : ρ < last0 (job_preemption_points j) GE : last0 (job_preemption_points j) -
job_last_nonpreemptive_segment j < ρ
False
rewrite last_seq_minus_last_distance_seq in GE; last by apply preemption_points_nondecreasing.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j ρ : duration C : job_preemptable j ρ POS : 0 < job_cost jLT : ρ < last0 (job_preemption_points j) GE : nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 < ρ
False
have EQ := antidensity_of_nondecreasing_seq.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j ρ : duration C : job_preemptable j ρ POS : 0 < job_cost jLT : ρ < last0 (job_preemption_points j) GE : nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 < ρ EQ : forall (xs : seq nat) (x n : nat),
nondecreasing_sequence xs ->
nth 0 xs n < x < nth 0 xs n.+1 -> x \notin xs
False
specialize (EQ (job_preemption_points j) ρ (size (job_preemption_points j)).-2 ).Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j ρ : duration C : job_preemptable j ρ POS : 0 < job_cost jLT : ρ < last0 (job_preemption_points j) GE : nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 < ρ EQ : nondecreasing_sequence (job_preemption_points j) ->
nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 < ρ <
nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 .+1 ->
ρ \notin job_preemption_points j
False
feed_n 2 EQ; first by apply preemption_points_nondecreasing. Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j ρ : duration C : job_preemptable j ρ POS : 0 < job_cost jLT : ρ < last0 (job_preemption_points j) GE : nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 < ρ EQ : nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 < ρ <
nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 .+1 ->
ρ \notin job_preemption_points j
nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 < ρ <
nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 .+1
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j ρ : duration C : job_preemptable j ρ POS : 0 < job_cost jLT : ρ < last0 (job_preemption_points j) GE : nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 < ρ EQ : nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 < ρ <
nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 .+1 ->
ρ \notin job_preemption_points j
nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 < ρ <
nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 .+1
apply /andP; split ; first by done .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j ρ : duration C : job_preemptable j ρ POS : 0 < job_cost jLT : ρ < last0 (job_preemption_points j) GE : nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 < ρ EQ : nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 < ρ <
nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 .+1 ->
ρ \notin job_preemption_points j
ρ <
nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 .+1
rewrite prednK; first by rewrite -last0_nth.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j ρ : duration C : job_preemptable j ρ POS : 0 < job_cost jLT : ρ < last0 (job_preemption_points j) GE : nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 < ρ EQ : nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 < ρ <
nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 .+1 ->
ρ \notin job_preemption_points j
0 < (size (job_preemption_points j)).-1
rewrite -(leq_add2r 1 ) !addn1 prednK.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j ρ : duration C : job_preemptable j ρ POS : 0 < job_cost jLT : ρ < last0 (job_preemption_points j) GE : nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 < ρ EQ : nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 < ρ <
nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 .+1 ->
ρ \notin job_preemption_points j
1 < size (job_preemption_points j)
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j ρ : duration C : job_preemptable j ρ POS : 0 < job_cost jLT : ρ < last0 (job_preemption_points j) GE : nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 < ρ EQ : nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 < ρ <
nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 .+1 ->
ρ \notin job_preemption_points j
1 < size (job_preemption_points j)
by apply size_of_preemption_points.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j ρ : duration C : job_preemptable j ρ POS : 0 < job_cost jLT : ρ < last0 (job_preemption_points j) GE : nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 < ρ EQ : nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 < ρ <
nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 .+1 ->
ρ \notin job_preemption_points j
0 < size (job_preemption_points j)
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j ρ : duration C : job_preemptable j ρ POS : 0 < job_cost jLT : ρ < last0 (job_preemption_points j) GE : nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 < ρ EQ : nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 < ρ <
nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 .+1 ->
ρ \notin job_preemption_points j
0 < size (job_preemption_points j)
by eapply leq_trans; last apply size_of_preemption_points.
} Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j ρ : duration C : job_preemptable j ρ POS : 0 < job_cost jLT : ρ < last0 (job_preemption_points j) GE : nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 < ρ EQ : ρ \notin job_preemption_points j
False
move : EQ => /negP EQ; apply : EQ.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j ρ : duration C : job_preemptable j ρ POS : 0 < job_cost jLT : ρ < last0 (job_preemption_points j) GE : nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 < ρ
ρ \in job_preemption_points j
apply conversion_preserves_equivalence; try done .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j ρ : duration C : job_preemptable j ρ POS : 0 < job_cost jLT : ρ < last0 (job_preemption_points j) GE : nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 < ρ
ρ <= job_cost j
eapply leq_trans; first by apply ltnW; exact LT.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j ρ : duration C : job_preemptable j ρ POS : 0 < job_cost jLT : ρ < last0 (job_preemption_points j) GE : nth 0 (job_preemption_points j)
(size (job_preemption_points j)).-2 < ρ
last0 (job_preemption_points j) <= job_cost j
by rewrite job_cost_is_last_element_of_preemption_points.
Qed .
(** In order to get a consistent schedule, the scheduler should respect
the notion of run-to-completion threshold. We assume that, after
a job reaches its run-to-completion threshold, it cannot be preempted
until its completion. *)
Lemma job_nonpreemptive_after_run_to_completion_threshold :
forall t t' ,
t <= t' ->
job_rtct j <= service sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t'.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
forall t t' : nat,
t <= t' ->
job_rtct j <= service sched j t ->
~~ completed_by sched j t' -> scheduled_at sched j t'
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j
forall t t' : nat,
t <= t' ->
job_rtct j <= service sched j t ->
~~ completed_by sched j t' -> scheduled_at sched j t'
intros ? ? LE TH COM.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j t, t' : nat LE : t <= t' TH : job_rtct j <= service sched j t COM : ~~ completed_by sched j t'
scheduled_at sched j t'
apply H_valid_preemption_model; first by done .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j t, t' : nat LE : t <= t' TH : job_rtct j <= service sched j t COM : ~~ completed_by sched j t'
~~ job_preemptable j (service sched j t')
apply job_cannot_be_preempted_within_last_segment; apply /andP; split .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j t, t' : nat LE : t <= t' TH : job_rtct j <= service sched j t COM : ~~ completed_by sched j t'
job_rtct j <= service sched j t'
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j t, t' : nat LE : t <= t' TH : job_rtct j <= service sched j t COM : ~~ completed_by sched j t'
job_rtct j <= service sched j t'
by apply leq_trans with (service sched j t); last apply service_monotonic.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j t, t' : nat LE : t <= t' TH : job_rtct j <= service sched j t COM : ~~ completed_by sched j t'
service sched j t' < job_cost j
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job arr_seq : arrival_sequence Job sched : schedule PState H_valid_preemption_model : valid_preemption_model
arr_seq sched j : Job H_j_arrives : arrives_in arr_seq j t, t' : nat LE : t <= t' TH : job_rtct j <= service sched j t COM : ~~ completed_by sched j t'
service sched j t' < job_cost j
by rewrite ltnNge.
Qed .
End RunToCompletionThreshold .
(** We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq
will be able to apply them automatically. *)
Global Hint Resolve job_run_to_completion_threshold_le_job_cost : basic_rt_facts.