Library prosa.classic.analysis.apa.bertogna_fp_comp
Require Import prosa.classic.util.all.
Require Import prosa.classic.analysis.apa.bertogna_fp_theory.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeIterationFP.
Import ResponseTimeAnalysisFP.
Section Analysis.
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_deadline: Job → time.
Variable job_task: Job → sporadic_task.
Let task_with_response_time := (sporadic_task × time)%type.
Variable num_cpus: nat.
Variable higher_priority: FP_policy sporadic_task.
Variable alpha: task_affinity sporadic_task num_cpus.
Variable alpha': task_affinity sporadic_task num_cpus.
Definition per_task_rta (tsk: sporadic_task)
(R_prev: seq task_with_response_time) (step: nat) :=
iter step
(fun t ⇒ task_cost tsk +
div_floor
(total_interference_bound_fp task_cost task_period alpha tsk
(alpha' tsk) R_prev t higher_priority)
#|alpha' tsk|)
(task_cost tsk).
Definition max_steps (tsk: sporadic_task) := task_deadline tsk - task_cost tsk + 1.
Definition fp_bound_of_task hp_pairs tsk :=
if hp_pairs is Some rt_bounds then
let R := per_task_rta tsk rt_bounds (max_steps tsk) in
if R ≤ task_deadline tsk then
Some (rcons rt_bounds (tsk, R))
else None
else None.
Definition fp_claimed_bounds (ts: seq sporadic_task) :=
foldl fp_bound_of_task (Some [::]) ts.
Definition fp_schedulable (ts: seq sporadic_task) :=
fp_claimed_bounds ts != None.
Section SimpleLemmas.
Lemma fp_claimed_bounds_unzip :
∀ ts hp_bounds,
fp_claimed_bounds ts = Some hp_bounds →
unzip1 hp_bounds = ts.
Lemma fp_claimed_bounds_rcons :
∀ ts' hp_bounds tsk1 tsk2 R,
(fp_claimed_bounds (rcons ts' tsk1) = Some (rcons hp_bounds (tsk2, R)) →
(fp_claimed_bounds ts' = Some hp_bounds ∧
tsk1 = tsk2 ∧
R = per_task_rta tsk1 hp_bounds (max_steps tsk1) ∧
R ≤ task_deadline tsk1)).
Lemma fp_claimed_bounds_take :
∀ ts hp_bounds i,
fp_claimed_bounds ts = Some hp_bounds →
i ≤ size hp_bounds →
fp_claimed_bounds (take i ts) = Some (take i hp_bounds).
Lemma fp_claimed_bounds_le_deadline :
∀ ts' rt_bounds tsk R,
fp_claimed_bounds ts' = Some rt_bounds →
(tsk, R) \in rt_bounds →
R ≤ task_deadline tsk.
Lemma fp_claimed_bounds_ge_cost :
∀ ts' rt_bounds tsk R,
fp_claimed_bounds ts' = Some rt_bounds →
(tsk, R) \in rt_bounds →
R ≥ task_cost tsk.
Lemma per_task_rta_fold :
∀ tsk rt_bounds,
task_cost tsk +
div_floor (total_interference_bound_fp task_cost task_period alpha tsk (alpha' tsk) rt_bounds
(per_task_rta tsk rt_bounds (max_steps tsk)) higher_priority) #|alpha' tsk|
= per_task_rta tsk rt_bounds (max_steps tsk).+1.
End SimpleLemmas.
Section HighPriorityTasks.
Variable ts: taskset_of sporadic_task.
Hypothesis H_task_set_is_sorted: sorted higher_priority ts.
Hypothesis H_task_set_has_unique_priorities:
FP_is_antisymmetric_over_task_set higher_priority ts.
Hypothesis H_priority_transitive: FP_is_transitive higher_priority.
Variable hp_bounds: seq task_with_response_time.
Variable R: time.
Hypothesis H_analysis_succeeds: fp_claimed_bounds ts = Some hp_bounds.
Variable elem: sporadic_task.
Let TASK := nth elem ts.
Lemma fp_claimed_bounds_hp_tasks_have_smaller_index :
∀ hp_idx idx,
hp_idx < size ts →
idx < size ts →
hp_idx != idx →
higher_priority (TASK hp_idx) (TASK idx) →
hp_idx < idx.
End HighPriorityTasks.
Section Convergence.
Variable ts_hp: seq sporadic_task.
Variable rt_bounds: seq task_with_response_time.
Hypothesis H_test_succeeds: fp_claimed_bounds ts_hp = Some rt_bounds.
Variable tsk: sporadic_task.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline (rcons ts_hp tsk).
Let f := per_task_rta tsk rt_bounds.
Hypothesis H_no_larger_than_deadline: f (max_steps tsk) ≤ task_deadline tsk.
Lemma bertogna_fp_comp_f_monotonic :
∀ x1 x2, x1 ≤ x2 → f x1 ≤ f x2.
Lemma bertogna_fp_comp_f_converges_early :
(∃ k, k ≤ max_steps tsk ∧ f k = f k.+1) →
f (max_steps tsk) = f (max_steps tsk).+1.
Section DerivingContradiction.
Hypothesis H_keeps_diverging:
∀ k,
k ≤ max_steps tsk → f k != f k.+1.
Lemma bertogna_fp_comp_f_increases :
∀ k,
k ≤ max_steps tsk →
f k < f k.+1.
Lemma bertogna_fp_comp_rt_grows_too_much :
∀ k,
k ≤ max_steps tsk →
f k > k + task_cost tsk - 1.
End DerivingContradiction.
Lemma per_task_rta_converges:
f (max_steps tsk) = f (max_steps tsk).+1.
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.
Hypothesis H_non_empty_affinity:
∀ tsk, tsk \in ts → #|alpha' tsk| > 0.
Hypothesis H_subaffinity:
∀ tsk, tsk \in ts → is_subaffinity (alpha' tsk) (alpha tsk).
Hypothesis H_task_set_is_sorted: sorted higher_priority ts.
Hypothesis H_task_set_has_unique_priorities:
FP_is_antisymmetric_over_task_set higher_priority ts.
Hypothesis H_priority_is_total:
FP_is_total_over_task_set higher_priority ts.
Hypothesis H_priority_transitive: FP_is_transitive higher_priority.
Variable 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_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_respects_affinity: respects_affinity job_task sched alpha.
Hypothesis H_work_conserving: apa_work_conserving job_arrival job_cost job_task arr_seq
sched alpha.
Hypothesis H_respects_FP_policy:
respects_FP_policy_under_weak_APA job_arrival job_cost job_task arr_seq sched
alpha higher_priority.
Let no_deadline_missed_by_task (tsk: sporadic_task) :=
task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched tsk.
Let 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 fp_analysis_yields_response_time_bounds :
∀ tsk R,
(tsk, R) \In fp_claimed_bounds ts →
response_time_bounded_by tsk R.
Hypothesis H_test_succeeds: fp_schedulable ts.
Theorem taskset_schedulable_by_fp_rta :
∀ tsk, tsk \in ts → no_deadline_missed_by_task tsk.
Theorem jobs_schedulable_by_fp_rta :
∀ j, arrives_in arr_seq j → no_deadline_missed_by_job j.
End MainProof.
End Analysis.
End ResponseTimeIterationFP.
Require Import prosa.classic.analysis.apa.bertogna_fp_theory.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeIterationFP.
Import ResponseTimeAnalysisFP.
Section Analysis.
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_deadline: Job → time.
Variable job_task: Job → sporadic_task.
Let task_with_response_time := (sporadic_task × time)%type.
Variable num_cpus: nat.
Variable higher_priority: FP_policy sporadic_task.
Variable alpha: task_affinity sporadic_task num_cpus.
Variable alpha': task_affinity sporadic_task num_cpus.
Definition per_task_rta (tsk: sporadic_task)
(R_prev: seq task_with_response_time) (step: nat) :=
iter step
(fun t ⇒ task_cost tsk +
div_floor
(total_interference_bound_fp task_cost task_period alpha tsk
(alpha' tsk) R_prev t higher_priority)
#|alpha' tsk|)
(task_cost tsk).
Definition max_steps (tsk: sporadic_task) := task_deadline tsk - task_cost tsk + 1.
Definition fp_bound_of_task hp_pairs tsk :=
if hp_pairs is Some rt_bounds then
let R := per_task_rta tsk rt_bounds (max_steps tsk) in
if R ≤ task_deadline tsk then
Some (rcons rt_bounds (tsk, R))
else None
else None.
Definition fp_claimed_bounds (ts: seq sporadic_task) :=
foldl fp_bound_of_task (Some [::]) ts.
Definition fp_schedulable (ts: seq sporadic_task) :=
fp_claimed_bounds ts != None.
Section SimpleLemmas.
Lemma fp_claimed_bounds_unzip :
∀ ts hp_bounds,
fp_claimed_bounds ts = Some hp_bounds →
unzip1 hp_bounds = ts.
Lemma fp_claimed_bounds_rcons :
∀ ts' hp_bounds tsk1 tsk2 R,
(fp_claimed_bounds (rcons ts' tsk1) = Some (rcons hp_bounds (tsk2, R)) →
(fp_claimed_bounds ts' = Some hp_bounds ∧
tsk1 = tsk2 ∧
R = per_task_rta tsk1 hp_bounds (max_steps tsk1) ∧
R ≤ task_deadline tsk1)).
Lemma fp_claimed_bounds_take :
∀ ts hp_bounds i,
fp_claimed_bounds ts = Some hp_bounds →
i ≤ size hp_bounds →
fp_claimed_bounds (take i ts) = Some (take i hp_bounds).
Lemma fp_claimed_bounds_le_deadline :
∀ ts' rt_bounds tsk R,
fp_claimed_bounds ts' = Some rt_bounds →
(tsk, R) \in rt_bounds →
R ≤ task_deadline tsk.
Lemma fp_claimed_bounds_ge_cost :
∀ ts' rt_bounds tsk R,
fp_claimed_bounds ts' = Some rt_bounds →
(tsk, R) \in rt_bounds →
R ≥ task_cost tsk.
Lemma per_task_rta_fold :
∀ tsk rt_bounds,
task_cost tsk +
div_floor (total_interference_bound_fp task_cost task_period alpha tsk (alpha' tsk) rt_bounds
(per_task_rta tsk rt_bounds (max_steps tsk)) higher_priority) #|alpha' tsk|
= per_task_rta tsk rt_bounds (max_steps tsk).+1.
End SimpleLemmas.
Section HighPriorityTasks.
Variable ts: taskset_of sporadic_task.
Hypothesis H_task_set_is_sorted: sorted higher_priority ts.
Hypothesis H_task_set_has_unique_priorities:
FP_is_antisymmetric_over_task_set higher_priority ts.
Hypothesis H_priority_transitive: FP_is_transitive higher_priority.
Variable hp_bounds: seq task_with_response_time.
Variable R: time.
Hypothesis H_analysis_succeeds: fp_claimed_bounds ts = Some hp_bounds.
Variable elem: sporadic_task.
Let TASK := nth elem ts.
Lemma fp_claimed_bounds_hp_tasks_have_smaller_index :
∀ hp_idx idx,
hp_idx < size ts →
idx < size ts →
hp_idx != idx →
higher_priority (TASK hp_idx) (TASK idx) →
hp_idx < idx.
End HighPriorityTasks.
Section Convergence.
Variable ts_hp: seq sporadic_task.
Variable rt_bounds: seq task_with_response_time.
Hypothesis H_test_succeeds: fp_claimed_bounds ts_hp = Some rt_bounds.
Variable tsk: sporadic_task.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline (rcons ts_hp tsk).
Let f := per_task_rta tsk rt_bounds.
Hypothesis H_no_larger_than_deadline: f (max_steps tsk) ≤ task_deadline tsk.
Lemma bertogna_fp_comp_f_monotonic :
∀ x1 x2, x1 ≤ x2 → f x1 ≤ f x2.
Lemma bertogna_fp_comp_f_converges_early :
(∃ k, k ≤ max_steps tsk ∧ f k = f k.+1) →
f (max_steps tsk) = f (max_steps tsk).+1.
Section DerivingContradiction.
Hypothesis H_keeps_diverging:
∀ k,
k ≤ max_steps tsk → f k != f k.+1.
Lemma bertogna_fp_comp_f_increases :
∀ k,
k ≤ max_steps tsk →
f k < f k.+1.
Lemma bertogna_fp_comp_rt_grows_too_much :
∀ k,
k ≤ max_steps tsk →
f k > k + task_cost tsk - 1.
End DerivingContradiction.
Lemma per_task_rta_converges:
f (max_steps tsk) = f (max_steps tsk).+1.
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.
Hypothesis H_non_empty_affinity:
∀ tsk, tsk \in ts → #|alpha' tsk| > 0.
Hypothesis H_subaffinity:
∀ tsk, tsk \in ts → is_subaffinity (alpha' tsk) (alpha tsk).
Hypothesis H_task_set_is_sorted: sorted higher_priority ts.
Hypothesis H_task_set_has_unique_priorities:
FP_is_antisymmetric_over_task_set higher_priority ts.
Hypothesis H_priority_is_total:
FP_is_total_over_task_set higher_priority ts.
Hypothesis H_priority_transitive: FP_is_transitive higher_priority.
Variable 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_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_respects_affinity: respects_affinity job_task sched alpha.
Hypothesis H_work_conserving: apa_work_conserving job_arrival job_cost job_task arr_seq
sched alpha.
Hypothesis H_respects_FP_policy:
respects_FP_policy_under_weak_APA job_arrival job_cost job_task arr_seq sched
alpha higher_priority.
Let no_deadline_missed_by_task (tsk: sporadic_task) :=
task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched tsk.
Let 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 fp_analysis_yields_response_time_bounds :
∀ tsk R,
(tsk, R) \In fp_claimed_bounds ts →
response_time_bounded_by tsk R.
Hypothesis H_test_succeeds: fp_schedulable ts.
Theorem taskset_schedulable_by_fp_rta :
∀ tsk, tsk \in ts → no_deadline_missed_by_task tsk.
Theorem jobs_schedulable_by_fp_rta :
∀ j, arrives_in arr_seq j → no_deadline_missed_by_job j.
End MainProof.
End Analysis.
End ResponseTimeIterationFP.