From b5863397fc668b7d9837c70b4b09147e719d2611 Mon Sep 17 00:00:00 2001
From: Felipe Cerqueira <felipec@mpi-sws.org>
Date: Tue, 17 Nov 2015 13:29:09 +0100
Subject: [PATCH] Fix EDF workload bound
---
BertognaResponseTimeDefs.v | 20 +++--------
BertognaResponseTimeDefsEDF.v | 63 ++++++++++++++++++++++++++++++++---
BertognaResponseTimeEDFComp.v | 22 ++++++------
3 files changed, 73 insertions(+), 32 deletions(-)
diff --git a/BertognaResponseTimeDefs.v b/BertognaResponseTimeDefs.v
index 7419bad87..6b2fb3b91 100644
--- a/BertognaResponseTimeDefs.v
+++ b/BertognaResponseTimeDefs.v
@@ -168,7 +168,7 @@ Module ResponseTimeAnalysis.
End Interference.
- Section InterferenceBound.
+ Section InterferenceBoundFP.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task -> nat.
@@ -199,7 +199,7 @@ Module ResponseTimeAnalysis.
End PerTask.
- Section FP.
+ Section AllTasks.
(* Assume an FP policy. *)
Variable higher_eq_priority: fp_policy sporadic_task.
@@ -212,21 +212,9 @@ Module ResponseTimeAnalysis.
\sum_((tsk_other, R_other) <- R_prev | is_interfering_task_fp tsk_other)
interference_bound (tsk_other, R_other).
- End FP.
+ End AllTasks.
- Section JLFP.
-
- Definition is_interfering_task_jlfp (tsk_other: sporadic_task) :=
- tsk_other != tsk.
-
- (* The total interference incurred by tsk is thus bounded by: *)
- Definition total_interference_bound_jlfp :=
- \sum_((tsk_other, R_other) <- R_prev | is_interfering_task_jlfp tsk_other)
- interference_bound (tsk_other, R_other).
-
- End JLFP.
-
- End InterferenceBound.
+ End InterferenceBoundFP.
Section ResponseTimeBound.
diff --git a/BertognaResponseTimeDefsEDF.v b/BertognaResponseTimeDefsEDF.v
index d79d28f78..d64a4c0b7 100644
--- a/BertognaResponseTimeDefsEDF.v
+++ b/BertognaResponseTimeDefsEDF.v
@@ -7,6 +7,61 @@ Module ResponseTimeAnalysisEDF.
Export Job SporadicTaskset Schedule Workload Schedulability ResponseTime Priority SporadicTaskArrival ResponseTimeAnalysis.
+ Section InterferenceBoundEDF.
+
+ Context {sporadic_task: eqType}.
+ Variable task_cost: sporadic_task -> nat.
+ Variable task_period: sporadic_task -> nat.
+ Variable task_deadline: sporadic_task -> nat.
+
+ (* Let tsk be the task to be analyzed. *)
+ Variable tsk: sporadic_task.
+
+ Let task_with_response_time := (sporadic_task * time)%type.
+
+ (* Assume a known response-time bound for each interfering task ... *)
+ Variable R_prev: seq task_with_response_time.
+
+ (* ... and an interval length delta. *)
+ Variable delta: time.
+
+ Section PerTask.
+
+ Variable tsk_R: task_with_response_time.
+ Let tsk_other := fst tsk_R.
+ Let R_other := snd tsk_R.
+
+ Definition workload_bound_edf :=
+ let d_tsk := task_deadline tsk in
+ let e_other := task_cost tsk_other in
+ let p_other := task_period tsk_other in
+ let d_other := task_deadline tsk_other in
+ (div_floor d_tsk p_other) * e_other +
+ minn e_other ((d_tsk %% p_other) - d_other + R_other).
+
+ Let basic_interference_bound := interference_bound task_cost task_period tsk delta tsk_R.
+
+ (* Based on the workload bound, Bertogna and Cirinei define the
+ following interference bound for a task. *)
+ Definition interference_bound_edf :=
+ minn basic_interference_bound workload_bound_edf.
+
+ End PerTask.
+
+ Section AllTasks.
+
+ Definition is_interfering_task_jlfp (tsk_other: sporadic_task) :=
+ tsk_other != tsk.
+
+ (* The total interference incurred by tsk is thus bounded by: *)
+ Definition total_interference_bound_edf :=
+ \sum_((tsk_other, R_other) <- R_prev | is_interfering_task_jlfp tsk_other)
+ interference_bound_edf (tsk_other, R_other).
+
+ End AllTasks.
+
+ End InterferenceBoundEDF.
+
Section ResponseTimeBound.
Context {sporadic_task: eqType}.
@@ -69,13 +124,13 @@ Module ResponseTimeAnalysisEDF.
(* Assume that the response-time bounds are a fixed-point of the
response-time recurrence. *)
+ Let I (tsk: sporadic_task) (delta: time) :=
+ total_interference_bound_edf task_cost task_period task_deadline tsk rt_bounds delta.
+
Hypothesis H_response_time_is_fixed_point :
forall tsk R,
(tsk, R) \in rt_bounds ->
- R = task_cost tsk +
- div_floor
- (total_interference_bound_jlfp task_cost task_period tsk rt_bounds R)
- num_cpus.
+ R = task_cost tsk + div_floor (I tsk R) num_cpus.
(* Assume that the response-time bounds are larger than task costs. *)
Hypothesis H_response_time_bounds_ge_cost:
diff --git a/BertognaResponseTimeEDFComp.v b/BertognaResponseTimeEDFComp.v
index 796d95c9e..ae88eaf5f 100755
--- a/BertognaResponseTimeEDFComp.v
+++ b/BertognaResponseTimeEDFComp.v
@@ -29,12 +29,13 @@ Module ResponseTimeIterationEDF.
Let max_steps (ts: taskset_of sporadic_task) :=
\max_(tsk <- ts) task_deadline tsk.
- Let response_time_bound (tsk: sporadic_task) (rt_bounds: seq task_with_response_time)
- (delta: time) :=
- task_cost tsk +
- div_floor
- (total_interference_bound_jlfp task_cost task_period tsk rt_bounds delta)
- num_cpus.
+ Let I (rt_bounds: seq task_with_response_time)
+ (tsk: sporadic_task) (delta: time) :=
+ total_interference_bound_edf task_cost task_period task_deadline tsk rt_bounds delta.
+
+ Let response_time_bound (rt_bounds: seq task_with_response_time)
+ (tsk: sporadic_task) (delta: time) :=
+ task_cost tsk + div_floor (I rt_bounds tsk delta) num_cpus.
Let initial_state (ts: taskset_of sporadic_task) :=
map (fun t => (t, task_cost t)) ts.
@@ -42,7 +43,7 @@ Module ResponseTimeIterationEDF.
Definition update_bound (rt_bounds: seq task_with_response_time)
(pair : task_with_response_time) :=
let (tsk, R) := pair in
- (tsk, response_time_bound tsk rt_bounds R).
+ (tsk, response_time_bound rt_bounds tsk R).
Definition edf_rta_iteration (rt_bounds: seq task_with_response_time) :=
map (update_bound rt_bounds) rt_bounds.
@@ -143,10 +144,7 @@ Module ResponseTimeIterationEDF.
forall tsk R rt_bounds,
R_list_edf ts = Some rt_bounds ->
(tsk, R) \in rt_bounds ->
- R = task_cost tsk +
- div_floor
- (total_interference_bound_jlfp task_cost task_period tsk rt_bounds R)
- num_cpus.
+ R = task_cost tsk + div_floor (I rt_bounds tsk R) num_cpus.
Proof.
admit.
Qed.
@@ -221,7 +219,7 @@ Module ResponseTimeIterationEDF.
set prev_state := iter step edf_rta_iteration (initial_state ts).
fold prev_state in IN, IHstep.
specialize (IHstep tsk IN); des.
- exists (response_time_bound tsk prev_state R).
+ exists (response_time_bound prev_state tsk R).
by apply/mapP; exists (tsk, R); [by done | by f_equal].
}
Qed.
--
GitLab