Library prosa.classic.implementation.apa.bertogna_edf_example
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.task prosa.classic.model.priority.
Require Import prosa.classic.model.schedule.global.schedulability.
Require Import prosa.classic.model.schedule.global.basic.schedule.
Require Import prosa.classic.model.schedule.apa.affinity prosa.classic.model.schedule.apa.interference prosa.classic.model.schedule.apa.platform.
Require Import prosa.classic.analysis.apa.workload_bound
prosa.classic.analysis.apa.interference_bound_edf
prosa.classic.analysis.apa.bertogna_edf_comp.
Require Import prosa.classic.implementation.apa.job
prosa.classic.implementation.apa.task
prosa.classic.implementation.apa.schedule
prosa.classic.implementation.apa.arrival_sequence.
From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq fintype bigop div.
Module ResponseTimeAnalysisEDF.
Import Job Schedule SporadicTaskset Priority Schedulability
Affinity Platform InterferenceBoundEDF WorkloadBound
Interference ResponseTimeIterationEDF.
Import ConcreteJob ConcreteTask ConcreteArrivalSequence ConcreteScheduler.
Section ExampleRTA.
Let num_cpus := 2.
Let cpu j := @Ordinal num_cpus j.
Program Let alpha1 : affinity num_cpus :=
(Build_set [:: cpu 0 _; cpu 1 _] _).
Program Let alpha2 : affinity num_cpus :=
(Build_set [:: cpu 0 _] _).
Program Let alpha3 : affinity num_cpus :=
(Build_set [:: cpu 1 _] _).
Let tsk1 := {| task_id := 1; task_cost := 3; task_period := 5;
task_deadline := 3; task_affinity := alpha1|}.
Let tsk2 := {| task_id := 2; task_cost := 2; task_period := 6;
task_deadline := 5; task_affinity := alpha2|}.
Let tsk3 := {| task_id := 3; task_cost := 2; task_period := 12;
task_deadline := 11; task_affinity := alpha3|}.
Program Let ts := Build_set [:: tsk1; tsk2; tsk3] _.
Section FactsAboutTaskset.
Fact ts_non_empty_affinities:
∀ tsk,
tsk \in ts →
#|task_affinity tsk| > 0.
Proof.
intros tsk IN.
by repeat (move: IN ⇒ /orP [/eqP EQ | IN]; subst; rewrite ?set_card; compute).
Qed.
Fact ts_has_valid_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Proof.
intros tsk IN.
by repeat (move: IN ⇒ /orP [/eqP EQ | IN]; subst; compute).
Qed.
Fact ts_has_constrained_deadlines:
∀ tsk,
tsk \in ts →
task_deadline tsk ≤ task_period tsk.
Proof.
intros tsk IN.
by repeat (move: IN ⇒ /orP [/eqP EQ | IN]; subst; compute).
Qed.
End FactsAboutTaskset.
Let schedulability_test :=
edf_schedulable (@task_cost _) (@task_period _)
(@task_deadline _) num_cpus task_affinity
task_affinity.
Fact schedulability_test_succeeds :
schedulability_test ts = true.
Proof.
unfold schedulability_test, edf_schedulable, edf_claimed_bounds; desf.
apply negbT in Heq; move: Heq ⇒ /negP ALL.
exfalso; apply ALL; clear ALL.
assert (STEPS: \sum_(tsk <- ts) (task_deadline tsk - task_cost tsk) + 1 = 13).
{
by rewrite unlock; compute.
} rewrite STEPS; clear STEPS.
Local Ltac f :=
unfold edf_rta_iteration; simpl;
unfold edf_response_time_bound, div_floor, total_interference_bound_edf, interference_bound_edf, interference_bound_generic, W, edf_specific_interference_bound, different_task_in, affinity_intersects; simpl;
rewrite !addnE !set_card !big_cons ?big_nil /=.
Local Ltac g := destruct master_key; f; simpl_exists_ord.
rewrite [edf_rta_iteration]lock; simpl.
unfold locked at 13; g.
unfold locked at 12; g.
unfold locked at 11; g.
unfold locked at 10; g.
unfold locked at 9; g.
unfold locked at 8; g.
unfold locked at 7; g.
unfold locked at 6; g.
unfold locked at 5; g.
unfold locked at 4; g.
unfold locked at 3; g.
unfold locked at 2; g.
by unfold locked at 1; g.
Qed.
Let arr_seq := periodic_arrival_sequence ts.
Let sched := scheduler job_arrival job_cost job_task num_cpus arr_seq task_affinity
(JLFP_to_JLDP (EDF job_arrival job_deadline)).
Let no_deadline_missed_by :=
task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched.
Corollary ts_is_schedulable:
∀ tsk,
tsk \in ts →
no_deadline_missed_by tsk.
Proof.
intros tsk IN.
have VALID := periodic_arrivals_valid_job_parameters ts ts_has_valid_parameters.
have VALIDTS := ts_has_valid_parameters.
unfold valid_sporadic_job, valid_realtime_job in *; des.
try ( apply taskset_schedulable_by_edf_rta with (task_cost := task_cost) (task_period := task_period)
(task_deadline := task_deadline) (alpha := task_affinity) (alpha' := task_affinity)
(ts0 := ts); try (by done) ) ||
apply taskset_schedulable_by_edf_rta with (task_cost := task_cost) (task_period := task_period)
(task_deadline := task_deadline) (alpha := task_affinity) (alpha' := task_affinity)
(ts := ts); try (by done).
- by apply ts_has_constrained_deadlines.
- by apply ts_non_empty_affinities.
- by ins.
- by apply periodic_arrivals_all_jobs_from_taskset.
- by apply periodic_arrivals_are_sporadic.
- by apply scheduler_jobs_come_from_arrival_sequence.
- by apply scheduler_jobs_must_arrive_to_execute.
- apply scheduler_completed_jobs_dont_execute.
-- by apply periodic_arrivals_are_consistent.
-- by apply periodic_arrivals_is_a_set.
- apply scheduler_sequential_jobs.
-- by apply periodic_arrivals_are_consistent.
-- by apply periodic_arrivals_is_a_set.
- by apply scheduler_respects_affinity.
- apply scheduler_apa_work_conserving.
-- by apply periodic_arrivals_are_consistent.
-- by apply periodic_arrivals_is_a_set.
-- by intros t; apply RM_is_transitive.
-- by intros t x y; apply leq_total.
- apply scheduler_respects_policy.
-- by apply periodic_arrivals_are_consistent.
-- by apply periodic_arrivals_is_a_set.
-- by intros t; apply RM_is_transitive.
-- by intros t x y; apply leq_total.
- by apply schedulability_test_succeeds.
Qed.
End ExampleRTA.
End ResponseTimeAnalysisEDF.
Require Import prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.task prosa.classic.model.priority.
Require Import prosa.classic.model.schedule.global.schedulability.
Require Import prosa.classic.model.schedule.global.basic.schedule.
Require Import prosa.classic.model.schedule.apa.affinity prosa.classic.model.schedule.apa.interference prosa.classic.model.schedule.apa.platform.
Require Import prosa.classic.analysis.apa.workload_bound
prosa.classic.analysis.apa.interference_bound_edf
prosa.classic.analysis.apa.bertogna_edf_comp.
Require Import prosa.classic.implementation.apa.job
prosa.classic.implementation.apa.task
prosa.classic.implementation.apa.schedule
prosa.classic.implementation.apa.arrival_sequence.
From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq fintype bigop div.
Module ResponseTimeAnalysisEDF.
Import Job Schedule SporadicTaskset Priority Schedulability
Affinity Platform InterferenceBoundEDF WorkloadBound
Interference ResponseTimeIterationEDF.
Import ConcreteJob ConcreteTask ConcreteArrivalSequence ConcreteScheduler.
Section ExampleRTA.
Let num_cpus := 2.
Let cpu j := @Ordinal num_cpus j.
Program Let alpha1 : affinity num_cpus :=
(Build_set [:: cpu 0 _; cpu 1 _] _).
Program Let alpha2 : affinity num_cpus :=
(Build_set [:: cpu 0 _] _).
Program Let alpha3 : affinity num_cpus :=
(Build_set [:: cpu 1 _] _).
Let tsk1 := {| task_id := 1; task_cost := 3; task_period := 5;
task_deadline := 3; task_affinity := alpha1|}.
Let tsk2 := {| task_id := 2; task_cost := 2; task_period := 6;
task_deadline := 5; task_affinity := alpha2|}.
Let tsk3 := {| task_id := 3; task_cost := 2; task_period := 12;
task_deadline := 11; task_affinity := alpha3|}.
Program Let ts := Build_set [:: tsk1; tsk2; tsk3] _.
Section FactsAboutTaskset.
Fact ts_non_empty_affinities:
∀ tsk,
tsk \in ts →
#|task_affinity tsk| > 0.
Proof.
intros tsk IN.
by repeat (move: IN ⇒ /orP [/eqP EQ | IN]; subst; rewrite ?set_card; compute).
Qed.
Fact ts_has_valid_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Proof.
intros tsk IN.
by repeat (move: IN ⇒ /orP [/eqP EQ | IN]; subst; compute).
Qed.
Fact ts_has_constrained_deadlines:
∀ tsk,
tsk \in ts →
task_deadline tsk ≤ task_period tsk.
Proof.
intros tsk IN.
by repeat (move: IN ⇒ /orP [/eqP EQ | IN]; subst; compute).
Qed.
End FactsAboutTaskset.
Let schedulability_test :=
edf_schedulable (@task_cost _) (@task_period _)
(@task_deadline _) num_cpus task_affinity
task_affinity.
Fact schedulability_test_succeeds :
schedulability_test ts = true.
Proof.
unfold schedulability_test, edf_schedulable, edf_claimed_bounds; desf.
apply negbT in Heq; move: Heq ⇒ /negP ALL.
exfalso; apply ALL; clear ALL.
assert (STEPS: \sum_(tsk <- ts) (task_deadline tsk - task_cost tsk) + 1 = 13).
{
by rewrite unlock; compute.
} rewrite STEPS; clear STEPS.
Local Ltac f :=
unfold edf_rta_iteration; simpl;
unfold edf_response_time_bound, div_floor, total_interference_bound_edf, interference_bound_edf, interference_bound_generic, W, edf_specific_interference_bound, different_task_in, affinity_intersects; simpl;
rewrite !addnE !set_card !big_cons ?big_nil /=.
Local Ltac g := destruct master_key; f; simpl_exists_ord.
rewrite [edf_rta_iteration]lock; simpl.
unfold locked at 13; g.
unfold locked at 12; g.
unfold locked at 11; g.
unfold locked at 10; g.
unfold locked at 9; g.
unfold locked at 8; g.
unfold locked at 7; g.
unfold locked at 6; g.
unfold locked at 5; g.
unfold locked at 4; g.
unfold locked at 3; g.
unfold locked at 2; g.
by unfold locked at 1; g.
Qed.
Let arr_seq := periodic_arrival_sequence ts.
Let sched := scheduler job_arrival job_cost job_task num_cpus arr_seq task_affinity
(JLFP_to_JLDP (EDF job_arrival job_deadline)).
Let no_deadline_missed_by :=
task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched.
Corollary ts_is_schedulable:
∀ tsk,
tsk \in ts →
no_deadline_missed_by tsk.
Proof.
intros tsk IN.
have VALID := periodic_arrivals_valid_job_parameters ts ts_has_valid_parameters.
have VALIDTS := ts_has_valid_parameters.
unfold valid_sporadic_job, valid_realtime_job in *; des.
try ( apply taskset_schedulable_by_edf_rta with (task_cost := task_cost) (task_period := task_period)
(task_deadline := task_deadline) (alpha := task_affinity) (alpha' := task_affinity)
(ts0 := ts); try (by done) ) ||
apply taskset_schedulable_by_edf_rta with (task_cost := task_cost) (task_period := task_period)
(task_deadline := task_deadline) (alpha := task_affinity) (alpha' := task_affinity)
(ts := ts); try (by done).
- by apply ts_has_constrained_deadlines.
- by apply ts_non_empty_affinities.
- by ins.
- by apply periodic_arrivals_all_jobs_from_taskset.
- by apply periodic_arrivals_are_sporadic.
- by apply scheduler_jobs_come_from_arrival_sequence.
- by apply scheduler_jobs_must_arrive_to_execute.
- apply scheduler_completed_jobs_dont_execute.
-- by apply periodic_arrivals_are_consistent.
-- by apply periodic_arrivals_is_a_set.
- apply scheduler_sequential_jobs.
-- by apply periodic_arrivals_are_consistent.
-- by apply periodic_arrivals_is_a_set.
- by apply scheduler_respects_affinity.
- apply scheduler_apa_work_conserving.
-- by apply periodic_arrivals_are_consistent.
-- by apply periodic_arrivals_is_a_set.
-- by intros t; apply RM_is_transitive.
-- by intros t x y; apply leq_total.
- apply scheduler_respects_policy.
-- by apply periodic_arrivals_are_consistent.
-- by apply periodic_arrivals_is_a_set.
-- by intros t; apply RM_is_transitive.
-- by intros t x y; apply leq_total.
- by apply schedulability_test_succeeds.
Qed.
End ExampleRTA.
End ResponseTimeAnalysisEDF.