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.facts.model.service_of_jobs.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.preemption.rtc_threshold.job_preemptable.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.analysis.abstract .definitions.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 of a job *)
(** In this module, we provide a sufficient condition under which a job
receives enough service to become non-preemptive. *)
(** Previously we defined the notion of run-to-completion threshold (see file
abstract.run_to_completion_threshold.v). Run-to-completion threshold is the
amount of service after which a job cannot be preempted until its completion.
In this section we prove that if cumulative interference inside a busy interval
is bounded by a certain constant then a job executes long enough to reach its
run-to-completion threshold and become non-preemptive. *)
Section AbstractRTARunToCompletionThreshold .
(** 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 uni-service ideal processor state model. *)
Context {PState : ProcessorState Job}.
Hypothesis H_ideal_progress_proc_model : ideal_progress_proc_model PState.
Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.
(** Consider any arrival sequence with consistent arrivals ... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
(** ... and any schedule of this arrival sequence. *)
Variable sched : schedule PState.
(** Assume we are provided with abstract functions for interference and interfering workload. *)
Variable interference : Job -> instant -> bool.
Variable interfering_workload : Job -> instant -> duration.
(** For simplicity, let's define some local names. *)
Let work_conserving := work_conserving arr_seq sched.
Let cumul_interference := cumul_interference interference.
Let cumul_interfering_workload := cumul_interfering_workload interfering_workload.
Let busy_interval := busy_interval sched interference interfering_workload.
(** We assume that the schedule is work-conserving. *)
Hypothesis H_work_conserving : work_conserving interference interfering_workload.
(** Let [j] be any job of task [tsk] with positive cost. *)
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_cost_positive : job_cost_positive j.
(** Next, consider any busy interval <<[t1, t2)>> of job [j]. *)
Variable t1 t2 : instant.
Hypothesis H_busy_interval : busy_interval j t1 t2.
(** First, we prove that job [j] completes by the end of the busy interval.
Note that the busy interval contains the execution of job j, in addition
time instant t2 is a quiet time. Thus by the definition of a quiet time
the job should be completed before time t2. *)
Lemma job_completes_within_busy_interval :
completed_by sched j t2.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2
completed_by sched j t2
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2
completed_by sched j t2
move : (H_busy_interval) => [[/andP [_ LT] [_ _]] [_ QT2]].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 LT : job_arrival j < t2 QT2 : ~~ pending_earlier_and_at sched j t2
completed_by sched j t2
unfold pending, has_arrived in QT2.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 LT : job_arrival j < t2 QT2 : ~~ pending_earlier_and_at sched j t2
completed_by sched j t2
move : QT2; rewrite /pending negb_and; move => /orP [QT2|QT2].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 LT : job_arrival j < t2 QT2 : ~~ arrived_before j t2
completed_by sched j t2
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 LT : job_arrival j < t2 QT2 : ~~ arrived_before j t2
completed_by sched j t2
by move : QT2 => /negP QT2; exfalso ; apply QT2, ltnW. } Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 LT : job_arrival j < t2 QT2 : ~~ ~~ completed_by sched j t2
completed_by sched j t2
by rewrite Bool.negb_involutive in QT2.
Qed .
(** In this section we show that the cumulative interference is a complement to
the total time where job [j] is scheduled inside the busy interval. *)
Section InterferenceIsComplement .
(** Consider any sub-interval <<[t, t + delta)>> inside the busy interval [t1, t2). *)
Variables (t : instant) (delta : duration).
Hypothesis H_greater_than_or_equal : t1 <= t.
Hypothesis H_less_or_equal : t + delta <= t2.
(** We prove that sum of cumulative service and cumulative interference
in the interval <<[t, t + delta)>> is equal to delta. *)
Lemma interference_is_complement_to_schedule :
service_during sched j t (t + delta) + cumul_interference j t (t + delta) = delta.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 t : instant delta : duration H_greater_than_or_equal : t1 <= t H_less_or_equal : t + delta <= t2
service_during sched j t (t + delta) +
cumul_interference j t (t + delta) = delta
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 t : instant delta : duration H_greater_than_or_equal : t1 <= t H_less_or_equal : t + delta <= t2
service_during sched j t (t + delta) +
cumul_interference j t (t + delta) = delta
rewrite /service_during /cumul_interference/service_at.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 t : instant delta : duration H_greater_than_or_equal : t1 <= t H_less_or_equal : t + delta <= t2
\sum_(t <= t < t + delta) service_in j (sched t) +
definitions.cumul_interference interference j t
(t + delta) = delta
rewrite -big_split //=.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 t : instant delta : duration H_greater_than_or_equal : t1 <= t H_less_or_equal : t + delta <= t2
\sum_(t <= i < t + delta)
(service_in j (sched i) + interference j i) = delta
rewrite -{2 }(sum_of_ones t delta).Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 t : instant delta : duration H_greater_than_or_equal : t1 <= t H_less_or_equal : t + delta <= t2
\sum_(t <= i < t + delta)
(service_in j (sched i) + interference j i) =
\sum_(t <= x < t + delta) 1
rewrite big_nat [in RHS]big_nat.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 t : instant delta : duration H_greater_than_or_equal : t1 <= t H_less_or_equal : t + delta <= t2
\sum_(t <= i < t + delta | t <= i < t + delta)
(service_in j (sched i) + interference j i) =
\sum_(t <= i < t + delta | t <= i < t + delta) 1
apply : eq_bigr=> x /andP[Lo Hi].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 t : instant delta : duration H_greater_than_or_equal : t1 <= t H_less_or_equal : t + delta <= t2 x : nat Lo : t <= x Hi : x < t + delta
service_in j (sched x) + interference j x = 1
move : (H_work_conserving j t1 t2 x) => Workj.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 t : instant delta : duration H_greater_than_or_equal : t1 <= t H_less_or_equal : t + delta <= t2 x : nat Lo : t <= x Hi : x < t + delta Workj : arrives_in arr_seq j ->
0 < job_cost j ->
definitions.busy_interval sched interference
interfering_workload j t1 t2 ->
t1 <= x < t2 ->
~ interference j x <-> scheduled_at sched j x
service_in j (sched x) + interference j x = 1
feed_n 4 Workj; try done . Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 t : instant delta : duration H_greater_than_or_equal : t1 <= t H_less_or_equal : t + delta <= t2 x : nat Lo : t <= x Hi : x < t + delta Workj : t1 <= x < t2 ->
~ interference j x <-> scheduled_at sched j x
t1 <= x < t2
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 t : instant delta : duration H_greater_than_or_equal : t1 <= t H_less_or_equal : t + delta <= t2 x : nat Lo : t <= x Hi : x < t + delta Workj : t1 <= x < t2 ->
~ interference j x <-> scheduled_at sched j x
t1 <= x < t2
by apply /andP; split ; eapply leq_trans; eauto 2 . } Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 t : instant delta : duration H_greater_than_or_equal : t1 <= t H_less_or_equal : t + delta <= t2 x : nat Lo : t <= x Hi : x < t + delta Workj : ~ interference j x <-> scheduled_at sched j x
service_in j (sched x) + interference j x = 1
destruct interference.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 t : instant delta : duration H_greater_than_or_equal : t1 <= t H_less_or_equal : t + delta <= t2 x : nat Lo : t <= x Hi : x < t + delta Workj : ~ true <-> scheduled_at sched j x
service_in j (sched x) + true = 1
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 t : instant delta : duration H_greater_than_or_equal : t1 <= t H_less_or_equal : t + delta <= t2 x : nat Lo : t <= x Hi : x < t + delta Workj : ~ true <-> scheduled_at sched j x
service_in j (sched x) + true = 1
replace (service_in _ _) with 0 ; auto ; symmetry .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 t : instant delta : duration H_greater_than_or_equal : t1 <= t H_less_or_equal : t + delta <= t2 x : nat Lo : t <= x Hi : x < t + delta Workj : ~ true <-> scheduled_at sched j x
service_in j (sched x) = 0
apply no_service_not_scheduled; auto .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 t : instant delta : duration H_greater_than_or_equal : t1 <= t H_less_or_equal : t + delta <= t2 x : nat Lo : t <= x Hi : x < t + delta Workj : ~ true <-> scheduled_at sched j x
~~ scheduled_at sched j x
now apply /negP; intros SCHED; apply Workj in SCHED; apply SCHED.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 t : instant delta : duration H_greater_than_or_equal : t1 <= t H_less_or_equal : t + delta <= t2 x : nat Lo : t <= x Hi : x < t + delta Workj : ~ false <-> scheduled_at sched j x
service_in j (sched x) + false = 1
- Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 t : instant delta : duration H_greater_than_or_equal : t1 <= t H_less_or_equal : t + delta <= t2 x : nat Lo : t <= x Hi : x < t + delta Workj : ~ false <-> scheduled_at sched j x
service_in j (sched x) + false = 1
replace (service_in _ _) with 1 ; auto ; symmetry .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 t : instant delta : duration H_greater_than_or_equal : t1 <= t H_less_or_equal : t + delta <= t2 x : nat Lo : t <= x Hi : x < t + delta Workj : ~ false <-> scheduled_at sched j x
service_in j (sched x) = 1
apply /eqP; rewrite eqn_leq; apply /andP; split .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 t : instant delta : duration H_greater_than_or_equal : t1 <= t H_less_or_equal : t + delta <= t2 x : nat Lo : t <= x Hi : x < t + delta Workj : ~ false <-> scheduled_at sched j x
service_in j (sched x) <= 1
+ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 t : instant delta : duration H_greater_than_or_equal : t1 <= t H_less_or_equal : t + delta <= t2 x : nat Lo : t <= x Hi : x < t + delta Workj : ~ false <-> scheduled_at sched j x
service_in j (sched x) <= 1
apply H_unit_service_proc_model.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 t : instant delta : duration H_greater_than_or_equal : t1 <= t H_less_or_equal : t + delta <= t2 x : nat Lo : t <= x Hi : x < t + delta Workj : ~ false <-> scheduled_at sched j x
0 < service_in j (sched x)
+ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 t : instant delta : duration H_greater_than_or_equal : t1 <= t H_less_or_equal : t + delta <= t2 x : nat Lo : t <= x Hi : x < t + delta Workj : ~ false <-> scheduled_at sched j x
0 < service_in j (sched x)
now apply H_ideal_progress_proc_model, Workj.
Qed .
End InterferenceIsComplement .
(** In this section, we prove a sufficient condition under which job [j] receives enough service. *)
Section InterferenceBoundedImpliesEnoughService .
(** Let progress_of_job be the desired service of job j. *)
Variable progress_of_job : duration.
Hypothesis H_progress_le_job_cost : progress_of_job <= job_cost j.
(** Assume that for some delta, the sum of desired progress and cumulative
interference is bounded by delta (i.e., the supply). *)
Variable delta : duration.
Hypothesis H_total_workload_is_bounded :
progress_of_job + cumul_interference j t1 (t1 + delta) <= delta.
(** Then, it must be the case that the job has received no less service than progress_of_job. *)
Theorem j_receives_at_least_run_to_completion_threshold :
service sched j (t1 + delta) >= progress_of_job.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j delta : duration H_total_workload_is_bounded : progress_of_job +
cumul_interference j t1
(t1 + delta) <= delta
progress_of_job <= service sched j (t1 + delta)
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j delta : duration H_total_workload_is_bounded : progress_of_job +
cumul_interference j t1
(t1 + delta) <= delta
progress_of_job <= service sched j (t1 + delta)
case NEQ: (t1 + delta <= t2); last first .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j delta : duration H_total_workload_is_bounded : progress_of_job +
cumul_interference j t1
(t1 + delta) <= delta NEQ : (t1 + delta <= t2) = false
progress_of_job <= service sched j (t1 + delta)
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j delta : duration H_total_workload_is_bounded : progress_of_job +
cumul_interference j t1
(t1 + delta) <= delta NEQ : (t1 + delta <= t2) = false
progress_of_job <= service sched j (t1 + delta)
intros .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j delta : duration H_total_workload_is_bounded : progress_of_job +
cumul_interference j t1
(t1 + delta) <= delta NEQ : (t1 + delta <= t2) = false
progress_of_job <= service sched j (t1 + delta)
have L8 := job_completes_within_busy_interval.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j delta : duration H_total_workload_is_bounded : progress_of_job +
cumul_interference j t1
(t1 + delta) <= delta NEQ : (t1 + delta <= t2) = false L8 : completed_by sched j t2
progress_of_job <= service sched j (t1 + delta)
apply leq_trans with (job_cost j); first by done .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j delta : duration H_total_workload_is_bounded : progress_of_job +
cumul_interference j t1
(t1 + delta) <= delta NEQ : (t1 + delta <= t2) = false L8 : completed_by sched j t2
job_cost j <= service sched j (t1 + delta)
rewrite /service.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j delta : duration H_total_workload_is_bounded : progress_of_job +
cumul_interference j t1
(t1 + delta) <= delta NEQ : (t1 + delta <= t2) = false L8 : completed_by sched j t2
job_cost j <= service_during sched j 0 (t1 + delta)
rewrite -(service_during_cat _ _ _ t2).Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j delta : duration H_total_workload_is_bounded : progress_of_job +
cumul_interference j t1
(t1 + delta) <= delta NEQ : (t1 + delta <= t2) = false L8 : completed_by sched j t2
job_cost j <=
service_during sched j 0 t2 +
service_during sched j t2 (t1 + delta)
apply leq_trans with (service_during sched j 0 t2); [by done | by rewrite leq_addr].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j delta : duration H_total_workload_is_bounded : progress_of_job +
cumul_interference j t1
(t1 + delta) <= delta NEQ : (t1 + delta <= t2) = false L8 : completed_by sched j t2
0 <= t2 <= t1 + delta
by apply /andP; split ; last (apply negbT in NEQ; apply ltnW; rewrite ltnNge).
} Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j delta : duration H_total_workload_is_bounded : progress_of_job +
cumul_interference j t1
(t1 + delta) <= delta NEQ : (t1 + delta <= t2) = true
progress_of_job <= service sched j (t1 + delta)
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j delta : duration H_total_workload_is_bounded : progress_of_job +
cumul_interference j t1
(t1 + delta) <= delta NEQ : (t1 + delta <= t2) = true
progress_of_job <= service sched j (t1 + delta)
move : H_total_workload_is_bounded => BOUND.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j delta : duration H_total_workload_is_bounded : progress_of_job +
cumul_interference j t1
(t1 + delta) <= delta NEQ : (t1 + delta <= t2) = true BOUND : progress_of_job +
cumul_interference j t1 (t1 + delta) <= delta
progress_of_job <= service sched j (t1 + delta)
rewrite addnC in BOUND.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j delta : duration H_total_workload_is_bounded : progress_of_job +
cumul_interference j t1
(t1 + delta) <= delta NEQ : (t1 + delta <= t2) = true BOUND : cumul_interference j t1 (t1 + delta) +
progress_of_job <= delta
progress_of_job <= service sched j (t1 + delta)
apply leq_subRL_impl in BOUND.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j delta : duration H_total_workload_is_bounded : progress_of_job +
cumul_interference j t1
(t1 + delta) <= delta NEQ : (t1 + delta <= t2) = true BOUND : progress_of_job <=
delta - cumul_interference j t1 (t1 + delta)
progress_of_job <= service sched j (t1 + delta)
apply leq_trans with (delta - cumul_interference j t1 (t1 + delta)); first by done .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j delta : duration H_total_workload_is_bounded : progress_of_job +
cumul_interference j t1
(t1 + delta) <= delta NEQ : (t1 + delta <= t2) = true BOUND : progress_of_job <=
delta - cumul_interference j t1 (t1 + delta)
delta - cumul_interference j t1 (t1 + delta) <=
service sched j (t1 + delta)
apply leq_trans with (service_during sched j t1 (t1 + delta)).Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j delta : duration H_total_workload_is_bounded : progress_of_job +
cumul_interference j t1
(t1 + delta) <= delta NEQ : (t1 + delta <= t2) = true BOUND : progress_of_job <=
delta - cumul_interference j t1 (t1 + delta)
delta - cumul_interference j t1 (t1 + delta) <=
service_during sched j t1 (t1 + delta)
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j delta : duration H_total_workload_is_bounded : progress_of_job +
cumul_interference j t1
(t1 + delta) <= delta NEQ : (t1 + delta <= t2) = true BOUND : progress_of_job <=
delta - cumul_interference j t1 (t1 + delta)
delta - cumul_interference j t1 (t1 + delta) <=
service_during sched j t1 (t1 + delta)
rewrite -{1 }[delta](interference_is_complement_to_schedule t1) //.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j delta : duration H_total_workload_is_bounded : progress_of_job +
cumul_interference j t1
(t1 + delta) <= delta NEQ : (t1 + delta <= t2) = true BOUND : progress_of_job <=
delta - cumul_interference j t1 (t1 + delta)
service_during sched j t1 (t1 + delta) +
cumul_interference j t1 (t1 + delta) -
cumul_interference j t1 (t1 + delta) <=
service_during sched j t1 (t1 + delta)
rewrite -addnBA // subnn addn0 //.
} Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j delta : duration H_total_workload_is_bounded : progress_of_job +
cumul_interference j t1
(t1 + delta) <= delta NEQ : (t1 + delta <= t2) = true BOUND : progress_of_job <=
delta - cumul_interference j t1 (t1 + delta)
service_during sched j t1 (t1 + delta) <=
service sched j (t1 + delta)
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j delta : duration H_total_workload_is_bounded : progress_of_job +
cumul_interference j t1
(t1 + delta) <= delta NEQ : (t1 + delta <= t2) = true BOUND : progress_of_job <=
delta - cumul_interference j t1 (t1 + delta)
service_during sched j t1 (t1 + delta) <=
service sched j (t1 + delta)
rewrite /service -[X in _ <= X](service_during_cat _ _ _ t1).Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j delta : duration H_total_workload_is_bounded : progress_of_job +
cumul_interference j t1
(t1 + delta) <= delta NEQ : (t1 + delta <= t2) = true BOUND : progress_of_job <=
delta - cumul_interference j t1 (t1 + delta)
service_during sched j t1 (t1 + delta) <=
service_during sched j 0 t1 +
service_during sched j t1 (t1 + delta)
rewrite leq_addl //.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 progress_of_job : duration H_progress_le_job_cost : progress_of_job <= job_cost j delta : duration H_total_workload_is_bounded : progress_of_job +
cumul_interference j t1
(t1 + delta) <= delta NEQ : (t1 + delta <= t2) = true BOUND : progress_of_job <=
delta - cumul_interference j t1 (t1 + delta)
0 <= t1 <= t1 + delta
by apply /andP; split ; last rewrite leq_addr.
}
}
Qed .
End InterferenceBoundedImpliesEnoughService .
(** In this section we prove a simple lemma about completion of
a job after is reaches run-to-completion threshold. *)
Section CompletionOfJobAfterRunToCompletionThreshold .
(** Assume that completed jobs do not execute ... *)
Hypothesis H_completed_jobs_dont_execute :
completed_jobs_dont_execute sched.
(** .. and the preemption model is valid. *)
Hypothesis H_valid_preemption_model :
valid_preemption_model arr_seq sched.
(** Then, job [j] must complete in [job_cost j - job_rtct j] time
units after it reaches run-to-completion threshold. *)
Lemma job_completes_after_reaching_run_to_completion_threshold :
forall t ,
job_rtct j <= service sched j t ->
completed_by sched j (t + (job_cost j - job_rtct j)).Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_preemption_model : valid_preemption_model
arr_seq sched
forall t : instant,
job_rtct j <= service sched j t ->
completed_by sched j (t + (job_cost j - job_rtct j))
Proof .Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_preemption_model : valid_preemption_model
arr_seq sched
forall t : instant,
job_rtct j <= service sched j t ->
completed_by sched j (t + (job_cost j - job_rtct j))
move => t ES.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_preemption_model : valid_preemption_model
arr_seq sched t : instant ES : job_rtct j <= service sched j t
completed_by sched j (t + (job_cost j - job_rtct j))
set (job_cost j - job_rtct j) as job_last.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_preemption_model : valid_preemption_model
arr_seq sched t : instant ES : job_rtct j <= service sched j t job_last := job_cost j - job_rtct j : nat
completed_by sched j (t + job_last)
have LSNP := @job_nonpreemptive_after_run_to_completion_threshold
Job H0 H1 _ arr_seq sched _ j _ t.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_preemption_model : valid_preemption_model
arr_seq sched t : instant ES : job_rtct j <= service sched j t job_last := job_cost j - job_rtct j : nat LSNP : valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_rtct j <= service sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t'
completed_by sched j (t + job_last)
apply negbNE; apply /negP; intros CONTR.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_preemption_model : valid_preemption_model
arr_seq sched t : instant ES : job_rtct j <= service sched j t job_last := job_cost j - job_rtct j : nat LSNP : valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_rtct j <= service sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' CONTR : ~~ completed_by sched j (t + job_last)
False
have SCHED: forall t' , t <= t' <= t + job_last -> scheduled_at sched j t'.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_preemption_model : valid_preemption_model
arr_seq sched t : instant ES : job_rtct j <= service sched j t job_last := job_cost j - job_rtct j : nat LSNP : valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_rtct j <= service sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' CONTR : ~~ completed_by sched j (t + job_last)
forall t' : nat,
t <= t' <= t + job_last -> scheduled_at sched j t'
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_preemption_model : valid_preemption_model
arr_seq sched t : instant ES : job_rtct j <= service sched j t job_last := job_cost j - job_rtct j : nat LSNP : valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_rtct j <= service sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' CONTR : ~~ completed_by sched j (t + job_last)
forall t' : nat,
t <= t' <= t + job_last -> scheduled_at sched j t'
move => t' /andP [GE LT].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_preemption_model : valid_preemption_model
arr_seq sched t : instant ES : job_rtct j <= service sched j t job_last := job_cost j - job_rtct j : nat LSNP : valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_rtct j <= service sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' CONTR : ~~ completed_by sched j (t + job_last) t' : nat GE : t <= t' LT : t' <= t + job_last
scheduled_at sched j t'
rewrite -[t'](@subnKC t) //.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_preemption_model : valid_preemption_model
arr_seq sched t : instant ES : job_rtct j <= service sched j t job_last := job_cost j - job_rtct j : nat LSNP : valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_rtct j <= service sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' CONTR : ~~ completed_by sched j (t + job_last) t' : nat GE : t <= t' LT : t' <= t + job_last
scheduled_at sched j (t + (t' - t))
eapply LSNP; eauto 2 ; first by rewrite leq_addr.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_preemption_model : valid_preemption_model
arr_seq sched t : instant ES : job_rtct j <= service sched j t job_last := job_cost j - job_rtct j : nat LSNP : valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_rtct j <= service sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' CONTR : ~~ completed_by sched j (t + job_last) t' : nat GE : t <= t' LT : t' <= t + job_last
~~ completed_by sched j (t + (t' - t))
rewrite subnKC //.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_preemption_model : valid_preemption_model
arr_seq sched t : instant ES : job_rtct j <= service sched j t job_last := job_cost j - job_rtct j : nat LSNP : valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_rtct j <= service sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' CONTR : ~~ completed_by sched j (t + job_last) t' : nat GE : t <= t' LT : t' <= t + job_last
~~ completed_by sched j t'
apply /negP; intros COMPL.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_preemption_model : valid_preemption_model
arr_seq sched t : instant ES : job_rtct j <= service sched j t job_last := job_cost j - job_rtct j : nat LSNP : valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_rtct j <= service sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' CONTR : ~~ completed_by sched j (t + job_last) t' : nat GE : t <= t' LT : t' <= t + job_last COMPL : completed_by sched j t'
False
move : CONTR => /negP Temp; apply : Temp.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_preemption_model : valid_preemption_model
arr_seq sched t : instant ES : job_rtct j <= service sched j t job_last := job_cost j - job_rtct j : nat LSNP : valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_rtct j <= service sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' t' : nat GE : t <= t' LT : t' <= t + job_last COMPL : completed_by sched j t'
completed_by sched j (t + job_last)
exact : completion_monotonic COMPL.
} Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_preemption_model : valid_preemption_model
arr_seq sched t : instant ES : job_rtct j <= service sched j t job_last := job_cost j - job_rtct j : nat LSNP : valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_rtct j <= service sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' CONTR : ~~ completed_by sched j (t + job_last) SCHED : forall t' : nat,
t <= t' <= t + job_last ->
scheduled_at sched j t'
False
have SERV: job_last + 1 <= \sum_(t <= t' < t + (job_last + 1 )) service_at sched j t'.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_preemption_model : valid_preemption_model
arr_seq sched t : instant ES : job_rtct j <= service sched j t job_last := job_cost j - job_rtct j : nat LSNP : valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_rtct j <= service sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' CONTR : ~~ completed_by sched j (t + job_last) SCHED : forall t' : nat,
t <= t' <= t + job_last ->
scheduled_at sched j t'
job_last + 1 <=
\sum_(t <= t' < t + (job_last + 1 ))
service_at sched j t'
{ Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_preemption_model : valid_preemption_model
arr_seq sched t : instant ES : job_rtct j <= service sched j t job_last := job_cost j - job_rtct j : nat LSNP : valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_rtct j <= service sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' CONTR : ~~ completed_by sched j (t + job_last) SCHED : forall t' : nat,
t <= t' <= t + job_last ->
scheduled_at sched j t'
job_last + 1 <=
\sum_(t <= t' < t + (job_last + 1 ))
service_at sched j t'
rewrite -{1 }[job_last + 1 ]addn0 -{2 }(subnn t) addnBA // addnC.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_preemption_model : valid_preemption_model
arr_seq sched t : instant ES : job_rtct j <= service sched j t job_last := job_cost j - job_rtct j : nat LSNP : valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_rtct j <= service sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' CONTR : ~~ completed_by sched j (t + job_last) SCHED : forall t' : nat,
t <= t' <= t + job_last ->
scheduled_at sched j t'
t + (job_last + 1 ) - t <=
\sum_(t <= t' < t + (job_last + 1 ))
service_at sched j t'
rewrite -{1 }[_+_-_]addn0 -[_+_-_]mul1n -iter_addn -big_const_nat.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_preemption_model : valid_preemption_model
arr_seq sched t : instant ES : job_rtct j <= service sched j t job_last := job_cost j - job_rtct j : nat LSNP : valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_rtct j <= service sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' CONTR : ~~ completed_by sched j (t + job_last) SCHED : forall t' : nat,
t <= t' <= t + job_last ->
scheduled_at sched j t'
\sum_(t <= i < t + (job_last + 1 )) 1 <=
\sum_(t <= t' < t + (job_last + 1 ))
service_at sched j t'
rewrite big_nat_cond [in X in _ <= X]big_nat_cond.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_preemption_model : valid_preemption_model
arr_seq sched t : instant ES : job_rtct j <= service sched j t job_last := job_cost j - job_rtct j : nat LSNP : valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_rtct j <= service sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' CONTR : ~~ completed_by sched j (t + job_last) SCHED : forall t' : nat,
t <= t' <= t + job_last ->
scheduled_at sched j t'
\sum_(t <= i < t + (job_last + 1 ) | (t <= i <
t +
(job_last + 1 )) &&
true) 1 <=
\sum_(t <= i < t + (job_last + 1 ) | (t <= i <
t +
(job_last + 1 )) &&
true)
service_at sched j i
rewrite leq_sum //.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_preemption_model : valid_preemption_model
arr_seq sched t : instant ES : job_rtct j <= service sched j t job_last := job_cost j - job_rtct j : nat LSNP : valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_rtct j <= service sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' CONTR : ~~ completed_by sched j (t + job_last) SCHED : forall t' : nat,
t <= t' <= t + job_last ->
scheduled_at sched j t'
forall i : nat,
(t <= i < t + (job_last + 1 )) && true ->
0 < service_at sched j i
move => t' /andP [NEQ _].Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_preemption_model : valid_preemption_model
arr_seq sched t : instant ES : job_rtct j <= service sched j t job_last := job_cost j - job_rtct j : nat LSNP : valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_rtct j <= service sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' CONTR : ~~ completed_by sched j (t + job_last) SCHED : forall t' : nat,
t <= t' <= t + job_last ->
scheduled_at sched j t't' : nat NEQ : t <= t' < t + (job_last + 1 )
0 < service_at sched j t'
apply H_ideal_progress_proc_model; apply SCHED.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_preemption_model : valid_preemption_model
arr_seq sched t : instant ES : job_rtct j <= service sched j t job_last := job_cost j - job_rtct j : nat LSNP : valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_rtct j <= service sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' CONTR : ~~ completed_by sched j (t + job_last) SCHED : forall t' : nat,
t <= t' <= t + job_last ->
scheduled_at sched j t't' : nat NEQ : t <= t' < t + (job_last + 1 )
t <= t' <= t + job_last
by rewrite addn1 addnS ltnS in NEQ.
} Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_preemption_model : valid_preemption_model
arr_seq sched t : instant ES : job_rtct j <= service sched j t job_last := job_cost j - job_rtct j : nat LSNP : valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_rtct j <= service sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' CONTR : ~~ completed_by sched j (t + job_last) SCHED : forall t' : nat,
t <= t' <= t + job_last ->
scheduled_at sched j t'SERV : job_last + 1 <=
\sum_(t <= t' <
t + (job_last + 1 ))
service_at sched j t'
False
move : (service_at_most_cost
_ H_completed_jobs_dont_execute j H_unit_service_proc_model
(t + job_last.+1 )).Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_preemption_model : valid_preemption_model
arr_seq sched t : instant ES : job_rtct j <= service sched j t job_last := job_cost j - job_rtct j : nat LSNP : valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_rtct j <= service sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' CONTR : ~~ completed_by sched j (t + job_last) SCHED : forall t' : nat,
t <= t' <= t + job_last ->
scheduled_at sched j t'SERV : job_last + 1 <=
\sum_(t <= t' <
t + (job_last + 1 ))
service_at sched j t'
service sched j (t + job_last.+1 ) <= job_cost j ->
False
rewrite leqNgt; move => /negP T; apply : T.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_preemption_model : valid_preemption_model
arr_seq sched t : instant ES : job_rtct j <= service sched j t job_last := job_cost j - job_rtct j : nat LSNP : valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_rtct j <= service sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' CONTR : ~~ completed_by sched j (t + job_last) SCHED : forall t' : nat,
t <= t' <= t + job_last ->
scheduled_at sched j t'SERV : job_last + 1 <=
\sum_(t <= t' <
t + (job_last + 1 ))
service_at sched j t'
job_cost j < service sched j (t + job_last.+1 )
rewrite /service -(service_during_cat _ _ _ t); last by (apply /andP; split ; last rewrite leq_addr).Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_preemption_model : valid_preemption_model
arr_seq sched t : instant ES : job_rtct j <= service sched j t job_last := job_cost j - job_rtct j : nat LSNP : valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_rtct j <= service sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' CONTR : ~~ completed_by sched j (t + job_last) SCHED : forall t' : nat,
t <= t' <= t + job_last ->
scheduled_at sched j t'SERV : job_last + 1 <=
\sum_(t <= t' <
t + (job_last + 1 ))
service_at sched j t'
job_cost j <
service_during sched j 0 t +
service_during sched j t (t + job_last.+1 )
apply leq_trans with (job_rtct j + service_during sched j t (t + job_last.+1 ));
last by rewrite leq_add2r.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_preemption_model : valid_preemption_model
arr_seq sched t : instant ES : job_rtct j <= service sched j t job_last := job_cost j - job_rtct j : nat LSNP : valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_rtct j <= service sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' CONTR : ~~ completed_by sched j (t + job_last) SCHED : forall t' : nat,
t <= t' <= t + job_last ->
scheduled_at sched j t'SERV : job_last + 1 <=
\sum_(t <= t' <
t + (job_last + 1 ))
service_at sched j t'
job_cost j <
job_rtct j +
service_during sched j t (t + job_last.+1 )
apply leq_trans with (job_rtct j + job_last.+1 ); last by rewrite leq_add2l /service_during -addn1.Job : JobType H : JobArrival Job H0 : JobCost Job H1 : JobPreemptable Job PState : ProcessorState Job H_ideal_progress_proc_model : ideal_progress_proc_model
PState H_unit_service_proc_model : unit_service_proc_model
PState arr_seq : arrival_sequence Job H_arrival_times_are_consistent : consistent_arrival_times
arr_seq sched : schedule PState interference : Job -> instant -> bool interfering_workload : Job -> instant -> duration work_conserving := definitions.work_conserving arr_seq
sched : (Job -> instant -> bool) ->
(Job -> instant -> duration) -> Prop cumul_interference := definitions.cumul_interference
interference : Job -> nat -> nat -> nat cumul_interfering_workload := definitions.cumul_interfering_workload
interfering_workload : Job -> nat -> nat -> nat busy_interval := definitions.busy_interval sched
interference interfering_workload : Job -> instant -> instant -> Prop H_work_conserving : work_conserving interference
interfering_workload j : Job H_j_arrives : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval j t1 t2 H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched H_valid_preemption_model : valid_preemption_model
arr_seq sched t : instant ES : job_rtct j <= service sched j t job_last := job_cost j - job_rtct j : nat LSNP : valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_rtct j <= service sched j t ->
~~ completed_by sched j t' ->
scheduled_at sched j t' CONTR : ~~ completed_by sched j (t + job_last) SCHED : forall t' : nat,
t <= t' <= t + job_last ->
scheduled_at sched j t'SERV : job_last + 1 <=
\sum_(t <= t' <
t + (job_last + 1 ))
service_at sched j t'
job_cost j < job_rtct j + job_last.+1
by rewrite addnS ltnS subnKC //; eapply job_run_to_completion_threshold_le_job_cost; eauto .
Qed .
End CompletionOfJobAfterRunToCompletionThreshold .
End AbstractRTARunToCompletionThreshold .