Library rt.implementation.apa.bertogna_fp_example
Require Import
rt.util.all.
Require Import rt.model.apa.job rt.model.apa.task rt.model.apa.affinity
rt.model.apa.schedule rt.model.apa.schedulability
rt.model.apa.priority rt.model.apa.platform
rt.model.apa.interference.
Require Import rt.analysis.apa.workload_bound
rt.analysis.apa.interference_bound_fp
rt.analysis.apa.bertogna_fp_comp.
Require Import rt.implementation.apa.job
rt.implementation.apa.task
rt.implementation.apa.schedule
rt.implementation.apa.arrival_sequence.
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 ∈ 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 ∈ 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 arr_seq :=
(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.
(* Let sched be the work-conserving RM APA scheduler. *)
Let sched := scheduler 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_cost job_deadline job_task sched.
(* Next, we prove that ts is schedulable with the result of the test. *)
Corollary ts_is_schedulable:
∀ tsk,
tsk ∈ ts →
no_deadline_missed_by tsk.
End ExampleRTA.
End ResponseTimeAnalysisFP.
Require Import rt.model.apa.job rt.model.apa.task rt.model.apa.affinity
rt.model.apa.schedule rt.model.apa.schedulability
rt.model.apa.priority rt.model.apa.platform
rt.model.apa.interference.
Require Import rt.analysis.apa.workload_bound
rt.analysis.apa.interference_bound_fp
rt.analysis.apa.bertogna_fp_comp.
Require Import rt.implementation.apa.job
rt.implementation.apa.task
rt.implementation.apa.schedule
rt.implementation.apa.arrival_sequence.
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 ∈ 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 ∈ 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 arr_seq :=
(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.
(* Let sched be the work-conserving RM APA scheduler. *)
Let sched := scheduler 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_cost job_deadline job_task sched.
(* Next, we prove that ts is schedulable with the result of the test. *)
Corollary ts_is_schedulable:
∀ tsk,
tsk ∈ ts →
no_deadline_missed_by tsk.
End ExampleRTA.
End ResponseTimeAnalysisFP.