From febf2ef8004127ef0ba3b40c70aabf4164c8f003 Mon Sep 17 00:00:00 2001
From: Felipe Cerqueira <felipec@mpi-sws.org>
Date: Tue, 10 Nov 2015 09:01:11 +0100
Subject: [PATCH] Start Guan analysis
---
GuanDefs.v | 629 ++++++++++++++++++++++++++++++++++++++++++++
GuanFP.v | 753 +++++++++++++++++++++++++++++++++++++++++++++++++++++
Vbase.v | 4 +-
helper.v | 35 ++-
4 files changed, 1408 insertions(+), 13 deletions(-)
create mode 100644 GuanDefs.v
create mode 100644 GuanFP.v
diff --git a/GuanDefs.v b/GuanDefs.v
new file mode 100644
index 000000000..80655854c
--- /dev/null
+++ b/GuanDefs.v
@@ -0,0 +1,629 @@
+Require Import Vbase TaskDefs JobDefs TaskArrivalDefs ScheduleDefs
+ PlatformDefs WorkloadDefs BertognaResponseTimeDefs SchedulabilityDefs PriorityDefs
+ ResponseTimeDefs divround helper
+ ssreflect ssrbool eqtype ssrnat seq fintype bigop div path tuple.
+
+Module ResponseTimeAnalysisGuan.
+
+ Import Job SporadicTaskset ScheduleOfTaskWithJitter Schedulability ResponseTime Priority SporadicTaskArrival.
+ Export Workload ResponseTimeAnalysis.
+
+ Section InterferenceBoundGuan.
+
+ Context {sporadic_task: eqType}.
+ Variable task_cost: sporadic_task -> nat.
+ Variable task_period: sporadic_task -> nat.
+ Variable task_deadline: sporadic_task -> nat.
+
+ Variable num_cpus: nat.
+ Variable higher_eq_priority: fp_policy sporadic_task.
+
+ (* 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 TasksetPartition.
+
+ (* Let's filter the list of task and response-times so that it only has interfering tasks. *)
+ Let interfering_tasks :=
+ [seq (tsk_other, R) <- R_prev | is_interfering_task_fp tsk higher_eq_priority tsk_other].
+
+ (* After that, we list all possible pairs of subsets of that list:
+ [(subset0, subset1), (subset0, subset2), ...]*)
+ Let all_combinations :=
+ zip (powerset interfering_tasks) (powerset interfering_tasks).
+
+ (* Finally, we let (NC, CI) be all the pairs of subsets that are partitions
+ and such that the number of carried-in tasks is at most num_cpus - 1. *)
+ Definition valid_NC_CI_partitions :=
+ [seq (NC, CI) <- all_combinations | no_intersection NC CI &&
+ (size CI <= num_cpus - 1)].
+ End TasksetPartition.
+
+ (* Based on Bertogna and Cirinei's interference bound, ... *)
+ Let I := interference_bound task_cost task_period tsk delta.
+
+ (* Guan et al.'s analysis defines an interference bound based on the maximum interference
+ across all partitions of (NC, CI), i.e., non-carried-in and carried-in tasks.
+ For the sake of simplicity, we compute the maximum by enumeration, instead of using
+ a linear-time algorithm. *)
+ Definition guan_interference_bound :=
+ \max_((NC, CI) <- valid_NC_CI_partitions)
+ (\sum_((tsk_other, R) <- NC) I (tsk_other,R) +
+ \sum_((tsk_other, R) <- CI) I (tsk_other,R)).
+
+ End InterferenceBoundGuan.
+
+ Section ResponseTimeBoundGuan.
+
+ 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_execute_after_jitter:
+ 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.
+
+ (* 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 sporadic_task.
+
+ Let interferes_with_tsk := is_interfering_task_fp tsk higher_eq_priority.
+
+ (* Assume that for any interfering task, a response-time
+ bound R_other is known. *)
+ Hypothesis H_all_interfering_tasks_in_hp_bounds:
+ [seq tsk_hp <- ts | interferes_with_tsk tsk_hp] = unzip1 hp_bounds.
+
+ Lemma exists_R :
+ forall hp_tsk,
+ hp_tsk \in ts ->
+ interferes_with_tsk hp_tsk ->
+ exists R,
+ (hp_tsk, R) \in hp_bounds.
+ Proof.
+ intros hp_tsk IN INTERF.
+ rewrite -[hp_bounds]zip_unzip; apply exists_unzip2.
+ by rewrite zip_unzip -H_all_interfering_tasks_in_hp_bounds mem_filter; apply/andP.
+ Qed.
+
+ Hypothesis H_response_time_of_interfering_tasks_is_known2:
+ 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, ... *)
+ Let I := total_interference_bound_fp task_cost task_period
+ tsk hp_bounds R higher_eq_priority.
+ Hypothesis H_response_time_recurrence_holds :
+ R = task_cost tsk + (div_floor I 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. *)
+ Theorem bertogna_cirinei_response_time_bound_fp_with_jitter :
+ 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_with_jitter,
+ 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_known2 into RESP,
+ H_all_interfering_tasks_in_hp_bounds into FST,
+ 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_jitter task_cost task_period task_jitter 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.
+
+ (* Note that j cannot have completed by job_arrival j + R either. *)
+ assert (COMPLETED': ~~ completed job_cost rate sched j (job_arrival j + R)).
+ {
+ apply/negP; unfold not; intro BUG.
+ apply completion_monotonic with (t' := job_arrival j + R') in BUG;
+ try (by ins);
+ [ by rewrite BUG in COMPLETED
+ | by unfold R'; rewrite addnA; apply leq_addr].
+ }
+
+ (* 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.
+ exploit (exists_R tsk_k); [by ins | by ins | intro INhp; des].
+ 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_jitter with (task_deadline0 := task_deadline) (job_cost0 := job_cost) (job_deadline0 := job_deadline) (job_jitter0 := job_jitter); 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 PARAMS2 JOBtsk'.
+ apply completion_monotonic with (t := job_arrival j' + R0); 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;
+ last by apply arrival_before_jitter with (job_jitter0 := job_jitter).
+ rewrite EQinterf 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 PARAMS1.
+ }
+ 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 PARAMS1.
+ 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_with_jitter =>
+ 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_with_jitter =>
+ interferes_with_tsk i &&
+ (R - task_cost tsk + 1 <= x i) &&
+ task_is_scheduled job_task sched i t)
+ (fun tsk_k0 : sporadic_task_with_jitter =>
+ 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) >
+ I).
+ {
+ 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 -FST -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 I, total_interference_bound_fp_jitter.
+ 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_jitter task_cost task_period task_jitter 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 UnderFPScheduling.
+
+ Section UnderJLFPScheduling.
+
+ (* to be completed... *)
+
+ End UnderJLFPScheduling.
+
+ End ResponseTimeBound.
+
+End ResponseTimeAnalysisJitter.
\ No newline at end of file
diff --git a/GuanFP.v b/GuanFP.v
new file mode 100644
index 000000000..d8de9d6da
--- /dev/null
+++ b/GuanFP.v
@@ -0,0 +1,753 @@
+Require Import Vbase JobDefs TaskDefs ScheduleDefs TaskArrivalDefs PriorityDefs WorkloadDefsJitter BertognaResponseTimeDefsJitter divround helper
+ ssreflect ssrbool eqtype ssrnat seq fintype bigop div path tuple.
+
+Module ResponseTimeIterationFPWithJitter.
+
+ Import Job ScheduleOfTaskWithJitter SporadicTaskset SporadicTaskArrival Priority WorkloadWithJitter ResponseTimeAnalysisJitter.
+
+ Section Analysis.
+
+ Context {sporadic_task_with_jitter: eqType}.
+ Variable task_cost: sporadic_task_with_jitter -> nat.
+ Variable task_period: sporadic_task_with_jitter -> nat.
+ Variable task_deadline: sporadic_task_with_jitter -> nat.
+ Variable task_jitter: sporadic_task_with_jitter -> nat.
+
+ Let task_with_response_time := (sporadic_task_with_jitter * nat)%type.
+
+ Context {Job: eqType}.
+ Variable job_cost: Job -> nat.
+ Variable job_deadline: Job -> nat.
+ Variable job_task: Job -> sporadic_task_with_jitter.
+ Variable job_jitter: Job -> nat.
+
+ Variable num_cpus: nat.
+ Variable higher_eq_priority: fp_policy sporadic_task_with_jitter.
+
+ (* Next we define the fixed-point iteration for computing
+ Bertogna's response-time bound for any task in ts. *)
+
+ Let I (tsk: sporadic_task_with_jitter)
+ (R_prev: seq task_with_response_time) (delta: time) :=
+ total_interference_bound_fp_jitter task_cost task_period task_jitter
+ tsk R_prev delta higher_eq_priority.
+
+ (* First, given a sequence of pairs R_prev = [..., (tsk_hp, R_hp)] of
+ response-time bounds for the higher-priority tasks, we compute
+ the response-time bound of tsk using the following iteration:
+
+ R_tsk <- f^step (R_tsk),
+ where f is the response-time recurrence,
+ step is the number of iterations,
+ and f^0 = task_cost tsk. *)
+ Definition per_task_rta (tsk: sporadic_task_with_jitter)
+ (R_prev: seq task_with_response_time) (step: nat) :=
+ iter step
+ (fun t => task_cost tsk +
+ div_floor (I tsk R_prev t) num_cpus)
+ (task_cost tsk).
+
+ (* To ensure that the iteration converges, we will apply per_task_rta
+ a "sufficient" number of times: task_deadline tsk + 1.
+ Note that (deadline + 1) is a pessimistic bound on the number of
+ steps, but we don't care about precise runtime complexity here. *)
+ Let max_steps (tsk: sporadic_task_with_jitter) :=
+ task_deadline tsk + 1.
+
+ (* Next we compute the response-time bounds for the entire task set.
+ Since high-priority tasks may not be schedulable, we allow the
+ computation to fail.
+ Thus, given the response-time bound of previous tasks, we either
+ (a) append the response-time bound (tsk, R) of the current task
+ to the list of pairs, or,
+ (b) return None if the response-time analysis failed. *)
+ Definition R_list_helper (hp_pairs: option (seq task_with_response_time))
+ (tsk: sporadic_task_with_jitter) :=
+ if hp_pairs is Some rt_bounds then
+ let R := per_task_rta tsk rt_bounds (max_steps tsk) in
+ let R' := R + task_jitter tsk in
+ if R' <= task_deadline tsk then
+ Some (rcons rt_bounds (tsk, R'))
+ else None
+ else None.
+
+ (* To return the complete list of response-time bounds for any task set,
+ we just apply foldl (reduce) using the function above. *)
+ Definition R_list (ts: taskset_of sporadic_task_with_jitter) : option (seq task_with_response_time) :=
+ foldl R_list_helper (Some [::]) ts.
+
+ (* The schedulability test simply checks if we got a list of
+ response-time bounds (i.e., if the computation did not fail). *)
+ Definition fp_schedulable (ts: taskset_of sporadic_task_with_jitter) :=
+ R_list ts != None.
+
+ Section AuxiliaryLemmas.
+
+ (* In this section, we prove several helper lemmas about the
+ list of response-time bounds, such as:
+ (1) Equality among tasks in R_list and in the task set.
+ (2) If (tsk, R) \in R_list, then R <= task_deadline tsk.
+ (3) If (tsk, R) \in R_list, then R >= task_cost tsk.
+ (4) If per_task_rta returns a bound <= deadline, then the
+ iteration reached a fixed-point. *)
+
+ Lemma R_list_rcons_prefix :
+ forall ts' hp_bounds tsk1 tsk2 R,
+ R_list (rcons ts' tsk1) = Some (rcons hp_bounds (tsk2, R)) ->
+ R_list ts' = Some hp_bounds.
+ Proof.
+ intros ts hp_bounds tsk1 tsk2 R SOME.
+ rewrite -cats1 in SOME.
+ unfold R_list in *.
+ rewrite foldl_cat in SOME.
+ simpl in SOME.
+ unfold R_list_helper in SOME.
+ desf; rewrite Heq; rename H0 into EQ.
+ move: EQ => /eqP EQ.
+ rewrite eqseq_rcons in EQ.
+ move: EQ => /andP [/eqP EQ _].
+ by f_equal.
+ Qed.
+
+ Lemma R_list_rcons_task :
+ forall ts' hp_bounds tsk1 tsk2 R,
+ R_list (rcons ts' tsk1) = Some (rcons hp_bounds (tsk2, R)) ->
+ tsk1 = tsk2.
+ Proof.
+ intros ts hp_bounds tsk1 tsk2 R SOME.
+ rewrite -cats1 in SOME.
+ unfold R_list in *.
+ rewrite foldl_cat in SOME.
+ simpl in SOME.
+ unfold R_list_helper in SOME.
+ desf; rename H0 into EQ.
+ move: EQ => /eqP EQ.
+ rewrite eqseq_rcons in EQ.
+ move: EQ => /andP [_ /eqP EQ].
+ by inversion EQ.
+ Qed.
+
+ Lemma R_list_rcons_response_time :
+ forall ts' hp_bounds tsk R,
+ R_list (rcons ts' tsk) = Some (rcons hp_bounds (tsk, R)) ->
+ R = per_task_rta tsk hp_bounds (max_steps tsk) + task_jitter tsk.
+ Proof.
+ intros ts hp_bounds tsk R SOME.
+ rewrite -cats1 in SOME.
+ unfold R_list in SOME.
+ rewrite foldl_cat in SOME.
+ simpl in SOME.
+ unfold R_list_helper in SOME.
+ desf; rename H0 into EQ; move: EQ => /eqP EQ.
+ rewrite eqseq_rcons in EQ; move: EQ => /andP [/eqP EQ1 /eqP EQ2].
+ by inversion EQ2; rewrite EQ1.
+ Qed.
+
+ Lemma R_list_le_deadline :
+ forall ts' rt_bounds tsk R,
+ R_list ts' = Some rt_bounds ->
+ (tsk, R) \in rt_bounds ->
+ R <= task_deadline tsk.
+ Proof.
+ intros ts; induction ts as [| ts' tsk_lst] using last_ind.
+ {
+ intros rt_bounds tsk R SOME IN.
+ by inversion SOME; subst; rewrite in_nil in IN.
+ }
+ {
+ intros rt_bounds tsk_i R SOME IN.
+ destruct (lastP rt_bounds) as [|rt_bounds (tsk_lst', R_lst)];
+ first by rewrite in_nil in IN.
+ rewrite mem_rcons in_cons in IN; move: IN => /orP IN.
+ destruct IN as [LAST | FRONT].
+ {
+ move: LAST => /eqP LAST.
+ rewrite -cats1 in SOME.
+ unfold R_list in *.
+ rewrite foldl_cat in SOME.
+ simpl in SOME.
+ unfold R_list_helper in SOME.
+ desf; rename H0 into EQ.
+ move: EQ => /eqP EQ.
+ rewrite eqseq_rcons in EQ.
+ move: EQ => /andP [_ /eqP EQ].
+ inversion EQ; subst.
+ by apply Heq0.
+ }
+ {
+ apply IHts with (rt_bounds := rt_bounds); last by ins.
+ by apply R_list_rcons_prefix in SOME.
+ }
+ }
+ Qed.
+
+ Lemma R_list_ge_cost :
+ forall ts' rt_bounds tsk R,
+ R_list ts' = Some rt_bounds ->
+ (tsk, R) \in rt_bounds ->
+ R >= task_cost tsk.
+ Proof.
+ intros ts; induction ts as [| ts' tsk_lst] using last_ind.
+ {
+ intros rt_bounds tsk R SOME IN.
+ by inversion SOME; subst; rewrite in_nil in IN.
+ }
+ {
+ intros rt_bounds tsk_i R SOME IN.
+ destruct (lastP rt_bounds) as [|rt_bounds (tsk_lst', R_lst)];
+ first by rewrite in_nil in IN.
+ rewrite mem_rcons in_cons in IN; move: IN => /orP IN.
+ destruct IN as [LAST | FRONT].
+ {
+ move: LAST => /eqP LAST.
+ rewrite -cats1 in SOME.
+ unfold R_list in *.
+ rewrite foldl_cat in SOME.
+ simpl in SOME.
+ unfold R_list_helper in SOME.
+ desf; rename H0 into EQ.
+ move: EQ => /eqP EQ.
+ rewrite eqseq_rcons in EQ.
+ move: EQ => /andP [_ /eqP EQ].
+ inversion EQ; subst.
+ by destruct (max_steps tsk_lst');
+ [by apply leq_addr | by rewrite -addnA leq_addr].
+ }
+ {
+ apply IHts with (rt_bounds := rt_bounds); last by ins.
+ by apply R_list_rcons_prefix in SOME.
+ }
+ }
+ Qed.
+
+ Lemma R_list_non_empty :
+ forall ts' rt_bounds tsk,
+ R_list ts' = Some rt_bounds ->
+ (tsk \in ts' <->
+ exists R,
+ (tsk, R) \in rt_bounds).
+ Proof.
+ intros ts; induction ts as [| ts' tsk_lst] using last_ind.
+ {
+ intros rt_bounds tsk SOME.
+ inversion SOME; rewrite in_nil; split; first by ins.
+ by intro EX; des; rewrite in_nil in EX.
+ }
+ {
+ intros rt_bounds tsk_i SOME.
+ destruct (lastP rt_bounds) as [|rt_bounds (tsk_lst', R_lst)].
+ {
+ split; last first; intro EX; des; first by rewrite in_nil in EX.
+ unfold R_list in *.
+ rewrite -cats1 foldl_cat in SOME.
+ simpl in SOME.
+ unfold R_list_helper in *; desf; rename H0 into EQ.
+ destruct l; first by ins.
+ by rewrite rcons_cons in EQ; inversion EQ.
+ }
+ split.
+ {
+ intros IN; rewrite mem_rcons in_cons in IN; move: IN => /orP IN.
+ destruct IN as [LAST | FRONT].
+ {
+ move: LAST => /eqP LAST; subst tsk_i.
+ generalize SOME; apply R_list_rcons_task in SOME; subst tsk_lst'; intro SOME.
+ exists R_lst.
+ by rewrite mem_rcons in_cons; apply/orP; left.
+ }
+ {
+ apply R_list_rcons_prefix in SOME.
+ exploit (IHts rt_bounds tsk_i); [by ins | intro EX].
+ apply EX in FRONT; des.
+ by exists R; rewrite mem_rcons in_cons; apply/orP; right.
+ }
+ }
+ {
+ intro IN; des.
+ rewrite mem_rcons in_cons in IN; move: IN => /orP IN.
+ destruct IN as [LAST | FRONT].
+ {
+ move: LAST => /eqP LAST.
+ inversion LAST; subst tsk_i R; clear LAST.
+ apply R_list_rcons_task in SOME; subst.
+ by rewrite mem_rcons in_cons; apply/orP; left.
+ }
+ {
+ rewrite mem_rcons in_cons; apply/orP; right.
+ exploit (IHts rt_bounds tsk_i);
+ [by apply R_list_rcons_prefix in SOME | intro EX].
+ by apply EX; exists R.
+ }
+ }
+ }
+ Qed.
+
+ (* To prove convergence of R, we first show convergence of rt_rec. *) Lemma per_task_rta_converges:
+ forall ts' tsk rt_bounds,
+ valid_sporadic_taskset task_cost task_period task_deadline ts' ->
+ R_list ts' = Some rt_bounds ->
+ per_task_rta tsk rt_bounds (max_steps tsk) <= task_deadline tsk ->
+ per_task_rta tsk rt_bounds (max_steps tsk) =
+ per_task_rta tsk rt_bounds (max_steps tsk).+1.
+ Proof.
+ unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
+
+ (* To simplify, let's call the function f.*)
+ intros ts' tsk rt_bounds VALID SOME LE;
+ set (f := per_task_rta tsk rt_bounds); fold f in LE.
+
+ (* First prove that f is monotonic.*)
+ assert (MON: forall x1 x2, x1 <= x2 -> f x1 <= f x2).
+ {
+ intros x1 x2 LEx; unfold f, per_task_rta.
+ apply fun_mon_iter_mon; [by ins | by ins; apply leq_addr |].
+ clear LEx x1 x2; intros x1 x2 LEx.
+
+ unfold div_floor, I, total_interference_bound_fp_jitter.
+ rewrite big_seq_cond [\sum_(i <- _ | let '(tsk_other, _) := i in
+ _ && (tsk_other != tsk))_]big_seq_cond.
+ rewrite leq_add2l leq_div2r // leq_sum //.
+
+ intros i; destruct (i \in rt_bounds) eqn:HP;
+ last by rewrite andFb.
+ destruct i as [i R]; intros _.
+ have GE_COST := (R_list_ge_cost ts' rt_bounds i R).
+ have INts := (R_list_non_empty ts' rt_bounds i SOME).
+ destruct INts as [_ EX]; exploit EX; [by exists R | intro IN].
+ unfold interference_bound_jitter; simpl.
+ rewrite leq_min; apply/andP; split.
+ {
+ apply leq_trans with (n := W_jitter task_cost task_period task_jitter i R x1);
+ first by apply geq_minl.
+ specialize (VALID i IN); des.
+ by apply W_jitter_monotonic; try (by ins); apply GE_COST.
+ }
+ {
+ apply leq_trans with (n := x1 - task_cost tsk + 1);
+ first by apply geq_minr.
+ by rewrite leq_add2r leq_sub2r //.
+ }
+ }
+
+ (* Either f converges by the deadline or not. *)
+ unfold max_steps in *; rewrite -> addn1 in *.
+ destruct ([exists k in 'I_(task_deadline tsk).+1,
+ f k == f k.+1]) eqn:EX.
+ {
+ move: EX => /exists_inP EX; destruct EX as [k _ ITERk].
+ move: ITERk => /eqP ITERk.
+ by apply iter_fix with (k := k);
+ [by ins | by apply ltnW, ltn_ord].
+ }
+ apply negbT in EX; rewrite negb_exists_in in EX.
+ move: EX => /forall_inP EX.
+ assert (GROWS: forall k: 'I_(task_deadline tsk).+1,
+ f k < f k.+1).
+ {
+ intros k; rewrite ltn_neqAle; apply/andP; split; first by apply EX.
+ apply MON, leqnSn.
+ }
+
+ (* If it doesn't converge, then it becomes larger than the deadline.
+ But initialy we assumed otherwise. Contradiction! *)
+ assert (BY1: f (task_deadline tsk).+1 > task_deadline tsk).
+ {
+ clear MON LE EX.
+ induction (task_deadline tsk).+1; first by ins.
+ apply leq_ltn_trans with (n := f n);
+ last by apply (GROWS (Ordinal (ltnSn n))).
+ apply IHn; intros k.
+ by apply (GROWS (widen_ord (leqnSn n) k)).
+ }
+ by apply leq_ltn_trans with (m := f (task_deadline tsk).+1) in BY1;
+ [by rewrite ltnn in BY1 | by ins].
+ Qed.
+
+ Lemma per_task_rta_fold :
+ forall tsk rt_bounds,
+ task_cost tsk +
+ div_floor (I tsk rt_bounds (per_task_rta tsk rt_bounds (max_steps tsk))) num_cpus
+ = per_task_rta tsk rt_bounds (max_steps tsk).+1.
+ Proof.
+ by ins.
+ Qed.
+
+ Lemma R_list_unzip1 :
+ forall ts' tsk hp_bounds R,
+ transitive higher_eq_priority ->
+ uniq (rcons ts' tsk) ->
+ sorted higher_eq_priority (rcons ts' tsk) ->
+ R_list (rcons ts' tsk) = Some (rcons hp_bounds (tsk, R)) ->
+ [seq tsk_hp <- rcons ts' tsk | is_interfering_task_fp tsk higher_eq_priority tsk_hp] =
+ unzip1 hp_bounds.
+ Proof.
+ intros ts tsk hp_bounds R TRANS.
+ revert tsk hp_bounds R.
+ induction ts as [| ts' tsk_lst] using last_ind.
+ {
+ intros tsk hp_bounds R _ _ SOME; simpl in *.
+ unfold is_interfering_task_fp.
+ rewrite eq_refl andbF.
+ destruct hp_bounds; first by ins.
+ unfold R_list in SOME; inversion SOME; desf.
+ by destruct hp_bounds.
+ }
+ {
+ intros tsk hp_bounds R UNIQ SORTED SOME.
+ destruct (lastP hp_bounds) as [| hp_bounds (tsk_lst', R_lst)].
+ {
+ apply R_list_rcons_prefix in SOME.
+ unfold R_list in SOME.
+ rewrite -cats1 foldl_cat in SOME.
+ unfold R_list_helper in SOME.
+ inversion SOME; desf.
+ by destruct l.
+ }
+ generalize SOME; apply R_list_rcons_prefix, R_list_rcons_task in SOME; subst tsk_lst'; intro SOME.
+ specialize (IHts tsk_lst hp_bounds R_lst).
+ rewrite filter_rcons in IHts.
+ unfold is_interfering_task_fp in IHts.
+ rewrite eq_refl andbF in IHts.
+ assert (NOTHP: is_interfering_task_fp tsk higher_eq_priority tsk = false).
+ {
+ by unfold is_interfering_task_fp; rewrite eq_refl andbF.
+ } rewrite filter_rcons NOTHP; clear NOTHP.
+ assert (HP: is_interfering_task_fp tsk higher_eq_priority tsk_lst).
+ {
+ unfold is_interfering_task_fp; apply/andP; split.
+ {
+ apply order_sorted_rcons with (x := tsk_lst) in SORTED; try (by ins).
+ by rewrite mem_rcons in_cons; apply/orP; left.
+ }
+ {
+ rewrite 2!rcons_uniq mem_rcons in_cons negb_or in UNIQ.
+ move : UNIQ => /andP [/andP [UNIQ _] _].
+ by rewrite eq_sym in UNIQ.
+ }
+ } rewrite filter_rcons HP; clear HP.
+ unfold unzip1; rewrite map_rcons /=; f_equal.
+ assert (SHIFT: [seq tsk_hp <- ts' | is_interfering_task_fp tsk higher_eq_priority tsk_hp] = [seq tsk_hp <- ts'
+ | is_interfering_task_fp tsk_lst higher_eq_priority tsk_hp]).
+ {
+ apply eq_in_filter; red.
+ unfold is_interfering_task_fp; intros x INx.
+ rewrite 2!rcons_uniq mem_rcons in_cons negb_or in UNIQ.
+ move: UNIQ => /andP [/andP [NEQ NOTIN] /andP [NOTIN' UNIQ]].
+ destruct (x == tsk) eqn:EQtsk.
+ {
+ move: EQtsk => /eqP EQtsk; subst.
+ by rewrite INx in NOTIN.
+ }
+ destruct (x == tsk_lst) eqn:EQlst.
+ {
+ move: EQlst => /eqP EQlst; subst.
+ by rewrite INx in NOTIN'.
+ }
+ rewrite 2!andbT.
+ generalize SORTED; intro SORTED'.
+ have bla := order_sorted_rcons.
+ apply order_sorted_rcons with (x0 := x) in SORTED; try (by ins);
+ last by rewrite mem_rcons in_cons; apply/orP; right.
+ rewrite SORTED.
+ apply sorted_rcons_prefix in SORTED'.
+ by apply order_sorted_rcons with (x0 := x) in SORTED'.
+ } rewrite SHIFT; clear SHIFT.
+ apply IHts.
+ by rewrite rcons_uniq in UNIQ; move: UNIQ => /andP [_ UNIQ].
+ by apply sorted_rcons_prefix in SORTED.
+ by apply R_list_rcons_prefix in SOME.
+ }
+ Qed.
+
+ End AuxiliaryLemmas.
+
+ Section Proof.
+
+ (* Consider a task set ts. *)
+ Variable ts: taskset_of sporadic_task_with_jitter.
+
+ (* Assume that higher_eq_priority is a total order.
+ Actually, it just needs to be total over the task set,
+ but to weaken the assumption, I have to re-prove many lemmas
+ about ordering in ssreflect. This can be done later. *)
+ Hypothesis H_valid_policy: valid_fp_policy higher_eq_priority.
+ Hypothesis H_unique_priorities: antisymmetric higher_eq_priority.
+
+ (* Assume the task set has no duplicates, ... *)
+ Hypothesis H_ts_is_a_set: uniq ts.
+
+ (* ...all tasks have valid parameters, ... *)
+ Hypothesis H_valid_task_parameters:
+ valid_sporadic_taskset task_cost task_period task_deadline ts.
+
+ (* ...restricted deadlines, ...*)
+ Hypothesis H_restricted_deadlines:
+ forall tsk, tsk \in ts -> task_deadline tsk <= task_period tsk.
+
+ (* ...and tasks are ordered by increasing priorities. *)
+ Hypothesis H_sorted_ts: sorted higher_eq_priority ts.
+
+ (* Next, consider any arrival sequence such that...*)
+ Context {arr_seq: arrival_sequence Job}.
+
+ (* ...all jobs come from task set ts, ...*)
+ Hypothesis H_all_jobs_from_taskset:
+ forall (j: JobIn arr_seq), job_task j \in ts.
+
+ (* ...they have valid parameters,...*)
+ Hypothesis H_valid_job_parameters:
+ forall (j: JobIn arr_seq),
+ valid_sporadic_job_with_jitter task_cost task_deadline task_jitter job_cost job_deadline job_task job_jitter j.
+
+ (* ... and satisfy the sporadic task model.*)
+ Hypothesis H_sporadic_tasks:
+ sporadic_task_model task_period arr_seq job_task.
+
+ (* Then, consider any platform with at least one CPU and unit
+ unit execution rate, where...*)
+ Variable rate: Job -> processor num_cpus -> nat.
+ Variable sched: schedule num_cpus arr_seq.
+ Hypothesis H_at_least_one_cpu :
+ num_cpus > 0.
+ Hypothesis H_rate_equals_one :
+ forall j cpu, rate j cpu = 1.
+
+ (* ...jobs only execute after the jitter and no longer
+ than their execution costs,... *)
+ Hypothesis H_jobs_execute_after_jitter:
+ jobs_execute_after_jitter job_jitter sched.
+ Hypothesis H_completed_jobs_dont_execute:
+ completed_jobs_dont_execute job_cost rate sched.
+
+ (* ...and do not execute in parallel. *)
+ Hypothesis H_no_parallelism:
+ jobs_dont_execute_in_parallel sched.
+
+ (* Assume the platform satisfies the global scheduling invariant. *)
+ Hypothesis H_global_scheduling_invariant:
+ forall (tsk: sporadic_task_with_jitter) (j: JobIn arr_seq) (t: time),
+ tsk \in ts ->
+ job_task j = tsk ->
+ backlogged job_cost rate sched j t ->
+ count
+ (fun tsk_other : _ =>
+ is_interfering_task_fp tsk higher_eq_priority tsk_other &&
+ task_is_scheduled job_task sched tsk_other t) ts = num_cpus.
+
+ Definition no_deadline_missed_by_task (tsk: sporadic_task_with_jitter) :=
+ task_misses_no_deadline job_cost job_deadline job_task rate sched tsk.
+ Definition no_deadline_missed_by_job :=
+ job_misses_no_deadline job_cost job_deadline rate sched.
+
+ Section HelperLemma.
+
+ (* The following lemma states that the response-time bounds
+ computed using R_list are valid. *)
+ Lemma R_list_has_response_time_bounds :
+ forall rt_bounds tsk R,
+ R_list ts = Some rt_bounds ->
+ (tsk, R) \in rt_bounds ->
+ forall j : JobIn arr_seq,
+ job_task j = tsk ->
+ completed job_cost rate sched j (job_arrival j + R).
+ Proof.
+ unfold valid_fp_policy, fp_is_transitive, fp_is_reflexive,
+ fp_is_total in *.
+ rename H_valid_job_parameters into JOBPARAMS,
+ H_valid_task_parameters into TASKPARAMS,
+ H_restricted_deadlines into RESTR,
+ H_completed_jobs_dont_execute into COMP,
+ H_jobs_execute_after_jitter into MUSTARRIVE,
+ H_global_scheduling_invariant into INVARIANT,
+ H_sorted_ts into SORT,
+ H_unique_priorities into UNIQ,
+ H_all_jobs_from_taskset into ALLJOBS,
+ H_ts_is_a_set into SET.
+ destruct H_valid_policy as [REFL [TRANS TOTAL]]; clear ALLJOBS.
+
+ unfold fp_schedulable, R_list in *.
+ induction ts as [| ts' tsk_i IH] using last_ind.
+ {
+ intros rt_bounds tsk R SOME IN.
+ by inversion SOME; subst; rewrite in_nil in IN.
+ }
+ {
+ intros rt_bounds tsk R SOME IN j JOBj.
+ destruct (lastP rt_bounds) as [| hp_bounds (tsk_lst, R_lst)];
+ first by rewrite in_nil in IN.
+ rewrite mem_rcons in_cons in IN; move: IN => /orP IN.
+ destruct IN as [LAST | BEGINNING]; last first.
+ {
+ apply IH with (rt_bounds := hp_bounds) (tsk := tsk); try (by ins).
+ by rewrite rcons_uniq in SET; move: SET => /andP [_ SET].
+ by ins; red; ins; apply TASKPARAMS; rewrite mem_rcons in_cons; apply/orP; right.
+ by ins; apply RESTR; rewrite mem_rcons in_cons; apply/orP; right.
+ by apply sorted_rcons_prefix in SORT.
+ {
+ intros tsk0 j0 t IN0 JOB0 BACK0.
+ exploit (INVARIANT tsk0 j0 t); try (by ins);
+ [by rewrite mem_rcons in_cons; apply/orP; right | intro INV].
+ rewrite -cats1 count_cat /= in INV.
+ unfold is_interfering_task_fp in INV.
+ generalize SOME; apply R_list_rcons_task in SOME; subst tsk_i; intro SOME.
+ assert (HP: higher_eq_priority tsk_lst tsk0 = false).
+ {
+ apply order_sorted_rcons with (x := tsk0) in SORT; [|by ins | by ins].
+ apply negbTE; apply/negP; unfold not; intro BUG.
+ exploit UNIQ; [by apply/andP; split; [by apply SORT | by ins] | intro EQ].
+ by rewrite rcons_uniq -EQ IN0 in SET.
+ }
+ by rewrite HP 2!andFb 2!addn0 in INV.
+ }
+ by apply R_list_rcons_prefix in SOME.
+ }
+ {
+ move: LAST => /eqP LAST.
+ inversion LAST as [[EQ1 EQ2]].
+ rewrite -> EQ1 in *; rewrite -> EQ2 in *; clear EQ1 EQ2 LAST.
+ generalize SOME; apply R_list_rcons_task in SOME; subst tsk_i; intro SOME.
+ generalize SOME; apply R_list_rcons_prefix in SOME; intro SOME'.
+ generalize SOME'; apply R_list_rcons_response_time in SOME'; intro SOME''; rewrite SOME'.
+ have BOUND := bertogna_cirinei_response_time_bound_fp_with_jitter.
+ unfold is_response_time_bound_of_task, job_has_completed_by in BOUND.
+ apply BOUND with (task_cost := task_cost) (task_period := task_period) (task_deadline := task_deadline) (job_deadline := job_deadline) (job_task := job_task) (tsk := tsk_lst) (job_jitter := job_jitter)
+ (ts := rcons ts' tsk_lst) (hp_bounds := hp_bounds)
+ (higher_eq_priority := higher_eq_priority); clear BOUND; try (by ins).
+ apply R_list_unzip1 with (R := R_lst); try (by ins).
+ {
+ intros hp_tsk R0 HP j0 JOB0.
+ apply IH with (rt_bounds := hp_bounds) (tsk := hp_tsk); try (by ins).
+ by rewrite rcons_uniq in SET; move: SET => /andP [_ SET].
+ by red; ins; apply TASKPARAMS; rewrite mem_rcons in_cons; apply/orP; right.
+ by ins; apply RESTR; rewrite mem_rcons in_cons; apply/orP; right.
+ by apply sorted_rcons_prefix in SORT.
+ {
+ intros tsk0 j1 t IN0 JOB1 BACK0.
+ exploit (INVARIANT tsk0 j1 t); try (by ins);
+ [by rewrite mem_rcons in_cons; apply/orP; right | intro INV].
+ rewrite -cats1 count_cat /= addn0 in INV.
+ unfold is_interfering_task_fp in INV.
+ assert (NOINTERF: higher_eq_priority tsk_lst tsk0 = false).
+ {
+ apply order_sorted_rcons with (x := tsk0) in SORT; [|by ins | by ins].
+ apply negbTE; apply/negP; unfold not; intro BUG.
+ exploit UNIQ; [by apply/andP; split; [by apply BUG | by ins] | intro EQ].
+ by rewrite rcons_uniq EQ IN0 in SET.
+ }
+ by rewrite NOINTERF 2!andFb addn0 in INV.
+ }
+ }
+ by ins; apply R_list_ge_cost with (ts' := ts') (rt_bounds := hp_bounds).
+ by ins; apply R_list_le_deadline with (ts' := ts') (rt_bounds := hp_bounds).
+ {
+ ins; exploit (INVARIANT tsk_lst j0 t); try (by ins).
+ by rewrite mem_rcons in_cons; apply/orP; left.
+ }
+ {
+ rewrite per_task_rta_fold.
+ apply per_task_rta_converges with (ts' := ts'); try (by ins).
+ {
+ red; ins; apply TASKPARAMS.
+ by rewrite mem_rcons in_cons; apply/orP; right.
+ }
+ apply leq_trans with (n := per_task_rta tsk_lst hp_bounds (max_steps tsk_lst) + task_jitter tsk_lst);
+ first by apply leq_addr.
+ rewrite -SOME'.
+ apply R_list_le_deadline with (ts' := rcons ts' tsk_lst)
+ (rt_bounds := rcons hp_bounds (tsk_lst, R_lst)); try (by ins).
+ by rewrite mem_rcons in_cons; apply/orP; left; apply/eqP.
+ }
+ }
+ }
+ Qed.
+
+ End HelperLemma.
+
+ (* If the schedulability test suceeds, ...*)
+ Hypothesis H_test_succeeds: fp_schedulable ts.
+
+ (*..., then no task misses its deadline,... *)
+ Theorem taskset_with_jitter_schedulable_by_fp_rta :
+ forall tsk, tsk \in ts -> no_deadline_missed_by_task tsk.
+ Proof.
+ unfold no_deadline_missed_by_task, task_misses_no_deadline,
+ job_misses_no_deadline, completed, valid_fp_policy,
+ fp_schedulable, fp_is_reflexive, fp_is_transitive,
+ fp_is_total, valid_sporadic_job_with_jitter,
+ valid_sporadic_job in *.
+ rename H_valid_job_parameters into JOBPARAMS,
+ H_valid_task_parameters into TASKPARAMS,
+ H_restricted_deadlines into RESTR,
+ H_completed_jobs_dont_execute into COMP,
+ H_jobs_execute_after_jitter into MUSTARRIVE,
+ H_global_scheduling_invariant into INVARIANT,
+ H_sorted_ts into SORT,
+ H_unique_priorities into UNIQ,
+ H_all_jobs_from_taskset into ALLJOBS,
+ H_test_succeeds into TEST.
+ destruct H_valid_policy as [REFL [TRANS TOTAL]].
+
+ move => tsk INtsk j /eqP JOBtsk.
+ have RLIST := (R_list_has_response_time_bounds).
+ have NONEMPTY := (R_list_non_empty ts).
+ have DL := (R_list_le_deadline ts).
+
+ destruct (R_list ts) as [rt_bounds |]; last by ins.
+ exploit (NONEMPTY rt_bounds tsk); [by ins | intros [EX _]; specialize (EX INtsk); des].
+ exploit (RLIST rt_bounds tsk R); [by ins | by ins | by apply JOBtsk | intro COMPLETED].
+ exploit (DL rt_bounds tsk R); [by ins | by ins | clear DL; intro DL].
+
+ rewrite eqn_leq; apply/andP; split; first by apply service_interval_le_cost.
+ apply leq_trans with (n := service rate sched j (job_arrival j + R)); last first.
+ {
+ unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
+ apply service_monotonic; rewrite leq_add2l.
+ specialize (JOBPARAMS j); des; rewrite JOBPARAMS2.
+ by rewrite JOBtsk.
+ }
+ rewrite leq_eqVlt; apply/orP; left; rewrite eq_sym.
+ by apply COMPLETED.
+ Qed.
+
+ (* ..., and the schedulability test yields safe response-time
+ bounds for each task. *)
+ Theorem fp_schedulability_test_with_jitter_yields_response_time_bounds :
+ forall tsk,
+ tsk \in ts ->
+ exists R,
+ R <= task_deadline tsk /\
+ forall (j: JobIn arr_seq),
+ job_task j = tsk ->
+ completed job_cost rate sched j (job_arrival j + R).
+ Proof.
+ intros tsk IN.
+ unfold fp_schedulable in *.
+ have TASKS := R_list_non_empty ts.
+ have BOUNDS := (R_list_has_response_time_bounds).
+ have DL := (R_list_le_deadline ts).
+ destruct (R_list ts) as [rt_bounds |]; last by ins.
+ exploit (TASKS rt_bounds tsk); [by ins | clear TASKS; intro EX].
+ destruct EX as [EX _]; specialize (EX IN); des.
+ exists R; split.
+ by apply DL with (rt_bounds0 := rt_bounds).
+ by ins; apply (BOUNDS rt_bounds tsk).
+ Qed.
+
+ (* For completeness, since all jobs of the arrival sequence
+ are spawned by the task set, we conclude that no job misses
+ its deadline. *)
+ Theorem jobs_with_jitter_schedulable_by_fp_rta :
+ forall (j: JobIn arr_seq), no_deadline_missed_by_job j.
+ Proof.
+ intros j.
+ have SCHED := taskset_with_jitter_schedulable_by_fp_rta.
+ unfold no_deadline_missed_by_task, task_misses_no_deadline in *.
+ apply SCHED with (tsk := job_task j); last by rewrite eq_refl.
+ by apply H_all_jobs_from_taskset.
+ Qed.
+
+ End Proof.
+
+ End Analysis.
+
+End ResponseTimeIterationFPWithJitter.
\ No newline at end of file
diff --git a/Vbase.v b/Vbase.v
index 9960c309c..0508e86f2 100644
--- a/Vbase.v
+++ b/Vbase.v
@@ -489,8 +489,8 @@ Ltac autos := clarsimp; auto with vlib.
Definition NW A (P: unit -> A) : A := P tt.
-Notation "<< x : t >>" := (NW (fun x => t)) (at level 80, x ident, no associativity).
-Notation "<< t >>" := (NW (fun _ => t)) (at level 79, no associativity).
+(*Notation "<< x : t >>" := (NW (fun x => t)) (at level 80, x ident, no associativity).
+Notation "<< t >>" := (NW (fun _ => t)) (at level 79, no associativity).*)
Ltac unnw := unfold NW in *.
Ltac rednw := red; unnw.
diff --git a/helper.v b/helper.v
index dce2f0ade..c5028e3f3 100644
--- a/helper.v
+++ b/helper.v
@@ -41,20 +41,25 @@ Notation "\sum_ ( ( m , n ) <- r | P ) F" :=
(\sum_(i <- r | (let '(m,n) := i in P))
(let '(m,n) := i in F)) : nat_scope.
-(*Reserved Notation "\big [ op / idx ]_ ( ( m , n ) <- r | P ) F"
- (at level 36, F at level 36, op, idx at level 10, i, r at level 50,
- format "'[' \big [ op / idx ]_ ( ( m , n ) <- r | P ) '/ ' F ']'").
+Reserved Notation "\max_ ( ( m , n ) <- r ) F"
+ (at level 41, F at level 41, m, n at level 50,
+ format "'[' \max_ ( ( m , n ) <- r ) '/ ' F ']'").
+
+Notation "\max_ ( ( m , n ) <- r ) F" :=
+ (\max_(i <- r) (let '(m,n) := i in F)) : nat_scope.
-Notation "\big [ op / idx ]_ ( ( m , n ) <- r | P ) F" :=
- (bigop idx op r
- (fun i => let '(m,n) := i in P%B)
- (fun i => let '(m,n) := i in F)) : big_scope.*)
+Reserved Notation "\max_ ( ( m , n ) <- r | P ) F"
+ (at level 41, F at level 30, P at level 41, m, n at level 50,
+ format "'[' \max_ ( ( m , n ) <- r | P ) '/ ' F ']'").
-(*Variable natlist: seq nat.
-Check (\sum_(x1 <- natlist) x1).
+Notation "\max_ ( ( m , n ) <- r | P ) F" :=
+ (\max_(i <- r | (let '(m,n) := i in P))
+ (let '(m,n) := i in F)) : nat_scope.
-Variable tuplelist: seq (nat * nat).
-Check (\sum_( (x1,x2) <- tuplelist | x1 + x2 > 1) (x1 + x2)).*)
+Notation "[ 'seq' ( x , y ) <- s | C ]" :=
+ (filter (fun i => let '(x,y) := i in C%B) s)
+ (at level 0, x at level 99,
+ format "[ '[hv' 'seq' ( x , y ) <- s '/ ' | C ] ']'") : seq_scope.
Reserved Notation "\cat_ ( i < n ) F"
(at level 41, F at level 41, i, n at level 50,
@@ -588,6 +593,14 @@ Proof.
}
Qed.
+(* Based on https://www.ps.uni-saarland.de/formalizations/fset/html/libs.fset.html *)
+Definition powerset {T: eqType} (l: seq T) : seq (seq T) :=
+ let mT := ((size l).-tuple bool) in
+ (map (fun m : mT => (mask m l)) (enum {: mT})).
+
+Definition no_intersection {T: eqType} (l1 l2: seq T) :=
+ ~~ has (mem l1) l2.
+
(*Program Definition fun_ord_to_nat2 {n} {T} (x0: T) (f: 'I_n -> T)
(x : nat) : T :=
match (x < n) with
--
GitLab