Library rt.analysis.apa.workload_bound
Require Import rt.util.all.
Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.task_arrival.
Require Import rt.model.schedule.global.response_time rt.model.schedule.global.schedulability
rt.model.schedule.global.workload.
Require Import rt.model.schedule.global.basic.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.
Module WorkloadBound.
Import Job SporadicTaskset Schedule ScheduleOfSporadicTask TaskArrival ResponseTime Schedulability Workload.
Section WorkloadBoundDef.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
(* Consider any task tsk with response-time bound R_tsk,
that is scheduled in an interval of length delta. *)
Variable tsk: sporadic_task.
Variable R_tsk: time.
Variable delta: time.
(* Based on the number of jobs that execute completely in the interval, ... *)
Definition max_jobs :=
div_floor (delta + R_tsk - task_cost tsk) (task_period tsk).
(* ... Bertogna and Cirinei's workload bound is defined as follows. *)
Definition W :=
let e_k := (task_cost tsk) in
let p_k := (task_period tsk) in
minn e_k (delta + R_tsk - e_k - max_jobs × p_k) + max_jobs × e_k.
End WorkloadBoundDef.
Section BasicLemmas.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
(* Let tsk be any task...*)
Variable tsk: sporadic_task.
(* ... with period > 0. *)
Hypothesis H_period_positive: task_period tsk > 0.
(* Let R1 <= R2 be two response-time bounds that
are larger than the cost of the tsk. *)
Variable R1 R2: time.
Hypothesis H_R_lower_bound: R1 ≥ task_cost tsk.
Hypothesis H_R1_le_R2: R1 ≤ R2.
Let workload_bound := W task_cost task_period tsk.
(* Then, Bertogna and Cirinei's workload bound is monotonically increasing. *)
Lemma W_monotonic :
∀ t1 t2,
t1 ≤ t2 →
workload_bound R1 t1 ≤ workload_bound R2 t2.
End BasicLemmas.
Section ProofWorkloadBound.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → sporadic_task.
Variable job_deadline: Job → time.
Variable arr_seq: arrival_sequence Job.
(* Assume that all jobs have valid parameters *)
Hypothesis H_jobs_have_valid_parameters :
∀ j,
arrives_in arr_seq j →
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
(* Consider any schedule. *)
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
(* Assumption: jobs only execute if they arrived.
This is used to eliminate jobs that arrive after end of the interval t1 + delta. *)
Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute job_arrival sched.
(* Assumption: jobs do not execute after they completed.
This is used to eliminate jobs that complete before the start of the interval t1. *)
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
(* Assumption: Jobs are sequential.
This is required to use interval lengths as a measure of service. *)
Hypothesis H_sequential_jobs: sequential_jobs sched.
(* Assumption: sporadic task model.
This is necessary to conclude that consecutive jobs ordered by arrival times
are separated by at least 'period' times units. *)
Hypothesis H_sporadic_tasks: sporadic_task_model task_period job_arrival job_task arr_seq.
(* Before starting the proof, let's give simpler names to the definitions. *)
Let job_has_completed_by := completed job_cost sched.
Let workload_of (tsk: sporadic_task) (t1 t2: time) := workload job_task sched tsk t1 t2.
(* Now we define the theorem. Let tsk be any task in the taskset. *)
Variable tsk: sporadic_task.
(* Assumption: the task must have valid parameters:
a) period > 0 (used in divisions)
b) deadline of the jobs = deadline of the task
c) cost <= period
(used to prove that the distance between the first and last
jobs is at least (cost + n*period), where n is the number
of middle jobs. If cost >> period, the claim does not hold
for every task set. *)
Hypothesis H_valid_task_parameters:
is_valid_sporadic_task task_cost task_period task_deadline tsk.
(* Assumption: the task must have a constrained deadline.
This is required to prove that n_k (max_jobs) from Bertogna
and Cirinei's formula accounts for at least the number of
middle jobs (i.e., number of jobs - 2 in the worst case). *)
Hypothesis H_constrained_deadline: task_deadline tsk ≤ task_period tsk.
(* Consider an interval t1, t1 + delta). *)
Variable t1 delta: time.
(* Assume that a response-time bound R_tsk for that task in any
schedule of this processor platform is also given, ... *)
Variable R_tsk: time.
Hypothesis H_response_time_bound :
∀ j,
arrives_in arr_seq j →
job_task j = tsk →
job_arrival j + R_tsk < t1 + delta →
job_has_completed_by j (job_arrival j + R_tsk).
(* ... such that R_tsk >= task_cost tsk and R_tsk <= task_deadline tsk. *)
Hypothesis H_response_time_ge_cost: R_tsk ≥ task_cost tsk.
Hypothesis H_no_deadline_miss: R_tsk ≤ task_deadline tsk.
Section MainProof.
(* In this section, we prove that the workload of a task in the
interval t1, t1 + delta) is bounded by W. *)
(* Let's simplify the names a bit. *)
Let t2 := t1 + delta.
Let n_k := max_jobs task_cost task_period tsk R_tsk delta.
Let workload_bound := W task_cost task_period tsk R_tsk delta.
(* Since we only care about the workload of tsk, we restrict
our view to the set of jobs of tsk scheduled in t1, t2). *)
Let scheduled_jobs :=
jobs_of_task_scheduled_between job_task sched tsk t1 t2.
(* Now, let's consider the list of interfering jobs sorted by arrival time. *)
Let earlier_arrival := fun x y ⇒ job_arrival x ≤ job_arrival y.
Let sorted_jobs := sort earlier_arrival scheduled_jobs.
(* The first step consists in simplifying the sum corresponding
to the workload. *)
Section SimplifyJobSequence.
(* After switching to the definition of workload based on a list
of jobs, we show that sorting the list preserves the sum. *)
Lemma workload_bound_simpl_by_sorting_scheduled_jobs :
workload_joblist job_task sched tsk t1 t2 =
\sum_(i <- sorted_jobs) service_during sched i t1 t2.
(* Remember that both sequences have the same set of elements *)
Lemma workload_bound_job_in_same_sequence :
∀ j,
(j \in scheduled_jobs) = (j \in sorted_jobs).
(* Remember that all jobs in the sorted sequence is an
interfering job of task tsk. *)
Lemma workload_bound_all_jobs_from_tsk :
∀ j_i,
j_i \in sorted_jobs →
arrives_in arr_seq j_i ∧
job_task j_i = tsk ∧
service_during sched j_i t1 t2 != 0 ∧
j_i \in jobs_scheduled_between sched t1 t2.
(* Remember that consecutive jobs are ordered by arrival. *)
Lemma workload_bound_jobs_ordered_by_arrival :
∀ i elem,
i < (size sorted_jobs).-1 →
earlier_arrival (nth elem sorted_jobs i) (nth elem sorted_jobs i.+1).
End SimplifyJobSequence.
(* Next, we show that if the number of jobs is no larger than n_k,
the workload bound trivially holds. *)
Section WorkloadNotManyJobs.
Lemma workload_bound_holds_for_at_most_n_k_jobs :
size sorted_jobs ≤ n_k →
\sum_(i <- sorted_jobs) service_during sched i t1 t2 ≤
workload_bound.
End WorkloadNotManyJobs.
(* Otherwise, assume that the number of jobs is larger than n_k >= 0.
First, consider the simple case with only one job. *)
Section WorkloadSingleJob.
(* Assume that there's at least one job in the sorted list. *)
Hypothesis H_at_least_one_job: size sorted_jobs > 0.
Variable elem: Job.
Let j_fst := nth elem sorted_jobs 0.
(* The first job is an interfering job of task tsk. *)
Lemma workload_bound_j_fst_is_job_of_tsk :
arrives_in arr_seq j_fst ∧
job_task j_fst = tsk ∧
service_during sched j_fst t1 t2 != 0 ∧
j_fst \in jobs_scheduled_between sched t1 t2.
(* The workload bound holds for the single job. *)
Lemma workload_bound_holds_for_a_single_job :
\sum_(0 ≤ i < 1) service_during sched (nth elem sorted_jobs i) t1 t2 ≤
workload_bound.
End WorkloadSingleJob.
(* Next, consider the last case where there are at least two jobs:
the first job j_fst, and the last job j_lst. *)
Section WorkloadTwoOrMoreJobs.
(* There are at least two jobs. *)
Variable num_mid_jobs: nat.
Hypothesis H_at_least_two_jobs : size sorted_jobs = num_mid_jobs.+2.
Variable elem: Job.
Let j_fst := nth elem sorted_jobs 0.
Let j_lst := nth elem sorted_jobs num_mid_jobs.+1.
(* The last job is an interfering job of task tsk. *)
Lemma workload_bound_j_lst_is_job_of_tsk :
arrives_in arr_seq j_lst ∧
job_task j_lst = tsk ∧
service_during sched j_lst t1 t2 != 0 ∧
j_lst \in jobs_scheduled_between sched t1 t2.
(* The response time of the first job must fall inside the interval. *)
Lemma workload_bound_response_time_of_first_job_inside_interval :
t1 ≤ job_arrival j_fst + R_tsk.
(* The arrival of the last job must also fall inside the interval. *)
Lemma workload_bound_last_job_arrives_before_end_of_interval :
job_arrival j_lst < t2.
(* Next, we upper-bound the service of the first and last jobs using their arrival times. *)
Lemma workload_bound_service_of_first_and_last_jobs :
service_during sched j_fst t1 t2 +
service_during sched j_lst t1 t2 ≤
(job_arrival j_fst + R_tsk - t1) + (t2 - job_arrival j_lst).
(* Simplify the expression from the previous lemma. *)
Lemma workload_bound_simpl_expression_with_first_and_last :
job_arrival j_fst + R_tsk - t1 + (t2 - job_arrival j_lst) =
delta + R_tsk - (job_arrival j_lst - job_arrival j_fst).
(* Bound the service of the middle jobs. *)
Lemma workload_bound_service_of_middle_jobs :
\sum_(0 ≤ i < num_mid_jobs)
service_during sched (nth elem sorted_jobs i.+1) t1 t2 ≤
num_mid_jobs × task_cost tsk.
(* Conclude that the distance between first and last is at least num_mid_jobs + 1 periods. *)
Lemma workload_bound_many_periods_in_between :
job_arrival j_lst - job_arrival j_fst ≥ num_mid_jobs.+1 × (task_period tsk).
(* Prove that n_k is at least the number of the middle jobs *)
Lemma workload_bound_n_k_covers_middle_jobs :
n_k ≥ num_mid_jobs.
(* If n_k = num_mid_jobs, then the workload bound holds. *)
Lemma workload_bound_n_k_equals_num_mid_jobs :
num_mid_jobs = n_k →
service_during sched j_lst t1 t2 +
service_during sched j_fst t1 t2 +
\sum_(0 ≤ i < num_mid_jobs)
service_during sched (nth elem sorted_jobs i.+1) t1 t2
≤ workload_bound.
(* If n_k = num_mid_jobs + 1, then the workload bound holds. *)
Lemma workload_bound_n_k_equals_num_mid_jobs_plus_1 :
num_mid_jobs.+1 = n_k →
service_during sched j_lst t1 t2 +
service_during sched j_fst t1 t2 +
\sum_(0 ≤ i < num_mid_jobs)
service_during sched (nth elem sorted_jobs i.+1) t1 t2
≤ workload_bound.
End WorkloadTwoOrMoreJobs.
(* Using the lemmas above, we prove the main theorem about the workload bound. *)
Theorem workload_bounded_by_W :
workload_of tsk t1 (t1 + delta) ≤ workload_bound.
End MainProof.
End ProofWorkloadBound.
End WorkloadBound.
Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.task_arrival.
Require Import rt.model.schedule.global.response_time rt.model.schedule.global.schedulability
rt.model.schedule.global.workload.
Require Import rt.model.schedule.global.basic.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.
Module WorkloadBound.
Import Job SporadicTaskset Schedule ScheduleOfSporadicTask TaskArrival ResponseTime Schedulability Workload.
Section WorkloadBoundDef.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
(* Consider any task tsk with response-time bound R_tsk,
that is scheduled in an interval of length delta. *)
Variable tsk: sporadic_task.
Variable R_tsk: time.
Variable delta: time.
(* Based on the number of jobs that execute completely in the interval, ... *)
Definition max_jobs :=
div_floor (delta + R_tsk - task_cost tsk) (task_period tsk).
(* ... Bertogna and Cirinei's workload bound is defined as follows. *)
Definition W :=
let e_k := (task_cost tsk) in
let p_k := (task_period tsk) in
minn e_k (delta + R_tsk - e_k - max_jobs × p_k) + max_jobs × e_k.
End WorkloadBoundDef.
Section BasicLemmas.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
(* Let tsk be any task...*)
Variable tsk: sporadic_task.
(* ... with period > 0. *)
Hypothesis H_period_positive: task_period tsk > 0.
(* Let R1 <= R2 be two response-time bounds that
are larger than the cost of the tsk. *)
Variable R1 R2: time.
Hypothesis H_R_lower_bound: R1 ≥ task_cost tsk.
Hypothesis H_R1_le_R2: R1 ≤ R2.
Let workload_bound := W task_cost task_period tsk.
(* Then, Bertogna and Cirinei's workload bound is monotonically increasing. *)
Lemma W_monotonic :
∀ t1 t2,
t1 ≤ t2 →
workload_bound R1 t1 ≤ workload_bound R2 t2.
End BasicLemmas.
Section ProofWorkloadBound.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → sporadic_task.
Variable job_deadline: Job → time.
Variable arr_seq: arrival_sequence Job.
(* Assume that all jobs have valid parameters *)
Hypothesis H_jobs_have_valid_parameters :
∀ j,
arrives_in arr_seq j →
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
(* Consider any schedule. *)
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
(* Assumption: jobs only execute if they arrived.
This is used to eliminate jobs that arrive after end of the interval t1 + delta. *)
Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute job_arrival sched.
(* Assumption: jobs do not execute after they completed.
This is used to eliminate jobs that complete before the start of the interval t1. *)
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
(* Assumption: Jobs are sequential.
This is required to use interval lengths as a measure of service. *)
Hypothesis H_sequential_jobs: sequential_jobs sched.
(* Assumption: sporadic task model.
This is necessary to conclude that consecutive jobs ordered by arrival times
are separated by at least 'period' times units. *)
Hypothesis H_sporadic_tasks: sporadic_task_model task_period job_arrival job_task arr_seq.
(* Before starting the proof, let's give simpler names to the definitions. *)
Let job_has_completed_by := completed job_cost sched.
Let workload_of (tsk: sporadic_task) (t1 t2: time) := workload job_task sched tsk t1 t2.
(* Now we define the theorem. Let tsk be any task in the taskset. *)
Variable tsk: sporadic_task.
(* Assumption: the task must have valid parameters:
a) period > 0 (used in divisions)
b) deadline of the jobs = deadline of the task
c) cost <= period
(used to prove that the distance between the first and last
jobs is at least (cost + n*period), where n is the number
of middle jobs. If cost >> period, the claim does not hold
for every task set. *)
Hypothesis H_valid_task_parameters:
is_valid_sporadic_task task_cost task_period task_deadline tsk.
(* Assumption: the task must have a constrained deadline.
This is required to prove that n_k (max_jobs) from Bertogna
and Cirinei's formula accounts for at least the number of
middle jobs (i.e., number of jobs - 2 in the worst case). *)
Hypothesis H_constrained_deadline: task_deadline tsk ≤ task_period tsk.
(* Consider an interval t1, t1 + delta). *)
Variable t1 delta: time.
(* Assume that a response-time bound R_tsk for that task in any
schedule of this processor platform is also given, ... *)
Variable R_tsk: time.
Hypothesis H_response_time_bound :
∀ j,
arrives_in arr_seq j →
job_task j = tsk →
job_arrival j + R_tsk < t1 + delta →
job_has_completed_by j (job_arrival j + R_tsk).
(* ... such that R_tsk >= task_cost tsk and R_tsk <= task_deadline tsk. *)
Hypothesis H_response_time_ge_cost: R_tsk ≥ task_cost tsk.
Hypothesis H_no_deadline_miss: R_tsk ≤ task_deadline tsk.
Section MainProof.
(* In this section, we prove that the workload of a task in the
interval t1, t1 + delta) is bounded by W. *)
(* Let's simplify the names a bit. *)
Let t2 := t1 + delta.
Let n_k := max_jobs task_cost task_period tsk R_tsk delta.
Let workload_bound := W task_cost task_period tsk R_tsk delta.
(* Since we only care about the workload of tsk, we restrict
our view to the set of jobs of tsk scheduled in t1, t2). *)
Let scheduled_jobs :=
jobs_of_task_scheduled_between job_task sched tsk t1 t2.
(* Now, let's consider the list of interfering jobs sorted by arrival time. *)
Let earlier_arrival := fun x y ⇒ job_arrival x ≤ job_arrival y.
Let sorted_jobs := sort earlier_arrival scheduled_jobs.
(* The first step consists in simplifying the sum corresponding
to the workload. *)
Section SimplifyJobSequence.
(* After switching to the definition of workload based on a list
of jobs, we show that sorting the list preserves the sum. *)
Lemma workload_bound_simpl_by_sorting_scheduled_jobs :
workload_joblist job_task sched tsk t1 t2 =
\sum_(i <- sorted_jobs) service_during sched i t1 t2.
(* Remember that both sequences have the same set of elements *)
Lemma workload_bound_job_in_same_sequence :
∀ j,
(j \in scheduled_jobs) = (j \in sorted_jobs).
(* Remember that all jobs in the sorted sequence is an
interfering job of task tsk. *)
Lemma workload_bound_all_jobs_from_tsk :
∀ j_i,
j_i \in sorted_jobs →
arrives_in arr_seq j_i ∧
job_task j_i = tsk ∧
service_during sched j_i t1 t2 != 0 ∧
j_i \in jobs_scheduled_between sched t1 t2.
(* Remember that consecutive jobs are ordered by arrival. *)
Lemma workload_bound_jobs_ordered_by_arrival :
∀ i elem,
i < (size sorted_jobs).-1 →
earlier_arrival (nth elem sorted_jobs i) (nth elem sorted_jobs i.+1).
End SimplifyJobSequence.
(* Next, we show that if the number of jobs is no larger than n_k,
the workload bound trivially holds. *)
Section WorkloadNotManyJobs.
Lemma workload_bound_holds_for_at_most_n_k_jobs :
size sorted_jobs ≤ n_k →
\sum_(i <- sorted_jobs) service_during sched i t1 t2 ≤
workload_bound.
End WorkloadNotManyJobs.
(* Otherwise, assume that the number of jobs is larger than n_k >= 0.
First, consider the simple case with only one job. *)
Section WorkloadSingleJob.
(* Assume that there's at least one job in the sorted list. *)
Hypothesis H_at_least_one_job: size sorted_jobs > 0.
Variable elem: Job.
Let j_fst := nth elem sorted_jobs 0.
(* The first job is an interfering job of task tsk. *)
Lemma workload_bound_j_fst_is_job_of_tsk :
arrives_in arr_seq j_fst ∧
job_task j_fst = tsk ∧
service_during sched j_fst t1 t2 != 0 ∧
j_fst \in jobs_scheduled_between sched t1 t2.
(* The workload bound holds for the single job. *)
Lemma workload_bound_holds_for_a_single_job :
\sum_(0 ≤ i < 1) service_during sched (nth elem sorted_jobs i) t1 t2 ≤
workload_bound.
End WorkloadSingleJob.
(* Next, consider the last case where there are at least two jobs:
the first job j_fst, and the last job j_lst. *)
Section WorkloadTwoOrMoreJobs.
(* There are at least two jobs. *)
Variable num_mid_jobs: nat.
Hypothesis H_at_least_two_jobs : size sorted_jobs = num_mid_jobs.+2.
Variable elem: Job.
Let j_fst := nth elem sorted_jobs 0.
Let j_lst := nth elem sorted_jobs num_mid_jobs.+1.
(* The last job is an interfering job of task tsk. *)
Lemma workload_bound_j_lst_is_job_of_tsk :
arrives_in arr_seq j_lst ∧
job_task j_lst = tsk ∧
service_during sched j_lst t1 t2 != 0 ∧
j_lst \in jobs_scheduled_between sched t1 t2.
(* The response time of the first job must fall inside the interval. *)
Lemma workload_bound_response_time_of_first_job_inside_interval :
t1 ≤ job_arrival j_fst + R_tsk.
(* The arrival of the last job must also fall inside the interval. *)
Lemma workload_bound_last_job_arrives_before_end_of_interval :
job_arrival j_lst < t2.
(* Next, we upper-bound the service of the first and last jobs using their arrival times. *)
Lemma workload_bound_service_of_first_and_last_jobs :
service_during sched j_fst t1 t2 +
service_during sched j_lst t1 t2 ≤
(job_arrival j_fst + R_tsk - t1) + (t2 - job_arrival j_lst).
(* Simplify the expression from the previous lemma. *)
Lemma workload_bound_simpl_expression_with_first_and_last :
job_arrival j_fst + R_tsk - t1 + (t2 - job_arrival j_lst) =
delta + R_tsk - (job_arrival j_lst - job_arrival j_fst).
(* Bound the service of the middle jobs. *)
Lemma workload_bound_service_of_middle_jobs :
\sum_(0 ≤ i < num_mid_jobs)
service_during sched (nth elem sorted_jobs i.+1) t1 t2 ≤
num_mid_jobs × task_cost tsk.
(* Conclude that the distance between first and last is at least num_mid_jobs + 1 periods. *)
Lemma workload_bound_many_periods_in_between :
job_arrival j_lst - job_arrival j_fst ≥ num_mid_jobs.+1 × (task_period tsk).
(* Prove that n_k is at least the number of the middle jobs *)
Lemma workload_bound_n_k_covers_middle_jobs :
n_k ≥ num_mid_jobs.
(* If n_k = num_mid_jobs, then the workload bound holds. *)
Lemma workload_bound_n_k_equals_num_mid_jobs :
num_mid_jobs = n_k →
service_during sched j_lst t1 t2 +
service_during sched j_fst t1 t2 +
\sum_(0 ≤ i < num_mid_jobs)
service_during sched (nth elem sorted_jobs i.+1) t1 t2
≤ workload_bound.
(* If n_k = num_mid_jobs + 1, then the workload bound holds. *)
Lemma workload_bound_n_k_equals_num_mid_jobs_plus_1 :
num_mid_jobs.+1 = n_k →
service_during sched j_lst t1 t2 +
service_during sched j_fst t1 t2 +
\sum_(0 ≤ i < num_mid_jobs)
service_during sched (nth elem sorted_jobs i.+1) t1 t2
≤ workload_bound.
End WorkloadTwoOrMoreJobs.
(* Using the lemmas above, we prove the main theorem about the workload bound. *)
Theorem workload_bounded_by_W :
workload_of tsk t1 (t1 + delta) ≤ workload_bound.
End MainProof.
End ProofWorkloadBound.
End WorkloadBound.