Commit 266c9014 authored by Felipe Cerqueira's avatar Felipe Cerqueira
Browse files

Replace nat with time + clean-up code

parent 179ca8e4
...@@ -14,7 +14,7 @@ ...@@ -14,7 +14,7 @@
# #
# This Makefile was generated by the command line : # This Makefile was generated by the command line :
# coq_makefile -R . rt ./util/ssromega.v ./util/lemmas.v ./util/Vbase.v ./util/divround.v ./implementation/basic/bertogna_edf_example.v ./implementation/basic/task.v ./implementation/basic/schedule.v ./implementation/basic/job.v ./implementation/basic/arrival_sequence.v ./implementation/jitter/bertogna_edf_example.v ./implementation/jitter/task.v ./implementation/jitter/schedule.v ./implementation/jitter/job.v ./implementation/jitter/arrival_sequence.v ./analysis/basic/bertogna_fp_theory.v ./analysis/basic/interference_bound_edf.v ./analysis/basic/interference_bound_fp.v ./analysis/basic/interference_bound.v ./analysis/basic/bertogna_edf_comp.v ./analysis/basic/bertogna_fp_comp.v ./analysis/basic/bertogna_edf_theory.v ./analysis/basic/workload_bound.v ./analysis/parallel/bertogna_fp_theory.v ./analysis/parallel/interference_bound_edf.v ./analysis/parallel/interference_bound_fp.v ./analysis/parallel/interference_bound.v ./analysis/parallel/bertogna_edf_comp.v ./analysis/parallel/bertogna_fp_comp.v ./analysis/parallel/bertogna_edf_theory.v ./analysis/parallel/workload_bound.v ./analysis/jitter/bertogna_fp_theory.v ./analysis/jitter/interference_bound_edf.v ./analysis/jitter/interference_bound_fp.v ./analysis/jitter/interference_bound.v ./analysis/jitter/bertogna_edf_comp.v ./analysis/jitter/bertogna_fp_comp.v ./analysis/jitter/bertogna_edf_theory.v ./analysis/jitter/workload_bound.v ./model/basic/schedulability.v ./model/basic/task.v ./model/basic/task_arrival.v ./model/basic/platform.v ./model/basic/schedule.v ./model/basic/priority.v ./model/basic/interference_edf.v ./model/basic/interference.v ./model/basic/workload.v ./model/basic/job.v ./model/basic/arrival_sequence.v ./model/basic/response_time.v ./model/basic/platform_fp.v ./model/jitter/schedulability.v ./model/jitter/task.v ./model/jitter/task_arrival.v ./model/jitter/platform.v ./model/jitter/schedule.v ./model/jitter/priority.v ./model/jitter/interference_edf.v ./model/jitter/interference.v ./model/jitter/workload.v ./model/jitter/job.v ./model/jitter/arrival_sequence.v ./model/jitter/response_time.v ./model/jitter/platform_fp.v -o Makefile # coq_makefile -R . rt ./util/ssromega.v ./util/lemmas.v ./util/Vbase.v ./util/divround.v ./implementation/basic/bertogna_edf_example.v ./implementation/basic/task.v ./implementation/basic/schedule.v ./implementation/basic/job.v ./implementation/basic/arrival_sequence.v ./implementation/jitter/bertogna_edf_example.v ./implementation/jitter/task.v ./implementation/jitter/schedule.v ./implementation/jitter/job.v ./implementation/jitter/arrival_sequence.v ./analysis/basic/bertogna_fp_theory.v ./analysis/basic/interference_bound_edf.v ./analysis/basic/interference_bound_fp.v ./analysis/basic/interference_bound.v ./analysis/basic/bertogna_edf_comp.v ./analysis/basic/bertogna_fp_comp.v ./analysis/basic/bertogna_edf_theory.v ./analysis/basic/workload_bound.v ./analysis/parallel/bertogna_fp_theory.v ./analysis/parallel/interference_bound_edf.v ./analysis/parallel/interference_bound_fp.v ./analysis/parallel/interference_bound.v ./analysis/parallel/bertogna_edf_comp.v ./analysis/parallel/bertogna_fp_comp.v ./analysis/parallel/bertogna_edf_theory.v ./analysis/parallel/workload_bound.v ./analysis/jitter/bertogna_fp_theory.v ./analysis/jitter/interference_bound_edf.v ./analysis/jitter/interference_bound_fp.v ./analysis/jitter/interference_bound.v ./analysis/jitter/bertogna_edf_comp.v ./analysis/jitter/bertogna_fp_comp.v ./analysis/jitter/bertogna_edf_theory.v ./analysis/jitter/workload_bound.v ./model/basic/time.v ./model/basic/schedulability.v ./model/basic/task.v ./model/basic/task_arrival.v ./model/basic/platform.v ./model/basic/schedule.v ./model/basic/priority.v ./model/basic/interference_edf.v ./model/basic/interference.v ./model/basic/workload.v ./model/basic/job.v ./model/basic/arrival_sequence.v ./model/basic/response_time.v ./model/basic/platform_fp.v ./model/jitter/time.v ./model/jitter/schedulability.v ./model/jitter/task.v ./model/jitter/task_arrival.v ./model/jitter/platform.v ./model/jitter/schedule.v ./model/jitter/priority.v ./model/jitter/interference_edf.v ./model/jitter/interference.v ./model/jitter/workload.v ./model/jitter/job.v ./model/jitter/arrival_sequence.v ./model/jitter/response_time.v ./model/jitter/platform_fp.v -o Makefile
# #
.DEFAULT_GOAL := all .DEFAULT_GOAL := all
...@@ -118,6 +118,7 @@ VFILES:=util/ssromega.v\ ...@@ -118,6 +118,7 @@ VFILES:=util/ssromega.v\
analysis/jitter/bertogna_fp_comp.v\ analysis/jitter/bertogna_fp_comp.v\
analysis/jitter/bertogna_edf_theory.v\ analysis/jitter/bertogna_edf_theory.v\
analysis/jitter/workload_bound.v\ analysis/jitter/workload_bound.v\
model/basic/time.v\
model/basic/schedulability.v\ model/basic/schedulability.v\
model/basic/task.v\ model/basic/task.v\
model/basic/task_arrival.v\ model/basic/task_arrival.v\
...@@ -131,6 +132,7 @@ VFILES:=util/ssromega.v\ ...@@ -131,6 +132,7 @@ VFILES:=util/ssromega.v\
model/basic/arrival_sequence.v\ model/basic/arrival_sequence.v\
model/basic/response_time.v\ model/basic/response_time.v\
model/basic/platform_fp.v\ model/basic/platform_fp.v\
model/jitter/time.v\
model/jitter/schedulability.v\ model/jitter/schedulability.v\
model/jitter/task.v\ model/jitter/task.v\
model/jitter/task_arrival.v\ model/jitter/task_arrival.v\
......
...@@ -7,22 +7,22 @@ Module ResponseTimeIterationEDF. ...@@ -7,22 +7,22 @@ Module ResponseTimeIterationEDF.
Import ResponseTimeAnalysisEDF. Import ResponseTimeAnalysisEDF.
(* In this section, we define the algorithm of Bertogna and Cirinei's (* In this section, we define the algorithm for Bertogna and Cirinei's
response-time analysis for EDF scheduling. *) response-time analysis for EDF scheduling. *)
Section Analysis. Section Analysis.
Context {sporadic_task: eqType}. Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task -> nat. Variable task_cost: sporadic_task -> time.
Variable task_period: sporadic_task -> nat. Variable task_period: sporadic_task -> time.
Variable task_deadline: sporadic_task -> nat. Variable task_deadline: sporadic_task -> time.
(* During the iterations of the algorithm, we pass around pairs (* As input for each iteration of the algorithm, we consider pairs
of tasks and computed response-time bounds. *) of tasks and computed response-time bounds. *)
Let task_with_response_time := (sporadic_task * nat)%type. Let task_with_response_time := (sporadic_task * time)%type.
Context {Job: eqType}. Context {Job: eqType}.
Variable job_cost: Job -> nat. Variable job_cost: Job -> time.
Variable job_deadline: Job -> nat. Variable job_deadline: Job -> time.
Variable job_task: Job -> sporadic_task. Variable job_task: Job -> sporadic_task.
(* Consider a platform with num_cpus processors. *) (* Consider a platform with num_cpus processors. *)
...@@ -66,16 +66,15 @@ Module ResponseTimeIterationEDF. ...@@ -66,16 +66,15 @@ Module ResponseTimeIterationEDF.
Definition edf_rta_iteration (rt_bounds: seq task_with_response_time) := Definition edf_rta_iteration (rt_bounds: seq task_with_response_time) :=
map (update_bound rt_bounds) rt_bounds. map (update_bound rt_bounds) rt_bounds.
(* To ensure that the procedure converges, we run the iteration a (* To ensure that the procedure converges, we stop the iteration
"sufficient" number of times: task_deadline tsk - task_cost tsk + 1. after a "sufficient" number of times, which corresponds to
This corresponds to the time complexity of the procedure. *) the time complexity of the procedure. *)
Let max_steps (ts: taskset_of sporadic_task) := Let max_steps (ts: taskset_of sporadic_task) :=
\sum_(tsk <- ts) (task_deadline tsk - task_cost tsk) + 1. \sum_(tsk <- ts) (task_deadline tsk - task_cost tsk) + 1.
(* This yields the following definition for the RTA. At the end of (* This yields the following definition for the RTA. At the end
the iteration, we check if all computed response-time bounds we check if all computed response-time bounds are less than
are less than or equal to the deadline, in which case they are or equal to the deadline, in which case they are valid. *)
valid. *)
Definition edf_claimed_bounds (ts: taskset_of sporadic_task) := Definition edf_claimed_bounds (ts: taskset_of sporadic_task) :=
let R_values := iter (max_steps ts) edf_rta_iteration (initial_state ts) in let R_values := iter (max_steps ts) edf_rta_iteration (initial_state ts) in
if (all R_le_deadline R_values) then if (all R_le_deadline R_values) then
...@@ -368,7 +367,7 @@ Module ResponseTimeIterationEDF. ...@@ -368,7 +367,7 @@ Module ResponseTimeIterationEDF.
rewrite (nth_map p0); rewrite (nth_map p0);
last by rewrite size_zip 2!size_map SIZE minnn in LTi. last by rewrite size_zip 2!size_map SIZE minnn in LTi.
unfold update_bound, edf_response_time_bound; desf; simpl. unfold update_bound, edf_response_time_bound; desf; simpl.
rename s into tsk_i, s0 into tsk_i', n into R_i, n0 into R_i', Heq into EQ, Heq0 into EQ'. rename s into tsk_i, s0 into tsk_i', t into R_i, t0 into R_i', Heq into EQ, Heq0 into EQ'.
assert (EQtsk: tsk_i = tsk_i'). assert (EQtsk: tsk_i = tsk_i').
{ {
destruct p0 as [tsk0 R0], p0' as [tsk0' R0']; simpl in H2; subst. destruct p0 as [tsk0 R0], p0' as [tsk0' R0']; simpl in H2; subst.
...@@ -481,7 +480,9 @@ Module ResponseTimeIterationEDF. ...@@ -481,7 +480,9 @@ Module ResponseTimeIterationEDF.
by rewrite in_cons; apply/orP; right; rewrite mem_nth. by rewrite in_cons; apply/orP; right; rewrite mem_nth.
} }
unfold is_valid_sporadic_task in *. unfold is_valid_sporadic_task in *.
destruct (nth elem x1' j) as [tsk_j R_j], (nth elem x2' j) as [tsk_j' R_j']. destruct (nth elem x1' j) as [tsk_j R_j] eqn:SUBST1,
(nth elem x2' j) as [tsk_j' R_j'] eqn:SUBST2.
rewrite SUBST1 SUBST2 in LEj; clear SUBST1 SUBST2.
simpl in FSTeq; rewrite -FSTeq; simpl in LEj; simpl in VALIDj; des. simpl in FSTeq; rewrite -FSTeq; simpl in LEj; simpl in VALIDj; des.
by apply interference_bound_edf_monotonic. by apply interference_bound_edf_monotonic.
} }
...@@ -658,7 +659,7 @@ Module ResponseTimeIterationEDF. ...@@ -658,7 +659,7 @@ Module ResponseTimeIterationEDF.
unfold update_bound; destruct i; simpl. unfold update_bound; destruct i; simpl.
rewrite subh1; first by rewrite -addnBA // subnn addn0. rewrite subh1; first by rewrite -addnBA // subnn addn0.
apply (edf_claimed_bounds_ge_cost ts step.+1). apply (edf_claimed_bounds_ge_cost ts step.+1).
by rewrite iterS; apply/mapP; exists (s, n). by rewrite iterS; apply/mapP; exists (s, t).
} }
rewrite -2!big_seq_cond. rewrite -2!big_seq_cond.
......
...@@ -18,13 +18,13 @@ Module ResponseTimeAnalysisEDF. ...@@ -18,13 +18,13 @@ Module ResponseTimeAnalysisEDF.
Section ResponseTimeBound. Section ResponseTimeBound.
Context {sporadic_task: eqType}. Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task -> nat. Variable task_cost: sporadic_task -> time.
Variable task_period: sporadic_task -> nat. Variable task_period: sporadic_task -> time.
Variable task_deadline: sporadic_task -> nat. Variable task_deadline: sporadic_task -> time.
Context {Job: eqType}. Context {Job: eqType}.
Variable job_cost: Job -> nat. Variable job_cost: Job -> time.
Variable job_deadline: Job -> nat. Variable job_deadline: Job -> time.
Variable job_task: Job -> sporadic_task. Variable job_task: Job -> sporadic_task.
(* Assume any job arrival sequence... *) (* Assume any job arrival sequence... *)
...@@ -56,28 +56,30 @@ Module ResponseTimeAnalysisEDF. ...@@ -56,28 +56,30 @@ Module ResponseTimeAnalysisEDF.
num_cpus > 0. num_cpus > 0.
(* Assume that we have a task set where all tasks have valid (* Assume that we have a task set where all tasks have valid
parameters and restricted deadlines. *) parameters and restricted deadlines, ... *)
Variable ts: taskset_of sporadic_task. Variable ts: taskset_of sporadic_task.
Hypothesis H_all_jobs_from_taskset:
forall (j: JobIn arr_seq), job_task j \in ts.
Hypothesis H_valid_task_parameters: Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts. valid_sporadic_taskset task_cost task_period task_deadline ts.
Hypothesis H_restricted_deadlines: Hypothesis H_restricted_deadlines:
forall tsk, tsk \in ts -> task_deadline tsk <= task_period tsk. forall tsk, tsk \in ts -> task_deadline tsk <= task_period tsk.
(* ... and that all jobs in the arrival sequence come from the task set. *)
Hypothesis H_all_jobs_from_taskset:
forall (j: JobIn arr_seq), job_task j \in ts.
Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) := Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
task_misses_no_deadline job_cost job_deadline job_task sched tsk. task_misses_no_deadline job_cost job_deadline job_task sched tsk.
Let response_time_bounded_by (tsk: sporadic_task) := Let response_time_bounded_by (tsk: sporadic_task) :=
is_response_time_bound_of_task job_cost job_task tsk sched. is_response_time_bound_of_task job_cost job_task tsk sched.
(* Assume a known response-time bound R is known... *) (* Assume that a response-time bound R is known... *)
Let task_with_response_time := (sporadic_task * time)%type. Let task_with_response_time := (sporadic_task * time)%type.
Variable rt_bounds: seq task_with_response_time. Variable rt_bounds: seq task_with_response_time.
(* ...for any task in the task set. *) (* ...for any task in the task set, ... *)
Hypothesis H_rt_bounds_contains_all_tasks: unzip1 rt_bounds = ts. Hypothesis H_rt_bounds_contains_all_tasks: unzip1 rt_bounds = ts.
(* Also, assume that R is a fixed-point of the response-time recurrence, ... *) (* ... such that R is a fixed-point of the response-time recurrence, ... *)
Let I (tsk: sporadic_task) (delta: time) := Let I (tsk: sporadic_task) (delta: time) :=
total_interference_bound_edf task_cost task_period task_deadline tsk rt_bounds delta. total_interference_bound_edf task_cost task_period task_deadline tsk rt_bounds delta.
Hypothesis H_response_time_is_fixed_point : Hypothesis H_response_time_is_fixed_point :
...@@ -94,10 +96,9 @@ Module ResponseTimeAnalysisEDF. ...@@ -94,10 +96,9 @@ Module ResponseTimeAnalysisEDF.
Hypothesis H_work_conserving: work_conserving job_cost sched. Hypothesis H_work_conserving: work_conserving job_cost sched.
Hypothesis H_edf_policy: enforces_JLDP_policy job_cost sched (EDF job_deadline). Hypothesis H_edf_policy: enforces_JLDP_policy job_cost sched (EDF job_deadline).
(* Assume that the task set has no duplicates. Otherwise, counting (* Assume that the task set has no duplicates. This is required to
the number of tasks that have some property does not make sense avoid problems when counting tasks (for example, when stating
(for example, for stating the global scheduling invariant as that the number of interfering tasks is at most num_cpus). *)
using number of scheduled interfering tasks = number of cpus). *)
Hypothesis H_ts_is_a_set : uniq ts. Hypothesis H_ts_is_a_set : uniq ts.
(* In order to prove that R is a response-time bound, we first present some lemmas. *) (* In order to prove that R is a response-time bound, we first present some lemmas. *)
...@@ -108,14 +109,14 @@ Module ResponseTimeAnalysisEDF. ...@@ -108,14 +109,14 @@ Module ResponseTimeAnalysisEDF.
Variable R: time. Variable R: time.
Hypothesis H_tsk_R_in_rt_bounds: (tsk, R) \in rt_bounds. Hypothesis H_tsk_R_in_rt_bounds: (tsk, R) \in rt_bounds.
(* Consider any job j of tsk. *) (* Consider any job j of tsk ... *)
Variable j: JobIn arr_seq. Variable j: JobIn arr_seq.
Hypothesis H_job_of_tsk: job_task j = tsk. Hypothesis H_job_of_tsk: job_task j = tsk.
(* Assume that job j did not complete on time, ... *) (* ... that did not complete on time, ... *)
Hypothesis H_j_not_completed: ~~ completed job_cost sched j (job_arrival j + R). Hypothesis H_j_not_completed: ~~ completed job_cost sched j (job_arrival j + R).
(* and that it is the first job not to satisfy its response-time bound. *) (* ... and that is the first job not to satisfy its response-time bound. *)
Hypothesis H_all_previous_jobs_completed_on_time : Hypothesis H_all_previous_jobs_completed_on_time :
forall (j_other: JobIn arr_seq) tsk_other R_other, forall (j_other: JobIn arr_seq) tsk_other R_other,
job_task j_other = tsk_other -> job_task j_other = tsk_other ->
...@@ -154,13 +155,13 @@ Module ResponseTimeAnalysisEDF. ...@@ -154,13 +155,13 @@ Module ResponseTimeAnalysisEDF.
Variable R_other: time. Variable R_other: time.
Hypothesis H_response_time_of_tsk_other: (tsk_other, R_other) \in rt_bounds. Hypothesis H_response_time_of_tsk_other: (tsk_other, R_other) \in rt_bounds.
(* Note that tsk_other is in task set ts ...*) (* Note that tsk_other is in the task set, ...*)
Lemma bertogna_edf_tsk_other_in_ts: tsk_other \in ts. Lemma bertogna_edf_tsk_other_in_ts: tsk_other \in ts.
Proof. Proof.
by rewrite -H_rt_bounds_contains_all_tasks; apply/mapP; exists (tsk_other, R_other). by rewrite -H_rt_bounds_contains_all_tasks; apply/mapP; exists (tsk_other, R_other).
Qed. Qed.
(* Also, R_other is larger than the cost of tsk_other. *) (* ... and R_other is larger than the cost of tsk_other. *)
Lemma bertogna_edf_R_other_ge_cost : Lemma bertogna_edf_R_other_ge_cost :
R_other >= task_cost tsk_other. R_other >= task_cost tsk_other.
Proof. Proof.
...@@ -193,7 +194,7 @@ Module ResponseTimeAnalysisEDF. ...@@ -193,7 +194,7 @@ Module ResponseTimeAnalysisEDF.
| by ins; apply BEFOREok with (tsk_other := tsk_other)]. | by ins; apply BEFOREok with (tsk_other := tsk_other)].
Qed. Qed.
(* Recall that the edf-specific interference bound also holds. *) (* Recall that the edf-specific interference bound also holds for tsk_other. *)
Lemma bertogna_edf_specific_bound_holds : Lemma bertogna_edf_specific_bound_holds :
x tsk_other <= edf_specific_bound tsk_other R_other. x tsk_other <= edf_specific_bound tsk_other R_other.
Proof. Proof.
...@@ -210,7 +211,6 @@ Module ResponseTimeAnalysisEDF. ...@@ -210,7 +211,6 @@ Module ResponseTimeAnalysisEDF.
(* Next we prove some lemmas that help to derive a contradiction.*) (* Next we prove some lemmas that help to derive a contradiction.*)
Section DerivingContradiction. Section DerivingContradiction.
(* 0) Since job j did not complete by its response time bound, it follows that (* 0) Since job j did not complete by its response time bound, it follows that
the total interference X >= R - e_k + 1. *) the total interference X >= R - e_k + 1. *)
Lemma bertogna_edf_too_much_interference : X >= R - task_cost tsk + 1. Lemma bertogna_edf_too_much_interference : X >= R - task_cost tsk + 1.
......
...@@ -12,17 +12,17 @@ Module ResponseTimeIterationFP. ...@@ -12,17 +12,17 @@ Module ResponseTimeIterationFP.
Section Analysis. Section Analysis.
Context {sporadic_task: eqType}. Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task -> nat. Variable task_cost: sporadic_task -> time.
Variable task_period: sporadic_task -> nat. Variable task_period: sporadic_task -> time.
Variable task_deadline: sporadic_task -> nat. Variable task_deadline: sporadic_task -> time.
(* During the iterations of the algorithm, we pass around pairs (* As input for each iteration of the algorithm, we consider pairs
of tasks and computed response-time bounds. *) of tasks and computed response-time bounds. *)
Let task_with_response_time := (sporadic_task * nat)%type. Let task_with_response_time := (sporadic_task * time)%type.
Context {Job: eqType}. Context {Job: eqType}.
Variable job_cost: Job -> nat. Variable job_cost: Job -> time.
Variable job_deadline: Job -> nat. Variable job_deadline: Job -> time.
Variable job_task: Job -> sporadic_task. Variable job_task: Job -> sporadic_task.
(* Consider a platform with num_cpus processors, ... *) (* Consider a platform with num_cpus processors, ... *)
...@@ -177,7 +177,7 @@ Module ResponseTimeIterationFP. ...@@ -177,7 +177,7 @@ Module ResponseTimeIterationFP.
Qed. Qed.
(* If the analysis suceeds, the computed response-time bounds are no larger (* If the analysis suceeds, the computed response-time bounds are no larger
than the deadline. *) than the deadlines ... *)
Lemma fp_claimed_bounds_le_deadline : Lemma fp_claimed_bounds_le_deadline :
forall ts' rt_bounds tsk R, forall ts' rt_bounds tsk R,
fp_claimed_bounds ts' = Some rt_bounds -> fp_claimed_bounds ts' = Some rt_bounds ->
...@@ -215,8 +215,7 @@ Module ResponseTimeIterationFP. ...@@ -215,8 +215,7 @@ Module ResponseTimeIterationFP.
} }
Qed. Qed.
(* If the analysis succeeds, the computed response-time bounds are no smaller (* ... and no smaller than the task costs. *)
than the task cost. *)
Lemma fp_claimed_bounds_ge_cost : Lemma fp_claimed_bounds_ge_cost :
forall ts' rt_bounds tsk R, forall ts' rt_bounds tsk R,
fp_claimed_bounds ts' = Some rt_bounds -> fp_claimed_bounds ts' = Some rt_bounds ->
...@@ -412,7 +411,7 @@ Module ResponseTimeIterationFP. ...@@ -412,7 +411,7 @@ Module ResponseTimeIterationFP.
} }
Qed. Qed.
(* If the iteration converged at an earlier step, then it remains stable. *) (* If the iteration converged at an earlier step, it remains as a fixed point. *)
Lemma bertogna_fp_comp_f_converges_early : Lemma bertogna_fp_comp_f_converges_early :
(exists k, k <= max_steps tsk /\ f k = f k.+1) -> (exists k, k <= max_steps tsk /\ f k = f k.+1) ->
f (max_steps tsk) = f (max_steps tsk).+1. f (max_steps tsk) = f (max_steps tsk).+1.
...@@ -517,10 +516,9 @@ Module ResponseTimeIterationFP. ...@@ -517,10 +516,9 @@ Module ResponseTimeIterationFP.
Variable ts: taskset_of sporadic_task. Variable ts: taskset_of sporadic_task.
(* Assume that higher_priority is a total strict order (<). (* Assume that higher_priority is a total strict order (<).
TODO: it doesn't have to be total over the entire domain, but TODO: it doesn't have to be total over the universe of tasks,
only within the task set. but only within the task set. However, to weaken this hypothesis
But to weaken the hypothesis, we need to re-prove some lemmas we need to re-prove some lemmas from ssreflect. *)
from ssreflect. *)
Hypothesis H_irreflexive: irreflexive higher_priority. Hypothesis H_irreflexive: irreflexive higher_priority.
Hypothesis H_transitive: transitive higher_priority. Hypothesis H_transitive: transitive higher_priority.
Hypothesis H_unique_priorities: antisymmetric higher_priority. Hypothesis H_unique_priorities: antisymmetric higher_priority.
...@@ -547,7 +545,7 @@ Module ResponseTimeIterationFP. ...@@ -547,7 +545,7 @@ Module ResponseTimeIterationFP.
Hypothesis H_all_jobs_from_taskset: Hypothesis H_all_jobs_from_taskset:
forall (j: JobIn arr_seq), job_task j \in ts. forall (j: JobIn arr_seq), job_task j \in ts.
(* ...they have valid parameters,...*) (* ...jobs have valid parameters,...*)
Hypothesis H_valid_job_parameters: Hypothesis H_valid_job_parameters:
forall (j: JobIn arr_seq), forall (j: JobIn arr_seq),
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j. valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
...@@ -587,8 +585,8 @@ Module ResponseTimeIterationFP. ...@@ -587,8 +585,8 @@ Module ResponseTimeIterationFP.
(* In the following theorem, we prove that any response-time bound contained (* In the following theorem, we prove that any response-time bound contained
in fp_claimed_bounds is safe. The proof follows by induction on the task set: in fp_claimed_bounds is safe. The proof follows by induction on the task set:
Induction hypothesis: all higher-priority tasks have safe response-time bounds. Induction hypothesis: assume all higher-priority tasks have safe response-time bounds.
Inductive step: We prove that the response-time bound of the current task is safe. Inductive step: we prove that the response-time bound of the current task is safe.
Note that the inductive step is a direct application of the main Theorem from Note that the inductive step is a direct application of the main Theorem from
bertogna_fp_theory.v. *) bertogna_fp_theory.v. *)
......
...@@ -15,13 +15,13 @@ Module ResponseTimeAnalysisFP. ...@@ -15,13 +15,13 @@ Module ResponseTimeAnalysisFP.
Section ResponseTimeBound. Section ResponseTimeBound.
Context {sporadic_task: eqType}. Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task -> nat. Variable task_cost: sporadic_task -> time.
Variable task_period: sporadic_task -> nat. Variable task_period: sporadic_task -> time.
Variable task_deadline: sporadic_task -> nat. Variable task_deadline: sporadic_task -> time.
Context {Job: eqType}. Context {Job: eqType}.
Variable job_cost: Job -> nat. Variable job_cost: Job -> time.
Variable job_deadline: Job -> nat. Variable job_deadline: Job -> time.
Variable job_task: Job -> sporadic_task. Variable job_task: Job -> sporadic_task.
(* Assume any job arrival sequence... *) (* Assume any job arrival sequence... *)
...@@ -52,8 +52,9 @@ Module ResponseTimeAnalysisFP. ...@@ -52,8 +52,9 @@ Module ResponseTimeAnalysisFP.
Hypothesis H_at_least_one_cpu : Hypothesis H_at_least_one_cpu :
num_cpus > 0. num_cpus > 0.
(* Assume that we have a task set (with no duplicates) where all jobs (* Consider a task set ts with no duplicates where all jobs
come from the task set and all tasks have valid parameters and restricted deadlines. *) come from the task set and all tasks have valid parameters
and restricted deadlines. *)
Variable ts: taskset_of sporadic_task. Variable ts: taskset_of sporadic_task.
Hypothesis H_ts_is_a_set: uniq ts. Hypothesis H_ts_is_a_set: uniq ts.
Hypothesis H_all_jobs_from_taskset: Hypothesis H_all_jobs_from_taskset:
...@@ -72,24 +73,21 @@ Module ResponseTimeAnalysisFP. ...@@ -72,24 +73,21 @@ Module ResponseTimeAnalysisFP.
Let is_response_time_bound (tsk: sporadic_task) := Let is_response_time_bound (tsk: sporadic_task) :=
is_response_time_bound_of_task job_cost job_task tsk sched. is_response_time_bound_of_task job_cost job_task tsk sched.
(* Assume a known response-time bound for any interfering task *) (* Assume a given FP policy. *)
Let task_with_response_time := (sporadic_task * time)%type.
Variable hp_bounds: seq task_with_response_time.
(* For FP scheduling, assume there exists a fixed task priority. *)
Variable higher_eq_priority: FP_policy sporadic_task. Variable higher_eq_priority: FP_policy sporadic_task.
Let can_interfere_with_tsk := fp_can_interfere_with higher_eq_priority tsk. Let can_interfere_with_tsk := fp_can_interfere_with higher_eq_priority tsk.
(* Assume that hp_bounds has exactly the tasks that interfere with tsk,... *)
Hypothesis H_hp_bounds_has_interfering_tasks:
[seq tsk_hp <- ts | can_interfere_with_tsk tsk_hp] = unzip1 hp_bounds.
(* ...and that all values in the pairs contain valid response-time bounds *) (* Assume a response-time bound is known... *)
Let task_with_response_time := (sporadic_task * time)%type.
Variable hp_bounds: seq task_with_response_time.
Hypothesis H_response_time_of_interfering_tasks_is_known: Hypothesis H_response_time_of_interfering_tasks_is_known:
forall hp_tsk R, forall hp_tsk R,
(hp_tsk, R) \in hp_bounds -> (hp_tsk, R) \in hp_bounds ->
is_response_time_bound_of_task job_cost job_task hp_tsk sched R. is_response_time_bound_of_task job_cost job_task hp_tsk sched R.
(* ... for any task in ts that interferes with tsk. *)
Hypothesis H_hp_bounds_has_interfering_tasks:
[seq tsk_hp <- ts | can_interfere_with_tsk tsk_hp] = unzip1 hp_bounds.
(* Assume that the response-time bounds are larger than task costs. *) (* Assume that the response-time bounds are larger than task costs. *)
Hypothesis H_response_time_bounds_ge_cost: Hypothesis H_response_time_bounds_ge_cost:
...@@ -169,7 +167,7 @@ Module ResponseTimeAnalysisFP. ...@@ -169,7 +167,7 @@ Module ResponseTimeAnalysisFP.
by apply/mapP; exists (tsk_other, R_other). by apply/mapP; exists (tsk_other, R_other).
Qed. Qed.
(*... and interferes with task tsk. *) (*... and interferes with tsk. *)
Lemma bertogna_fp_tsk_other_interferes: can_interfere_with_tsk tsk_other. Lemma bertogna_fp_tsk_other_interferes: can_interfere_with_tsk tsk_other.
Proof. Proof.
rename H_hp_bounds_has_interfering_tasks into UNZIP, rename H_hp_bounds_has_interfering_tasks into UNZIP,
......
...@@ -11,9 +11,9 @@ Module InterferenceBoundGeneric. ...@@ -11,9 +11,9 @@ Module InterferenceBoundGeneric.
Import Schedule WorkloadBound. Import Schedule WorkloadBound.
Context {sporadic_task: eqType}. Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task -> nat. Variable task_cost: sporadic_task -> time.
Variable task_period: sporadic_task -> nat. Variable task_period: sporadic_task -> time.
Variable task_deadline: sporadic_task -> nat. Variable task_deadline: sporadic_task -> time.
(* Let tsk be the task to be analyzed. *) (* Let tsk be the task to be analyzed. *)
Variable tsk: sporadic_task. Variable tsk: sporadic_task.
......
...@@ -19,9 +19,9 @@ Module InterferenceBoundEDF. ...@@ -19,9 +19,9 @@ Module InterferenceBoundEDF.
Section SpecificBoundDef. Section SpecificBoundDef.
Context {sporadic_task: eqType}. Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task -> nat. Variable task_cost: sporadic_task -> time.
Variable task_period: sporadic_task -> nat. Variable task_period: sporadic_task -> time.
Variable task_deadline: sporadic_task -> nat. Variable task_deadline: sporadic_task -> time.
(* Let tsk be the task to be analyzed. *) (* Let tsk be the task to be analyzed. *)
Variable tsk: sporadic_task. Variable tsk: sporadic_task.
...@@ -29,7 +29,7 @@ Module InterferenceBoundEDF. ...@@ -29,7 +29,7 @@ Module InterferenceBoundEDF.
(* Consider the interference incurred by tsk in a window of length delta... *) (* Consider the interference incurred by tsk in a window of length delta... *)
Variable <