Library prosa.classic.analysis.global.parallel.bertogna_edf_comp
Require Import prosa.classic.util.all.
Require Import prosa.classic.analysis.global.parallel.bertogna_edf_theory.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeIterationEDF.
Import ResponseTimeAnalysisEDF.
Section Analysis.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Let task_with_response_time := (sporadic_task × time)%type.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → sporadic_task.
Variable num_cpus: nat.
Let I (rt_bounds: seq task_with_response_time)
(tsk: sporadic_task) (delta: time) :=
total_interference_bound_edf task_cost task_period task_deadline tsk rt_bounds delta.
Definition edf_response_time_bound (rt_bounds: seq task_with_response_time)
(tsk: sporadic_task) (delta: time) :=
task_cost tsk + div_floor (I rt_bounds tsk delta) num_cpus.
Definition R_le_deadline (pair: task_with_response_time) :=
let (tsk, R) := pair in
R ≤ task_deadline tsk.
Definition update_bound (rt_bounds: seq task_with_response_time)
(pair : task_with_response_time) :=
let (tsk, R) := pair in
(tsk, edf_response_time_bound rt_bounds tsk R).
Let initial_state (ts: seq sporadic_task) :=
map (fun t ⇒ (t, task_cost t)) ts.
Definition edf_rta_iteration (rt_bounds: seq task_with_response_time) :=
map (update_bound rt_bounds) rt_bounds.
Let max_steps (ts: seq sporadic_task) :=
\sum_(tsk <- ts) (task_deadline tsk - task_cost tsk) + 1.
Definition edf_claimed_bounds (ts: seq sporadic_task) :=
let R_values := iter (max_steps ts) edf_rta_iteration (initial_state ts) in
if (all R_le_deadline R_values) then
Some R_values
else None.
Definition edf_schedulable (ts: seq sporadic_task) :=
edf_claimed_bounds ts != None.
Section SimpleLemmas.
Lemma edf_claimed_bounds_unzip1_update_bound :
∀ l rt_bounds,
unzip1 (map (update_bound rt_bounds) l) = unzip1 l.
Lemma edf_claimed_bounds_unzip1_iteration :
∀ l k,
unzip1 (iter k edf_rta_iteration (initial_state l)) = l.
Lemma edf_claimed_bounds_size :
∀ l k,
size (iter k edf_rta_iteration (initial_state l)) = size l.
Lemma edf_claimed_bounds_ge_cost :
∀ l k tsk R,
(tsk, R) \in (iter k edf_rta_iteration (initial_state l)) →
R ≥ task_cost tsk.
Lemma edf_claimed_bounds_le_deadline :
∀ ts rt_bounds tsk R,
edf_claimed_bounds ts = Some rt_bounds →
(tsk, R) \in rt_bounds →
R ≤ task_deadline tsk.
Lemma edf_claimed_bounds_has_R_for_every_task :
∀ ts rt_bounds tsk,
edf_claimed_bounds ts = Some rt_bounds →
tsk \in ts →
∃ R,
(tsk, R) \in rt_bounds.
End SimpleLemmas.
Section Convergence.
Variable ts: seq sporadic_task.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Let f (k: nat) := iter k edf_rta_iteration (initial_state ts).
Let all_le := fun (l1 l2: list task_with_response_time) ⇒
(unzip1 l1 == unzip1 l2) &&
all (fun p ⇒ (snd (fst p)) ≤ (snd (snd p))) (zip l1 l2).
Let one_lt := fun (l1 l2: list task_with_response_time) ⇒
(unzip1 l1 == unzip1 l2) &&
has (fun p ⇒ (snd (fst p)) < (snd (snd p))) (zip l1 l2).
Section RelationProperties.
Lemma all_le_reflexive : reflexive all_le.
Lemma all_le_transitive: transitive all_le.
Lemma bertogna_edf_comp_iteration_preserves_minimum :
∀ step, all_le (initial_state ts) (f step).
Lemma bertogna_edf_comp_iteration_inductive (P : seq task_with_response_time → Type) :
P (initial_state ts) →
(∀ k, P (f k) → P (f (k.+1))) →
P (f (max_steps ts)).
Lemma bertogna_edf_comp_iteration_preserves_order :
∀ l1 l2,
all_le (initial_state ts) l1 →
all_le l1 l2 →
all_le (edf_rta_iteration l1) (edf_rta_iteration l2).
Lemma bertogna_edf_comp_iteration_monotonic: ∀ k, all_le (f k) (f k.+1).
End RelationProperties.
Lemma bertogna_edf_comp_f_converges_with_no_tasks :
size ts = 0 →
f (max_steps ts) = f (max_steps ts).+1.
Lemma bertogna_edf_comp_f_converges_early :
(∃ k, k ≤ max_steps ts ∧ f k = f k.+1) →
f (max_steps ts) = f (max_steps ts).+1.
Section DerivingContradiction.
Hypothesis H_at_least_one_task: size ts > 0.
Hypothesis H_keeps_diverging:
∀ k,
k ≤ max_steps ts → f k != f k.+1.
Lemma bertogna_edf_comp_f_increases :
∀ k,
k ≤ max_steps ts → one_lt (f k) (f k.+1).
Lemma bertogna_edf_comp_rt_grows_too_much :
∀ k,
k ≤ max_steps ts →
\sum_((tsk, R) <- f k) (R - task_cost tsk) + 1 > k.
End DerivingContradiction.
Lemma edf_claimed_bounds_finds_fixed_point_of_list :
∀ rt_bounds,
edf_claimed_bounds ts = Some rt_bounds →
valid_sporadic_taskset task_cost task_period task_deadline ts →
f (max_steps ts) = edf_rta_iteration (f (max_steps ts)).
Lemma edf_claimed_bounds_finds_least_fixed_point :
∀ v,
all_le (initial_state ts) v →
v = edf_rta_iteration v →
all_le (f (max_steps ts)) v.
Theorem edf_claimed_bounds_finds_fixed_point_for_each_bound :
∀ tsk R rt_bounds,
edf_claimed_bounds ts = Some rt_bounds →
(tsk, R) \in rt_bounds →
R = edf_response_time_bound rt_bounds tsk R.
End Convergence.
Section MainProof.
Variable ts: taskset_of sporadic_task.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Hypothesis H_constrained_deadlines:
∀ tsk, tsk \in ts → task_deadline tsk ≤ task_period tsk.
Context {arr_seq: arrival_sequence Job}.
Hypothesis H_all_jobs_from_taskset:
∀ j, arrives_in arr_seq j → job_task j \in ts.
Hypothesis H_valid_job_parameters:
∀ j,
arrives_in arr_seq j →
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period job_arrival job_task arr_seq.
Variable sched: schedule Job num_cpus.
Hypothesis H_at_least_one_cpu: num_cpus > 0.
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_work_conserving: work_conserving job_arrival job_cost arr_seq sched.
Hypothesis H_edf_policy: respects_JLFP_policy job_arrival job_cost arr_seq sched
(EDF job_arrival job_deadline).
Definition no_deadline_missed_by_task (tsk: sporadic_task) :=
task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched tsk.
Definition no_deadline_missed_by_job :=
job_misses_no_deadline job_arrival job_cost job_deadline sched.
Let response_time_bounded_by (tsk: sporadic_task) :=
is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched tsk.
Theorem edf_analysis_yields_response_time_bounds :
∀ tsk R,
(tsk, R) \In edf_claimed_bounds ts →
response_time_bounded_by tsk R.
Hypothesis H_test_succeeds: edf_schedulable ts.
Theorem taskset_schedulable_by_edf_rta :
∀ tsk, tsk \in ts → no_deadline_missed_by_task tsk.
Theorem jobs_schedulable_by_edf_rta :
∀ j, arrives_in arr_seq j → no_deadline_missed_by_job j.
End MainProof.
End Analysis.
End ResponseTimeIterationEDF.
Require Import prosa.classic.analysis.global.parallel.bertogna_edf_theory.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeIterationEDF.
Import ResponseTimeAnalysisEDF.
Section Analysis.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Let task_with_response_time := (sporadic_task × time)%type.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → sporadic_task.
Variable num_cpus: nat.
Let I (rt_bounds: seq task_with_response_time)
(tsk: sporadic_task) (delta: time) :=
total_interference_bound_edf task_cost task_period task_deadline tsk rt_bounds delta.
Definition edf_response_time_bound (rt_bounds: seq task_with_response_time)
(tsk: sporadic_task) (delta: time) :=
task_cost tsk + div_floor (I rt_bounds tsk delta) num_cpus.
Definition R_le_deadline (pair: task_with_response_time) :=
let (tsk, R) := pair in
R ≤ task_deadline tsk.
Definition update_bound (rt_bounds: seq task_with_response_time)
(pair : task_with_response_time) :=
let (tsk, R) := pair in
(tsk, edf_response_time_bound rt_bounds tsk R).
Let initial_state (ts: seq sporadic_task) :=
map (fun t ⇒ (t, task_cost t)) ts.
Definition edf_rta_iteration (rt_bounds: seq task_with_response_time) :=
map (update_bound rt_bounds) rt_bounds.
Let max_steps (ts: seq sporadic_task) :=
\sum_(tsk <- ts) (task_deadline tsk - task_cost tsk) + 1.
Definition edf_claimed_bounds (ts: seq sporadic_task) :=
let R_values := iter (max_steps ts) edf_rta_iteration (initial_state ts) in
if (all R_le_deadline R_values) then
Some R_values
else None.
Definition edf_schedulable (ts: seq sporadic_task) :=
edf_claimed_bounds ts != None.
Section SimpleLemmas.
Lemma edf_claimed_bounds_unzip1_update_bound :
∀ l rt_bounds,
unzip1 (map (update_bound rt_bounds) l) = unzip1 l.
Lemma edf_claimed_bounds_unzip1_iteration :
∀ l k,
unzip1 (iter k edf_rta_iteration (initial_state l)) = l.
Lemma edf_claimed_bounds_size :
∀ l k,
size (iter k edf_rta_iteration (initial_state l)) = size l.
Lemma edf_claimed_bounds_ge_cost :
∀ l k tsk R,
(tsk, R) \in (iter k edf_rta_iteration (initial_state l)) →
R ≥ task_cost tsk.
Lemma edf_claimed_bounds_le_deadline :
∀ ts rt_bounds tsk R,
edf_claimed_bounds ts = Some rt_bounds →
(tsk, R) \in rt_bounds →
R ≤ task_deadline tsk.
Lemma edf_claimed_bounds_has_R_for_every_task :
∀ ts rt_bounds tsk,
edf_claimed_bounds ts = Some rt_bounds →
tsk \in ts →
∃ R,
(tsk, R) \in rt_bounds.
End SimpleLemmas.
Section Convergence.
Variable ts: seq sporadic_task.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Let f (k: nat) := iter k edf_rta_iteration (initial_state ts).
Let all_le := fun (l1 l2: list task_with_response_time) ⇒
(unzip1 l1 == unzip1 l2) &&
all (fun p ⇒ (snd (fst p)) ≤ (snd (snd p))) (zip l1 l2).
Let one_lt := fun (l1 l2: list task_with_response_time) ⇒
(unzip1 l1 == unzip1 l2) &&
has (fun p ⇒ (snd (fst p)) < (snd (snd p))) (zip l1 l2).
Section RelationProperties.
Lemma all_le_reflexive : reflexive all_le.
Lemma all_le_transitive: transitive all_le.
Lemma bertogna_edf_comp_iteration_preserves_minimum :
∀ step, all_le (initial_state ts) (f step).
Lemma bertogna_edf_comp_iteration_inductive (P : seq task_with_response_time → Type) :
P (initial_state ts) →
(∀ k, P (f k) → P (f (k.+1))) →
P (f (max_steps ts)).
Lemma bertogna_edf_comp_iteration_preserves_order :
∀ l1 l2,
all_le (initial_state ts) l1 →
all_le l1 l2 →
all_le (edf_rta_iteration l1) (edf_rta_iteration l2).
Lemma bertogna_edf_comp_iteration_monotonic: ∀ k, all_le (f k) (f k.+1).
End RelationProperties.
Lemma bertogna_edf_comp_f_converges_with_no_tasks :
size ts = 0 →
f (max_steps ts) = f (max_steps ts).+1.
Lemma bertogna_edf_comp_f_converges_early :
(∃ k, k ≤ max_steps ts ∧ f k = f k.+1) →
f (max_steps ts) = f (max_steps ts).+1.
Section DerivingContradiction.
Hypothesis H_at_least_one_task: size ts > 0.
Hypothesis H_keeps_diverging:
∀ k,
k ≤ max_steps ts → f k != f k.+1.
Lemma bertogna_edf_comp_f_increases :
∀ k,
k ≤ max_steps ts → one_lt (f k) (f k.+1).
Lemma bertogna_edf_comp_rt_grows_too_much :
∀ k,
k ≤ max_steps ts →
\sum_((tsk, R) <- f k) (R - task_cost tsk) + 1 > k.
End DerivingContradiction.
Lemma edf_claimed_bounds_finds_fixed_point_of_list :
∀ rt_bounds,
edf_claimed_bounds ts = Some rt_bounds →
valid_sporadic_taskset task_cost task_period task_deadline ts →
f (max_steps ts) = edf_rta_iteration (f (max_steps ts)).
Lemma edf_claimed_bounds_finds_least_fixed_point :
∀ v,
all_le (initial_state ts) v →
v = edf_rta_iteration v →
all_le (f (max_steps ts)) v.
Theorem edf_claimed_bounds_finds_fixed_point_for_each_bound :
∀ tsk R rt_bounds,
edf_claimed_bounds ts = Some rt_bounds →
(tsk, R) \in rt_bounds →
R = edf_response_time_bound rt_bounds tsk R.
End Convergence.
Section MainProof.
Variable ts: taskset_of sporadic_task.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Hypothesis H_constrained_deadlines:
∀ tsk, tsk \in ts → task_deadline tsk ≤ task_period tsk.
Context {arr_seq: arrival_sequence Job}.
Hypothesis H_all_jobs_from_taskset:
∀ j, arrives_in arr_seq j → job_task j \in ts.
Hypothesis H_valid_job_parameters:
∀ j,
arrives_in arr_seq j →
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period job_arrival job_task arr_seq.
Variable sched: schedule Job num_cpus.
Hypothesis H_at_least_one_cpu: num_cpus > 0.
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_work_conserving: work_conserving job_arrival job_cost arr_seq sched.
Hypothesis H_edf_policy: respects_JLFP_policy job_arrival job_cost arr_seq sched
(EDF job_arrival job_deadline).
Definition no_deadline_missed_by_task (tsk: sporadic_task) :=
task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched tsk.
Definition no_deadline_missed_by_job :=
job_misses_no_deadline job_arrival job_cost job_deadline sched.
Let response_time_bounded_by (tsk: sporadic_task) :=
is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched tsk.
Theorem edf_analysis_yields_response_time_bounds :
∀ tsk R,
(tsk, R) \In edf_claimed_bounds ts →
response_time_bounded_by tsk R.
Hypothesis H_test_succeeds: edf_schedulable ts.
Theorem taskset_schedulable_by_edf_rta :
∀ tsk, tsk \in ts → no_deadline_missed_by_task tsk.
Theorem jobs_schedulable_by_edf_rta :
∀ j, arrives_in arr_seq j → no_deadline_missed_by_job j.
End MainProof.
End Analysis.
End ResponseTimeIterationEDF.