Library prosa.classic.analysis.uni.arrival_curves.workload_bound
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.job
prosa.classic.model.arrival.basic.task_arrival
prosa.classic.model.priority.
Require Import prosa.classic.model.schedule.uni.service
prosa.classic.model.schedule.uni.workload
prosa.classic.model.schedule.uni.schedule.
Require Import prosa.classic.model.arrival.curves.bounds.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
Module MaxArrivalsWorkloadBound.
Import Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service.
Section Lemmas.
Context {Task: eqType}.
Variable task_cost: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → Task.
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_arr_seq_is_a_set: arrival_sequence_is_a_set arr_seq.
Variable sched: schedule Job.
Hypothesis H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq.
Variable higher_eq_priority: FP_policy Task.
Let jlfp_higher_eq_priority := FP_to_JLFP job_task higher_eq_priority.
Let arrivals_between := jobs_arrived_between arr_seq.
Section RequestBoundFunction.
Variable max_arrivals: Task → time → nat.
Section SingleTask.
Variable tsk: Task.
Variable delta: time.
Definition task_request_bound_function := task_cost tsk × max_arrivals tsk delta.
End SingleTask.
Section AllTasks.
Variable ts: list Task.
Variable tsk: Task.
Variable delta: time.
Let is_hep_task tsk_other := higher_eq_priority tsk_other tsk.
Let is_other_hep_task tsk_other := higher_eq_priority tsk_other tsk && (tsk_other != tsk).
Definition total_request_bound_function :=
\sum_(tsk <- ts) task_request_bound_function tsk delta.
Definition total_hep_request_bound_function_FP :=
\sum_(tsk_other <- ts | is_hep_task tsk_other)
task_request_bound_function tsk_other delta.
Definition total_ohep_request_bound_function_FP :=
\sum_(tsk_other <- ts | is_other_hep_task tsk_other)
task_request_bound_function tsk_other delta.
End AllTasks.
End RequestBoundFunction.
Section ProofWorkloadBound.
Variable ts: list Task.
Variable tsk: Task.
Hypothesis H_tsk_in_ts: tsk \in ts.
Hypothesis H_job_cost_le_task_cost:
∀ j,
arrives_in arr_seq j →
job_cost_le_task_cost task_cost job_cost job_task j.
Hypothesis H_all_jobs_from_taskset:
∀ j, arrives_in arr_seq j → job_task j \in ts.
Variable max_arrivals: Task → time → nat.
Hypothesis H_is_arrival_bound:
is_arrival_bound_for_taskset job_task arr_seq max_arrivals ts.
Let task_rbf := task_request_bound_function max_arrivals tsk.
Let total_rbf := total_request_bound_function max_arrivals ts.
Let total_hep_rbf := total_hep_request_bound_function_FP max_arrivals ts tsk.
Let total_ohep_rbf := total_ohep_request_bound_function_FP max_arrivals ts tsk.
Variable j: Job.
Hypothesis H_j_arrives: arrives_in arr_seq j.
Hypothesis H_job_of_tsk: job_task j = tsk.
Let same_task j1 j2 := job_task j1 == job_task j2.
Let other_higher_eq_priority j1 j2 := jlfp_higher_eq_priority j1 j2 && (~~ same_task j1 j2).
Let total_workload t1 t2 :=
workload_of_jobs job_cost (arrivals_between t1 t2) (fun j ⇒ true).
Let total_hep_workload t1 t2 :=
workload_of_jobs job_cost (arrivals_between t1 t2)
(fun j_other ⇒ jlfp_higher_eq_priority j_other j).
Let total_ohep_workload t1 t2 :=
workload_of_jobs job_cost (arrivals_between t1 t2)
(fun j_other ⇒ other_higher_eq_priority j_other j).
Let task_workload (t1: time) (t2: time) :=
workload_of_jobs job_cost (arrivals_between t1 t2)
(fun j_other ⇒ same_task j_other j).
Section WorkloadIsBoundedByRBF.
Variable t: time.
Variable delta: time.
Lemma task_workload_le_task_rbf:
task_workload t (t + delta) ≤ task_rbf delta.
Proof.
unfold task_workload.
unfold task_rbf, task_request_bound_function.
unfold is_arrival_bound in ×.
unfold arrivals_between.
set l := jobs_arrived_between arr_seq t delta.
apply leq_trans with (
task_cost tsk × num_arrivals_of_task job_task arr_seq tsk t (t + delta)).
{
rewrite /num_arrivals_of_task -sum1_size big_distrr /= big_filter.
rewrite -/l /workload_of_jobs.
rewrite /is_job_of_task /same_task H_job_of_tsk muln1.
apply leq_sum_seq; move ⇒ j0 IN0 /eqP EQ.
rewrite -EQ.
apply H_job_cost_le_task_cost.
by apply in_arrivals_implies_arrived in IN0.
}
{
rewrite leq_mul2l; apply/orP; right.
rewrite -{2}[delta](addKn t).
apply H_is_arrival_bound; first by done.
by rewrite leq_addr.
}
Qed.
Lemma total_workload_le_total_rbf:
total_ohep_workload t (t + delta) ≤ total_ohep_rbf delta.
Proof.
rewrite /total_ohep_rbf /total_ohep_request_bound_function_FP
/task_request_bound_function.
rewrite /total_ohep_workload /workload_of_jobs
/other_higher_eq_priority.
rewrite /jlfp_higher_eq_priority
/FP_to_JLFP /same_task H_job_of_tsk.
rewrite /arrivals_between.
set l := jobs_arrived_between arr_seq t (t + delta).
set hep := higher_eq_priority.
apply leq_trans with
(\sum_(tsk' <- ts | hep tsk' tsk && (tsk' != tsk))
(\sum_(j0 <- l | job_task j0 == tsk') job_cost j0)).
{
intros.
have EXCHANGE :=
exchange_big_dep
(fun x ⇒ hep (job_task x) tsk && (job_task x != tsk)).
rewrite EXCHANGE /=; last by move ⇒ tsk0 j0 HEP /eqP JOB0; rewrite JOB0.
rewrite /workload_of_jobs -/l big_seq_cond [X in _ ≤ X]big_seq_cond.
apply leq_sum; move ⇒ j0 /andP [IN0 HP0].
rewrite big_mkcond (big_rem (job_task j0)) /=;
first by rewrite HP0 andTb eq_refl; apply leq_addr.
by apply in_arrivals_implies_arrived in IN0;
apply H_all_jobs_from_taskset.
}
apply leq_sum_seq; intros tsk0 INtsk0 HP0.
apply leq_trans with (
task_cost tsk0 × num_arrivals_of_task job_task arr_seq tsk0 t (t + delta)).
{
rewrite /num_arrivals_of_task -sum1_size big_distrr /= big_filter.
rewrite -/l /workload_of_jobs.
rewrite /is_job_of_task muln1.
apply leq_sum_seq; move ⇒ j0 IN0 /eqP EQ.
rewrite -EQ.
apply H_job_cost_le_task_cost.
by apply in_arrivals_implies_arrived in IN0.
}
{
rewrite leq_mul2l; apply/orP; right.
rewrite -{2}[delta](addKn t).
apply H_is_arrival_bound; first by done.
by rewrite leq_addr.
}
Qed.
Lemma total_workload_le_total_rbf':
total_hep_workload t (t + delta) ≤ total_hep_rbf delta.
Proof.
intros.
rewrite /total_hep_rbf /total_hep_request_bound_function_FP
/task_request_bound_function.
rewrite /total_hep_workload /workload_of_jobs
/jlfp_higher_eq_priority /FP_to_JLFP /same_task H_job_of_tsk.
rewrite /arrivals_between.
set l := jobs_arrived_between arr_seq t (t + delta).
set hep := higher_eq_priority.
apply leq_trans with
(n := \sum_(tsk' <- ts | hep tsk' tsk)
(\sum_(j0 <- l | job_task j0 == tsk') job_cost j0)).
{
intros.
have EXCHANGE := exchange_big_dep (fun x ⇒ hep (job_task x) tsk).
rewrite EXCHANGE /=; last by move ⇒ tsk0 j0 HEP /eqP JOB0; rewrite JOB0.
rewrite /workload_of_jobs -/l big_seq_cond [X in _ ≤ X]big_seq_cond.
apply leq_sum; move ⇒ j0 /andP [IN0 HP0].
rewrite big_mkcond (big_rem (job_task j0)) /=;
first by rewrite HP0 andTb eq_refl; apply leq_addr.
by apply in_arrivals_implies_arrived in IN0;
apply H_all_jobs_from_taskset.
}
apply leq_sum_seq; intros tsk0 INtsk0 HP0.
apply leq_trans with (
task_cost tsk0 × num_arrivals_of_task job_task arr_seq tsk0 t (t + delta)).
{
rewrite /num_arrivals_of_task -sum1_size big_distrr /= big_filter.
rewrite -/l /workload_of_jobs.
rewrite /is_job_of_task muln1.
apply leq_sum_seq; move ⇒ j0 IN0 /eqP EQ.
rewrite -EQ.
apply H_job_cost_le_task_cost.
by apply in_arrivals_implies_arrived in IN0.
}
{
rewrite leq_mul2l; apply/orP; right.
rewrite -{2}[delta](addKn t).
apply H_is_arrival_bound; [by done | by rewrite leq_addr].
}
Qed.
Lemma total_workload_le_total_rbf'':
total_workload t (t + delta) ≤ total_rbf delta.
Proof.
intros.
rewrite /total_rbf
/task_request_bound_function.
rewrite /total_workload /workload_of_jobs.
rewrite /arrivals_between.
set l := jobs_arrived_between arr_seq t (t + delta).
rewrite big_mkcond //=.
apply leq_trans with
(n := \sum_(tsk' <- ts)
(\sum_(j0 <- l | job_task j0 == tsk') job_cost j0)).
{
intros.
have EXCHANGE := exchange_big_dep predT.
rewrite EXCHANGE /=; last by done.
rewrite /workload_of_jobs -/l big_seq_cond [X in _ ≤ X]big_seq_cond.
apply leq_sum; move ⇒ j0 /andP [IN0 HP0].
rewrite big_mkcond (big_rem (job_task j0)) /=.
rewrite eq_refl; apply leq_addr.
by apply in_arrivals_implies_arrived in IN0;
apply H_all_jobs_from_taskset.
}
apply leq_sum_seq; intros tsk0 INtsk0 HP0.
apply leq_trans with (
task_cost tsk0 × num_arrivals_of_task job_task arr_seq tsk0 t (t + delta)).
{
rewrite /num_arrivals_of_task -sum1_size big_distrr /= big_filter.
rewrite -/l /workload_of_jobs.
rewrite /is_job_of_task muln1.
apply leq_sum_seq; move ⇒ j0 IN0 /eqP EQ.
rewrite -EQ.
apply H_job_cost_le_task_cost.
by apply in_arrivals_implies_arrived in IN0.
}
{
rewrite leq_mul2l; apply/orP; right.
rewrite -{2}[delta](addKn t).
apply H_is_arrival_bound; [by done | by rewrite leq_addr].
}
Qed.
End WorkloadIsBoundedByRBF.
End ProofWorkloadBound.
End Lemmas.
End MaxArrivalsWorkloadBound.
Require Import prosa.classic.model.arrival.basic.job
prosa.classic.model.arrival.basic.task_arrival
prosa.classic.model.priority.
Require Import prosa.classic.model.schedule.uni.service
prosa.classic.model.schedule.uni.workload
prosa.classic.model.schedule.uni.schedule.
Require Import prosa.classic.model.arrival.curves.bounds.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
Module MaxArrivalsWorkloadBound.
Import Job ArrivalCurves TaskArrival Priority UniprocessorSchedule Workload Service.
Section Lemmas.
Context {Task: eqType}.
Variable task_cost: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → Task.
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_arr_seq_is_a_set: arrival_sequence_is_a_set arr_seq.
Variable sched: schedule Job.
Hypothesis H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq.
Variable higher_eq_priority: FP_policy Task.
Let jlfp_higher_eq_priority := FP_to_JLFP job_task higher_eq_priority.
Let arrivals_between := jobs_arrived_between arr_seq.
Section RequestBoundFunction.
Variable max_arrivals: Task → time → nat.
Section SingleTask.
Variable tsk: Task.
Variable delta: time.
Definition task_request_bound_function := task_cost tsk × max_arrivals tsk delta.
End SingleTask.
Section AllTasks.
Variable ts: list Task.
Variable tsk: Task.
Variable delta: time.
Let is_hep_task tsk_other := higher_eq_priority tsk_other tsk.
Let is_other_hep_task tsk_other := higher_eq_priority tsk_other tsk && (tsk_other != tsk).
Definition total_request_bound_function :=
\sum_(tsk <- ts) task_request_bound_function tsk delta.
Definition total_hep_request_bound_function_FP :=
\sum_(tsk_other <- ts | is_hep_task tsk_other)
task_request_bound_function tsk_other delta.
Definition total_ohep_request_bound_function_FP :=
\sum_(tsk_other <- ts | is_other_hep_task tsk_other)
task_request_bound_function tsk_other delta.
End AllTasks.
End RequestBoundFunction.
Section ProofWorkloadBound.
Variable ts: list Task.
Variable tsk: Task.
Hypothesis H_tsk_in_ts: tsk \in ts.
Hypothesis H_job_cost_le_task_cost:
∀ j,
arrives_in arr_seq j →
job_cost_le_task_cost task_cost job_cost job_task j.
Hypothesis H_all_jobs_from_taskset:
∀ j, arrives_in arr_seq j → job_task j \in ts.
Variable max_arrivals: Task → time → nat.
Hypothesis H_is_arrival_bound:
is_arrival_bound_for_taskset job_task arr_seq max_arrivals ts.
Let task_rbf := task_request_bound_function max_arrivals tsk.
Let total_rbf := total_request_bound_function max_arrivals ts.
Let total_hep_rbf := total_hep_request_bound_function_FP max_arrivals ts tsk.
Let total_ohep_rbf := total_ohep_request_bound_function_FP max_arrivals ts tsk.
Variable j: Job.
Hypothesis H_j_arrives: arrives_in arr_seq j.
Hypothesis H_job_of_tsk: job_task j = tsk.
Let same_task j1 j2 := job_task j1 == job_task j2.
Let other_higher_eq_priority j1 j2 := jlfp_higher_eq_priority j1 j2 && (~~ same_task j1 j2).
Let total_workload t1 t2 :=
workload_of_jobs job_cost (arrivals_between t1 t2) (fun j ⇒ true).
Let total_hep_workload t1 t2 :=
workload_of_jobs job_cost (arrivals_between t1 t2)
(fun j_other ⇒ jlfp_higher_eq_priority j_other j).
Let total_ohep_workload t1 t2 :=
workload_of_jobs job_cost (arrivals_between t1 t2)
(fun j_other ⇒ other_higher_eq_priority j_other j).
Let task_workload (t1: time) (t2: time) :=
workload_of_jobs job_cost (arrivals_between t1 t2)
(fun j_other ⇒ same_task j_other j).
Section WorkloadIsBoundedByRBF.
Variable t: time.
Variable delta: time.
Lemma task_workload_le_task_rbf:
task_workload t (t + delta) ≤ task_rbf delta.
Proof.
unfold task_workload.
unfold task_rbf, task_request_bound_function.
unfold is_arrival_bound in ×.
unfold arrivals_between.
set l := jobs_arrived_between arr_seq t delta.
apply leq_trans with (
task_cost tsk × num_arrivals_of_task job_task arr_seq tsk t (t + delta)).
{
rewrite /num_arrivals_of_task -sum1_size big_distrr /= big_filter.
rewrite -/l /workload_of_jobs.
rewrite /is_job_of_task /same_task H_job_of_tsk muln1.
apply leq_sum_seq; move ⇒ j0 IN0 /eqP EQ.
rewrite -EQ.
apply H_job_cost_le_task_cost.
by apply in_arrivals_implies_arrived in IN0.
}
{
rewrite leq_mul2l; apply/orP; right.
rewrite -{2}[delta](addKn t).
apply H_is_arrival_bound; first by done.
by rewrite leq_addr.
}
Qed.
Lemma total_workload_le_total_rbf:
total_ohep_workload t (t + delta) ≤ total_ohep_rbf delta.
Proof.
rewrite /total_ohep_rbf /total_ohep_request_bound_function_FP
/task_request_bound_function.
rewrite /total_ohep_workload /workload_of_jobs
/other_higher_eq_priority.
rewrite /jlfp_higher_eq_priority
/FP_to_JLFP /same_task H_job_of_tsk.
rewrite /arrivals_between.
set l := jobs_arrived_between arr_seq t (t + delta).
set hep := higher_eq_priority.
apply leq_trans with
(\sum_(tsk' <- ts | hep tsk' tsk && (tsk' != tsk))
(\sum_(j0 <- l | job_task j0 == tsk') job_cost j0)).
{
intros.
have EXCHANGE :=
exchange_big_dep
(fun x ⇒ hep (job_task x) tsk && (job_task x != tsk)).
rewrite EXCHANGE /=; last by move ⇒ tsk0 j0 HEP /eqP JOB0; rewrite JOB0.
rewrite /workload_of_jobs -/l big_seq_cond [X in _ ≤ X]big_seq_cond.
apply leq_sum; move ⇒ j0 /andP [IN0 HP0].
rewrite big_mkcond (big_rem (job_task j0)) /=;
first by rewrite HP0 andTb eq_refl; apply leq_addr.
by apply in_arrivals_implies_arrived in IN0;
apply H_all_jobs_from_taskset.
}
apply leq_sum_seq; intros tsk0 INtsk0 HP0.
apply leq_trans with (
task_cost tsk0 × num_arrivals_of_task job_task arr_seq tsk0 t (t + delta)).
{
rewrite /num_arrivals_of_task -sum1_size big_distrr /= big_filter.
rewrite -/l /workload_of_jobs.
rewrite /is_job_of_task muln1.
apply leq_sum_seq; move ⇒ j0 IN0 /eqP EQ.
rewrite -EQ.
apply H_job_cost_le_task_cost.
by apply in_arrivals_implies_arrived in IN0.
}
{
rewrite leq_mul2l; apply/orP; right.
rewrite -{2}[delta](addKn t).
apply H_is_arrival_bound; first by done.
by rewrite leq_addr.
}
Qed.
Lemma total_workload_le_total_rbf':
total_hep_workload t (t + delta) ≤ total_hep_rbf delta.
Proof.
intros.
rewrite /total_hep_rbf /total_hep_request_bound_function_FP
/task_request_bound_function.
rewrite /total_hep_workload /workload_of_jobs
/jlfp_higher_eq_priority /FP_to_JLFP /same_task H_job_of_tsk.
rewrite /arrivals_between.
set l := jobs_arrived_between arr_seq t (t + delta).
set hep := higher_eq_priority.
apply leq_trans with
(n := \sum_(tsk' <- ts | hep tsk' tsk)
(\sum_(j0 <- l | job_task j0 == tsk') job_cost j0)).
{
intros.
have EXCHANGE := exchange_big_dep (fun x ⇒ hep (job_task x) tsk).
rewrite EXCHANGE /=; last by move ⇒ tsk0 j0 HEP /eqP JOB0; rewrite JOB0.
rewrite /workload_of_jobs -/l big_seq_cond [X in _ ≤ X]big_seq_cond.
apply leq_sum; move ⇒ j0 /andP [IN0 HP0].
rewrite big_mkcond (big_rem (job_task j0)) /=;
first by rewrite HP0 andTb eq_refl; apply leq_addr.
by apply in_arrivals_implies_arrived in IN0;
apply H_all_jobs_from_taskset.
}
apply leq_sum_seq; intros tsk0 INtsk0 HP0.
apply leq_trans with (
task_cost tsk0 × num_arrivals_of_task job_task arr_seq tsk0 t (t + delta)).
{
rewrite /num_arrivals_of_task -sum1_size big_distrr /= big_filter.
rewrite -/l /workload_of_jobs.
rewrite /is_job_of_task muln1.
apply leq_sum_seq; move ⇒ j0 IN0 /eqP EQ.
rewrite -EQ.
apply H_job_cost_le_task_cost.
by apply in_arrivals_implies_arrived in IN0.
}
{
rewrite leq_mul2l; apply/orP; right.
rewrite -{2}[delta](addKn t).
apply H_is_arrival_bound; [by done | by rewrite leq_addr].
}
Qed.
Lemma total_workload_le_total_rbf'':
total_workload t (t + delta) ≤ total_rbf delta.
Proof.
intros.
rewrite /total_rbf
/task_request_bound_function.
rewrite /total_workload /workload_of_jobs.
rewrite /arrivals_between.
set l := jobs_arrived_between arr_seq t (t + delta).
rewrite big_mkcond //=.
apply leq_trans with
(n := \sum_(tsk' <- ts)
(\sum_(j0 <- l | job_task j0 == tsk') job_cost j0)).
{
intros.
have EXCHANGE := exchange_big_dep predT.
rewrite EXCHANGE /=; last by done.
rewrite /workload_of_jobs -/l big_seq_cond [X in _ ≤ X]big_seq_cond.
apply leq_sum; move ⇒ j0 /andP [IN0 HP0].
rewrite big_mkcond (big_rem (job_task j0)) /=.
rewrite eq_refl; apply leq_addr.
by apply in_arrivals_implies_arrived in IN0;
apply H_all_jobs_from_taskset.
}
apply leq_sum_seq; intros tsk0 INtsk0 HP0.
apply leq_trans with (
task_cost tsk0 × num_arrivals_of_task job_task arr_seq tsk0 t (t + delta)).
{
rewrite /num_arrivals_of_task -sum1_size big_distrr /= big_filter.
rewrite -/l /workload_of_jobs.
rewrite /is_job_of_task muln1.
apply leq_sum_seq; move ⇒ j0 IN0 /eqP EQ.
rewrite -EQ.
apply H_job_cost_le_task_cost.
by apply in_arrivals_implies_arrived in IN0.
}
{
rewrite leq_mul2l; apply/orP; right.
rewrite -{2}[delta](addKn t).
apply H_is_arrival_bound; [by done | by rewrite leq_addr].
}
Qed.
End WorkloadIsBoundedByRBF.
End ProofWorkloadBound.
End Lemmas.
End MaxArrivalsWorkloadBound.