Library prosa.classic.analysis.uni.jitter.fp_rta_comp
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.priority.
Require Import prosa.classic.model.arrival.basic.task.
Require Import prosa.classic.model.arrival.jitter.job prosa.classic.model.arrival.jitter.arrival_sequence
prosa.classic.model.arrival.jitter.task_arrival.
Require Import prosa.classic.model.schedule.uni.schedulability
prosa.classic.model.schedule.uni.response_time.
Require Import prosa.classic.model.schedule.uni.jitter.schedule prosa.classic.model.schedule.uni.jitter.platform.
Require Import prosa.classic.analysis.uni.jitter.workload_bound_fp prosa.classic.analysis.uni.jitter.fp_rta_theory.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path ssrfun.
Module ResponseTimeIterationFP.
Import JobWithJitter UniprocessorScheduleWithJitter TaskArrivalWithJitter
SporadicTaskset WorkloadBoundFP Priority ResponseTime
ResponseTime Schedulability Platform ResponseTimeAnalysisFP.
Section Analysis.
Context {SporadicTask: eqType}.
Variable task_cost: SporadicTask → time.
Variable task_period: SporadicTask → time.
Variable task_deadline: SporadicTask → time.
Variable task_jitter: SporadicTask → time.
Let task_with_response_time := (SporadicTask × time)%type.
Variable higher_eq_priority: FP_policy SporadicTask.
Definition max_steps (tsk: SporadicTask) :=
task_deadline tsk - task_cost tsk + 1.
Let workload_bound :=
total_workload_bound_fp task_cost task_period task_jitter higher_eq_priority.
Definition per_task_rta ts tsk :=
iter_fixpoint (workload_bound ts tsk) (max_steps tsk) (task_cost tsk).
Let is_valid_bound tsk_R :=
if tsk_R is (tsk, Some R) then
if task_jitter tsk + R ≤ task_deadline tsk then
Some (tsk, R)
else None
else None.
Definition fp_claimed_bounds ts: option (seq task_with_response_time) :=
let possible_bounds := [seq (tsk, per_task_rta ts tsk) | tsk <- ts] in
if all is_valid_bound possible_bounds then
Some (pmap is_valid_bound possible_bounds)
else None.
Definition fp_schedulable (ts: seq SporadicTask) :=
fp_claimed_bounds ts != None.
Section Lemmas.
Variable ts: seq SporadicTask.
Variable rt_bounds: seq task_with_response_time.
Hypothesis H_analysis_succeeds:
fp_claimed_bounds ts = Some rt_bounds.
Section BoundExists.
Variable tsk: SporadicTask.
Hypothesis H_tsk_in_ts: tsk \in ts.
Lemma fp_claimed_bounds_for_every_task:
∃ R, (tsk, R) \in rt_bounds.
End BoundExists.
Section PropertiesOfBound.
Variable tsk: SporadicTask.
Variable R: time.
Hypothesis H_tsk_R_computed: (tsk, R) \in rt_bounds.
Lemma fp_claimed_bounds_from_taskset:
tsk \in ts.
Lemma fp_claimed_bounds_computes_iteration:
per_task_rta ts tsk = Some R.
Lemma fp_claimed_bounds_yields_fixed_point :
R = workload_bound ts tsk R.
Lemma fp_claimed_bounds_le_deadline:
task_jitter tsk + R ≤ task_deadline tsk.
Section FixedPoint.
Hypothesis H_priority_is_reflexive:
FP_is_reflexive higher_eq_priority.
Hypothesis H_cost_positive: task_cost tsk > 0.
Hypothesis H_period_positive:
∀ tsk, tsk \in ts → task_period tsk > 0.
Lemma fp_claimed_bounds_ge_cost:
R ≥ task_cost tsk.
Corollary fp_claimed_bounds_gt_zero: R > 0.
End FixedPoint.
End PropertiesOfBound.
End Lemmas.
End Analysis.
Section ProvingCorrectness.
Context {SporadicTask: eqType}.
Variable task_cost: SporadicTask → time.
Variable task_period: SporadicTask → time.
Variable task_deadline: SporadicTask → time.
Variable task_jitter: SporadicTask → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_jitter: Job → time.
Variable job_task: Job → SporadicTask.
Variable ts: seq SporadicTask.
Hypothesis H_positive_costs: ∀ tsk, tsk \in ts → task_cost tsk > 0.
Hypothesis H_positive_periods: ∀ tsk, tsk \in ts → task_period tsk > 0.
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_arr_seq_is_a_set: arrival_sequence_is_a_set arr_seq.
Hypothesis H_all_jobs_from_taskset:
∀ j,
arrives_in arr_seq j →
job_task j \in ts.
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period job_arrival job_task arr_seq.
Hypothesis H_job_cost_le_task_cost:
∀ j,
arrives_in arr_seq j →
job_cost j ≤ task_cost (job_task j).
Hypothesis H_job_jitter_le_task_jitter:
∀ j,
arrives_in arr_seq j →
job_jitter j ≤ task_jitter (job_task j).
Hypothesis H_job_deadline_eq_task_deadline:
∀ j,
arrives_in arr_seq j →
job_deadline j = task_deadline (job_task j).
Variable higher_eq_priority: FP_policy SporadicTask.
Hypothesis H_priority_reflexive: FP_is_reflexive higher_eq_priority.
Hypothesis H_priority_transitive: FP_is_transitive higher_eq_priority.
Variable sched: schedule Job.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
Hypothesis H_jobs_execute_after_jitter: jobs_execute_after_jitter job_arrival job_jitter sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
Hypothesis H_work_conserving: work_conserving job_arrival job_cost job_jitter arr_seq sched.
Hypothesis H_respects_FP_policy:
respects_FP_policy job_arrival job_cost job_jitter job_task arr_seq sched higher_eq_priority.
Let no_deadline_missed_by_task :=
task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched.
Let no_deadline_missed_by_job :=
job_misses_no_deadline job_arrival job_cost job_deadline sched.
Let response_time_bounded_by:=
is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched.
Let RTA_claimed_bounds :=
fp_claimed_bounds task_cost task_period task_deadline task_jitter higher_eq_priority ts.
Let claimed_to_be_schedulable :=
fp_schedulable task_cost task_period task_deadline task_jitter higher_eq_priority ts.
Theorem fp_analysis_yields_response_time_bounds :
∀ tsk R,
(tsk, R) \In RTA_claimed_bounds →
response_time_bounded_by tsk (task_jitter tsk + R).
Section AnalysisIsSufficient.
Hypothesis H_test_succeeds: claimed_to_be_schedulable.
Theorem taskset_schedulable_by_fp_rta :
∀ tsk, tsk \in ts → no_deadline_missed_by_task tsk.
Theorem jobs_schedulable_by_fp_rta :
∀ j,
arrives_in arr_seq j →
no_deadline_missed_by_job j.
End AnalysisIsSufficient.
End ProvingCorrectness.
End ResponseTimeIterationFP.
Require Import prosa.classic.model.priority.
Require Import prosa.classic.model.arrival.basic.task.
Require Import prosa.classic.model.arrival.jitter.job prosa.classic.model.arrival.jitter.arrival_sequence
prosa.classic.model.arrival.jitter.task_arrival.
Require Import prosa.classic.model.schedule.uni.schedulability
prosa.classic.model.schedule.uni.response_time.
Require Import prosa.classic.model.schedule.uni.jitter.schedule prosa.classic.model.schedule.uni.jitter.platform.
Require Import prosa.classic.analysis.uni.jitter.workload_bound_fp prosa.classic.analysis.uni.jitter.fp_rta_theory.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path ssrfun.
Module ResponseTimeIterationFP.
Import JobWithJitter UniprocessorScheduleWithJitter TaskArrivalWithJitter
SporadicTaskset WorkloadBoundFP Priority ResponseTime
ResponseTime Schedulability Platform ResponseTimeAnalysisFP.
Section Analysis.
Context {SporadicTask: eqType}.
Variable task_cost: SporadicTask → time.
Variable task_period: SporadicTask → time.
Variable task_deadline: SporadicTask → time.
Variable task_jitter: SporadicTask → time.
Let task_with_response_time := (SporadicTask × time)%type.
Variable higher_eq_priority: FP_policy SporadicTask.
Definition max_steps (tsk: SporadicTask) :=
task_deadline tsk - task_cost tsk + 1.
Let workload_bound :=
total_workload_bound_fp task_cost task_period task_jitter higher_eq_priority.
Definition per_task_rta ts tsk :=
iter_fixpoint (workload_bound ts tsk) (max_steps tsk) (task_cost tsk).
Let is_valid_bound tsk_R :=
if tsk_R is (tsk, Some R) then
if task_jitter tsk + R ≤ task_deadline tsk then
Some (tsk, R)
else None
else None.
Definition fp_claimed_bounds ts: option (seq task_with_response_time) :=
let possible_bounds := [seq (tsk, per_task_rta ts tsk) | tsk <- ts] in
if all is_valid_bound possible_bounds then
Some (pmap is_valid_bound possible_bounds)
else None.
Definition fp_schedulable (ts: seq SporadicTask) :=
fp_claimed_bounds ts != None.
Section Lemmas.
Variable ts: seq SporadicTask.
Variable rt_bounds: seq task_with_response_time.
Hypothesis H_analysis_succeeds:
fp_claimed_bounds ts = Some rt_bounds.
Section BoundExists.
Variable tsk: SporadicTask.
Hypothesis H_tsk_in_ts: tsk \in ts.
Lemma fp_claimed_bounds_for_every_task:
∃ R, (tsk, R) \in rt_bounds.
End BoundExists.
Section PropertiesOfBound.
Variable tsk: SporadicTask.
Variable R: time.
Hypothesis H_tsk_R_computed: (tsk, R) \in rt_bounds.
Lemma fp_claimed_bounds_from_taskset:
tsk \in ts.
Lemma fp_claimed_bounds_computes_iteration:
per_task_rta ts tsk = Some R.
Lemma fp_claimed_bounds_yields_fixed_point :
R = workload_bound ts tsk R.
Lemma fp_claimed_bounds_le_deadline:
task_jitter tsk + R ≤ task_deadline tsk.
Section FixedPoint.
Hypothesis H_priority_is_reflexive:
FP_is_reflexive higher_eq_priority.
Hypothesis H_cost_positive: task_cost tsk > 0.
Hypothesis H_period_positive:
∀ tsk, tsk \in ts → task_period tsk > 0.
Lemma fp_claimed_bounds_ge_cost:
R ≥ task_cost tsk.
Corollary fp_claimed_bounds_gt_zero: R > 0.
End FixedPoint.
End PropertiesOfBound.
End Lemmas.
End Analysis.
Section ProvingCorrectness.
Context {SporadicTask: eqType}.
Variable task_cost: SporadicTask → time.
Variable task_period: SporadicTask → time.
Variable task_deadline: SporadicTask → time.
Variable task_jitter: SporadicTask → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_jitter: Job → time.
Variable job_task: Job → SporadicTask.
Variable ts: seq SporadicTask.
Hypothesis H_positive_costs: ∀ tsk, tsk \in ts → task_cost tsk > 0.
Hypothesis H_positive_periods: ∀ tsk, tsk \in ts → task_period tsk > 0.
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_arr_seq_is_a_set: arrival_sequence_is_a_set arr_seq.
Hypothesis H_all_jobs_from_taskset:
∀ j,
arrives_in arr_seq j →
job_task j \in ts.
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period job_arrival job_task arr_seq.
Hypothesis H_job_cost_le_task_cost:
∀ j,
arrives_in arr_seq j →
job_cost j ≤ task_cost (job_task j).
Hypothesis H_job_jitter_le_task_jitter:
∀ j,
arrives_in arr_seq j →
job_jitter j ≤ task_jitter (job_task j).
Hypothesis H_job_deadline_eq_task_deadline:
∀ j,
arrives_in arr_seq j →
job_deadline j = task_deadline (job_task j).
Variable higher_eq_priority: FP_policy SporadicTask.
Hypothesis H_priority_reflexive: FP_is_reflexive higher_eq_priority.
Hypothesis H_priority_transitive: FP_is_transitive higher_eq_priority.
Variable sched: schedule Job.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
Hypothesis H_jobs_execute_after_jitter: jobs_execute_after_jitter job_arrival job_jitter sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
Hypothesis H_work_conserving: work_conserving job_arrival job_cost job_jitter arr_seq sched.
Hypothesis H_respects_FP_policy:
respects_FP_policy job_arrival job_cost job_jitter job_task arr_seq sched higher_eq_priority.
Let no_deadline_missed_by_task :=
task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched.
Let no_deadline_missed_by_job :=
job_misses_no_deadline job_arrival job_cost job_deadline sched.
Let response_time_bounded_by:=
is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched.
Let RTA_claimed_bounds :=
fp_claimed_bounds task_cost task_period task_deadline task_jitter higher_eq_priority ts.
Let claimed_to_be_schedulable :=
fp_schedulable task_cost task_period task_deadline task_jitter higher_eq_priority ts.
Theorem fp_analysis_yields_response_time_bounds :
∀ tsk R,
(tsk, R) \In RTA_claimed_bounds →
response_time_bounded_by tsk (task_jitter tsk + R).
Section AnalysisIsSufficient.
Hypothesis H_test_succeeds: claimed_to_be_schedulable.
Theorem taskset_schedulable_by_fp_rta :
∀ tsk, tsk \in ts → no_deadline_missed_by_task tsk.
Theorem jobs_schedulable_by_fp_rta :
∀ j,
arrives_in arr_seq j →
no_deadline_missed_by_job j.
End AnalysisIsSufficient.
End ProvingCorrectness.
End ResponseTimeIterationFP.