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.
Lemma total_workload_le_total_rbf:
total_ohep_workload t (t + delta) ≤ total_ohep_rbf delta.
Lemma total_workload_le_total_rbf':
total_hep_workload t (t + delta) ≤ total_hep_rbf delta.
Lemma total_workload_le_total_rbf'':
total_workload t (t + delta) ≤ total_rbf delta.
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.
Lemma total_workload_le_total_rbf:
total_ohep_workload t (t + delta) ≤ total_ohep_rbf delta.
Lemma total_workload_le_total_rbf':
total_hep_workload t (t + delta) ≤ total_hep_rbf delta.
Lemma total_workload_le_total_rbf'':
total_workload t (t + delta) ≤ total_rbf delta.
End WorkloadIsBoundedByRBF.
End ProofWorkloadBound.
End Lemmas.
End MaxArrivalsWorkloadBound.