Library rt.implementation.apa.bertogna_edf_example
Require Import rt.util.all.
Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task rt.model.priority.
Require Import rt.model.schedule.global.schedulability.
Require Import rt.model.schedule.global.basic.schedule.
Require Import rt.model.schedule.apa.affinity rt.model.schedule.apa.interference rt.model.schedule.apa.platform.
Require Import rt.analysis.apa.workload_bound
rt.analysis.apa.interference_bound_edf
rt.analysis.apa.bertogna_edf_comp.
Require Import rt.implementation.apa.job
rt.implementation.apa.task
rt.implementation.apa.schedule
rt.implementation.apa.arrival_sequence.
Module ResponseTimeAnalysisEDF.
Import Job Schedule SporadicTaskset Priority Schedulability
Affinity Platform InterferenceBoundEDF WorkloadBound
Interference ResponseTimeIterationEDF.
Import ConcreteJob ConcreteTask ConcreteArrivalSequence ConcreteScheduler.
(* In this section, we instantiate a simple example to show that the theorems
contain no contradictory assumptions. *)
Section ExampleRTA.
(* Assume there are two processors. *)
Let num_cpus := 2.
(* Let (cpu j) denote the j-th processor *)
Let cpu j := @Ordinal num_cpus j.
(* Define alpha1 := {cpu 0, cpu 1} with the two processors. *)
Program Let alpha1 : affinity num_cpus :=
(Build_set [:: cpu 0 _; cpu 1 _] _).
(* Define the singleton affinity alpha2 := {cpu 0}. *)
Program Let alpha2 : affinity num_cpus :=
(Build_set [:: cpu 0 _] _).
(* Define the singleton affinity alpha3 := {cpu 1}. *)
Program Let alpha3 : affinity num_cpus :=
(Build_set [:: cpu 1 _] _).
(* Now we create three tasks using the affinities above ... *)
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|}.
(* ... and group these tasks into task set ts. *)
Program Let ts := Build_set [:: tsk1; tsk2; tsk3] _.
(* In this section, we let Coq compute a few properties about ts. *)
Section FactsAboutTaskset.
(* There are no empty affinities. *)
Fact ts_non_empty_affinities:
∀ tsk,
tsk \in ts →
#|task_affinity tsk| > 0.
(* The tasks have valid parameters (e.g., cost > 0). *)
Fact ts_has_valid_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
(* The task set has constrained deadlines. *)
Fact ts_has_constrained_deadlines:
∀ tsk,
tsk \in ts →
task_deadline tsk ≤ task_period tsk.
End FactsAboutTaskset.
(* Next, recall the EDF RTA schedulability test for APA scheduling.
Note that the task functions (from implementation/apa/task.v)
require num_cpus as a parameter, so we leave a blank space so that
can be inferred automatically. *)
Let schedulability_test :=
edf_schedulable (@task_cost _) (@task_period _)
(@task_deadline _) num_cpus task_affinity
task_affinity. (* For simplicity, we use subaffinity alpha' = alpha. *)
(* Now, we guide Coq to compute the schedulability test function
and show it returns true. *)
Fact schedulability_test_succeeds :
schedulability_test ts = true.
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.
(* Let arr_seq be the periodic arrival sequence from ts. *)
Let arr_seq := periodic_arrival_sequence ts.
(* Let sched be the weak APA EDF scheduler. *)
Let sched := scheduler job_arrival job_cost job_task num_cpus arr_seq task_affinity
(JLFP_to_JLDP (EDF job_arrival job_deadline)).
(* Recall the definition of deadline miss. *)
Let no_deadline_missed_by :=
task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched.
(* To show that the RTA works, we infer the schedulability of the task
set from the result of the RTA procedure. *)
Corollary ts_is_schedulable:
∀ tsk,
tsk \in ts →
no_deadline_missed_by tsk.
End ExampleRTA.
End ResponseTimeAnalysisEDF.
Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task rt.model.priority.
Require Import rt.model.schedule.global.schedulability.
Require Import rt.model.schedule.global.basic.schedule.
Require Import rt.model.schedule.apa.affinity rt.model.schedule.apa.interference rt.model.schedule.apa.platform.
Require Import rt.analysis.apa.workload_bound
rt.analysis.apa.interference_bound_edf
rt.analysis.apa.bertogna_edf_comp.
Require Import rt.implementation.apa.job
rt.implementation.apa.task
rt.implementation.apa.schedule
rt.implementation.apa.arrival_sequence.
Module ResponseTimeAnalysisEDF.
Import Job Schedule SporadicTaskset Priority Schedulability
Affinity Platform InterferenceBoundEDF WorkloadBound
Interference ResponseTimeIterationEDF.
Import ConcreteJob ConcreteTask ConcreteArrivalSequence ConcreteScheduler.
(* In this section, we instantiate a simple example to show that the theorems
contain no contradictory assumptions. *)
Section ExampleRTA.
(* Assume there are two processors. *)
Let num_cpus := 2.
(* Let (cpu j) denote the j-th processor *)
Let cpu j := @Ordinal num_cpus j.
(* Define alpha1 := {cpu 0, cpu 1} with the two processors. *)
Program Let alpha1 : affinity num_cpus :=
(Build_set [:: cpu 0 _; cpu 1 _] _).
(* Define the singleton affinity alpha2 := {cpu 0}. *)
Program Let alpha2 : affinity num_cpus :=
(Build_set [:: cpu 0 _] _).
(* Define the singleton affinity alpha3 := {cpu 1}. *)
Program Let alpha3 : affinity num_cpus :=
(Build_set [:: cpu 1 _] _).
(* Now we create three tasks using the affinities above ... *)
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|}.
(* ... and group these tasks into task set ts. *)
Program Let ts := Build_set [:: tsk1; tsk2; tsk3] _.
(* In this section, we let Coq compute a few properties about ts. *)
Section FactsAboutTaskset.
(* There are no empty affinities. *)
Fact ts_non_empty_affinities:
∀ tsk,
tsk \in ts →
#|task_affinity tsk| > 0.
(* The tasks have valid parameters (e.g., cost > 0). *)
Fact ts_has_valid_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
(* The task set has constrained deadlines. *)
Fact ts_has_constrained_deadlines:
∀ tsk,
tsk \in ts →
task_deadline tsk ≤ task_period tsk.
End FactsAboutTaskset.
(* Next, recall the EDF RTA schedulability test for APA scheduling.
Note that the task functions (from implementation/apa/task.v)
require num_cpus as a parameter, so we leave a blank space so that
can be inferred automatically. *)
Let schedulability_test :=
edf_schedulable (@task_cost _) (@task_period _)
(@task_deadline _) num_cpus task_affinity
task_affinity. (* For simplicity, we use subaffinity alpha' = alpha. *)
(* Now, we guide Coq to compute the schedulability test function
and show it returns true. *)
Fact schedulability_test_succeeds :
schedulability_test ts = true.
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.
(* Let arr_seq be the periodic arrival sequence from ts. *)
Let arr_seq := periodic_arrival_sequence ts.
(* Let sched be the weak APA EDF scheduler. *)
Let sched := scheduler job_arrival job_cost job_task num_cpus arr_seq task_affinity
(JLFP_to_JLDP (EDF job_arrival job_deadline)).
(* Recall the definition of deadline miss. *)
Let no_deadline_missed_by :=
task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched.
(* To show that the RTA works, we infer the schedulability of the task
set from the result of the RTA procedure. *)
Corollary ts_is_schedulable:
∀ tsk,
tsk \in ts →
no_deadline_missed_by tsk.
End ExampleRTA.
End ResponseTimeAnalysisEDF.