From 76d2066654ede12c08fd79d0784e6229fcd4ba94 Mon Sep 17 00:00:00 2001
From: Felipe Cerqueira <felipec@mpi-sws.org>
Date: Tue, 15 Sep 2015 10:40:36 +0200
Subject: [PATCH] Add comments to RTA
---
BertognaResponseTimeDefs.v | 159 ++++++++++++++++++++++++-------------
1 file changed, 104 insertions(+), 55 deletions(-)
diff --git a/BertognaResponseTimeDefs.v b/BertognaResponseTimeDefs.v
index f086a5b3d..fcc67bc28 100644
--- a/BertognaResponseTimeDefs.v
+++ b/BertognaResponseTimeDefs.v
@@ -9,45 +9,59 @@ Module ResponseTimeAnalysis.
Section Interference.
+ (* Assume any job arrival sequence...*)
Context {Job: eqType}.
Variable job_cost: Job -> nat.
Variable job_task: Job -> sporadic_task.
Context {arr_seq: arrival_sequence Job}.
+ (* ... and any platform. *)
Context {num_cpus: nat}.
Variable rate: Job -> processor num_cpus -> nat.
Variable sched: schedule num_cpus arr_seq.
+ (* Consider any job j in a time interval [t1, t2), and ... *)
Variable j: JobIn arr_seq.
Variable t1 t2: time.
+ (* recall the definition of backlogged (pending and not scheduled). *)
Let job_is_backlogged (t: time) :=
backlogged job_cost rate sched j t.
+ (* We define the total interference incurred by job j during [t1, t2)
+ as the cumulative time in which j is backlogged in this interval. *)
Definition total_interference :=
\sum_(t1 <= t < t2) job_is_backlogged t.
Section TaskInterference.
+ (* In order to define task interference, consider any task tsk. *)
Variable tsk: sporadic_task.
- Definition has_job_of_tsk (cpu: processor num_cpus) (t: time) :=
+ Definition schedules_job_of_tsk (cpu: processor num_cpus) (t: time) :=
match (sched cpu t) with
| Some j' => job_task j' == tsk
| None => false
end.
-
- Definition tsk_is_scheduled (t: time) :=
- [exists cpu in processor num_cpus, has_job_of_tsk cpu t].
-
+
+ (* We know that tsk is scheduled at time t if there exists a processor
+ scheduling a job of tsk. *)
+ Definition task_is_scheduled (t: time) :=
+ [exists cpu in processor num_cpus, schedules_job_of_tsk cpu t].
+
+ (* We define the total interference incurred by tsk during [t1, t2)
+ as the cumulative time in which tsk is scheduled. *)
Definition task_interference :=
\sum_(t1 <= t < t2)
- (job_is_backlogged t && tsk_is_scheduled t).
+ (job_is_backlogged t && task_is_scheduled t).
+ (* Note that this definition assumes that no multiple jobs of
+ the same task execute in parallel (task precedence). *)
End TaskInterference.
Section BasicLemmas.
+ (* Interference cannot be larger than the considered time window. *)
Lemma total_interference_le_delta : total_interference <= t2 - t1.
Proof.
unfold total_interference.
@@ -60,24 +74,30 @@ Module ResponseTimeAnalysis.
Section CorrespondenceWithService.
+ (* Assume that jobs do not execute in parallel, ...*)
Hypothesis no_parallelism:
jobs_dont_execute_in_parallel sched.
+ (* and that processors have unit speed. *)
Hypothesis rate_equals_one :
forall j cpu, rate j cpu = 1.
+ (* Also assume that jobs only execute after they arrived
+ and no longer than their execution costs. *)
Hypothesis jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute sched.
-
Hypothesis completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost rate sched.
-
+
+ (* If job j had already arrived at time t1 and did not yet
+ complete by time t2, ...*)
Hypothesis job_has_arrived :
has_arrived j t1.
-
Hypothesis job_is_not_complete :
~~ completed job_cost rate sched j t2.
+ (* then the service received by j during [t1, t2) equals
+ the cumulative time in which it did not incur interference. *)
Lemma complement_of_interf_equals_service :
\sum_(t1 <= t < t2) service_at rate sched j t =
t2 - t1 - total_interference.
@@ -158,11 +178,12 @@ Module ResponseTimeAnalysis.
(* ... and an interval length delta. *)
Variable delta: time.
- (* Based on Bertogna and Cirinei's workload bound, ... *)
+ (* Based on the workload bound, ... *)
Let workload_bound (tsk_other: sporadic_task) :=
W tsk_other (R_other tsk_other) delta.
- (* ... we define interference bounds for FP and JLFP scheduling. *)
+ (* Bertogna and Cirinei define the following interference bound
+ for a task. *)
Definition interference_bound (tsk_other: sporadic_task) :=
minn (workload_bound tsk_other) (delta - (task_cost tsk) + 1).
@@ -171,7 +192,7 @@ Module ResponseTimeAnalysis.
(* Assume an FP policy. *)
Variable higher_eq_priority: fp_policy.
- (* Under FP scheduling, lower-priority tasks do not cause interference. *)
+ (* Under FP scheduling, lower-priority tasks don't interfere. *)
Let interference_caused_by (tsk_other: sporadic_task) :=
if (higher_eq_priority tsk_other tsk) && (tsk_other != tsk) then
interference_bound tsk_other
@@ -186,7 +207,7 @@ Module ResponseTimeAnalysis.
Section InterferenceJLFP.
- (* Under JLFP scheduling, all the other tasks may cause interference. *)
+ (* Under JLFP scheduling, all other tasks may cause interference. *)
Let interference_caused_by (tsk_other: sporadic_task) :=
if tsk_other != tsk then
interference_bound tsk_other
@@ -202,71 +223,96 @@ Module ResponseTimeAnalysis.
End InterferenceBound.
Section ResponseTimeBound.
-
+
+ (* Assume any job arrival sequence... *)
Context {Job: eqType}.
Variable job_cost: Job -> nat.
Variable job_deadline: Job -> nat.
Variable job_task: Job -> sporadic_task.
-
Context {arr_seq: arrival_sequence Job}.
- Hypothesis sporadic_tasks: sporadic_task_model arr_seq job_task.
-
+ (* ... in which jobs arrive sporadically and have valid parameters. *)
+ Hypothesis H_sporadic_tasks: sporadic_task_model arr_seq job_task.
+ Hypothesis H_valid_job_parameters:
+ forall (j: JobIn arr_seq),
+ (valid_sporadic_task_job job_cost job_deadline job_task) j.
+
+ (* Consider any schedule such that...*)
Variable num_cpus: nat.
Variable rate: Job -> processor num_cpus -> nat.
Variable sched: schedule num_cpus arr_seq.
+ (* ...jobs do not execute before their arrival times nor longer
+ than their execution costs. *)
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost rate sched.
-
+
+ (* Also assume that jobs do not execute in parallel, processors have
+ unit speed, and that there exists at least one processor. *)
Hypothesis H_no_parallelism:
jobs_dont_execute_in_parallel sched.
Hypothesis H_rate_equals_one :
forall j cpu, rate j cpu = 1.
Hypothesis H_at_least_one_cpu :
num_cpus > 0.
-
+
+ (* Assume that we have a task set where all tasks have valid
+ parameters and restricted deadlines. *)
Variable ts: sporadic_taskset.
Hypothesis H_valid_task_parameters: valid_sporadic_taskset ts.
- Hypothesis H_valid_job_parameters:
- forall (j: JobIn arr_seq),
- (valid_sporadic_task_job job_cost job_deadline job_task) j.
-
Hypothesis H_restricted_deadlines:
forall tsk, tsk \in ts -> task_deadline tsk <= task_period tsk.
-
+
+ (* Next, consider some task tsk in the task set that is
+ to be analyzed. *)
Variable tsk: sporadic_task.
Hypothesis task_in_ts: tsk \in ts.
Definition no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
task_misses_no_deadline job_cost job_deadline job_task rate sched tsk.
-
Definition is_response_time_bound (tsk: sporadic_task) :=
is_response_time_bound_of_task job_cost job_task tsk rate sched.
-
+
+ (* Assume that we know a response-time bound for the
+ tasks that interfere with tsk. *)
Variable R_other: sporadic_task -> time.
+ (* We derive the response-time bounds for FP and EDF scheduling
+ separately. *)
Section UnderFPScheduling.
+ (* For FP scheduling, assume there exists a fixed task priority. *)
Variable higher_eq_priority: fp_policy.
+ (* We say that tsk can be interfered with by tsk_other if
+ tsk_other is a different task from the task set that has
+ higher or equal priority. *)
Definition is_interfering_task (tsk_other: sporadic_task) :=
(tsk_other \in ts) &&
higher_eq_priority tsk_other tsk &&
(tsk_other != tsk).
+ (* Assume that for any interfering task, a response-time
+ bound R_other is known. *)
Hypothesis H_response_time_of_interfering_tasks_is_known:
forall tsk_other job_cost,
is_interfering_task tsk_other ->
- is_response_time_bound_of_task job_cost job_task tsk_other rate sched (R_other tsk_other).
+ is_response_time_bound_of_task job_cost job_task tsk_other
+ rate sched (R_other tsk_other).
+ (* Assume that no deadline is missed by any interfering task. *)
Hypothesis H_interfering_tasks_miss_no_deadlines:
forall tsk_other,
is_interfering_task tsk_other ->
- task_misses_no_deadline job_cost job_deadline job_task rate sched tsk_other.
+ task_misses_no_deadline job_cost job_deadline job_task rate
+ sched tsk_other.
+ (* Assume that the schedule satisfies the global scheduling
+ invariant, i.e., if any job of tsk is backlogged, all
+ the processors must be busy with jobs of equal or higher
+ priority. *)
Hypothesis H_global_scheduling_invariant:
forall (j: JobIn arr_seq) (t: time),
job_task j = tsk ->
@@ -274,28 +320,31 @@ Module ResponseTimeAnalysis.
count
(fun tsk_other : sporadic_task =>
is_interfering_task tsk_other &&
- tsk_is_scheduled job_task sched tsk_other t) ts = num_cpus.
+ task_is_scheduled job_task sched tsk_other t) ts = num_cpus.
- (* Bertogna and Cirinei's response-time bound recurrence *)
- Definition response_time_recurrence_fp R :=
+ (* Next, we define Bertogna and Cirinei's response-time bound recurrence *)
+
+ (* Let R be any time. *)
+ Variable R: time.
+
+ (* Bertogna and Cirinei's response-time analysis states that
+ if R is a fixed-point of the following recurrence, ... *)
+ Hypothesis H_response_time_recurrence_holds :
R = task_cost tsk +
div_floor
- (total_interference_bound_fp ts tsk R_other R higher_eq_priority)
+ (total_interference_bound_fp ts tsk R_other
+ R higher_eq_priority)
num_cpus.
- Variable R: time.
-
- Hypothesis H_response_time_recurrence_holds:
- response_time_recurrence_fp R.
-
+ (*..., and R is no larger than the deadline of tsk, ...*)
Hypothesis H_response_time_no_larger_than_deadline:
R <= task_deadline tsk.
-
+
+ (* ..., then R bounds the response time of tsk in any schedule. *)
Theorem bertogna_cirinei_response_time_bound_fp :
is_response_time_bound tsk R.
Proof.
- unfold response_time_recurrence_fp,
- is_response_time_bound, is_response_time_bound_of_task,
+ unfold is_response_time_bound, is_response_time_bound_of_task,
job_has_completed_by, completed,
completed_jobs_dont_execute,
valid_sporadic_task_job in *.
@@ -350,13 +399,13 @@ Module ResponseTimeAnalysis.
apply leq_sum; intros t _.
rewrite -mulnb -[\sum_(_ < _) _]mul1n.
apply leq_mul; first by apply leq_b1.
- destruct (tsk_is_scheduled job_task sched tsk_k t) eqn:SCHED;
+ destruct (task_is_scheduled job_task sched tsk_k t) eqn:SCHED;
last by ins.
- unfold tsk_is_scheduled in SCHED.
+ unfold task_is_scheduled in SCHED.
move: SCHED =>/exists_inP SCHED; destruct SCHED as [cpu _ HAScpu].
rewrite -> bigD1 with (j := cpu); simpl; last by ins.
apply ltn_addr.
- unfold service_of_task, has_job_of_tsk in *.
+ unfold service_of_task, schedules_job_of_tsk in *.
by destruct (sched cpu t);[by rewrite HAScpu mul1n RATE|by ins].
}
@@ -415,7 +464,7 @@ Module ResponseTimeAnalysis.
last by rewrite (eq_bigr (fun i => 0));
[by rewrite big_const_seq iter_addn mul0n addn0 mul0n|by ins].
rewrite big_mkcond mul1n /=.
- rewrite (eq_bigr (fun i => (if is_interfering_task i && tsk_is_scheduled job_task sched i t then 1 else 0)));
+ rewrite (eq_bigr (fun i => (if is_interfering_task i && task_is_scheduled job_task sched i t then 1 else 0)));
last by ins; destruct (is_interfering_task i); rewrite ?andTb ?andFb; ins.
by rewrite -big_mkcond sum1_count; apply (INVARIANT j).
}
@@ -464,13 +513,13 @@ Module ResponseTimeAnalysis.
{
set some_interference_A := fun t =>
backlogged job_cost rate sched j t &&
- has (fun tsk_k => (is_interfering_task tsk_k && ((x tsk_k) >= R - task_cost tsk + 1) && tsk_is_scheduled job_task sched tsk_k t)) ts.
+ has (fun tsk_k => (is_interfering_task tsk_k && ((x tsk_k) >= R - task_cost tsk + 1) && task_is_scheduled job_task sched tsk_k t)) ts.
set total_interference_B := fun t =>
backlogged job_cost rate sched j t *
count (fun tsk_k =>
is_interfering_task tsk_k &&
((x tsk_k) < R - task_cost tsk + 1) &&
- tsk_is_scheduled job_task sched tsk_k t) ts.
+ task_is_scheduled job_task sched tsk_k t) ts.
apply leq_trans with ((\sum_(job_arrival j <= t < job_arrival j + R) some_interference_A t) * (num_cpus - card)).
{
@@ -482,7 +531,7 @@ Module ResponseTimeAnalysis.
apply leq_sum; ins.
destruct (backlogged job_cost rate sched j i);
[rewrite 2!andTb | by ins].
- destruct (tsk_is_scheduled job_task sched tsk_a i) eqn:SCHEDa;
+ destruct (task_is_scheduled job_task sched tsk_a i) eqn:SCHEDa;
[apply eq_leq; symmetry | by ins].
apply/eqP; rewrite eqb1.
apply/hasP; exists tsk_a; first by ins.
@@ -499,7 +548,7 @@ Module ResponseTimeAnalysis.
destruct (has (fun tsk_k : sporadic_task =>
is_interfering_task tsk_k &&
(R - task_cost tsk + 1 <= x tsk_k) &&
- tsk_is_scheduled job_task sched tsk_k t) ts) eqn:HAS;
+ task_is_scheduled job_task sched tsk_k t) ts) eqn:HAS;
last by ins.
rewrite mul1n; move: HAS => /hasP HAS.
destruct HAS as [tsk_k INk H].
@@ -510,12 +559,12 @@ Module ResponseTimeAnalysis.
unfold card.
set interfering_tasks_at_t :=
- [seq tsk_k <- ts | is_interfering_task tsk_k && tsk_is_scheduled job_task sched tsk_k t].
+ [seq tsk_k <- ts | is_interfering_task tsk_k && task_is_scheduled job_task sched tsk_k t].
rewrite -(count_filter (fun i => true)) in COUNT.
fold interfering_tasks_at_t in COUNT.
rewrite count_predT in COUNT.
- apply leq_trans with (n := num_cpus - count (fun i => is_interfering_task i && (x i >= R - task_cost tsk + 1) && tsk_is_scheduled job_task sched i t) ts).
+ apply leq_trans with (n := num_cpus - count (fun i => is_interfering_task i && (x i >= R - task_cost tsk + 1) && task_is_scheduled job_task sched i t) ts).
{
apply leq_sub2l.
rewrite -2!sum1_count big_mkcond /=.
@@ -523,7 +572,7 @@ Module ResponseTimeAnalysis.
apply leq_sum; intros i _.
unfold x; destruct (is_interfering_task i);
[rewrite andTb | by rewrite 2!andFb].
- destruct (tsk_is_scheduled job_task sched i t);
+ destruct (task_is_scheduled job_task sched i t);
[by rewrite andbT | by rewrite andbF].
}
@@ -533,11 +582,11 @@ Module ResponseTimeAnalysis.
count (predU (fun i : sporadic_task =>
is_interfering_task i &&
(R - task_cost tsk + 1 <= x i) &&
- tsk_is_scheduled job_task sched i t)
+ task_is_scheduled job_task sched i t)
(fun tsk_k0 : sporadic_task =>
is_interfering_task tsk_k0 &&
(x tsk_k0 < R - task_cost tsk + 1) &&
- tsk_is_scheduled job_task sched tsk_k0 t))
+ task_is_scheduled job_task sched tsk_k0 t))
ts); last by apply leq_addr.
apply leq_trans with (n := size interfering_tasks_at_t);
first by rewrite COUNT.
@@ -547,7 +596,7 @@ Module ResponseTimeAnalysis.
apply eq_count; red; simpl.
intros i.
destruct (is_interfering_task i),
- (tsk_is_scheduled job_task sched i t);
+ (task_is_scheduled job_task sched i t);
rewrite 3?andTb ?andFb ?andbF ?andbT /=; try ins.
by rewrite leqNgt orNb.
}
@@ -557,7 +606,7 @@ Module ResponseTimeAnalysis.
(fun i => \sum_(job_arrival j <= t < job_arrival j + R)
is_interfering_task i &&
backlogged job_cost rate sched j t &&
- tsk_is_scheduled job_task sched i t));
+ task_is_scheduled job_task sched i t));
last first.
{
ins; destruct (is_interfering_task i);
--
GitLab