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.
(* In this file, we define the workload bound for jitter-aware FP scheduling. *)
Module WorkloadBoundFP.
Import JobWithJitter SporadicTaskset UniprocessorScheduleWithJitter Priority Workload
TaskArrivalWithJitter ArrivalBounds.
(* First, we define a bound for the workload of a single task. *)
Section SingleTask.
Context {Task: eqType}.
Variable task_cost: Task → time.
Variable task_period: Task → time.
Variable task_jitter: Task → time.
(* Consider any task tsk to be scheduled in a given interval of length delta. *)
Variable tsk: Task.
Variable delta: time.
(* Based on the maximum number of jobs of tsk that can execute in the interval, ... *)
Definition max_jobs := div_ceil (delta + task_jitter tsk) (task_period tsk).
(* ... we define the following workload bound for the task. *)
Definition task_workload_bound_FP := max_jobs × task_cost tsk.
End SingleTask.
(* In this section, we define a bound for the workload all tasks with
higher or equal priority. *)
Section AllTasks.
Context {Task: eqType}.
Variable task_cost: Task → time.
Variable task_period: Task → time.
Variable task_jitter: Task → time.
(* Assume any FP policy. *)
Variable higher_eq_priority: FP_policy Task.
(* Consider a task set ts... *)
Variable ts: list Task.
(* ...and let tsk be the task to be analyzed. *)
Variable tsk: Task.
(* Let delta be the length of the interval of interest. *)
Variable delta: time.
(* Recall the definition of higher-or-equal-priority task and
the per-task workload bound for FP scheduling (defined above). *)
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.
(* Using the sum of individual workload bounds, we define the following bound
for the total workload of tasks of higher-or-equal priority (with respect
to tsk) in any interval of length delta. *)
Definition total_workload_bound_fp :=
\sum_(tsk_other <- ts | is_hep_task tsk_other) W tsk_other.
End AllTasks.
(* In this section, we prove some basic lemmas about the workload bound. *)
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.
(* Assume any FP policy. *)
Variable higher_eq_priority: FP_policy Task.
(* Consider a task set ts... *)
Variable ts: list Task.
(* ...and let tsk be any task in ts. *)
Variable tsk: Task.
Hypothesis H_tsk_in_ts: tsk \in ts.
(* Recall the workload bound for uniprocessor FP scheduling. *)
Let workload_bound :=
total_workload_bound_fp task_cost task_period task_jitter higher_eq_priority ts tsk.
(* In this section we prove that the workload bound in a time window of
length (task_cost tsk) is as large as (task_cost tsk) time units.
(This is an important initial condition for the fixed-point iteration.) *)
Section NoSmallerThanCost.
(* Assume that the priority order is reflexive... *)
Hypothesis H_priority_is_reflexive: FP_is_reflexive higher_eq_priority.
(* ...and that the cost and period of task tsk are positive. *)
Hypothesis H_cost_positive: task_cost tsk > 0.
Hypothesis H_period_positive: task_period tsk > 0.
(* Then, we prove that the workload bound in an interval of length (task_cost tsk)
cannot be smaller than (task_cost tsk). *)
Lemma total_workload_bound_fp_ge_cost:
workload_bound (task_cost tsk) ≥ task_cost tsk.
End NoSmallerThanCost.
(* In this section, we prove that the workload bound is monotonically non-decreasing. *)
Section NonDecreasing.
(* Assume that the period of every task in the task set is positive. *)
Hypothesis H_period_positive:
∀ tsk,
tsk \in ts →
task_period tsk > 0.
(* Then, the workload bound is a monotonically non-decreasing function.
(This is an important property for the fixed-point iteration.) *)
Lemma total_workload_bound_fp_non_decreasing:
∀ delta1 delta2,
delta1 ≤ delta2 →
workload_bound delta1 ≤ workload_bound delta2.
End NonDecreasing.
End BasicLemmas.
(* In this section, we prove that any fixed point R = workload_bound R
is indeed a workload bound for any interval of length R. *)
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.
(* Let ts be any task set... *)
Variable ts: seq Task.
(* ...with positive task periods. *)
Hypothesis H_positive_periods:
∀ tsk, tsk \in ts → task_period tsk > 0.
(* Consider any job arrival sequence with consistent, duplicate-free arrivals. *)
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.
(* First, let's define some local names for clarity. *)
Let actual_arrivals := actual_arrivals_between job_arrival job_jitter arr_seq.
(* Next, assume that all jobs come from the task set, ...*)
Hypothesis H_all_jobs_from_taskset:
∀ j, arrives_in arr_seq j → job_task j \in ts.
(* ...the cost of each job is bounded by the cost of its task, ... *)
Hypothesis H_job_cost_le_task_cost:
∀ j,
arrives_in arr_seq j →
job_cost j ≤ task_cost (job_task j).
(* ...and the jitter of each job is bounded by the jitter of its task. *)
Hypothesis H_job_jitter_le_task_jitter:
∀ j,
arrives_in arr_seq j →
job_jitter j ≤ task_jitter (job_task j).
(* Assume that jobs arrived sporadically. *)
Hypothesis H_sporadic_arrivals:
sporadic_task_model task_period job_arrival job_task arr_seq.
(* Then, let tsk be any task in ts. *)
Variable tsk: Task.
Hypothesis H_tsk_in_ts: tsk \in ts.
(* For a given fixed-priority policy, ... *)
Variable higher_eq_priority: FP_policy Task.
(* ...we recall the definitions of higher-or-equal-priority workload and the workload bound. *)
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.
(* Next, consider any R that is a fixed point of the following equation,
i.e., the claimed workload bound is equal to the interval length. *)
Variable R: time.
Hypothesis H_fixed_point: R = workload_bound R.
(* Then, we prove that R bounds the workload of jobs of higher-or-equal-priority tasks
with actual arrival time (including jitter) in t, t + 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.
(* In this file, we define the workload bound for jitter-aware FP scheduling. *)
Module WorkloadBoundFP.
Import JobWithJitter SporadicTaskset UniprocessorScheduleWithJitter Priority Workload
TaskArrivalWithJitter ArrivalBounds.
(* First, we define a bound for the workload of a single task. *)
Section SingleTask.
Context {Task: eqType}.
Variable task_cost: Task → time.
Variable task_period: Task → time.
Variable task_jitter: Task → time.
(* Consider any task tsk to be scheduled in a given interval of length delta. *)
Variable tsk: Task.
Variable delta: time.
(* Based on the maximum number of jobs of tsk that can execute in the interval, ... *)
Definition max_jobs := div_ceil (delta + task_jitter tsk) (task_period tsk).
(* ... we define the following workload bound for the task. *)
Definition task_workload_bound_FP := max_jobs × task_cost tsk.
End SingleTask.
(* In this section, we define a bound for the workload all tasks with
higher or equal priority. *)
Section AllTasks.
Context {Task: eqType}.
Variable task_cost: Task → time.
Variable task_period: Task → time.
Variable task_jitter: Task → time.
(* Assume any FP policy. *)
Variable higher_eq_priority: FP_policy Task.
(* Consider a task set ts... *)
Variable ts: list Task.
(* ...and let tsk be the task to be analyzed. *)
Variable tsk: Task.
(* Let delta be the length of the interval of interest. *)
Variable delta: time.
(* Recall the definition of higher-or-equal-priority task and
the per-task workload bound for FP scheduling (defined above). *)
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.
(* Using the sum of individual workload bounds, we define the following bound
for the total workload of tasks of higher-or-equal priority (with respect
to tsk) in any interval of length delta. *)
Definition total_workload_bound_fp :=
\sum_(tsk_other <- ts | is_hep_task tsk_other) W tsk_other.
End AllTasks.
(* In this section, we prove some basic lemmas about the workload bound. *)
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.
(* Assume any FP policy. *)
Variable higher_eq_priority: FP_policy Task.
(* Consider a task set ts... *)
Variable ts: list Task.
(* ...and let tsk be any task in ts. *)
Variable tsk: Task.
Hypothesis H_tsk_in_ts: tsk \in ts.
(* Recall the workload bound for uniprocessor FP scheduling. *)
Let workload_bound :=
total_workload_bound_fp task_cost task_period task_jitter higher_eq_priority ts tsk.
(* In this section we prove that the workload bound in a time window of
length (task_cost tsk) is as large as (task_cost tsk) time units.
(This is an important initial condition for the fixed-point iteration.) *)
Section NoSmallerThanCost.
(* Assume that the priority order is reflexive... *)
Hypothesis H_priority_is_reflexive: FP_is_reflexive higher_eq_priority.
(* ...and that the cost and period of task tsk are positive. *)
Hypothesis H_cost_positive: task_cost tsk > 0.
Hypothesis H_period_positive: task_period tsk > 0.
(* Then, we prove that the workload bound in an interval of length (task_cost tsk)
cannot be smaller than (task_cost tsk). *)
Lemma total_workload_bound_fp_ge_cost:
workload_bound (task_cost tsk) ≥ task_cost tsk.
End NoSmallerThanCost.
(* In this section, we prove that the workload bound is monotonically non-decreasing. *)
Section NonDecreasing.
(* Assume that the period of every task in the task set is positive. *)
Hypothesis H_period_positive:
∀ tsk,
tsk \in ts →
task_period tsk > 0.
(* Then, the workload bound is a monotonically non-decreasing function.
(This is an important property for the fixed-point iteration.) *)
Lemma total_workload_bound_fp_non_decreasing:
∀ delta1 delta2,
delta1 ≤ delta2 →
workload_bound delta1 ≤ workload_bound delta2.
End NonDecreasing.
End BasicLemmas.
(* In this section, we prove that any fixed point R = workload_bound R
is indeed a workload bound for any interval of length R. *)
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.
(* Let ts be any task set... *)
Variable ts: seq Task.
(* ...with positive task periods. *)
Hypothesis H_positive_periods:
∀ tsk, tsk \in ts → task_period tsk > 0.
(* Consider any job arrival sequence with consistent, duplicate-free arrivals. *)
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.
(* First, let's define some local names for clarity. *)
Let actual_arrivals := actual_arrivals_between job_arrival job_jitter arr_seq.
(* Next, assume that all jobs come from the task set, ...*)
Hypothesis H_all_jobs_from_taskset:
∀ j, arrives_in arr_seq j → job_task j \in ts.
(* ...the cost of each job is bounded by the cost of its task, ... *)
Hypothesis H_job_cost_le_task_cost:
∀ j,
arrives_in arr_seq j →
job_cost j ≤ task_cost (job_task j).
(* ...and the jitter of each job is bounded by the jitter of its task. *)
Hypothesis H_job_jitter_le_task_jitter:
∀ j,
arrives_in arr_seq j →
job_jitter j ≤ task_jitter (job_task j).
(* Assume that jobs arrived sporadically. *)
Hypothesis H_sporadic_arrivals:
sporadic_task_model task_period job_arrival job_task arr_seq.
(* Then, let tsk be any task in ts. *)
Variable tsk: Task.
Hypothesis H_tsk_in_ts: tsk \in ts.
(* For a given fixed-priority policy, ... *)
Variable higher_eq_priority: FP_policy Task.
(* ...we recall the definitions of higher-or-equal-priority workload and the workload bound. *)
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.
(* Next, consider any R that is a fixed point of the following equation,
i.e., the claimed workload bound is equal to the interval length. *)
Variable R: time.
Hypothesis H_fixed_point: R = workload_bound R.
(* Then, we prove that R bounds the workload of jobs of higher-or-equal-priority tasks
with actual arrival time (including jitter) in t, t + R). *)
Lemma fp_workload_bound_holds:
∀ t,
actual_hp_workload t (t + R) ≤ R.
End ProofWorkloadBound.
End WorkloadBoundFP.