Built with
Alectryon , running Coq+SerAPI v8.19.0+0.19.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.analysis.facts.interference.[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] [Loading ML file ring_plugin.cmxs (using legacy method) ... done ] [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ] Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.analysis.facts.model.restricted_supply.schedule.
Require Import prosa.analysis.facts.priority.fifo.
Require Import prosa.analysis.facts.model.rbf.
(** * Higher-or-Equal-Priority Interference Bound under FIFO *)
(** In this file, we introduce a bound on the cumulative interference
from higher- and equal-priority under FIFO scheduling. *)
Section RTAforFullyPreemptiveFIFOModelwithArrivalCurves .
(** Consider any type of tasks, each characterized by a WCET
[task_cost] and an arrival curve [max_arrivals] ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
Context `{MaxArrivals Task}.
(** ... and any type of jobs associated with these tasks, where each
job has a task [job_task], a cost [job_cost], and an arrival
time [job_arrival]. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobCost Job}.
Context `{JobArrival Job}.
(** Consider any kind of unit-supply uniprocessor model. *)
Context `{PState : ProcessorState Job}.
Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
(** Consider any arrival sequence [arr_seq] with consistent, non-duplicate arrivals. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
(** We further require that a job's cost cannot exceed its task's stated WCET. *)
Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
(** We consider an arbitrary task set [ts] ... *)
Variable ts : seq Task.
(** ... and assume that all jobs stem from tasks in this task set. *)
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
(** We assume that [max_arrivals] is a family of valid arrival
curves that constrains the arrival sequence [arr_seq], i.e., for
any task [tsk] in [ts], [max_arrival tsk] is (1) an arrival
bound of [tsk], and ... *)
Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
(** ... (2) a monotonic function that equals 0 for the empty interval [delta = 0]. *)
Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
(** Let [tsk] be any task in [ts] that is to be analyzed. *)
Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.
(** Consider any schedule ... *)
Variable sched : schedule PState.
(** ... where jobs do not execute before their arrival nor after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
(** Next, we establish a bound on the interference produced by higher- and
equal-priority jobs. *)
(** Consider a job [j] of the task under analysis [tsk] with a positive cost. *)
Variable j : Job.
Hypothesis H_job_of_task : job_of_task tsk j.
Hypothesis H_j_in_arrivals : arrives_in arr_seq j.
Hypothesis H_job_cost_positive : job_cost_positive j.
(** Consider the busy window of [j] and denote it as <<[t1, t2)>>. *)
Variable t1 t2 : instant.
Hypothesis H_busy_window : classical.busy_interval arr_seq sched j t1 t2.
(** Consider any arbitrary sub-interval <<[t1, Δ)>> within the busy
window of [j]. *)
Variable Δ : instant.
Hypothesis H_in_busy : t1 + Δ < t2.
(** The cumulative interference from higher- and equal-priority jobs
during <<[t1, Δ)>> is bounded as follows. *)
Lemma bound_on_hep_workload :
cumulative_another_hep_job_interference arr_seq sched j t1 (t1 + Δ) <=
\sum_(tsko <- ts) task_request_bound_function tsko (job_arrival j - t1 + ε) - task_cost tsk.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2
cumulative_another_hep_job_interference arr_seq sched
j t1 (t1 + Δ) <=
\sum_(tsko <- ts)
task_request_bound_function tsko
(job_arrival j - t1 + 1 ) - task_cost tsk
Proof .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2
cumulative_another_hep_job_interference arr_seq sched
j t1 (t1 + Δ) <=
\sum_(tsko <- ts)
task_request_bound_function tsko
(job_arrival j - t1 + 1 ) - task_cost tsk
move : (H_busy_window) => [[_ [_ [_ /andP [ARR1 ARR2]]]] _].Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2
cumulative_another_hep_job_interference arr_seq sched
j t1 (t1 + Δ) <=
\sum_(tsko <- ts)
task_request_bound_function tsko
(job_arrival j - t1 + 1 ) - task_cost tsk
rewrite (cumulative_i_ohep_eq_service_of_ohep _ arr_seq) => //; last eauto 6 with basic_rt_facts; last first .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2
quiet_time arr_seq sched j t1
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2
quiet_time arr_seq sched j t1
by move : (H_busy_window) => [[_ [Q _]] _]. } Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2
service_of_other_hep_jobs arr_seq sched j t1 (t1 + Δ) <=
\sum_(tsko <- ts)
task_request_bound_function tsko
(job_arrival j - t1 + 1 ) - task_cost tsk
eapply leq_trans; first by apply service_of_jobs_le_workload => //.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2
workload_of_jobs (another_hep_job^~ j)
(arrivals_between arr_seq t1 (t1 + Δ)) <=
\sum_(tsko <- ts)
task_request_bound_function tsko
(job_arrival j - t1 + 1 ) - task_cost tsk
rewrite (leqRW (workload_equal_subset _ _ _ _ _ _ _)) => //.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2
workload_of_jobs (fun j0 : Job => j0 != j)
(arrivals_between arr_seq t1 (job_arrival j + 1 )) <=
\sum_(tsko <- ts)
task_request_bound_function tsko
(job_arrival j - t1 + 1 ) - task_cost tsk
rewrite (workload_minus_job_cost j)//;
last by apply job_in_arrivals_between => //; last by rewrite addn1.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2
workload_of_jobs predT
(arrivals_between arr_seq t1 (job_arrival j + 1 )) -
job_cost j <=
\sum_(tsko <- ts)
task_request_bound_function tsko
(job_arrival j - t1 + 1 ) - task_cost tsk
rewrite /workload_of_jobs (big_rem tsk) //=
(addnC (task_request_bound_function tsk (job_arrival j - t1 + ε))).Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2
\sum_(j <- arrivals_between arr_seq t1
(job_arrival j + 1 )) job_cost j -
job_cost j <=
\sum_(y <- rem (T:=Task) tsk ts)
task_request_bound_function y
(job_arrival j - t1 + 1 ) +
task_request_bound_function tsk
(job_arrival j - t1 + 1 ) - task_cost tsk
rewrite -addnBA; last first .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2
task_cost tsk <=
task_request_bound_function tsk
(job_arrival j - t1 + 1 )
- Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2
task_cost tsk <=
task_request_bound_function tsk
(job_arrival j - t1 + 1 )
apply leq_trans with (task_request_bound_function tsk ε).Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2
task_cost tsk <= task_request_bound_function tsk 1
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2
task_cost tsk <= task_request_bound_function tsk 1
by apply : task_rbf_1_ge_task_cost; exact : non_pathological_max_arrivals. } Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2
task_request_bound_function tsk 1 <=
task_request_bound_function tsk
(job_arrival j - t1 + 1 )
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2
task_request_bound_function tsk 1 <=
task_request_bound_function tsk
(job_arrival j - t1 + 1 )
by apply task_rbf_monotone; [apply H_valid_arrival_curve | lia ]. }
- Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2
\sum_(j <- arrivals_between arr_seq t1
(job_arrival j + 1 )) job_cost j -
job_cost j <=
\sum_(y <- rem (T:=Task) tsk ts)
task_request_bound_function y
(job_arrival j - t1 + 1 ) +
(task_request_bound_function tsk
(job_arrival j - t1 + 1 ) - task_cost tsk)
eapply leq_trans; last first .Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2
?n <=
\sum_(y <- rem (T:=Task) tsk ts)
task_request_bound_function y
(job_arrival j - t1 + 1 ) +
(task_request_bound_function tsk
(job_arrival j - t1 + 1 ) - task_cost tsk)
{ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2
?n <=
\sum_(y <- rem (T:=Task) tsk ts)
task_request_bound_function y
(job_arrival j - t1 + 1 ) +
(task_request_bound_function tsk
(job_arrival j - t1 + 1 ) - task_cost tsk)
by erewrite leq_add2l; apply task_rbf_without_job_under_analysis; (try apply ARR1) => //; lia . } Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2
\sum_(j <- arrivals_between arr_seq t1
(job_arrival j + 1 )) job_cost j -
job_cost j <=
\sum_(y <- rem (T:=Task) tsk ts)
task_request_bound_function y
(job_arrival j - t1 + 1 ) +
(task_workload_between arr_seq tsk t1
(t1 + (job_arrival j - t1 + 1 )) - job_cost j)
rewrite addnBA.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2
\sum_(j <- arrivals_between arr_seq t1
(job_arrival j + 1 )) job_cost j -
job_cost j <=
\sum_(y <- rem (T:=Task) tsk ts)
task_request_bound_function y
(job_arrival j - t1 + 1 ) +
task_workload_between arr_seq tsk t1
(t1 + (job_arrival j - t1 + 1 )) - job_cost j
+ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2
\sum_(j <- arrivals_between arr_seq t1
(job_arrival j + 1 )) job_cost j -
job_cost j <=
\sum_(y <- rem (T:=Task) tsk ts)
task_request_bound_function y
(job_arrival j - t1 + 1 ) +
task_workload_between arr_seq tsk t1
(t1 + (job_arrival j - t1 + 1 )) - job_cost j
rewrite leq_sub2r //; eapply leq_trans.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2
\sum_(j <- arrivals_between arr_seq t1
(job_arrival j + 1 )) job_cost j <= ?n
* Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2
\sum_(j <- arrivals_between arr_seq t1
(job_arrival j + 1 )) job_cost j <= ?n
apply sum_over_partitions_le => j' inJOBS => _.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2 j' : Job inJOBS : j'
\in arrivals_between arr_seq t1
(job_arrival j + 1 )
?x_to_y j' \in ?ys
by apply H_all_jobs_from_taskset, (in_arrivals_implies_arrived _ _ _ _ inJOBS).
* Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2
\sum_(y <- ts)
\sum_(x <- arrivals_between arr_seq t1
(job_arrival j + 1 ) | xpredT x &&
([eta job_task]
x == y))
job_cost x <=
\sum_(y <- rem (T:=Task) tsk ts)
task_request_bound_function y
(job_arrival j - t1 + 1 ) +
task_workload_between arr_seq tsk t1
(t1 + (job_arrival j - t1 + 1 ))
rewrite (big_rem tsk) //= addnC leq_add //; last by rewrite addnA subnKC.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2
\sum_(y <- rem (T:=Task) tsk ts)
\sum_(x <- arrivals_between arr_seq t1
(job_arrival j + 1 ) | job_task x == y)
job_cost x <=
\sum_(y <- rem (T:=Task) tsk ts)
task_request_bound_function y
(job_arrival j - t1 + 1 )
rewrite big_seq_cond [in X in _ <= X]big_seq_cond big_mkcond [in X in _ <= X]big_mkcond //=.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2
\sum_(i <- rem (T:=Task) tsk ts)
(if (i \in rem (T:=Task) tsk ts) && true
then
\sum_(x <- arrivals_between arr_seq t1
(job_arrival j + 1 ) | job_task x ==
i) job_cost x
else 0 ) <=
\sum_(i <- rem (T:=Task) tsk ts)
(if (i \in rem (T:=Task) tsk ts) && true
then
task_request_bound_function i
(job_arrival j - t1 + 1 )
else 0 )
apply leq_sum => tsk' _; rewrite andbC //=.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2 tsk' : Task
(if tsk' \in rem (T:=Task) tsk ts
then
\sum_(x <- arrivals_between arr_seq t1
(job_arrival j + 1 ) | job_task x ==
tsk') job_cost x
else 0 ) <=
(if tsk' \in rem (T:=Task) tsk ts
then
task_request_bound_function tsk'
(job_arrival j - t1 + 1 )
else 0 )
destruct (tsk' \in rem (T:=Task) tsk ts) eqn :IN; last by [].Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2 tsk' : Task IN : (tsk' \in rem (T:=Task) tsk ts) = true
\sum_(x <- arrivals_between arr_seq t1
(job_arrival j + 1 ) | job_task x == tsk')
job_cost x <=
task_request_bound_function tsk'
(job_arrival j - t1 + 1 )
apply rem_in in IN.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2 tsk' : Task IN : tsk' \in ts
\sum_(x <- arrivals_between arr_seq t1
(job_arrival j + 1 ) | job_task x == tsk')
job_cost x <=
task_request_bound_function tsk'
(job_arrival j - t1 + 1 )
eapply leq_trans;
last by apply (task_workload_le_task_rbf _ _ _ IN H_valid_job_cost H_is_arrival_curve t1).Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2 tsk' : Task IN : tsk' \in ts
\sum_(x <- arrivals_between arr_seq t1
(job_arrival j + 1 ) | job_task x == tsk')
job_cost x <=
workload_of_jobs (job_of_task tsk')
(arrivals_between arr_seq t1
(t1 + (job_arrival j - t1 + 1 )))
by rewrite addnBAC //= subnKC //= addn1; apply leqW.
+ Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2
job_cost j <=
task_workload_between arr_seq tsk t1
(t1 + (job_arrival j - t1 + 1 ))
move : H_job_of_task => TSKj.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2 TSKj : job_of_task tsk j
job_cost j <=
task_workload_between arr_seq tsk t1
(t1 + (job_arrival j - t1 + 1 ))
rewrite /task_workload_between /task_workload /workload_of_jobs (big_rem j) //=;
first by rewrite TSKj; apply leq_addr.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2 TSKj : job_of_task tsk j
j
\in arrivals_between arr_seq t1
(t1 + (job_arrival j - t1 + 1 ))
apply job_in_arrivals_between => //.Task : TaskType H : TaskCost Task H0 : MaxArrivals Task Job : JobType H1 : JobTask Job Task H2 : JobCost Job H3 : JobArrival Job PState : ProcessorState Job H_uniprocessor_proc_model : uniprocessor_model PState H_unit_supply_proc_model : unit_supply_proc_model
PState arr_seq : arrival_sequence Job H_valid_arrival_sequence : valid_arrival_sequence
arr_seq H_valid_job_cost : arrivals_have_valid_job_costs
arr_seq ts : seq Task H_all_jobs_from_taskset : all_jobs_from_taskset
arr_seq ts H_is_arrival_curve : taskset_respects_max_arrivals
arr_seq ts H_valid_arrival_curve : valid_taskset_arrival_curve ts
max_arrivals tsk : Task H_tsk_in_ts : tsk \in ts sched : schedule PState H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_completed_jobs_dont_execute : completed_jobs_dont_execute
sched j : Job H_job_of_task : job_of_task tsk j H_j_in_arrivals : arrives_in arr_seq j H_job_cost_positive : job_cost_positive j t1, t2 : instant H_busy_window : busy_interval arr_seq sched j t1 t2 Δ : instant H_in_busy : t1 + Δ < t2 ARR1 : t1 <= job_arrival j ARR2 : job_arrival j < t2 TSKj : job_of_task tsk j
job_arrival j < t1 + (job_arrival j - t1 + 1 )
by lia .
Qed .
End RTAforFullyPreemptiveFIFOModelwithArrivalCurves .