Library prosa.classic.analysis.global.basic.workload_bound
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.schedule.global.workload prosa.classic.model.schedule.global.response_time
prosa.classic.model.schedule.global.schedulability.
Require Import prosa.classic.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.
Variable tsk: sporadic_task.
Variable R_tsk: time.
Variable delta: time.
Definition max_jobs :=
div_floor (delta + R_tsk - task_cost tsk) (task_period tsk).
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.
Variable tsk: sporadic_task.
Hypothesis H_period_positive: task_period tsk > 0.
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.
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.
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.
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.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_sequential_jobs: sequential_jobs sched.
Hypothesis H_sporadic_tasks: sporadic_task_model task_period job_arrival job_task arr_seq.
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.
Variable tsk: sporadic_task.
Hypothesis H_valid_task_parameters:
is_valid_sporadic_task task_cost task_period task_deadline tsk.
Hypothesis H_constrained_deadline: task_deadline tsk ≤ task_period tsk.
Variable t1 delta: time.
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).
Hypothesis H_response_time_ge_cost: R_tsk ≥ task_cost tsk.
Hypothesis H_no_deadline_miss: R_tsk ≤ task_deadline tsk.
Section MainProof.
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.
Let scheduled_jobs :=
jobs_of_task_scheduled_between job_task sched tsk t1 t2.
Let earlier_arrival := fun x y ⇒ job_arrival x ≤ job_arrival y.
Let sorted_jobs := sort earlier_arrival scheduled_jobs.
Section SimplifyJobSequence.
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.
Lemma workload_bound_job_in_same_sequence :
∀ j,
(j \in scheduled_jobs) = (j \in sorted_jobs).
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.
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.
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.
Section WorkloadSingleJob.
Hypothesis H_at_least_one_job: size sorted_jobs > 0.
Variable elem: Job.
Let j_fst := nth elem sorted_jobs 0.
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.
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.
Section WorkloadTwoOrMoreJobs.
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.
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.
Lemma workload_bound_response_time_of_first_job_inside_interval :
t1 ≤ job_arrival j_fst + R_tsk.
Lemma workload_bound_last_job_arrives_before_end_of_interval :
job_arrival j_lst < t2.
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).
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).
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.
Lemma workload_bound_many_periods_in_between :
job_arrival j_lst - job_arrival j_fst ≥ num_mid_jobs.+1 × (task_period tsk).
Lemma workload_bound_n_k_covers_middle_jobs :
n_k ≥ num_mid_jobs.
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.
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.
Theorem workload_bounded_by_W :
workload_of tsk t1 (t1 + delta) ≤ workload_bound.
End MainProof.
End ProofWorkloadBound.
End WorkloadBound.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.schedule.global.workload prosa.classic.model.schedule.global.response_time
prosa.classic.model.schedule.global.schedulability.
Require Import prosa.classic.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.
Variable tsk: sporadic_task.
Variable R_tsk: time.
Variable delta: time.
Definition max_jobs :=
div_floor (delta + R_tsk - task_cost tsk) (task_period tsk).
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.
Variable tsk: sporadic_task.
Hypothesis H_period_positive: task_period tsk > 0.
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.
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.
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.
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.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_sequential_jobs: sequential_jobs sched.
Hypothesis H_sporadic_tasks: sporadic_task_model task_period job_arrival job_task arr_seq.
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.
Variable tsk: sporadic_task.
Hypothesis H_valid_task_parameters:
is_valid_sporadic_task task_cost task_period task_deadline tsk.
Hypothesis H_constrained_deadline: task_deadline tsk ≤ task_period tsk.
Variable t1 delta: time.
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).
Hypothesis H_response_time_ge_cost: R_tsk ≥ task_cost tsk.
Hypothesis H_no_deadline_miss: R_tsk ≤ task_deadline tsk.
Section MainProof.
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.
Let scheduled_jobs :=
jobs_of_task_scheduled_between job_task sched tsk t1 t2.
Let earlier_arrival := fun x y ⇒ job_arrival x ≤ job_arrival y.
Let sorted_jobs := sort earlier_arrival scheduled_jobs.
Section SimplifyJobSequence.
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.
Lemma workload_bound_job_in_same_sequence :
∀ j,
(j \in scheduled_jobs) = (j \in sorted_jobs).
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.
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.
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.
Section WorkloadSingleJob.
Hypothesis H_at_least_one_job: size sorted_jobs > 0.
Variable elem: Job.
Let j_fst := nth elem sorted_jobs 0.
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.
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.
Section WorkloadTwoOrMoreJobs.
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.
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.
Lemma workload_bound_response_time_of_first_job_inside_interval :
t1 ≤ job_arrival j_fst + R_tsk.
Lemma workload_bound_last_job_arrives_before_end_of_interval :
job_arrival j_lst < t2.
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).
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).
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.
Lemma workload_bound_many_periods_in_between :
job_arrival j_lst - job_arrival j_fst ≥ num_mid_jobs.+1 × (task_period tsk).
Lemma workload_bound_n_k_covers_middle_jobs :
n_k ≥ num_mid_jobs.
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.
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.
Theorem workload_bounded_by_W :
workload_of tsk t1 (t1 + delta) ≤ workload_bound.
End MainProof.
End ProofWorkloadBound.
End WorkloadBound.