Commit b71f34f7 authored by Felipe Cerqueira's avatar Felipe Cerqueira

Add RTA for parallel jobs

We use simpler, more pessimistic interference bounds to
prove that Bertogna and Cirinei's RTA works for parallel jobs.
parent b40399b2
......@@ -14,7 +14,7 @@
#
# This Makefile was generated by the command line :
# coq_makefile -R . rt ./util/ssromega.v ./util/lemmas.v ./util/Vbase.v ./util/divround.v ./implementation/basic/bertogna_edf_example.v ./implementation/basic/task.v ./implementation/basic/schedule.v ./implementation/basic/job.v ./implementation/basic/arrival_sequence.v ./implementation/jitter/bertogna_edf_example.v ./implementation/jitter/task.v ./implementation/jitter/schedule.v ./implementation/jitter/job.v ./implementation/jitter/arrival_sequence.v ./analysis/basic/bertogna_fp_theory.v ./analysis/basic/interference_bound_edf.v ./analysis/basic/interference_bound_fp.v ./analysis/basic/interference_bound.v ./analysis/basic/bertogna_edf_comp.v ./analysis/basic/bertogna_fp_comp.v ./analysis/basic/bertogna_edf_theory.v ./analysis/basic/workload_bound.v ./analysis/jitter/bertogna_fp_theory.v ./analysis/jitter/interference_bound_edf.v ./analysis/jitter/interference_bound_fp.v ./analysis/jitter/interference_bound.v ./analysis/jitter/bertogna_edf_comp.v ./analysis/jitter/bertogna_fp_comp.v ./analysis/jitter/bertogna_edf_theory.v ./analysis/jitter/workload_bound.v ./model/basic/schedulability.v ./model/basic/task.v ./model/basic/task_arrival.v ./model/basic/platform.v ./model/basic/schedule.v ./model/basic/priority.v ./model/basic/interference_edf.v ./model/basic/interference.v ./model/basic/workload.v ./model/basic/job.v ./model/basic/arrival_sequence.v ./model/basic/response_time.v ./model/basic/platform_fp.v ./model/jitter/schedulability.v ./model/jitter/task.v ./model/jitter/task_arrival.v ./model/jitter/platform.v ./model/jitter/schedule.v ./model/jitter/priority.v ./model/jitter/interference_edf.v ./model/jitter/interference.v ./model/jitter/workload.v ./model/jitter/job.v ./model/jitter/arrival_sequence.v ./model/jitter/response_time.v ./model/jitter/platform_fp.v -o Makefile
# coq_makefile -R . rt ./util/ssromega.v ./util/lemmas.v ./util/Vbase.v ./util/divround.v ./implementation/basic/bertogna_edf_example.v ./implementation/basic/task.v ./implementation/basic/schedule.v ./implementation/basic/job.v ./implementation/basic/arrival_sequence.v ./implementation/jitter/bertogna_edf_example.v ./implementation/jitter/task.v ./implementation/jitter/schedule.v ./implementation/jitter/job.v ./implementation/jitter/arrival_sequence.v ./analysis/basic/bertogna_fp_theory.v ./analysis/basic/interference_bound_edf.v ./analysis/basic/interference_bound_fp.v ./analysis/basic/interference_bound.v ./analysis/basic/bertogna_edf_comp.v ./analysis/basic/bertogna_fp_comp.v ./analysis/basic/bertogna_edf_theory.v ./analysis/basic/workload_bound.v ./analysis/parallel/bertogna_fp_theory.v ./analysis/parallel/interference_bound_edf.v ./analysis/parallel/interference_bound_fp.v ./analysis/parallel/interference_bound.v ./analysis/parallel/bertogna_edf_comp.v ./analysis/parallel/bertogna_fp_comp.v ./analysis/parallel/bertogna_edf_theory.v ./analysis/parallel/workload_bound.v ./analysis/jitter/bertogna_fp_theory.v ./analysis/jitter/interference_bound_edf.v ./analysis/jitter/interference_bound_fp.v ./analysis/jitter/interference_bound.v ./analysis/jitter/bertogna_edf_comp.v ./analysis/jitter/bertogna_fp_comp.v ./analysis/jitter/bertogna_edf_theory.v ./analysis/jitter/workload_bound.v ./model/basic/schedulability.v ./model/basic/task.v ./model/basic/task_arrival.v ./model/basic/platform.v ./model/basic/schedule.v ./model/basic/priority.v ./model/basic/interference_edf.v ./model/basic/interference.v ./model/basic/workload.v ./model/basic/job.v ./model/basic/arrival_sequence.v ./model/basic/response_time.v ./model/basic/platform_fp.v ./model/jitter/schedulability.v ./model/jitter/task.v ./model/jitter/task_arrival.v ./model/jitter/platform.v ./model/jitter/schedule.v ./model/jitter/priority.v ./model/jitter/interference_edf.v ./model/jitter/interference.v ./model/jitter/workload.v ./model/jitter/job.v ./model/jitter/arrival_sequence.v ./model/jitter/response_time.v ./model/jitter/platform_fp.v -o Makefile
#
.DEFAULT_GOAL := all
......@@ -102,6 +102,14 @@ VFILES:=util/ssromega.v\
analysis/basic/bertogna_fp_comp.v\
analysis/basic/bertogna_edf_theory.v\
analysis/basic/workload_bound.v\
analysis/parallel/bertogna_fp_theory.v\
analysis/parallel/interference_bound_edf.v\
analysis/parallel/interference_bound_fp.v\
analysis/parallel/interference_bound.v\
analysis/parallel/bertogna_edf_comp.v\
analysis/parallel/bertogna_fp_comp.v\
analysis/parallel/bertogna_edf_theory.v\
analysis/parallel/workload_bound.v\
analysis/jitter/bertogna_fp_theory.v\
analysis/jitter/interference_bound_edf.v\
analysis/jitter/interference_bound_fp.v\
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
Add LoadPath "../../" as rt.
Require Import rt.util.Vbase rt.util.lemmas.
Require Import rt.model.basic.schedule.
Require Import rt.analysis.parallel.workload_bound.
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module InterferenceBoundGeneric.
Section Definitions.
Import Schedule WorkloadBound.
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_generic :=
W task_cost task_period tsk_other R_other delta.
End PerTask.
End Definitions.
End InterferenceBoundGeneric.
\ No newline at end of file
This diff is collapsed.
Add LoadPath "../.." as rt.
Require Import rt.util.Vbase rt.util.lemmas.
Require Import rt.model.basic.schedule rt.model.basic.priority rt.model.basic.workload
rt.model.basic.interference.
Require Import rt.analysis.parallel.workload_bound rt.analysis.parallel.interference_bound.
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module InterferenceBoundFP.
Import Schedule WorkloadBound Priority Interference.
Export InterferenceBoundGeneric.
Section Definitions.
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.
(* Assume an FP policy. *)
Variable higher_eq_priority: FP_policy sporadic_task.
Let can_interfere_with_tsk := fp_can_interfere_with higher_eq_priority tsk.
Let total_interference_bound := interference_bound_generic task_cost task_period delta.
(* The total interference incurred by tsk is bounded by the sum
of individual task interferences. *)
Definition total_interference_bound_fp :=
\sum_((tsk_other, R_other) <- R_prev | can_interfere_with_tsk tsk_other)
total_interference_bound (tsk_other, R_other).
End Definitions.
End InterferenceBoundFP.
\ No newline at end of file
This diff is collapsed.
......@@ -79,7 +79,20 @@ Module Interference.
(job_is_backlogged t && scheduled sched job_other t).
End JobInterference.
Section JobInterferenceParallelism.
(* Let job_other be a job that interferes with j. *)
Variable job_other: JobIn arr_seq.
(* The interference caused by job_other is defined as follows. *)
Definition job_interference_with_parallelism (t1 t2: time) :=
\sum_(t1 <= t < t2)
\sum_(cpu < num_cpus)
(job_is_backlogged t && scheduled_on sched job_other cpu t).
End JobInterferenceParallelism.
Section TaskInterference.
(* In order to define task interference, consider any interfering task tsk_other. *)
......@@ -104,6 +117,19 @@ Module Interference.
End TaskInterference.
Section TaskInterferenceParallelism.
Variable tsk_other: sporadic_task.
(* We define the total interference incurred by tsk during [t1, t2)
as the cumulative time in which tsk is scheduled. *)
Definition task_interference_with_parallelism (t1 t2: time) :=
\sum_(t1 <= t < t2)
\sum_(cpu < num_cpus)
(job_is_backlogged t && schedules_job_of_tsk tsk_other cpu t).
End TaskInterferenceParallelism.
Section TaskInterferenceJobList.
Variable tsk_other: sporadic_task.
......@@ -150,6 +176,18 @@ Module Interference.
unfold service_at; rewrite (bigD1 cpu); last by done.
by apply leq_trans with (n := 1).
Qed.
Lemma job_interference_with_parallelism_le_service :
forall j_other t1 t2,
job_interference_with_parallelism j_other t1 t2 <= service_during sched j_other t1 t2.
Proof.
intros j_other t1 t2; unfold job_interference_with_parallelism, service_during.
apply leq_sum; intros t _.
unfold service_at; rewrite [\sum_(_ < _ | scheduled_on _ _ _ _)_]big_mkcond.
apply leq_sum; intros cpu _.
destruct (job_is_backlogged t); [rewrite andTb | by rewrite andFb].
by destruct (scheduled_on sched j_other cpu t).
Qed.
Lemma task_interference_le_workload :
forall tsk t1 t2,
......@@ -168,6 +206,18 @@ Module Interference.
by destruct (sched cpu t); [rewrite HAScpu | by done].
Qed.
Lemma task_interference_with_parallelism_le_workload :
forall tsk t1 t2,
task_interference_with_parallelism tsk t1 t2 <= workload job_task sched tsk t1 t2.
Proof.
unfold task_interference_with_parallelism, workload; intros tsk t1 t2.
apply leq_sum; intros t _.
apply leq_sum; intros cpu _.
destruct (job_is_backlogged t); [rewrite andTb | by rewrite andFb].
unfold schedules_job_of_tsk, service_of_task.
by destruct (sched cpu t).
Qed.
End BasicLemmas.
(* If we assume no intra-task parallelism, the two definitions
......
......@@ -55,6 +55,44 @@ Module InterferenceEDF.
}
Qed.
(* Under EDF scheduling, a job only causes interference if its deadline
is not larger than the deadline of the analyzed job. *)
Lemma interference_with_parallelism_under_edf_implies_shorter_deadlines :
forall (j j': JobIn arr_seq) t1 t2,
job_interference_with_parallelism job_cost sched j' j t1 t2 != 0 ->
job_arrival j + job_deadline j <= job_arrival j' + job_deadline j'.
Proof.
rename H_scheduler_uses_EDF into PRIO.
intros j j' t1 t2 INTERF.
unfold job_interference_with_parallelism in INTERF.
destruct ([exists t': 'I_t2,
[exists cpu: processor num_cpus,
(t' >= t1) && backlogged job_cost sched j' t' &&
scheduled sched j t']]) eqn:EX.
{
move: EX => /existsP [t' /existsP [cpu /andP [/andP [LE BACK] SCHED]]].
by eapply PRIO in SCHED; last by apply BACK.
}
{
apply negbT in EX; rewrite negb_exists in EX; move: EX => /forallP ALL.
rewrite big_nat_cond (eq_bigr (fun x => 0)) in INTERF;
first by rewrite -big_nat_cond big_const_nat iter_addn mul0n addn0 eq_refl in INTERF.
move => i /andP [/andP [GEi LTi] _].
specialize (ALL (Ordinal LTi)).
rewrite negb_exists in ALL.
move: ALL => /forallP ALL.
rewrite (eq_bigr (fun x => 0));
first by rewrite big_const_ord iter_addn mul0n addn0.
intros cpu _; specialize (ALL cpu); simpl in ALL.
destruct (backlogged job_cost sched j' i); last by rewrite andFb.
rewrite GEi 2!andTb in ALL; rewrite andTb.
rewrite negb_exists in ALL; move: ALL => /forallP NOTSCHED.
specialize (NOTSCHED cpu); rewrite negb_and in NOTSCHED.
move: NOTSCHED => /orP [BUG | NOTSCHED]; first by done.
by apply/eqP; rewrite eqb0.
}
Qed.
End Lemmas.
End InterferenceEDF.
\ No newline at end of file
Add LoadPath ".." as rt.
Require Import rt.util.Vbase.
Require Import ssrbool ssrnat div.
Definition div_floor (x y: nat) : nat := x %/ y.
......
Add LoadPath ".." as rt.
Require Import rt.util.Vbase rt.util.ssromega.
Require Import rt.util.Vbase rt.util.divround rt.util.ssromega.
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop tuple path div.
(* Here we define a more verbose notation for projections of pairs... *)
......@@ -563,6 +563,36 @@ Section Arithmetic.
}
Qed.
Lemma ceil_neq0 :
forall x y,
x > 0 ->
y > 0 ->
div_ceil x y > 0.
Proof.
unfold div_ceil; intros x y GEx GEy.
destruct (y %| x) eqn:DIV; last by done.
by rewrite divn_gt0; first by apply dvdn_leq.
Qed.
Lemma leq_divceil2r :
forall d m n,
d > 0 ->
m <= n ->
div_ceil m d <= div_ceil n d.
Proof.
unfold div_ceil; intros d m n GT0 LE.
destruct (d %| m) eqn:DIVm, (d %| n) eqn:DIVn;
[by apply leq_div2r | | | by apply leq_div2r].
by apply leq_trans with (n := n %/ d); first by apply leq_div2r.
{
rewrite leq_eqVlt in LE; move: LE => /orP [/eqP EQ | LT];
first by subst; rewrite DIVn in DIVm.
rewrite ltn_divLR //.
apply leq_trans with (n := n); first by done.
by apply eq_leq; symmetry; apply/eqP; rewrite -dvdn_eq.
}
Qed.
Lemma min_lt_same :
forall x y z,
minn x z < minn y z -> x < y.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment