Library prosa.classic.analysis.uni.jitter.workload_bound_fp
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.priority.
Require Import prosa.classic.model.arrival.jitter.job
prosa.classic.model.arrival.jitter.task_arrival
prosa.classic.model.arrival.jitter.arrival_bounds.
Require Import prosa.classic.model.schedule.uni.workload.
Require Import prosa.classic.model.schedule.uni.jitter.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.
Module WorkloadBoundFP.
Import JobWithJitter SporadicTaskset UniprocessorScheduleWithJitter Priority Workload
TaskArrivalWithJitter ArrivalBounds.
Section SingleTask.
Context {Task: eqType}.
Variable task_cost: Task → time.
Variable task_period: Task → time.
Variable task_jitter: Task → time.
Variable tsk: Task.
Variable delta: time.
Definition max_jobs := div_ceil (delta + task_jitter tsk) (task_period tsk).
Definition task_workload_bound_FP := max_jobs × task_cost tsk.
End SingleTask.
Section AllTasks.
Context {Task: eqType}.
Variable task_cost: Task → time.
Variable task_period: Task → time.
Variable task_jitter: Task → time.
Variable higher_eq_priority: FP_policy Task.
Variable ts: list Task.
Variable tsk: Task.
Variable delta: time.
Let is_hep_task tsk_other := higher_eq_priority tsk_other tsk.
Let W tsk_other :=
task_workload_bound_FP task_cost task_period task_jitter tsk_other delta.
Definition total_workload_bound_fp :=
\sum_(tsk_other <- ts | is_hep_task tsk_other) W tsk_other.
End AllTasks.
Section BasicLemmas.
Context {Task: eqType}.
Variable task_cost: Task → time.
Variable task_period: Task → time.
Variable task_deadline: Task → time.
Variable task_jitter: Task → time.
Variable higher_eq_priority: FP_policy Task.
Variable ts: list Task.
Variable tsk: Task.
Hypothesis H_tsk_in_ts: tsk \in ts.
Let workload_bound :=
total_workload_bound_fp task_cost task_period task_jitter higher_eq_priority ts tsk.
Section NoSmallerThanCost.
Hypothesis H_priority_is_reflexive: FP_is_reflexive higher_eq_priority.
Hypothesis H_cost_positive: task_cost tsk > 0.
Hypothesis H_period_positive: task_period tsk > 0.
Lemma total_workload_bound_fp_ge_cost:
workload_bound (task_cost tsk) ≥ task_cost tsk.
End NoSmallerThanCost.
Section NonDecreasing.
Hypothesis H_period_positive:
∀ tsk,
tsk \in ts →
task_period tsk > 0.
Lemma total_workload_bound_fp_non_decreasing:
∀ delta1 delta2,
delta1 ≤ delta2 →
workload_bound delta1 ≤ workload_bound delta2.
End NonDecreasing.
End BasicLemmas.
Section ProofWorkloadBound.
Context {Task: eqType}.
Variable task_cost: Task → time.
Variable task_period: Task → time.
Variable task_jitter: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_jitter: Job → time.
Variable job_task: Job → Task.
Variable ts: seq Task.
Hypothesis H_positive_periods:
∀ tsk, tsk \in ts → task_period tsk > 0.
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_arrival_sequence_is_a_set: arrival_sequence_is_a_set arr_seq.
Let actual_arrivals := actual_arrivals_between job_arrival job_jitter arr_seq.
Hypothesis H_all_jobs_from_taskset:
∀ j, arrives_in arr_seq j → job_task j \in ts.
Hypothesis H_job_cost_le_task_cost:
∀ j,
arrives_in arr_seq j →
job_cost j ≤ task_cost (job_task j).
Hypothesis H_job_jitter_le_task_jitter:
∀ j,
arrives_in arr_seq j →
job_jitter j ≤ task_jitter (job_task j).
Hypothesis H_sporadic_arrivals:
sporadic_task_model task_period job_arrival job_task arr_seq.
Variable tsk: Task.
Hypothesis H_tsk_in_ts: tsk \in ts.
Variable higher_eq_priority: FP_policy Task.
Let actual_hp_workload t1 t2 :=
workload_of_higher_or_equal_priority_tasks job_cost job_task (actual_arrivals t1 t2)
higher_eq_priority tsk.
Let workload_bound :=
total_workload_bound_fp task_cost task_period task_jitter higher_eq_priority ts tsk.
Variable R: time.
Hypothesis H_fixed_point: R = workload_bound R.
Lemma fp_workload_bound_holds:
∀ t,
actual_hp_workload t (t + R) ≤ R.
End ProofWorkloadBound.
End WorkloadBoundFP.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.priority.
Require Import prosa.classic.model.arrival.jitter.job
prosa.classic.model.arrival.jitter.task_arrival
prosa.classic.model.arrival.jitter.arrival_bounds.
Require Import prosa.classic.model.schedule.uni.workload.
Require Import prosa.classic.model.schedule.uni.jitter.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.
Module WorkloadBoundFP.
Import JobWithJitter SporadicTaskset UniprocessorScheduleWithJitter Priority Workload
TaskArrivalWithJitter ArrivalBounds.
Section SingleTask.
Context {Task: eqType}.
Variable task_cost: Task → time.
Variable task_period: Task → time.
Variable task_jitter: Task → time.
Variable tsk: Task.
Variable delta: time.
Definition max_jobs := div_ceil (delta + task_jitter tsk) (task_period tsk).
Definition task_workload_bound_FP := max_jobs × task_cost tsk.
End SingleTask.
Section AllTasks.
Context {Task: eqType}.
Variable task_cost: Task → time.
Variable task_period: Task → time.
Variable task_jitter: Task → time.
Variable higher_eq_priority: FP_policy Task.
Variable ts: list Task.
Variable tsk: Task.
Variable delta: time.
Let is_hep_task tsk_other := higher_eq_priority tsk_other tsk.
Let W tsk_other :=
task_workload_bound_FP task_cost task_period task_jitter tsk_other delta.
Definition total_workload_bound_fp :=
\sum_(tsk_other <- ts | is_hep_task tsk_other) W tsk_other.
End AllTasks.
Section BasicLemmas.
Context {Task: eqType}.
Variable task_cost: Task → time.
Variable task_period: Task → time.
Variable task_deadline: Task → time.
Variable task_jitter: Task → time.
Variable higher_eq_priority: FP_policy Task.
Variable ts: list Task.
Variable tsk: Task.
Hypothesis H_tsk_in_ts: tsk \in ts.
Let workload_bound :=
total_workload_bound_fp task_cost task_period task_jitter higher_eq_priority ts tsk.
Section NoSmallerThanCost.
Hypothesis H_priority_is_reflexive: FP_is_reflexive higher_eq_priority.
Hypothesis H_cost_positive: task_cost tsk > 0.
Hypothesis H_period_positive: task_period tsk > 0.
Lemma total_workload_bound_fp_ge_cost:
workload_bound (task_cost tsk) ≥ task_cost tsk.
End NoSmallerThanCost.
Section NonDecreasing.
Hypothesis H_period_positive:
∀ tsk,
tsk \in ts →
task_period tsk > 0.
Lemma total_workload_bound_fp_non_decreasing:
∀ delta1 delta2,
delta1 ≤ delta2 →
workload_bound delta1 ≤ workload_bound delta2.
End NonDecreasing.
End BasicLemmas.
Section ProofWorkloadBound.
Context {Task: eqType}.
Variable task_cost: Task → time.
Variable task_period: Task → time.
Variable task_jitter: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_jitter: Job → time.
Variable job_task: Job → Task.
Variable ts: seq Task.
Hypothesis H_positive_periods:
∀ tsk, tsk \in ts → task_period tsk > 0.
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_arrival_sequence_is_a_set: arrival_sequence_is_a_set arr_seq.
Let actual_arrivals := actual_arrivals_between job_arrival job_jitter arr_seq.
Hypothesis H_all_jobs_from_taskset:
∀ j, arrives_in arr_seq j → job_task j \in ts.
Hypothesis H_job_cost_le_task_cost:
∀ j,
arrives_in arr_seq j →
job_cost j ≤ task_cost (job_task j).
Hypothesis H_job_jitter_le_task_jitter:
∀ j,
arrives_in arr_seq j →
job_jitter j ≤ task_jitter (job_task j).
Hypothesis H_sporadic_arrivals:
sporadic_task_model task_period job_arrival job_task arr_seq.
Variable tsk: Task.
Hypothesis H_tsk_in_ts: tsk \in ts.
Variable higher_eq_priority: FP_policy Task.
Let actual_hp_workload t1 t2 :=
workload_of_higher_or_equal_priority_tasks job_cost job_task (actual_arrivals t1 t2)
higher_eq_priority tsk.
Let workload_bound :=
total_workload_bound_fp task_cost task_period task_jitter higher_eq_priority ts tsk.
Variable R: time.
Hypothesis H_fixed_point: R = workload_bound R.
Lemma fp_workload_bound_holds:
∀ t,
actual_hp_workload t (t + R) ≤ R.
End ProofWorkloadBound.
End WorkloadBoundFP.