Built with
Alectryon , running Coq+SerAPI v8.15.0+0.15.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.analysis.definitions.job_properties.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Require Export prosa.analysis.facts.behavior.all .Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Export prosa.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]
(** * Lemmas About Abstract Busy Intervals *)
(** In this file we prove a few basic lemmas about the notion of
an abstract busy interval. *)
Section LemmasAboutAbstractBusyInterval .
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Consider any kind of processor state model. *)
Context {PState : ProcessorState Job}.
(** Assume we are provided with abstract functions for interference
and interfering workload. *)
Context `{Interference Job}.
Context `{InterferingWorkload Job}.
(** Consider any arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
(** Consider an arbitrary task [tsk]. *)
Variable tsk : Task.
(** Next, consider any work-conserving ideal uni-processor schedule
of this arrival sequence ... *)
Variable sched : schedule PState.
Hypothesis H_work_conserving : work_conserving arr_seq sched.
(** ... where jobs do not execute before their arrival. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
(** Consider an arbitrary job [j] with positive cost. Notice that a
positive-cost assumption is required to ensure that one cannot
construct a busy interval without any workload inside of it. *)
Variable j : Job.
Hypothesis H_from_arrival_sequence : arrives_in arr_seq j.
Hypothesis H_job_cost_positive : job_cost_positive j.
(** Consider a busy interval <<[t1, t2)>> of job [j]. *)
Variable t1 t2 : instant.
Hypothesis H_busy_interval : busy_interval sched 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 must be completed
before time [t2]. *)
Lemma job_completes_within_busy_interval :
completed_by sched j t2.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H3 : Interference Job H4 : InterferingWorkload Job arr_seq : arrival_sequence Job tsk : Task sched : schedule PState H_work_conserving : work_conserving arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2
completed_by sched j t2
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H3 : Interference Job H4 : InterferingWorkload Job arr_seq : arrival_sequence Job tsk : Task sched : schedule PState H_work_conserving : work_conserving arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2
completed_by sched j t2
move : (H_busy_interval) => [[/andP [_ LT] [_ _]] [_ QT2]].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H3 : Interference Job H4 : InterferingWorkload Job arr_seq : arrival_sequence Job tsk : Task sched : schedule PState H_work_conserving : work_conserving arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched 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.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H3 : Interference Job H4 : InterferingWorkload Job arr_seq : arrival_sequence Job tsk : Task sched : schedule PState H_work_conserving : work_conserving arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched 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].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H3 : Interference Job H4 : InterferingWorkload Job arr_seq : arrival_sequence Job tsk : Task sched : schedule PState H_work_conserving : work_conserving arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 LT : job_arrival j < t2 QT2 : ~~ arrived_before j t2
completed_by sched j t2
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H3 : Interference Job H4 : InterferingWorkload Job arr_seq : arrival_sequence Job tsk : Task sched : schedule PState H_work_conserving : work_conserving arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched 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. } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H3 : Interference Job H4 : InterferingWorkload Job arr_seq : arrival_sequence Job tsk : Task sched : schedule PState H_work_conserving : work_conserving arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched 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 .
(** We show that, similarly to the classical notion of busy
interval, the job does not receive service before the busy
interval starts. *)
Lemma no_service_before_busy_interval :
forall t , service sched j t = service_during sched j t1 t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H3 : Interference Job H4 : InterferingWorkload Job arr_seq : arrival_sequence Job tsk : Task sched : schedule PState H_work_conserving : work_conserving arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2
forall t : instant,
service sched j t = service_during sched j t1 t
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H3 : Interference Job H4 : InterferingWorkload Job arr_seq : arrival_sequence Job tsk : Task sched : schedule PState H_work_conserving : work_conserving arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2
forall t : instant,
service sched j t = service_during sched j t1 t
move => t; move : (H_busy_interval) => [[/andP [LE1 LE2] [QT1 AQT]] QT2].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H3 : Interference Job H4 : InterferingWorkload Job arr_seq : arrival_sequence Job tsk : Task sched : schedule PState H_work_conserving : work_conserving arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 t : instant LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2
service sched j t = service_during sched j t1 t
destruct (leqP t1 t) as [NEQ1|NEQ1]; first destruct (leqP t2 t) as [NEQ2|NEQ2].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H3 : Interference Job H4 : InterferingWorkload Job arr_seq : arrival_sequence Job tsk : Task sched : schedule PState H_work_conserving : work_conserving arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 t : instant LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2 NEQ1 : t1 <= t NEQ2 : t2 <= t
service sched j t = service_during sched j t1 t
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H3 : Interference Job H4 : InterferingWorkload Job arr_seq : arrival_sequence Job tsk : Task sched : schedule PState H_work_conserving : work_conserving arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 t : instant LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2 NEQ1 : t1 <= t NEQ2 : t2 <= t
service sched j t = service_during sched j t1 t
apply /eqP; rewrite eqn_leq; apply /andP; split .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H3 : Interference Job H4 : InterferingWorkload Job arr_seq : arrival_sequence Job tsk : Task sched : schedule PState H_work_conserving : work_conserving arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 t : instant LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2 NEQ1 : t1 <= t NEQ2 : t2 <= t
service sched j t <= service_during sched j t1 t
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H3 : Interference Job H4 : InterferingWorkload Job arr_seq : arrival_sequence Job tsk : Task sched : schedule PState H_work_conserving : work_conserving arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 t : instant LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2 NEQ1 : t1 <= t NEQ2 : t2 <= t
service sched j t <= service_during sched j t1 t
rewrite /service -(service_during_cat _ _ _ t1);
[ | by apply /andP; split ; lia ].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H3 : Interference Job H4 : InterferingWorkload Job arr_seq : arrival_sequence Job tsk : Task sched : schedule PState H_work_conserving : work_conserving arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 t : instant LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2 NEQ1 : t1 <= t NEQ2 : t2 <= t
service_during sched j 0 t1 +
service_during sched j t1 t <=
service_during sched j t1 t
by rewrite cumulative_service_before_job_arrival_zero; eauto 2 .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H3 : Interference Job H4 : InterferingWorkload Job arr_seq : arrival_sequence Job tsk : Task sched : schedule PState H_work_conserving : work_conserving arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 t : instant LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2 NEQ1 : t1 <= t NEQ2 : t2 <= t
service_during sched j t1 t <= service sched j t
+ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H3 : Interference Job H4 : InterferingWorkload Job arr_seq : arrival_sequence Job tsk : Task sched : schedule PState H_work_conserving : work_conserving arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 t : instant LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2 NEQ1 : t1 <= t NEQ2 : t2 <= t
service_during sched j t1 t <= service sched j t
rewrite /service -[in X in _ <= X](service_during_cat _ _ _ t1);
[ | by apply /andP; split ; lia ].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H3 : Interference Job H4 : InterferingWorkload Job arr_seq : arrival_sequence Job tsk : Task sched : schedule PState H_work_conserving : work_conserving arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 t : instant LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2 NEQ1 : t1 <= t NEQ2 : t2 <= t
service_during sched j t1 t <=
service_during sched j 0 t1 +
service_during sched j t1 t
by (erewrite cumulative_service_before_job_arrival_zero with (t1 := 0 )
|| erewrite cumulative_service_before_job_arrival_zero with (t3 := 0 )); rt_eauto.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H3 : Interference Job H4 : InterferingWorkload Job arr_seq : arrival_sequence Job tsk : Task sched : schedule PState H_work_conserving : work_conserving arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 t : instant LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2 NEQ1 : t1 <= t NEQ2 : t < t2
service sched j t = service_during sched j t1 t
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H3 : Interference Job H4 : InterferingWorkload Job arr_seq : arrival_sequence Job tsk : Task sched : schedule PState H_work_conserving : work_conserving arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 t : instant LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2 NEQ1 : t1 <= t NEQ2 : t < t2
service sched j t = service_during sched j t1 t
rewrite /service -(service_during_cat _ _ _ t1);
[ | by apply /andP; split ; lia ].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H3 : Interference Job H4 : InterferingWorkload Job arr_seq : arrival_sequence Job tsk : Task sched : schedule PState H_work_conserving : work_conserving arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 t : instant LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2 NEQ1 : t1 <= t NEQ2 : t < t2
service_during sched j 0 t1 +
service_during sched j t1 t =
service_during sched j t1 t
by rewrite cumulative_service_before_job_arrival_zero; eauto 2 .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H3 : Interference Job H4 : InterferingWorkload Job arr_seq : arrival_sequence Job tsk : Task sched : schedule PState H_work_conserving : work_conserving arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 t : instant LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2 NEQ1 : t < t1
service sched j t = service_during sched j t1 t
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H3 : Interference Job H4 : InterferingWorkload Job arr_seq : arrival_sequence Job tsk : Task sched : schedule PState H_work_conserving : work_conserving arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 t : instant LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2 NEQ1 : t < t1
service sched j t = service_during sched j t1 t
rewrite service_during_geq; last by lia .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H3 : Interference Job H4 : InterferingWorkload Job arr_seq : arrival_sequence Job tsk : Task sched : schedule PState H_work_conserving : work_conserving arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 t : instant LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2 NEQ1 : t < t1
service sched j t = 0
by rewrite /service cumulative_service_before_job_arrival_zero; auto ; lia .
Qed .
(** Since the job cannot arrive before the busy interval starts and
completes by the end of the busy interval, it receives at least
[job_cost j] units of service within the interval. *)
Lemma service_within_busy_interval_ge_job_cost :
job_cost j <= service_during sched j t1 t2.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H3 : Interference Job H4 : InterferingWorkload Job arr_seq : arrival_sequence Job tsk : Task sched : schedule PState H_work_conserving : work_conserving arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2
job_cost j <= service_during sched j t1 t2
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H3 : Interference Job H4 : InterferingWorkload Job arr_seq : arrival_sequence Job tsk : Task sched : schedule PState H_work_conserving : work_conserving arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2
job_cost j <= service_during sched j t1 t2
move : (H_busy_interval) => [[/andP [LE1 LE2] [QT1 AQT]] QT2].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H3 : Interference Job H4 : InterferingWorkload Job arr_seq : arrival_sequence Job tsk : Task sched : schedule PState H_work_conserving : work_conserving arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2
job_cost j <= service_during sched j t1 t2
rewrite -[service_during _ _ _ _]add0n.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H3 : Interference Job H4 : InterferingWorkload Job arr_seq : arrival_sequence Job tsk : Task sched : schedule PState H_work_conserving : work_conserving arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2
job_cost j <= 0 + service_during sched j t1 t2
(erewrite <-cumulative_service_before_job_arrival_zero with (t1 := 0 )
|| erewrite <-cumulative_service_before_job_arrival_zero with (t3 := 0 )); rt_eauto. Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H3 : Interference Job H4 : InterferingWorkload Job arr_seq : arrival_sequence Job tsk : Task sched : schedule PState H_work_conserving : work_conserving arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2
job_cost j <=
service_during sched j 0 t1 +
service_during sched j t1 t2
rewrite service_during_cat; last by apply /andP; split ; lia .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H3 : Interference Job H4 : InterferingWorkload Job arr_seq : arrival_sequence Job tsk : Task sched : schedule PState H_work_conserving : work_conserving arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2
job_cost j <= service_during sched j 0 t2
rewrite -/(completed_by sched j t2).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job PState : ProcessorState Job H3 : Interference Job H4 : InterferingWorkload Job arr_seq : arrival_sequence Job tsk : Task sched : schedule PState H_work_conserving : work_conserving arr_seq sched H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job H_from_arrival_sequence : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_interval : busy_interval sched j t1 t2 LE1 : t1 <= job_arrival j LE2 : job_arrival j < t2 QT1 : quiet_time sched j t1 AQT : forall t : nat,
t1 < t < t2 -> ~ quiet_time sched j tQT2 : quiet_time sched j t2
completed_by sched j t2
by eapply job_completes_within_busy_interval; rt_eauto.
Qed .
End LemmasAboutAbstractBusyInterval .