Library prosa.classic.implementation.uni.susp.dynamic.oblivious.fp_rta_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.uni.schedule prosa.classic.model.schedule.uni.schedulability.
Require Import prosa.classic.model.schedule.uni.susp.suspension_intervals.
Require Import prosa.classic.analysis.uni.basic.workload_bound_fp.
Require Import prosa.classic.analysis.uni.susp.dynamic.oblivious.fp_rta.
Require Import prosa.classic.implementation.uni.susp.dynamic.job
prosa.classic.implementation.uni.susp.dynamic.task
prosa.classic.implementation.uni.susp.dynamic.arrival_sequence.
Require Import prosa.classic.implementation.uni.susp.schedule.
From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
Module ResponseTimeAnalysisFP.
Import Job UniprocessorSchedule SporadicTaskset Priority Schedulability
SuspensionIntervals SuspensionObliviousFP WorkloadBoundFP.
Import ConcreteJob ConcreteTask ConcreteArrivalSequence ConcreteScheduler.
(* In this section, we run the suspension-oblivious FP RTA on a simple task set
to show that the theorems contain no contradictory assumptions. *)
Section ExampleRTA.
Let tsk1 := {| task_id := 1; task_cost := 1; task_period := 5;
task_deadline := 5; task_suspension_bound := 1 |}.
Let tsk2 := {| task_id := 2; task_cost := 1; task_period := 5;
task_deadline := 5; task_suspension_bound := 0|}.
Let tsk3 := {| task_id := 3; task_cost := 1; task_period := 6;
task_deadline := 6; task_suspension_bound := 1|}.
(* Let ts be a task set containing these three tasks, ... *)
Program Let ts := Build_set [:: tsk1; tsk2; tsk3] _.
(* ...which can be shown to have valid parameters. *)
Fact ts_has_valid_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
(* Now let's inflate the task costs with the suspension-bounds. *)
Let inflated_cost := inflated_task_cost task_cost task_suspension_bound.
(* After the inflation, note that the task costs are no larger than deadlines and periods. *)
Fact inflated_cost_le_deadline_and_period:
∀ tsk,
tsk \in ts →
inflated_cost tsk ≤ task_deadline tsk ∧
inflated_cost tsk ≤ task_period tsk.
(* Next, recall the FP RTA schedulability test using RM as the FP policy
and the inflated task costs. *)
Let RTA_claimed_bounds :=
fp_claimed_bounds inflated_cost task_period task_deadline (RM task_period).
Let schedulability_test :=
fp_schedulable inflated_cost task_period task_deadline (RM task_period).
(* First, we show that the schedulability test returns the following bounds, ... *)
Fact RTA_yields_these_bounds :
RTA_claimed_bounds ts = Some [:: (tsk1, 3); (tsk2, 3); (tsk3, 5)].
(* ...so the schedulability test indeed returns true. *)
Fact schedulability_test_succeeds :
schedulability_test ts = true.
(* Now, let's show that the task set is schedulable. *)
(* Let arr_seq be the periodic arrival sequence from ts... *)
Let arr_seq := periodic_arrival_sequence ts.
(* ...where jobs have total suspension times that are no larger than
the suspension bound of their tasks. *)
Variable next_suspension: job_suspension concrete_job_eqType.
Hypothesis H_dynamic_suspensions:
dynamic_suspension_model job_cost job_task next_suspension task_suspension_bound.
(* Also assume rate-monotonic priorities. *)
Let higher_eq_priority := FP_to_JLDP job_task (RM task_period).
(* Next, let sched be the suspension-aware RM schedule with those job suspension times. *)
Let sched := scheduler job_arrival job_cost arr_seq next_suspension higher_eq_priority.
(* To conclude, based on 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.
(* ...we use the result of the suspension-oblivious FP RTA to conclude that
no task misses its deadline. *)
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.uni.schedule prosa.classic.model.schedule.uni.schedulability.
Require Import prosa.classic.model.schedule.uni.susp.suspension_intervals.
Require Import prosa.classic.analysis.uni.basic.workload_bound_fp.
Require Import prosa.classic.analysis.uni.susp.dynamic.oblivious.fp_rta.
Require Import prosa.classic.implementation.uni.susp.dynamic.job
prosa.classic.implementation.uni.susp.dynamic.task
prosa.classic.implementation.uni.susp.dynamic.arrival_sequence.
Require Import prosa.classic.implementation.uni.susp.schedule.
From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
Module ResponseTimeAnalysisFP.
Import Job UniprocessorSchedule SporadicTaskset Priority Schedulability
SuspensionIntervals SuspensionObliviousFP WorkloadBoundFP.
Import ConcreteJob ConcreteTask ConcreteArrivalSequence ConcreteScheduler.
(* In this section, we run the suspension-oblivious FP RTA on a simple task set
to show that the theorems contain no contradictory assumptions. *)
Section ExampleRTA.
Let tsk1 := {| task_id := 1; task_cost := 1; task_period := 5;
task_deadline := 5; task_suspension_bound := 1 |}.
Let tsk2 := {| task_id := 2; task_cost := 1; task_period := 5;
task_deadline := 5; task_suspension_bound := 0|}.
Let tsk3 := {| task_id := 3; task_cost := 1; task_period := 6;
task_deadline := 6; task_suspension_bound := 1|}.
(* Let ts be a task set containing these three tasks, ... *)
Program Let ts := Build_set [:: tsk1; tsk2; tsk3] _.
(* ...which can be shown to have valid parameters. *)
Fact ts_has_valid_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
(* Now let's inflate the task costs with the suspension-bounds. *)
Let inflated_cost := inflated_task_cost task_cost task_suspension_bound.
(* After the inflation, note that the task costs are no larger than deadlines and periods. *)
Fact inflated_cost_le_deadline_and_period:
∀ tsk,
tsk \in ts →
inflated_cost tsk ≤ task_deadline tsk ∧
inflated_cost tsk ≤ task_period tsk.
(* Next, recall the FP RTA schedulability test using RM as the FP policy
and the inflated task costs. *)
Let RTA_claimed_bounds :=
fp_claimed_bounds inflated_cost task_period task_deadline (RM task_period).
Let schedulability_test :=
fp_schedulable inflated_cost task_period task_deadline (RM task_period).
(* First, we show that the schedulability test returns the following bounds, ... *)
Fact RTA_yields_these_bounds :
RTA_claimed_bounds ts = Some [:: (tsk1, 3); (tsk2, 3); (tsk3, 5)].
(* ...so the schedulability test indeed returns true. *)
Fact schedulability_test_succeeds :
schedulability_test ts = true.
(* Now, let's show that the task set is schedulable. *)
(* Let arr_seq be the periodic arrival sequence from ts... *)
Let arr_seq := periodic_arrival_sequence ts.
(* ...where jobs have total suspension times that are no larger than
the suspension bound of their tasks. *)
Variable next_suspension: job_suspension concrete_job_eqType.
Hypothesis H_dynamic_suspensions:
dynamic_suspension_model job_cost job_task next_suspension task_suspension_bound.
(* Also assume rate-monotonic priorities. *)
Let higher_eq_priority := FP_to_JLDP job_task (RM task_period).
(* Next, let sched be the suspension-aware RM schedule with those job suspension times. *)
Let sched := scheduler job_arrival job_cost arr_seq next_suspension higher_eq_priority.
(* To conclude, based on 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.
(* ...we use the result of the suspension-oblivious FP RTA to conclude that
no task misses its deadline. *)
Corollary ts_is_schedulable:
∀ tsk,
tsk \in ts →
no_deadline_missed_by tsk.
End ExampleRTA.
End ResponseTimeAnalysisFP.