Library prosa.classic.implementation.apa.bertogna_fp_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_fp
prosa.classic.analysis.apa.bertogna_fp_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 fintype seq bigop div.
Module ResponseTimeAnalysisFP.
Import Job Schedule SporadicTaskset Priority Schedulability Platform
Interference InterferenceBoundFP WorkloadBound
ResponseTimeIterationFP Affinity.
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.
(* Then, let arr_seq be the periodic arrival sequence from ts. *)
Let arr_seq := periodic_arrival_sequence ts.
(* Assume rate-monotonic priorities. *)
Let higher_priority : JLDP_policy (@concrete_job_eqType num_cpus) :=
FP_to_JLDP job_task (RM task_period).
Section FactsAboutPriorityOrder.
Lemma ts_has_unique_priorities :
FP_is_antisymmetric_over_task_set (RM task_period) ts.
Lemma priority_is_total :
FP_is_total_over_task_set (RM task_period) ts.
End FactsAboutPriorityOrder.
(* Next, recall the FP 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 :=
fp_schedulable (@task_cost _) (@task_period _) (@task_deadline _)
num_cpus (RM task_period) task_affinity
task_affinity. (* For simplicity, we use subaffinity alpha' = alpha. *)
(* Now we show that the schedulability test returns true. *)
Fact schedulability_test_succeeds :
schedulability_test ts = true.
Ltac f := unfold div_floor;
rewrite !big_cons big_nil /= /higher_priority_task_in /=
/affinity_intersects !addn0 /= ?set_card ?divn1 ?addn0;
unfold interference_bound_generic, W, max_jobs, div_floor;
rewrite addn1 ?addn0.
Ltac g :=
rewrite /total_interference_bound_fp /interference_bound_generic
/W /max_jobs /div_floor !big_cons big_nil /= /higher_priority_task_in /=
/affinity_intersects.
(* Let sched be the work-conserving RM APA scheduler. *)
Let sched :=
scheduler job_arrival job_cost job_task num_cpus arr_seq task_affinity higher_priority.
(* 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.
(* Next, we prove that ts is schedulable with the result of the test. *)
Corollary ts_is_schedulable:
∀ tsk,
tsk \in ts →
no_deadline_missed_by tsk.
End ExampleRTA.
End ResponseTimeAnalysisFP.
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_fp
prosa.classic.analysis.apa.bertogna_fp_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 fintype seq bigop div.
Module ResponseTimeAnalysisFP.
Import Job Schedule SporadicTaskset Priority Schedulability Platform
Interference InterferenceBoundFP WorkloadBound
ResponseTimeIterationFP Affinity.
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.
(* Then, let arr_seq be the periodic arrival sequence from ts. *)
Let arr_seq := periodic_arrival_sequence ts.
(* Assume rate-monotonic priorities. *)
Let higher_priority : JLDP_policy (@concrete_job_eqType num_cpus) :=
FP_to_JLDP job_task (RM task_period).
Section FactsAboutPriorityOrder.
Lemma ts_has_unique_priorities :
FP_is_antisymmetric_over_task_set (RM task_period) ts.
Lemma priority_is_total :
FP_is_total_over_task_set (RM task_period) ts.
End FactsAboutPriorityOrder.
(* Next, recall the FP 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 :=
fp_schedulable (@task_cost _) (@task_period _) (@task_deadline _)
num_cpus (RM task_period) task_affinity
task_affinity. (* For simplicity, we use subaffinity alpha' = alpha. *)
(* Now we show that the schedulability test returns true. *)
Fact schedulability_test_succeeds :
schedulability_test ts = true.
Ltac f := unfold div_floor;
rewrite !big_cons big_nil /= /higher_priority_task_in /=
/affinity_intersects !addn0 /= ?set_card ?divn1 ?addn0;
unfold interference_bound_generic, W, max_jobs, div_floor;
rewrite addn1 ?addn0.
Ltac g :=
rewrite /total_interference_bound_fp /interference_bound_generic
/W /max_jobs /div_floor !big_cons big_nil /= /higher_priority_task_in /=
/affinity_intersects.
(* Let sched be the work-conserving RM APA scheduler. *)
Let sched :=
scheduler job_arrival job_cost job_task num_cpus arr_seq task_affinity higher_priority.
(* 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.
(* Next, we prove that ts is schedulable with the result of the test. *)
Corollary ts_is_schedulable:
∀ tsk,
tsk \in ts →
no_deadline_missed_by tsk.
End ExampleRTA.
End ResponseTimeAnalysisFP.