Forked from
RT-PROOFS / PROSA - Formally Proven Schedulability Analysis
992 commits behind the upstream repository.
-
Felipe Cerqueira authoredFelipe Cerqueira authored
BertognaResponseTimeDefs.v 32.74 KiB
Require Import Vbase TaskDefs JobDefs TaskArrivalDefs ScheduleDefs
PlatformDefs WorkloadDefs SchedulabilityDefs PriorityDefs
ResponseTimeDefs divround helper
ssreflect ssrbool eqtype ssrnat seq fintype bigop div path tuple.
Module ResponseTimeAnalysis.
Export Job SporadicTaskset Schedule Workload Schedulability ResponseTime Priority SporadicTaskArrival.
Section Interference.
Context {sporadic_task: eqType}.
Context {Job: eqType}.
Variable job_cost: Job -> nat.
Variable job_task: Job -> sporadic_task.
(* Assume any job arrival sequence...*)
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 schedules_job_of_tsk (cpu: processor num_cpus) (t: time) :=
match (sched cpu t) with
| Some j' => job_task j' == tsk
| None => false
end.
(* 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 && 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.
apply leq_trans with (n := \sum_(t1 <= t < t2) 1); first by apply leq_sum; ins; apply leq_b1.
by rewrite big_const_nat iter_addn mul1n addn0 leqnn.
Qed.
End BasicLemmas.
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.
Proof.
unfold completed, total_interference, job_is_backlogged,
backlogged, service_during, pending.
rename no_parallelism into NOPAR,
rate_equals_one into RATE,
jobs_must_arrive_to_execute into MUSTARRIVE,
completed_jobs_dont_execute into COMP,
job_is_not_complete into NOTCOMP.
assert (SERVICE_ONE: forall j t, service_at rate sched j t <= 1).
by ins; apply service_at_le_max_rate; ins; rewrite RATE.
(* Reorder terms... *)
apply/eqP; rewrite subh4; first last.
{
rewrite -[t2 - t1]mul1n -[1*_]addn0 -iter_addn -big_const_nat.
by apply leq_sum; ins; apply leq_b1.
}
{
rewrite -[t2 - t1]mul1n -[1*_]addn0 -iter_addn -big_const_nat.
by apply leq_sum; ins; apply service_at_le_max_rate; ins; rewrite RATE.
}
apply/eqP.
apply eq_trans with (y := \sum_(t1 <= t < t2)
(1 - service_at rate sched j t));
last first.
{
apply/eqP; rewrite <- eqn_add2r with (p := \sum_(t1 <= t < t2)
service_at rate sched j t).
rewrite subh1; last first.
rewrite -[t2 - t1]mul1n -[1*_]addn0 -iter_addn -big_const_nat.
by apply leq_sum; ins; apply SERVICE_ONE.
rewrite -addnBA // subnn addn0 -big_split /=.
rewrite -[t2 - t1]mul1n -[1*_]addn0 -iter_addn -big_const_nat. apply/eqP; apply eq_bigr; ins; rewrite subh1;
[by rewrite -addnBA // subnn addn0 | by apply SERVICE_ONE].
}
rewrite big_nat_cond [\sum_(_ <= _ < _ | true)_]big_nat_cond.
apply eq_bigr; intro t; rewrite andbT; move => /andP [GEt1 LTt2].
destruct (~~ scheduled sched j t) eqn:SCHED; last first.
{
apply negbFE in SCHED; unfold scheduled in *.
move: SCHED => /exists_inP SCHED; destruct SCHED as [cpu INcpu SCHEDcpu].
rewrite andbF; apply/eqP.
rewrite -(eqn_add2r (service_at rate sched j t)) add0n.
rewrite subh1; last by apply SERVICE_ONE.
rewrite -addnBA // subnn addn0.
rewrite eqn_leq; apply/andP; split; first by apply SERVICE_ONE.
unfold service_at; rewrite (bigD1 cpu) /=; last by apply SCHEDcpu.
apply leq_trans with (n := rate j cpu);
[by rewrite RATE | by apply leq_addr].
}
apply not_scheduled_no_service with (rate0 := rate) in SCHED.
rewrite SCHED subn0 andbT; apply/eqP; rewrite eqb1.
apply/andP; split; first by apply leq_trans with (n := t1).
apply/negP; unfold not; intro BUG.
apply completion_monotonic with (t' := t2) in BUG; [ | by ins | by apply ltnW].
by rewrite BUG in NOTCOMP.
Qed.
End CorrespondenceWithService.
End Interference.
Section InterferenceBoundFP.
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.
(* Based on the workload bound, Bertogna and Cirinei define the
following interference bound for a task. *)
Definition interference_bound :=
minn (W task_cost task_period tsk_other R_other delta) (delta - (task_cost tsk) + 1).
End PerTask.
Section AllTasks.
(* Assume an FP policy. *)
Variable higher_eq_priority: fp_policy sporadic_task.
Definition is_interfering_task_fp (tsk_other: sporadic_task) :=
higher_eq_priority tsk_other tsk && (tsk_other != tsk).
(* The total interference incurred by tsk is thus bounded by: *) Definition total_interference_bound_fp :=
\sum_((tsk_other, R_other) <- R_prev | is_interfering_task_fp tsk_other)
interference_bound (tsk_other, R_other).
End AllTasks.
End InterferenceBoundFP.
Section ResponseTimeBound.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task -> nat.
Variable task_period: sporadic_task -> nat.
Variable task_deadline: sporadic_task -> nat.
Context {Job: eqType}.
Variable job_cost: Job -> nat.
Variable job_deadline: Job -> nat.
Variable job_task: Job -> sporadic_task.
(* Assume any job arrival sequence... *)
Context {arr_seq: arrival_sequence Job}.
(* ... in which jobs arrive sporadically and have valid parameters. *)
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period arr_seq job_task.
Hypothesis H_valid_job_parameters:
forall (j: JobIn arr_seq),
valid_sporadic_job task_cost task_deadline 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: taskset_of sporadic_task.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Hypothesis H_restricted_deadlines:
forall tsk, tsk \in ts -> task_deadline tsk <= task_period tsk.
(* Next, consider a task tsk that is to be analyzed. *)
Variable tsk: sporadic_task.
Hypothesis task_in_ts: tsk \in ts.
Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
task_misses_no_deadline job_cost job_deadline job_task rate sched tsk.
Let is_response_time_bound (tsk: sporadic_task) :=
is_response_time_bound_of_task job_cost job_task tsk rate sched.
(* Assume a known response-time bound for any interfering task *)
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.
Let interferes_with_tsk := is_interfering_task_fp tsk higher_eq_priority.
(* Assume that hp_bounds has exactly the tasks that interfere with tsk,... *)
Hypothesis H_hp_bounds_has_interfering_tasks:
[seq tsk_hp <- ts | interferes_with_tsk tsk_hp] = unzip1 hp_bounds.
(* ...and that all values in the pairs contain valid response-time bounds *)
Hypothesis H_response_time_of_interfering_tasks_is_known:
forall hp_tsk R,
(hp_tsk, R) \in hp_bounds ->
is_response_time_bound_of_task job_cost job_task hp_tsk rate sched R.
(* Assume that the response-time bounds are larger than task costs. *)
Hypothesis H_response_time_bounds_ge_cost:
forall hp_tsk R,
(hp_tsk, R) \in hp_bounds -> R >= task_cost hp_tsk.
(* Assume that no deadline is missed by any interfering task, i.e.,
response-time bound R_other <= deadline. *)
Hypothesis H_interfering_tasks_miss_no_deadlines:
forall hp_tsk R,
(hp_tsk, R) \in hp_bounds -> R <= task_deadline hp_tsk.
(* 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 ->
backlogged job_cost rate sched j t ->
count
(fun tsk_other : sporadic_task =>
is_interfering_task_fp tsk higher_eq_priority tsk_other &&
task_is_scheduled job_task sched tsk_other t) ts = num_cpus.
(* 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 task_cost task_period tsk hp_bounds R higher_eq_priority)
num_cpus.
(*..., 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 is_response_time_bound, is_response_time_bound_of_task,
job_has_completed_by, completed,
completed_jobs_dont_execute,
valid_sporadic_job in *.
rename H_completed_jobs_dont_execute into COMP,
H_response_time_recurrence_holds into REC,
H_valid_job_parameters into PARAMS,
H_valid_task_parameters into TASK_PARAMS, H_restricted_deadlines into RESTR,
H_response_time_of_interfering_tasks_is_known into RESP,
H_hp_bounds_has_interfering_tasks into UNZIP,
H_interfering_tasks_miss_no_deadlines into NOMISS,
H_rate_equals_one into RATE,
H_global_scheduling_invariant into INVARIANT,
H_response_time_bounds_ge_cost into GE_COST.
intros j JOBtsk.
(* For simplicity, let x denote per-task interference under FP
scheduling, and let X denote the total interference. *)
set x := fun hp_tsk =>
if (hp_tsk \in ts) && interferes_with_tsk hp_tsk then
task_interference job_cost job_task rate sched j
(job_arrival j) (job_arrival j + R) hp_tsk
else 0.
set X := total_interference job_cost rate sched j (job_arrival j) (job_arrival j + R).
(* Let's recall the workload bound under FP scheduling. *)
set workload_bound := fun (tup: task_with_response_time) =>
let (tsk_k, R_k) := tup in
if interferes_with_tsk tsk_k then
W task_cost task_period tsk_k R_k R
else 0.
(* Now we start the proof. Assume by contradiction that job j
is not complete at time (job_arrival j + R). *)
destruct (completed job_cost rate sched j (job_arrival j + R)) eqn:COMPLETED;
first by move: COMPLETED => /eqP COMPLETED; rewrite COMPLETED eq_refl.
apply negbT in COMPLETED; exfalso.
(* Since j has not completed, recall the time when it is not
executing is the total interference. *)
exploit (complement_of_interf_equals_service job_cost rate sched j (job_arrival j)
(job_arrival j + R));
last intro EQinterf; ins; unfold has_arrived;
first by apply leqnn.
rewrite {2}[_ + R]addnC -addnBA // subnn addn0 in EQinterf.
(* In order to derive a contradiction, we first show that
the interference x_k of any task is no larger than the
workload bound W_k. *)
assert (WORKLOAD: forall tsk_k,
(tsk_k \in ts) && interferes_with_tsk tsk_k ->
forall R_k,
(tsk_k, R_k) \in hp_bounds ->
x tsk_k <= workload_bound (tsk_k, R_k)).
{
move => tsk_k /andP [INk INTERk] R_k HPk.
unfold x, workload_bound; rewrite INk INTERk andbT.
apply leq_trans with (n := workload job_task rate sched tsk_k
(job_arrival j) (job_arrival j + R)).
{
unfold task_interference, workload.
apply leq_sum; intros t _.
rewrite -mulnb -[\sum_(_ < _) _]mul1n.
apply leq_mul; first by apply leq_b1.
destruct (task_is_scheduled job_task sched tsk_k t) eqn:SCHED; last by ins.
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, schedules_job_of_tsk in *.
by destruct (sched cpu t);[by rewrite HAScpu mul1n RATE|by ins].
}
{
apply workload_bounded_by_W with (task_deadline0 := task_deadline) (job_cost0 := job_cost) (job_deadline0 := job_deadline); ins;
[ by rewrite RATE
| by apply TASK_PARAMS
| by apply RESTR | by red; red; ins; apply (RESP tsk_k)
| by apply GE_COST |].
red; red; move => j' /eqP JOBtsk' _;
unfold job_misses_no_deadline.
specialize (PARAMS j'); des.
rewrite PARAMS1 JOBtsk'.
apply completion_monotonic with (t := job_arrival j' + R_k); ins;
[by rewrite leq_add2l; apply NOMISS | by apply (RESP tsk_k)].
}
}
(* In the remaining of the proof, we show that the workload bound
W_k is less than the task interference x (contradiction!).
For that, we require a few auxiliary lemmas: *)
(* 1) We show that the total interference X >= R - e_k + 1.
Otherwise, job j would have completed on time. *)
assert (INTERF: X >= R - task_cost tsk + 1).
{
unfold completed in COMPLETED.
rewrite addn1.
move: COMPLETED; rewrite neq_ltn; move => /orP COMPLETED; des;
last first.
{
apply (leq_ltn_trans (COMP j (job_arrival j + R))) in COMPLETED.
by rewrite ltnn in COMPLETED.
}
apply leq_trans with (n := R - service rate sched j (job_arrival j + R)); last first.
{
unfold service; rewrite service_before_arrival_eq_service_during; ins.
rewrite EQinterf.
rewrite subKn; first by ins.
{
unfold total_interference.
rewrite -{1}[_ j]add0n big_addn addnC -addnBA // subnn addn0.
rewrite -{2}[R]subn0 -[R-_]mul1n -[1*_]addn0 -iter_addn.
by rewrite -big_const_nat leq_sum //; ins; apply leq_b1.
}
}
{
apply ltn_sub2l; last first.
{
apply leq_trans with (n := job_cost j); first by ins.
by rewrite -JOBtsk; specialize (PARAMS j); des; apply PARAMS0.
}
apply leq_trans with (n := job_cost j); first by ins.
apply leq_trans with (n := task_cost tsk);
first by rewrite -JOBtsk; specialize (PARAMS j); des; apply PARAMS0.
by rewrite REC; apply leq_addr.
}
}
(* 2) Then, we prove that the sum of the interference of each
task is equal to the total interference multiplied by the
number of processors. This holds because interference only
occurs when all processors are busy with some task. *)
assert(ALLBUSY: \sum_(tsk_k <- ts) x tsk_k = X * num_cpus).
{
unfold x, X, total_interference, task_interference.
rewrite -big_mkcond -exchange_big big_distrl /=.
apply eq_big_nat; move => t LTt.
destruct (backlogged job_cost rate sched j t) eqn:BACK;
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 (i \in ts) && interferes_with_tsk i &&
task_is_scheduled job_task sched i t then 1 else 0))); last first.
{
ins; destruct ((i \in ts) && interferes_with_tsk i) eqn:IN; [by rewrite andTb | by rewrite andFb].
}
rewrite (eq_bigr (fun i => if (i \in ts) && true then (if interferes_with_tsk i && task_is_scheduled job_task sched i t then 1 else 0) else 0));
last by ins; destruct (i \in ts) eqn:IN; rewrite ?andTb ?andFb.
by rewrite -big_mkcond -big_seq_cond -big_mkcond sum1_count; apply (INVARIANT j).
}
(* 3) Next, we prove the auxiliary lemma from the paper. *)
assert (MINSERV: \sum_(tsk_k <- ts) x tsk_k >=
(R - task_cost tsk + 1) * num_cpus ->
\sum_(tsk_k <- ts) minn (x tsk_k) (R - task_cost tsk + 1) >=
(R - task_cost tsk + 1) * num_cpus).
{
intro SUMLESS.
set more_interf := fun tsk_k => x tsk_k >= R - task_cost tsk + 1.
rewrite [\sum_(_ <- _) minn _ _](bigID more_interf) /=.
unfold more_interf, minn.
rewrite [\sum_(_ <- _ | R - _ + _ <= _)_](eq_bigr (fun i => R - task_cost tsk + 1));
last first.
{
intros i COND; rewrite leqNgt in COND.
destruct (R - task_cost tsk + 1 > x i); ins.
}
rewrite [\sum_(_ <- _ | ~~_)_](eq_big (fun i => x i < R - task_cost tsk + 1)
(fun i => x i));
[| by red; ins; rewrite ltnNge
| by intros i COND; rewrite -ltnNge in COND; rewrite COND].
(* Case 1 |A| = 0 *)
destruct (~~ has (fun i => R - task_cost tsk + 1 <= x i) ts) eqn:HASa.
{
rewrite [\sum_(_ <- _ | _ <= _) _]big_hasC; last by apply HASa.
rewrite big_seq_cond; move: HASa => /hasPn HASa.
rewrite add0n (eq_bigl (fun i => (i \in ts) && true));
last by red; intros tsk_k; destruct (tsk_k \in ts) eqn:INk;
[by rewrite andTb ltnNge; apply HASa | by rewrite andFb].
by rewrite -big_seq_cond.
} apply negbFE in HASa.
set cardA := count (fun i => R - task_cost tsk + 1 <= x i) ts.
destruct (cardA >= num_cpus) eqn:CARD.
{
apply leq_trans with ((R - task_cost tsk + 1) * cardA);
first by rewrite leq_mul2l; apply/orP; right.
unfold cardA; rewrite -sum1_count big_distrr /=.
rewrite -[\sum_(_ <- _ | _) _]addn0.
by apply leq_add; [by apply leq_sum; ins; rewrite muln1|by ins].
} apply negbT in CARD; rewrite -ltnNge in CARD.
assert (GEsum: \sum_(i <- ts | x i < R - task_cost tsk + 1) x i >=
(R - task_cost tsk + 1) * (num_cpus - cardA)).
{
set some_interference_A := fun t =>
backlogged job_cost rate sched j t &&
has (fun tsk_k => (interferes_with_tsk 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 =>
interferes_with_tsk tsk_k &&
((x tsk_k) < R - task_cost tsk + 1) &&
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 - cardA)).
{
rewrite leq_mul2r; apply/orP; right.
move: HASa => /hasP HASa; destruct HASa as [tsk_a INa LEa].
apply leq_trans with (n := x tsk_a); first by apply LEa. unfold x, task_interference, some_interference_A.
destruct ((tsk_a \in ts) && interferes_with_tsk tsk_a) eqn:INTERFa;
last by ins.
move: INTERFa => /andP INTERFa; des.
apply leq_sum; ins.
destruct (backlogged job_cost rate sched j i);
[rewrite 2!andTb | by ins].
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.
apply/andP; split; last by ins.
by apply/andP; split; ins.
}
apply leq_trans with (\sum_(job_arrival j <= t < job_arrival j + R)
total_interference_B t).
{
rewrite big_distrl /=.
apply leq_sum; intros t _.
unfold some_interference_A, total_interference_B.
destruct (backlogged job_cost rate sched j t) eqn:BACK;
[rewrite andTb mul1n | by ins].
destruct (has (fun tsk_k : sporadic_task =>
interferes_with_tsk tsk_k &&
(R - task_cost tsk + 1 <= x tsk_k) &&
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].
move: H => /andP [/andP [INTERFk LEk] SCHEDk].
exploit INVARIANT;
[by apply JOBtsk | by apply BACK | intro COUNT].
unfold cardA.
set interfering_tasks_at_t :=
[seq tsk_k <- ts | interferes_with_tsk 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 => interferes_with_tsk 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 /=.
rewrite [\sum_(_ <- _ | _ <= _)_]big_mkcond /=.
apply leq_sum; intros i _.
unfold x; destruct (interferes_with_tsk i);
[rewrite andTb | by rewrite 2!andFb].
destruct (task_is_scheduled job_task sched i t);
[by rewrite andbT | by rewrite andbF].
}
rewrite leq_subLR.
rewrite -count_predUI.
apply leq_trans with (n :=
count (predU (fun i : sporadic_task =>
interferes_with_tsk i &&
(R - task_cost tsk + 1 <= x i) &&
task_is_scheduled job_task sched i t)
(fun tsk_k0 : sporadic_task =>
interferes_with_tsk tsk_k0 &&
(x tsk_k0 < R - task_cost tsk + 1) &&
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.
unfold interfering_tasks_at_t.
rewrite -count_predT count_filter.
rewrite leq_eqVlt; apply/orP; left; apply/eqP.
apply eq_count; red; simpl.
intros i.
destruct (interferes_with_tsk i),
(task_is_scheduled job_task sched i t);
rewrite 3?andTb ?andFb ?andbF ?andbT /=; try ins.
by rewrite leqNgt orNb.
}
{
unfold x at 2, task_interference.
rewrite [\sum_(i <- ts | _) _](eq_bigr
(fun i => \sum_(job_arrival j <= t < job_arrival j + R)
(i \in ts) && interferes_with_tsk i &&
backlogged job_cost rate sched j t &&
task_is_scheduled job_task sched i t));
last first.
{
ins; destruct ((i \in ts) && interferes_with_tsk i) eqn:INTERi;
first by move: INTERi => /andP [_ INTERi]; apply eq_bigr; ins; rewrite INTERi andTb.
by rewrite (eq_bigr (fun i => 0));
[by rewrite big_const_nat iter_addn mul0n addn0 | by ins].
}
{
rewrite exchange_big /=; apply leq_sum; intros t _.
unfold total_interference_B.
destruct (backlogged job_cost rate sched j t); last by ins.
rewrite mul1n -sum1_count.
rewrite big_seq_cond big_mkcond [\sum_(i <- ts | _ < _) _]big_mkcond.
apply leq_sum; ins; destruct (x i<R - task_cost tsk + 1);
[by rewrite 2!andbT andbA | by rewrite 2!andbF].
}
}
}
rewrite big_const_seq iter_addn addn0; fold cardA.
apply leq_trans with (n := (R-task_cost tsk+1)*cardA +
(R-task_cost tsk+1)*(num_cpus-cardA));
last by rewrite leq_add2l.
by rewrite -mulnDr subnKC //; apply ltnW.
}
(* 4) Now, we prove that the Bertogna's interference bound
is not enough to cover the sum of the "minimum" term over
all tasks (artifact of the proof by contradiction). *)
assert (SUM: \sum_((tsk_k, R_k) <- hp_bounds)
minn (x tsk_k) (R - task_cost tsk + 1) >
total_interference_bound_fp task_cost task_period tsk hp_bounds
R higher_eq_priority).
{
apply leq_trans with (n := \sum_(tsk_k <- ts) minn (x tsk_k) (R - task_cost tsk + 1));
last first.
{
rewrite (eq_bigr (fun i => minn (x (fst i)) (R - task_cost tsk + 1)));
last by ins; destruct i.
apply leq_trans with (n := \sum_(tsk_k <- ts | interferes_with_tsk tsk_k) minn (x tsk_k) (R - task_cost tsk + 1)).
{
rewrite [\sum_(_ <- _ | interferes_with_tsk _)_]big_mkcond eq_leq //.
apply eq_bigr; intros i _; unfold x.
by destruct (interferes_with_tsk i); rewrite ?andbT ?andbF ?min0n.
}
have MAP := big_map (fun x => fst x) (fun i => true) (fun i => minn (x i) (R - task_cost tsk + 1)).
by unfold unzip1 in *; rewrite -MAP -UNZIP -big_filter.
}
apply ltn_div_trunc with (d := num_cpus);
first by apply H_at_least_one_cpu.
rewrite -(ltn_add2l (task_cost tsk)) -REC.
rewrite -addn1 -leq_subLR. rewrite -[R + 1 - _]subh1; last by rewrite REC; apply leq_addr.
rewrite leq_divRL; last by apply H_at_least_one_cpu.
apply MINSERV.
apply leq_trans with (n := X * num_cpus); last by rewrite ALLBUSY.
by rewrite leq_mul2r; apply/orP; right; apply INTERF.
}
(* 5) This implies that there exists a tuple (tsk_k, R_k) such that
min (x_k, R - e_i + 1) > min (W_k, R - e_i + 1). *)
assert (EX: has (fun tup : task_with_response_time =>
let (tsk_k, R_k) := tup in
(tsk_k \in ts) &&
interferes_with_tsk tsk_k &&
(minn (x tsk_k) (R - task_cost tsk + 1) >
minn (workload_bound (tsk_k, snd tup)) (R - task_cost tsk + 1)))
hp_bounds).
{
apply/negP; unfold not; intro NOTHAS.
move: NOTHAS => /negP /hasPn ALL.
rewrite -[_ < _]negbK in SUM.
move: SUM => /negP SUM; apply SUM; rewrite -leqNgt.
unfold total_interference_bound_fp.
rewrite [\sum_(i <- _ | let '(tsk_other, _) := i in _)_]big_mkcond.
rewrite big_seq_cond [\sum_(i <- _ | true) _]big_seq_cond.
apply leq_sum; move => tsk_k /andP [HPk _]; destruct tsk_k as [tsk_k R_k].
specialize (ALL (tsk_k, R_k) HPk).
unfold interference_bound, workload_bound, x in *.
fold (interferes_with_tsk); destruct (interferes_with_tsk tsk_k) eqn:INTERFk;
[rewrite andbT in ALL; rewrite andbT | by rewrite andbF min0n].
destruct (tsk_k \in ts) eqn:INk; last by rewrite min0n.
by rewrite andTb -leqNgt in ALL.
}
(* For this particular task, we show that x_k > W_k.
This contradicts the previous claim. *)
move: EX => /hasP EX; destruct EX as [tup_k HPk LTmin].
destruct tup_k as [tsk_k R_k]; simpl in LTmin.
move: LTmin => /andP [INTERFk LTmin]; move: (INTERFk) => /andP [INk INTERFk'].
rewrite INTERFk' in LTmin; unfold minn at 1 in LTmin.
destruct (W task_cost task_period tsk_k R_k R < R - task_cost tsk + 1); rewrite leq_min in LTmin;
last by move: LTmin => /andP [_ BUG]; rewrite ltnn in BUG.
move: LTmin => /andP [BUG _]; des.
specialize (WORKLOAD tsk_k INTERFk R_k HPk).
apply leq_ltn_trans with (p := x tsk_k) in WORKLOAD; first by rewrite ltnn in WORKLOAD.
by unfold workload_bound; rewrite INTERFk'; apply BUG.
Qed.
End ResponseTimeBound.
End ResponseTimeAnalysis.