Library prosa.analysis.abstract.run_to_completion
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.analysis.facts.model.service_of_jobs.
Require Export prosa.analysis.facts.preemption.rtc_threshold.job_preemptable.
Require Export prosa.analysis.abstract.definitions.
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.
Consider any type of tasks ...
... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
In addition, we assume existence of a function
mapping jobs to their preemption points.
Consider any kind of uni-service ideal processor state model.
Context {PState : Type}.
Context `{ProcessorState Job PState}.
Hypothesis H_ideal_progress_proc_model : ideal_progress_proc_model PState.
Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.
Context `{ProcessorState Job PState}.
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.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
... and any schedule of this arrival sequence.
Assume that the job costs are no larger than the task costs.
Let [tsk] be any task that is to be analyzed.
Assume we are provided with abstract functions for interference and interfering workload.
Variable interference : Job → instant → bool.
Variable interfering_workload : Job → instant → duration.
Variable interfering_workload : Job → instant → duration.
For simplicity, let's define some local names.
Let work_conserving := work_conserving arr_seq sched tsk.
Let cumul_interference := cumul_interference interference.
Let cumul_interfering_workload := cumul_interfering_workload interfering_workload.
Let busy_interval := busy_interval sched interference interfering_workload.
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.
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_of_tsk : job_task j = tsk.
Hypothesis H_job_cost_positive : job_cost_positive j.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_task j = tsk.
Hypothesis H_job_cost_positive : job_cost_positive j.
Next, consider any busy interval [t1, t2) of job [j].
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 665)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
move: (H_busy_interval) ⇒ [[/andP [_ LT] [_ _]] [_ QT2]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 746)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 747)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 803)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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
subgoal 2 (ID 804) is:
completed_by sched j t2
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 803)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 804)
subgoal 1 (ID 804) is:
completed_by sched j t2
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 804)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
completed_by sched j t2.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 665)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
move: (H_busy_interval) ⇒ [[/andP [_ LT] [_ _]] [_ QT2]].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 746)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 747)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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].
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 803)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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
subgoal 2 (ID 804) is:
completed_by sched j t2
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 803)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 804)
subgoal 1 (ID 804) is:
completed_by sched j t2
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 804)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
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.
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.
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 671)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
rewrite /service_during /cumul_interference/service_at.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 686)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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 <= t0 < t + delta) service_in j (sched t0) +
definitions.cumul_interference interference j t (t + delta) = delta
----------------------------------------------------------------------------- *)
rewrite -big_split //=.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 697)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 721)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 745)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 838)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 840)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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 ->
job_task j = tsk ->
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 5 Workj; try done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 865)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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
subgoal 2 (ID 870) is:
service_in j (sched x) + interference j x = 1
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 865)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 870)
subgoal 1 (ID 870) is:
service_in j (sched x) + interference j x = 1
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 870)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 973)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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
subgoal 2 (ID 974) is:
service_in j (sched x) + false = 1
----------------------------------------------------------------------------- *)
- replace (service_in _ _) with 0; auto; symmetry.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 988)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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
subgoal 2 (ID 974) is:
service_in j (sched x) + false = 1
----------------------------------------------------------------------------- *)
apply no_service_not_scheduled; auto.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 999)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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
subgoal 2 (ID 974) is:
service_in j (sched x) + false = 1
----------------------------------------------------------------------------- *)
now apply/negP; intros SCHED; apply Workj in SCHED; apply SCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 974)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1050)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1135)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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
subgoal 2 (ID 1136) is:
0 < service_in j (sched x)
----------------------------------------------------------------------------- *)
+ apply H_unit_service_proc_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1136)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End InterferenceIsComplement.
service_during sched j t (t + delta) + cumul_interference j t (t + delta) = delta.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 671)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
rewrite /service_during /cumul_interference/service_at.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 686)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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 <= t0 < t + delta) service_in j (sched t0) +
definitions.cumul_interference interference j t (t + delta) = delta
----------------------------------------------------------------------------- *)
rewrite -big_split //=.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 697)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 721)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 745)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 838)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 840)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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 ->
job_task j = tsk ->
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 5 Workj; try done.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 865)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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
subgoal 2 (ID 870) is:
service_in j (sched x) + interference j x = 1
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 865)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 870)
subgoal 1 (ID 870) is:
service_in j (sched x) + interference j x = 1
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 870)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 973)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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
subgoal 2 (ID 974) is:
service_in j (sched x) + false = 1
----------------------------------------------------------------------------- *)
- replace (service_in _ _) with 0; auto; symmetry.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 988)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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
subgoal 2 (ID 974) is:
service_in j (sched x) + false = 1
----------------------------------------------------------------------------- *)
apply no_service_not_scheduled; auto.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 999)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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
subgoal 2 (ID 974) is:
service_in j (sched x) + false = 1
----------------------------------------------------------------------------- *)
now apply/negP; intros SCHED; apply Workj in SCHED; apply SCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 974)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1050)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 1135)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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
subgoal 2 (ID 1136) is:
0 < service_in j (sched x)
----------------------------------------------------------------------------- *)
+ apply H_unit_service_proc_model.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1136)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End InterferenceIsComplement.
In this section, we prove a sufficient condition under which job [j] receives enough service.
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.
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.
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 671)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
case NEQ: (t1 + delta ≤ t2); last first.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 751)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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)
subgoal 2 (ID 715) is:
progress_of_job <= service sched j (t1 + delta)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 751)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
have L8 := job_completes_within_busy_interval.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 756)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 760)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 767)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 789)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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)
subgoal 2 (ID 790) is:
0 <= t2 <= t1 + delta
----------------------------------------------------------------------------- *)
apply leq_trans with (service_during sched j 0 t2); [by done | by rewrite leq_addr].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 790)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 715)
subgoal 1 (ID 715) is:
progress_of_job <= service sched j (t1 + delta)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 715)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 715)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 835)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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)
----------------------------------------------------------------------------- *)
apply subh3 in BOUND.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 836)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 839)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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)).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 843)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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)
subgoal 2 (ID 844) is:
service_during sched j t1 (t1 + delta) <= service sched j (t1 + delta)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 843)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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) //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 849)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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 //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 844)
subgoal 1 (ID 844) is:
service_during sched j t1 (t1 + delta) <= service sched j (t1 + delta)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 844)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 844)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 946)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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)
subgoal 2 (ID 947) is:
0 <= t1 <= t1 + delta
----------------------------------------------------------------------------- *)
rewrite leq_addl //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 947)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End InterferenceBoundedImpliesEnoughService.
service sched j (t1 + delta) ≥ progress_of_job.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 671)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
case NEQ: (t1 + delta ≤ t2); last first.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 751)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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)
subgoal 2 (ID 715) is:
progress_of_job <= service sched j (t1 + delta)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 751)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
have L8 := job_completes_within_busy_interval.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 756)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 760)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 767)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 789)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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)
subgoal 2 (ID 790) is:
0 <= t2 <= t1 + delta
----------------------------------------------------------------------------- *)
apply leq_trans with (service_during sched j 0 t2); [by done | by rewrite leq_addr].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 790)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 715)
subgoal 1 (ID 715) is:
progress_of_job <= service sched j (t1 + delta)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 715)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 715)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 835)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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)
----------------------------------------------------------------------------- *)
apply subh3 in BOUND.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 836)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 839)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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)).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 843)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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)
subgoal 2 (ID 844) is:
service_during sched j t1 (t1 + delta) <= service sched j (t1 + delta)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 843)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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) //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 849)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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 //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 844)
subgoal 1 (ID 844) is:
service_during sched j t1 (t1 + delta) <= service sched j (t1 + delta)
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 844)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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)
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 844)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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).
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 946)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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)
subgoal 2 (ID 947) is:
0 <= t1 <= t1 + delta
----------------------------------------------------------------------------- *)
rewrite leq_addl //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 947)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End InterferenceBoundedImpliesEnoughService.
In this section we prove a simple lemma about completion of
a job after is reaches run-to-completion threshold.
Assume that completed jobs do not execute ...
.. and the preemption model is valid.
Then, job [j] must complete in [job_cost j - job_run_to_completion_threshold j] time
units after it reaches run-to-completion threshold.
Lemma job_completes_after_reaching_run_to_completion_threshold:
∀ t,
job_run_to_completion_threshold j ≤ service sched j t →
completed_by sched j (t + (job_cost j - job_run_to_completion_threshold j)).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 691)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t ->
completed_by sched j (t + (job_cost j - job_run_to_completion_threshold j))
----------------------------------------------------------------------------- *)
Proof.
move ⇒ t ES.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 693)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
============================
completed_by sched j (t + (job_cost j - job_run_to_completion_threshold j))
----------------------------------------------------------------------------- *)
set (job_cost j - job_run_to_completion_threshold j) as job_last.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 700)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
============================
completed_by sched j (t + job_last)
----------------------------------------------------------------------------- *)
have LSNP := @job_nonpreemptive_after_run_to_completion_threshold
Job H2 H3 _ _ arr_seq sched _ j _ t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 713)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 736)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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: ∀ t', t ≤ t' ≤ t + job_last → scheduled_at sched j t'.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 741)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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'
subgoal 2 (ID 743) is:
False
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 741)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 784)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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) //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 788)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 816)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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 //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 846)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 891)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 925)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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)
----------------------------------------------------------------------------- *)
apply completion_monotonic with (t0 := t'); try done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 743)
subgoal 1 (ID 743) is:
False
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 743)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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'.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 939)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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'
subgoal 2 (ID 941) is:
False
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 939)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 983)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1018)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1041)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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 //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1050)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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 _].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1117)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1119)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 941)
subgoal 1 (ID 941) is:
False
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 941)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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
----------------------------------------------------------------------------- *)
eapply service_at_most_cost with (j0 := j) (t0 := t + job_last.+1) in H_completed_jobs_dont_execute; auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1182)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
H_job_cost_positive : job_cost_positive j
t1, t2 : instant
H_busy_interval : busy_interval j t1 t2
t : instant
job_last := job_cost j - job_run_to_completion_threshold j : nat
H_completed_jobs_dont_execute : service sched j (t + succn job_last) <=
job_cost j
H_valid_preemption_model : valid_preemption_model arr_seq sched
ES : job_run_to_completion_threshold j <= service sched j t
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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: H_completed_jobs_dont_execute; rewrite leqNgt; move ⇒ /negP T; apply: T.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1229)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
H_job_cost_positive : job_cost_positive j
t1, t2 : instant
H_busy_interval : busy_interval j t1 t2
t : instant
job_last := job_cost j - job_run_to_completion_threshold j : nat
H_completed_jobs_dont_execute : service sched j (t + succn job_last) <=
job_cost j
H_valid_preemption_model : valid_preemption_model arr_seq sched
ES : job_run_to_completion_threshold j <= service sched j t
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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 + succn job_last)
----------------------------------------------------------------------------- *)
rewrite /service -(service_during_cat _ _ _ t); last by (apply/andP; split; last rewrite leq_addr).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1258)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
H_job_cost_positive : job_cost_positive j
t1, t2 : instant
H_busy_interval : busy_interval j t1 t2
t : instant
job_last := job_cost j - job_run_to_completion_threshold j : nat
H_completed_jobs_dont_execute : service sched j (t + succn job_last) <=
job_cost j
H_valid_preemption_model : valid_preemption_model arr_seq sched
ES : job_run_to_completion_threshold j <= service sched j t
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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 + succn job_last)
----------------------------------------------------------------------------- *)
apply leq_trans with (job_run_to_completion_threshold j + service_during sched j t (t + job_last.+1));
last by rewrite leq_add2r.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1297)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
H_job_cost_positive : job_cost_positive j
t1, t2 : instant
H_busy_interval : busy_interval j t1 t2
t : instant
job_last := job_cost j - job_run_to_completion_threshold j : nat
H_completed_jobs_dont_execute : service sched j (t + succn job_last) <=
job_cost j
H_valid_preemption_model : valid_preemption_model arr_seq sched
ES : job_run_to_completion_threshold j <= service sched j t
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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_run_to_completion_threshold j +
service_during sched j t (t + succn job_last)
----------------------------------------------------------------------------- *)
apply leq_trans with (job_run_to_completion_threshold j + job_last.+1); last by rewrite leq_add2l /service_during -addn1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1307)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
H_job_cost_positive : job_cost_positive j
t1, t2 : instant
H_busy_interval : busy_interval j t1 t2
t : instant
job_last := job_cost j - job_run_to_completion_threshold j : nat
H_completed_jobs_dont_execute : service sched j (t + succn job_last) <=
job_cost j
H_valid_preemption_model : valid_preemption_model arr_seq sched
ES : job_run_to_completion_threshold j <= service sched j t
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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_run_to_completion_threshold j + succn job_last
----------------------------------------------------------------------------- *)
by rewrite addnS ltnS subnKC //; eapply job_run_to_completion_threshold_le_job_cost; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End CompletionOfJobAfterRunToCompletionThreshold.
End AbstractRTARunToCompletionThreshold.
∀ t,
job_run_to_completion_threshold j ≤ service sched j t →
completed_by sched j (t + (job_cost j - job_run_to_completion_threshold j)).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 691)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t ->
completed_by sched j (t + (job_cost j - job_run_to_completion_threshold j))
----------------------------------------------------------------------------- *)
Proof.
move ⇒ t ES.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 693)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
============================
completed_by sched j (t + (job_cost j - job_run_to_completion_threshold j))
----------------------------------------------------------------------------- *)
set (job_cost j - job_run_to_completion_threshold j) as job_last.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 700)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
============================
completed_by sched j (t + job_last)
----------------------------------------------------------------------------- *)
have LSNP := @job_nonpreemptive_after_run_to_completion_threshold
Job H2 H3 _ _ arr_seq sched _ j _ t.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 713)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 736)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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: ∀ t', t ≤ t' ≤ t + job_last → scheduled_at sched j t'.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 741)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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'
subgoal 2 (ID 743) is:
False
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 741)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 784)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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) //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 788)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 816)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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 //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 846)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 891)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 925)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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)
----------------------------------------------------------------------------- *)
apply completion_monotonic with (t0 := t'); try done.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 743)
subgoal 1 (ID 743) is:
False
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 743)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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'.
(* ----------------------------------[ coqtop ]---------------------------------
2 subgoals (ID 939)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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'
subgoal 2 (ID 941) is:
False
----------------------------------------------------------------------------- *)
{
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 939)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 983)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1018)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1041)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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 //.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1050)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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 _].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1117)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1119)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 941)
subgoal 1 (ID 941) is:
False
----------------------------------------------------------------------------- *)
}
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 941)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
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_run_to_completion_threshold j <= service sched j t
job_last := job_cost j - job_run_to_completion_threshold j : nat
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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
----------------------------------------------------------------------------- *)
eapply service_at_most_cost with (j0 := j) (t0 := t + job_last.+1) in H_completed_jobs_dont_execute; auto.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1182)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
H_job_cost_positive : job_cost_positive j
t1, t2 : instant
H_busy_interval : busy_interval j t1 t2
t : instant
job_last := job_cost j - job_run_to_completion_threshold j : nat
H_completed_jobs_dont_execute : service sched j (t + succn job_last) <=
job_cost j
H_valid_preemption_model : valid_preemption_model arr_seq sched
ES : job_run_to_completion_threshold j <= service sched j t
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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: H_completed_jobs_dont_execute; rewrite leqNgt; move ⇒ /negP T; apply: T.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1229)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
H_job_cost_positive : job_cost_positive j
t1, t2 : instant
H_busy_interval : busy_interval j t1 t2
t : instant
job_last := job_cost j - job_run_to_completion_threshold j : nat
H_completed_jobs_dont_execute : service sched j (t + succn job_last) <=
job_cost j
H_valid_preemption_model : valid_preemption_model arr_seq sched
ES : job_run_to_completion_threshold j <= service sched j t
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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 + succn job_last)
----------------------------------------------------------------------------- *)
rewrite /service -(service_during_cat _ _ _ t); last by (apply/andP; split; last rewrite leq_addr).
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1258)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
H_job_cost_positive : job_cost_positive j
t1, t2 : instant
H_busy_interval : busy_interval j t1 t2
t : instant
job_last := job_cost j - job_run_to_completion_threshold j : nat
H_completed_jobs_dont_execute : service sched j (t + succn job_last) <=
job_cost j
H_valid_preemption_model : valid_preemption_model arr_seq sched
ES : job_run_to_completion_threshold j <= service sched j t
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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 + succn job_last)
----------------------------------------------------------------------------- *)
apply leq_trans with (job_run_to_completion_threshold j + service_during sched j t (t + job_last.+1));
last by rewrite leq_add2r.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1297)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
H_job_cost_positive : job_cost_positive j
t1, t2 : instant
H_busy_interval : busy_interval j t1 t2
t : instant
job_last := job_cost j - job_run_to_completion_threshold j : nat
H_completed_jobs_dont_execute : service sched j (t + succn job_last) <=
job_cost j
H_valid_preemption_model : valid_preemption_model arr_seq sched
ES : job_run_to_completion_threshold j <= service sched j t
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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_run_to_completion_threshold j +
service_during sched j t (t + succn job_last)
----------------------------------------------------------------------------- *)
apply leq_trans with (job_run_to_completion_threshold j + job_last.+1); last by rewrite leq_add2l /service_during -addn1.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 1307)
Task : TaskType
H : TaskCost Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
H3 : JobPreemptable Job
PState : Type
H4 : ProcessorState Job PState
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
H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq
tsk : Task
interference : Job -> instant -> bool
interfering_workload : Job -> instant -> duration
work_conserving := definitions.work_conserving arr_seq sched tsk
: (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_of_tsk : job_task j = tsk
H_job_cost_positive : job_cost_positive j
t1, t2 : instant
H_busy_interval : busy_interval j t1 t2
t : instant
job_last := job_cost j - job_run_to_completion_threshold j : nat
H_completed_jobs_dont_execute : service sched j (t + succn job_last) <=
job_cost j
H_valid_preemption_model : valid_preemption_model arr_seq sched
ES : job_run_to_completion_threshold j <= service sched j t
LSNP : forall p : ProcessorState Job PState,
valid_preemption_model arr_seq sched ->
arrives_in arr_seq j ->
forall t' : nat,
t <= t' ->
job_run_to_completion_threshold 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_run_to_completion_threshold j + succn job_last
----------------------------------------------------------------------------- *)
by rewrite addnS ltnS subnKC //; eapply job_run_to_completion_threshold_le_job_cost; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End CompletionOfJobAfterRunToCompletionThreshold.
End AbstractRTARunToCompletionThreshold.