Library prosa.classic.analysis.uni.basic.fp_rta_comp
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.arrival_sequence prosa.classic.model.priority
prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.schedule.uni.schedule prosa.classic.model.schedule.uni.schedulability prosa.classic.model.schedule.uni.response_time.
Require Import prosa.classic.model.schedule.uni.basic.platform.
Require Import prosa.classic.analysis.uni.basic.workload_bound_fp prosa.classic.analysis.uni.basic.fp_rta_theory.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path ssrfun.
Module ResponseTimeIterationFP.
Import Job SporadicTaskset UniprocessorSchedule WorkloadBoundFP Priority
ResponseTime Schedulability Platform TaskArrival ResponseTimeAnalysisFP.
Section Analysis.
Context {SporadicTask: eqType}.
Variable task_cost: SporadicTask → time.
Variable task_period: SporadicTask → time.
Variable task_deadline: 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 W := total_workload_bound_fp task_cost task_period higher_eq_priority.
Definition per_task_rta ts tsk :=
iter_fixpoint (W ts tsk) (max_steps tsk) (task_cost tsk).
Let is_valid_bound tsk_R :=
if tsk_R is (tsk, Some R) then
if 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.
Proof.
rename H_analysis_succeeds into SOME.
move: SOME; rewrite /fp_claimed_bounds.
case ALL: all; [case ⇒ SOME | by done].
move: ALL ⇒ /allP ALL.
have IN: (tsk, per_task_rta ts tsk) \in
[seq (tsk, per_task_rta ts tsk) | tsk <- ts];
first by apply/mapP; ∃ tsk.
specialize (ALL _ IN); move: ALL.
rewrite /is_valid_bound; case RTA: per_task_rta ⇒ [R|] //.
case DL: (R ≤ _); last by done.
move ⇒ _; ∃ R; rewrite -SOME.
rewrite mem_pmap; apply/mapP.
∃ (tsk, Some R); first by rewrite -RTA.
by rewrite /is_valid_bound DL.
Qed.
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.
Proof.
rename H_analysis_succeeds into SOME, H_tsk_R_computed into IN.
move: SOME; rewrite /fp_claimed_bounds.
case: all; [case ⇒ SOME | by done].
move: IN; rewrite -SOME mem_pmap.
move ⇒ /mapP [[tsk' someR]].
rewrite /is_valid_bound; case: someR; last by done.
move ⇒ R'; case: (R' ≤ _); last by done.
move ⇒ IN; case ⇒ EQ1 EQ2; subst tsk' R'.
by move: IN ⇒ /mapP [tsk' IN]; case; move ⇒ EQ1; subst tsk'.
Qed.
Lemma fp_claimed_bounds_computes_iteration:
per_task_rta ts tsk = Some R.
Proof.
rename H_analysis_succeeds into SOME, H_tsk_R_computed into IN.
move: SOME; rewrite /fp_claimed_bounds.
case: all; [case ⇒ SOME | by done].
move: IN; rewrite -SOME mem_pmap.
move ⇒ /mapP [[tsk' someR]].
rewrite /is_valid_bound; case: someR; last by done.
move ⇒ R'; case: (R' ≤ _); last by done.
move ⇒ IN; case ⇒ EQ1 EQ2; subst tsk' R'.
by move: IN ⇒ /mapP [tsk' IN]; case; move ⇒ EQ1 ->; subst tsk'.
Qed.
Lemma fp_claimed_bounds_yields_fixed_point :
R = W ts tsk R.
Proof.
rename H_analysis_succeeds into SOME, H_tsk_R_computed into IN.
move: SOME; rewrite /fp_claimed_bounds.
case: all; [case ⇒ SOME | by done].
move: IN; rewrite -SOME mem_pmap.
move ⇒ /mapP [[tsk' someR]].
rewrite /is_valid_bound; case: someR; last by done.
move ⇒ R'; case: (R' ≤ _); last by done.
move ⇒ IN; case ⇒ EQ1 EQ2; subst tsk' R'.
move: IN ⇒ /mapP [tsk' IN]; case; move ⇒ EQ1; subst tsk'.
move ⇒ RESP; symmetry in RESP; move: RESP.
rewrite /per_task_rta.
set f := W _ _; set s := max_steps _; set x0 := task_cost _.
case (iter_fixpoint_cases f s x0) ⇒ [NONE | [R' [SOME' EQ]]];
first by rewrite NONE.
by rewrite SOME'; case ⇒ H; subst.
Qed.
Lemma fp_claimed_bounds_le_deadline:
R ≤ task_deadline tsk.
Proof.
rename H_analysis_succeeds into SOME, H_tsk_R_computed into IN.
move: SOME; rewrite /fp_claimed_bounds.
case: all; [case ⇒ SOME | by done].
move: IN; rewrite -SOME mem_pmap.
move ⇒ /mapP [[tsk' someR]].
rewrite /is_valid_bound; case: someR; last by done.
move ⇒ R'; case LE: (R' ≤ _); last by done.
by move ⇒ IN; case ⇒ EQ1 EQ2; subst tsk' R'.
Qed.
Section BoundPositive.
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_gt_zero :
R > 0.
Proof.
set f := W ts tsk; set s := max_steps tsk; set x0 := task_cost tsk.
apply leq_trans with (n := task_cost tsk);
first by apply H_cost_positive.
have GE: task_cost tsk ≤ f (task_cost tsk).
{
apply total_workload_bound_fp_ge_cost; try (by done).
- by apply fp_claimed_bounds_from_taskset.
- by apply H_period_positive, fp_claimed_bounds_from_taskset.
}
have TRANS: transitive leq by rewrite /transitive;apply leq_trans.
have MON: monotone f leq.
{
by intros x1 x2 LE;
apply total_workload_bound_fp_non_decreasing.
}
apply leq_trans with (n := task_cost tsk); first by done.
try ( apply iter_fixpoint_ge_bottom with (f0 := f) (max_steps := s);
try (by done) ) ||
apply iter_fixpoint_ge_bottom with (f := f) (max_steps := s);
try (by done).
by apply fp_claimed_bounds_computes_iteration.
Qed.
End BoundPositive.
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.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → SporadicTask.
Variable ts: taskset_of SporadicTask.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_no_duplicate_arrivals: 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_valid_job_parameters:
∀ j,
arrives_in arr_seq j →
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period job_arrival job_task arr_seq.
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_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_work_conserving: work_conserving job_arrival job_cost arr_seq sched.
Hypothesis H_respects_FP_policy:
respects_FP_policy job_arrival job_cost 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 higher_eq_priority ts.
Let claimed_to_be_schedulable :=
fp_schedulable task_cost task_period task_deadline higher_eq_priority ts.
Theorem fp_analysis_yields_response_time_bounds :
∀ tsk R,
(tsk, R) \In RTA_claimed_bounds →
response_time_bounded_by tsk R.
Proof.
rename H_valid_task_parameters into PARAMS,
H_valid_job_parameters into JOBPARAMS.
unfold valid_sporadic_job, valid_realtime_job,
valid_sporadic_taskset, is_valid_sporadic_task in ×.
unfold RTA_claimed_bounds; intros tsk R.
case SOME: fp_claimed_bounds ⇒ [rt_bounds|] IN; last by done.
try ( apply uniprocessor_response_time_bound_fp with
(task_cost0 := task_cost) (task_period0 := task_period)
(ts0 := ts) (task_deadline0 := task_deadline)
(job_deadline0 := job_deadline)
(higher_eq_priority0 := higher_eq_priority); try (by done) ) ||
apply uniprocessor_response_time_bound_fp with
(task_cost := task_cost) (task_period := task_period)
(ts := ts) (task_deadline := task_deadline)
(job_deadline := job_deadline)
(higher_eq_priority := higher_eq_priority); try (by done).
{
( try ( apply fp_claimed_bounds_gt_zero with (task_cost0 := task_cost)
(task_period0 := task_period) (task_deadline0 := task_deadline)
(higher_eq_priority0 := higher_eq_priority) (ts0 := ts)
(rt_bounds0 := rt_bounds) (tsk0 := tsk) ) ||
apply fp_claimed_bounds_gt_zero with (task_cost := task_cost)
(task_period := task_period) (task_deadline := task_deadline)
(higher_eq_priority := higher_eq_priority) (ts := ts)
(rt_bounds := rt_bounds) (tsk := tsk)); try (by done).
{
feed (PARAMS tsk) ; last by move: PARAMS ⇒ [P1 _].
try ( by apply fp_claimed_bounds_from_taskset with
(task_cost0 := task_cost) (task_period0 := task_period)
(task_deadline0 := task_deadline) (rt_bounds0 := rt_bounds)
(higher_eq_priority0 := higher_eq_priority) (R0 := R) ) ||
by apply fp_claimed_bounds_from_taskset with
(task_cost := task_cost) (task_period := task_period)
(task_deadline := task_deadline) (rt_bounds := rt_bounds)
(higher_eq_priority := higher_eq_priority) (R := R).
}
by intros tsk0 IN0; specialize (PARAMS tsk0 IN0); des.
}
try ( by apply fp_claimed_bounds_yields_fixed_point with
(task_deadline0 := task_deadline) (rt_bounds0 := rt_bounds) ) ||
by apply fp_claimed_bounds_yields_fixed_point with
(task_deadline := task_deadline) (rt_bounds := rt_bounds).
Qed.
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.
Proof.
have RTA := fp_analysis_yields_response_time_bounds.
rename H_test_succeeds into TEST, H_valid_job_parameters into JOBPARAMS.
unfold claimed_to_be_schedulable, fp_schedulable in ×.
have RESP := fp_claimed_bounds_for_every_task task_cost task_period task_deadline
higher_eq_priority ts.
have DL := fp_claimed_bounds_le_deadline task_cost task_period task_deadline
higher_eq_priority ts.
move:TEST; case TEST:(fp_claimed_bounds _ _ _ _ _) ⇒ [rt_bounds|] _//.
intros tsk IN.
move: (RESP rt_bounds TEST tsk IN) ⇒ [R INbounds].
specialize (DL rt_bounds TEST tsk R INbounds).
( try ( apply task_completes_before_deadline with
(task_deadline0 := task_deadline) (R0 := R) ) ||
apply task_completes_before_deadline with
(task_deadline := task_deadline) (R := R)); try (by done);
first by intros j ARRj; specialize (JOBPARAMS j ARRj); move: JOBPARAMS ⇒ [_ [_ EQ]].
by apply RTA; rewrite /RTA_claimed_bounds TEST.
Qed.
Theorem jobs_schedulable_by_fp_rta :
∀ j,
arrives_in arr_seq j →
no_deadline_missed_by_job j.
Proof.
intros j ARRj.
have SCHED := taskset_schedulable_by_fp_rta.
unfold no_deadline_missed_by_task, task_misses_no_deadline in ×.
apply SCHED with (tsk := job_task j); try (by done).
by apply H_all_jobs_from_taskset.
Qed.
End AnalysisIsSufficient.
End ProvingCorrectness.
End ResponseTimeIterationFP.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.arrival_sequence prosa.classic.model.priority
prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.schedule.uni.schedule prosa.classic.model.schedule.uni.schedulability prosa.classic.model.schedule.uni.response_time.
Require Import prosa.classic.model.schedule.uni.basic.platform.
Require Import prosa.classic.analysis.uni.basic.workload_bound_fp prosa.classic.analysis.uni.basic.fp_rta_theory.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path ssrfun.
Module ResponseTimeIterationFP.
Import Job SporadicTaskset UniprocessorSchedule WorkloadBoundFP Priority
ResponseTime Schedulability Platform TaskArrival ResponseTimeAnalysisFP.
Section Analysis.
Context {SporadicTask: eqType}.
Variable task_cost: SporadicTask → time.
Variable task_period: SporadicTask → time.
Variable task_deadline: 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 W := total_workload_bound_fp task_cost task_period higher_eq_priority.
Definition per_task_rta ts tsk :=
iter_fixpoint (W ts tsk) (max_steps tsk) (task_cost tsk).
Let is_valid_bound tsk_R :=
if tsk_R is (tsk, Some R) then
if 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.
Proof.
rename H_analysis_succeeds into SOME.
move: SOME; rewrite /fp_claimed_bounds.
case ALL: all; [case ⇒ SOME | by done].
move: ALL ⇒ /allP ALL.
have IN: (tsk, per_task_rta ts tsk) \in
[seq (tsk, per_task_rta ts tsk) | tsk <- ts];
first by apply/mapP; ∃ tsk.
specialize (ALL _ IN); move: ALL.
rewrite /is_valid_bound; case RTA: per_task_rta ⇒ [R|] //.
case DL: (R ≤ _); last by done.
move ⇒ _; ∃ R; rewrite -SOME.
rewrite mem_pmap; apply/mapP.
∃ (tsk, Some R); first by rewrite -RTA.
by rewrite /is_valid_bound DL.
Qed.
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.
Proof.
rename H_analysis_succeeds into SOME, H_tsk_R_computed into IN.
move: SOME; rewrite /fp_claimed_bounds.
case: all; [case ⇒ SOME | by done].
move: IN; rewrite -SOME mem_pmap.
move ⇒ /mapP [[tsk' someR]].
rewrite /is_valid_bound; case: someR; last by done.
move ⇒ R'; case: (R' ≤ _); last by done.
move ⇒ IN; case ⇒ EQ1 EQ2; subst tsk' R'.
by move: IN ⇒ /mapP [tsk' IN]; case; move ⇒ EQ1; subst tsk'.
Qed.
Lemma fp_claimed_bounds_computes_iteration:
per_task_rta ts tsk = Some R.
Proof.
rename H_analysis_succeeds into SOME, H_tsk_R_computed into IN.
move: SOME; rewrite /fp_claimed_bounds.
case: all; [case ⇒ SOME | by done].
move: IN; rewrite -SOME mem_pmap.
move ⇒ /mapP [[tsk' someR]].
rewrite /is_valid_bound; case: someR; last by done.
move ⇒ R'; case: (R' ≤ _); last by done.
move ⇒ IN; case ⇒ EQ1 EQ2; subst tsk' R'.
by move: IN ⇒ /mapP [tsk' IN]; case; move ⇒ EQ1 ->; subst tsk'.
Qed.
Lemma fp_claimed_bounds_yields_fixed_point :
R = W ts tsk R.
Proof.
rename H_analysis_succeeds into SOME, H_tsk_R_computed into IN.
move: SOME; rewrite /fp_claimed_bounds.
case: all; [case ⇒ SOME | by done].
move: IN; rewrite -SOME mem_pmap.
move ⇒ /mapP [[tsk' someR]].
rewrite /is_valid_bound; case: someR; last by done.
move ⇒ R'; case: (R' ≤ _); last by done.
move ⇒ IN; case ⇒ EQ1 EQ2; subst tsk' R'.
move: IN ⇒ /mapP [tsk' IN]; case; move ⇒ EQ1; subst tsk'.
move ⇒ RESP; symmetry in RESP; move: RESP.
rewrite /per_task_rta.
set f := W _ _; set s := max_steps _; set x0 := task_cost _.
case (iter_fixpoint_cases f s x0) ⇒ [NONE | [R' [SOME' EQ]]];
first by rewrite NONE.
by rewrite SOME'; case ⇒ H; subst.
Qed.
Lemma fp_claimed_bounds_le_deadline:
R ≤ task_deadline tsk.
Proof.
rename H_analysis_succeeds into SOME, H_tsk_R_computed into IN.
move: SOME; rewrite /fp_claimed_bounds.
case: all; [case ⇒ SOME | by done].
move: IN; rewrite -SOME mem_pmap.
move ⇒ /mapP [[tsk' someR]].
rewrite /is_valid_bound; case: someR; last by done.
move ⇒ R'; case LE: (R' ≤ _); last by done.
by move ⇒ IN; case ⇒ EQ1 EQ2; subst tsk' R'.
Qed.
Section BoundPositive.
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_gt_zero :
R > 0.
Proof.
set f := W ts tsk; set s := max_steps tsk; set x0 := task_cost tsk.
apply leq_trans with (n := task_cost tsk);
first by apply H_cost_positive.
have GE: task_cost tsk ≤ f (task_cost tsk).
{
apply total_workload_bound_fp_ge_cost; try (by done).
- by apply fp_claimed_bounds_from_taskset.
- by apply H_period_positive, fp_claimed_bounds_from_taskset.
}
have TRANS: transitive leq by rewrite /transitive;apply leq_trans.
have MON: monotone f leq.
{
by intros x1 x2 LE;
apply total_workload_bound_fp_non_decreasing.
}
apply leq_trans with (n := task_cost tsk); first by done.
try ( apply iter_fixpoint_ge_bottom with (f0 := f) (max_steps := s);
try (by done) ) ||
apply iter_fixpoint_ge_bottom with (f := f) (max_steps := s);
try (by done).
by apply fp_claimed_bounds_computes_iteration.
Qed.
End BoundPositive.
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.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → SporadicTask.
Variable ts: taskset_of SporadicTask.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_no_duplicate_arrivals: 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_valid_job_parameters:
∀ j,
arrives_in arr_seq j →
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period job_arrival job_task arr_seq.
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_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_work_conserving: work_conserving job_arrival job_cost arr_seq sched.
Hypothesis H_respects_FP_policy:
respects_FP_policy job_arrival job_cost 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 higher_eq_priority ts.
Let claimed_to_be_schedulable :=
fp_schedulable task_cost task_period task_deadline higher_eq_priority ts.
Theorem fp_analysis_yields_response_time_bounds :
∀ tsk R,
(tsk, R) \In RTA_claimed_bounds →
response_time_bounded_by tsk R.
Proof.
rename H_valid_task_parameters into PARAMS,
H_valid_job_parameters into JOBPARAMS.
unfold valid_sporadic_job, valid_realtime_job,
valid_sporadic_taskset, is_valid_sporadic_task in ×.
unfold RTA_claimed_bounds; intros tsk R.
case SOME: fp_claimed_bounds ⇒ [rt_bounds|] IN; last by done.
try ( apply uniprocessor_response_time_bound_fp with
(task_cost0 := task_cost) (task_period0 := task_period)
(ts0 := ts) (task_deadline0 := task_deadline)
(job_deadline0 := job_deadline)
(higher_eq_priority0 := higher_eq_priority); try (by done) ) ||
apply uniprocessor_response_time_bound_fp with
(task_cost := task_cost) (task_period := task_period)
(ts := ts) (task_deadline := task_deadline)
(job_deadline := job_deadline)
(higher_eq_priority := higher_eq_priority); try (by done).
{
( try ( apply fp_claimed_bounds_gt_zero with (task_cost0 := task_cost)
(task_period0 := task_period) (task_deadline0 := task_deadline)
(higher_eq_priority0 := higher_eq_priority) (ts0 := ts)
(rt_bounds0 := rt_bounds) (tsk0 := tsk) ) ||
apply fp_claimed_bounds_gt_zero with (task_cost := task_cost)
(task_period := task_period) (task_deadline := task_deadline)
(higher_eq_priority := higher_eq_priority) (ts := ts)
(rt_bounds := rt_bounds) (tsk := tsk)); try (by done).
{
feed (PARAMS tsk) ; last by move: PARAMS ⇒ [P1 _].
try ( by apply fp_claimed_bounds_from_taskset with
(task_cost0 := task_cost) (task_period0 := task_period)
(task_deadline0 := task_deadline) (rt_bounds0 := rt_bounds)
(higher_eq_priority0 := higher_eq_priority) (R0 := R) ) ||
by apply fp_claimed_bounds_from_taskset with
(task_cost := task_cost) (task_period := task_period)
(task_deadline := task_deadline) (rt_bounds := rt_bounds)
(higher_eq_priority := higher_eq_priority) (R := R).
}
by intros tsk0 IN0; specialize (PARAMS tsk0 IN0); des.
}
try ( by apply fp_claimed_bounds_yields_fixed_point with
(task_deadline0 := task_deadline) (rt_bounds0 := rt_bounds) ) ||
by apply fp_claimed_bounds_yields_fixed_point with
(task_deadline := task_deadline) (rt_bounds := rt_bounds).
Qed.
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.
Proof.
have RTA := fp_analysis_yields_response_time_bounds.
rename H_test_succeeds into TEST, H_valid_job_parameters into JOBPARAMS.
unfold claimed_to_be_schedulable, fp_schedulable in ×.
have RESP := fp_claimed_bounds_for_every_task task_cost task_period task_deadline
higher_eq_priority ts.
have DL := fp_claimed_bounds_le_deadline task_cost task_period task_deadline
higher_eq_priority ts.
move:TEST; case TEST:(fp_claimed_bounds _ _ _ _ _) ⇒ [rt_bounds|] _//.
intros tsk IN.
move: (RESP rt_bounds TEST tsk IN) ⇒ [R INbounds].
specialize (DL rt_bounds TEST tsk R INbounds).
( try ( apply task_completes_before_deadline with
(task_deadline0 := task_deadline) (R0 := R) ) ||
apply task_completes_before_deadline with
(task_deadline := task_deadline) (R := R)); try (by done);
first by intros j ARRj; specialize (JOBPARAMS j ARRj); move: JOBPARAMS ⇒ [_ [_ EQ]].
by apply RTA; rewrite /RTA_claimed_bounds TEST.
Qed.
Theorem jobs_schedulable_by_fp_rta :
∀ j,
arrives_in arr_seq j →
no_deadline_missed_by_job j.
Proof.
intros j ARRj.
have SCHED := taskset_schedulable_by_fp_rta.
unfold no_deadline_missed_by_task, task_misses_no_deadline in ×.
apply SCHED with (tsk := job_task j); try (by done).
by apply H_all_jobs_from_taskset.
Qed.
End AnalysisIsSufficient.
End ProvingCorrectness.
End ResponseTimeIterationFP.