diff --git a/Makefile b/Makefile
index 01a416522d6f4ce43dbd5929fe141a88ffecfd59..0a093288b4363e726d0d90ca6ed3c43364a0233d 100644
--- a/Makefile
+++ b/Makefile
@@ -14,7 +14,7 @@
#
# This Makefile was generated by the command line :
-# coq_makefile -f _CoqProject ./util/ssromega.v ./util/seqset.v ./util/sorting.v ./util/step_function.v ./util/minmax.v ./util/powerset.v ./util/all.v ./util/ord_quantifier.v ./util/nat.v ./util/sum.v ./util/bigord.v ./util/counting.v ./util/tactics.v ./util/induction.v ./util/list.v ./util/divround.v ./util/bigcat.v ./util/fixedpoint.v ./util/notation.v ./analysis/global/jitter/bertogna_fp_comp.v ./analysis/global/jitter/interference_bound_edf.v ./analysis/global/jitter/workload_bound.v ./analysis/global/jitter/bertogna_edf_comp.v ./analysis/global/jitter/bertogna_fp_theory.v ./analysis/global/jitter/interference_bound.v ./analysis/global/jitter/interference_bound_fp.v ./analysis/global/jitter/bertogna_edf_theory.v ./analysis/global/parallel/bertogna_fp_comp.v ./analysis/global/parallel/interference_bound_edf.v ./analysis/global/parallel/workload_bound.v ./analysis/global/parallel/bertogna_edf_comp.v ./analysis/global/parallel/bertogna_fp_theory.v ./analysis/global/parallel/interference_bound.v ./analysis/global/parallel/interference_bound_fp.v ./analysis/global/parallel/bertogna_edf_theory.v ./analysis/global/basic/bertogna_fp_comp.v ./analysis/global/basic/interference_bound_edf.v ./analysis/global/basic/workload_bound.v ./analysis/global/basic/bertogna_edf_comp.v ./analysis/global/basic/bertogna_fp_theory.v ./analysis/global/basic/interference_bound.v ./analysis/global/basic/interference_bound_fp.v ./analysis/global/basic/bertogna_edf_theory.v ./analysis/apa/bertogna_fp_comp.v ./analysis/apa/interference_bound_edf.v ./analysis/apa/workload_bound.v ./analysis/apa/bertogna_edf_comp.v ./analysis/apa/bertogna_fp_theory.v ./analysis/apa/interference_bound.v ./analysis/apa/interference_bound_fp.v ./analysis/apa/bertogna_edf_theory.v ./analysis/uni/susp/dynamic/oblivious/fp_rta.v ./analysis/uni/susp/dynamic/oblivious/reduction.v ./analysis/uni/jitter/workload_bound_fp.v ./analysis/uni/jitter/fp_rta_comp.v ./analysis/uni/jitter/fp_rta_theory.v ./analysis/uni/basic/workload_bound_fp.v ./analysis/uni/basic/fp_rta_comp.v ./analysis/uni/basic/fp_rta_theory.v ./model/suspension.v ./model/schedule/partitioned/schedulability.v ./model/schedule/partitioned/schedule.v ./model/schedule/global/workload.v ./model/schedule/global/schedulability.v ./model/schedule/global/jitter/interference_edf.v ./model/schedule/global/jitter/interference.v ./model/schedule/global/jitter/job.v ./model/schedule/global/jitter/constrained_deadlines.v ./model/schedule/global/jitter/schedule.v ./model/schedule/global/jitter/platform.v ./model/schedule/global/response_time.v ./model/schedule/global/basic/interference_edf.v ./model/schedule/global/basic/interference.v ./model/schedule/global/basic/constrained_deadlines.v ./model/schedule/global/basic/schedule.v ./model/schedule/global/basic/platform.v ./model/schedule/apa/interference_edf.v ./model/schedule/apa/interference.v ./model/schedule/apa/affinity.v ./model/schedule/apa/constrained_deadlines.v ./model/schedule/apa/platform.v ./model/schedule/uni/workload.v ./model/schedule/uni/transformation/construction.v ./model/schedule/uni/susp/suspension_intervals.v ./model/schedule/uni/susp/last_execution.v ./model/schedule/uni/susp/schedule.v ./model/schedule/uni/susp/platform.v ./model/schedule/uni/schedulability.v ./model/schedule/uni/jitter/workload.v ./model/schedule/uni/jitter/busy_interval.v ./model/schedule/uni/jitter/schedule.v ./model/schedule/uni/jitter/platform.v ./model/schedule/uni/jitter/service.v ./model/schedule/uni/schedule_of_task.v ./model/schedule/uni/response_time.v ./model/schedule/uni/schedule.v ./model/schedule/uni/basic/arrival_bounds.v ./model/schedule/uni/basic/busy_interval.v ./model/schedule/uni/basic/platform.v ./model/schedule/uni/service.v ./model/arrival/jitter/arrival_sequence.v ./model/arrival/jitter/task_arrival.v ./model/arrival/jitter/job.v ./model/arrival/jitter/arrival_bounds.v ./model/arrival/basic/arrival_sequence.v ./model/arrival/basic/task.v ./model/arrival/basic/task_arrival.v ./model/arrival/basic/job.v ./model/arrival/basic/arrival_bounds.v ./model/priority.v ./model/time.v ./implementation/arrival_sequence.v ./implementation/task.v ./implementation/global/jitter/arrival_sequence.v ./implementation/global/jitter/task.v ./implementation/global/jitter/bertogna_edf_example.v ./implementation/global/jitter/job.v ./implementation/global/jitter/bertogna_fp_example.v ./implementation/global/jitter/schedule.v ./implementation/global/parallel/bertogna_edf_example.v ./implementation/global/parallel/bertogna_fp_example.v ./implementation/global/basic/bertogna_edf_example.v ./implementation/global/basic/bertogna_fp_example.v ./implementation/global/basic/schedule.v ./implementation/job.v ./implementation/apa/arrival_sequence.v ./implementation/apa/task.v ./implementation/apa/bertogna_edf_example.v ./implementation/apa/job.v ./implementation/apa/bertogna_fp_example.v ./implementation/apa/schedule.v ./implementation/uni/susp/dynamic/arrival_sequence.v ./implementation/uni/susp/dynamic/task.v ./implementation/uni/susp/dynamic/job.v ./implementation/uni/susp/dynamic/oblivious/fp_rta_example.v ./implementation/uni/susp/schedule.v ./implementation/uni/jitter/arrival_sequence.v ./implementation/uni/jitter/task.v ./implementation/uni/jitter/job.v ./implementation/uni/jitter/fp_rta_example.v ./implementation/uni/jitter/schedule.v ./implementation/uni/basic/fp_rta_example.v ./implementation/uni/basic/schedule.v -o Makefile
+# coq_makefile -f _CoqProject ./util/ssromega.v ./util/seqset.v ./util/sorting.v ./util/step_function.v ./util/minmax.v ./util/powerset.v ./util/all.v ./util/ord_quantifier.v ./util/nat.v ./util/sum.v ./util/bigord.v ./util/counting.v ./util/tactics.v ./util/induction.v ./util/list.v ./util/divround.v ./util/bigcat.v ./util/fixedpoint.v ./util/notation.v ./analysis/global/jitter/bertogna_fp_comp.v ./analysis/global/jitter/interference_bound_edf.v ./analysis/global/jitter/workload_bound.v ./analysis/global/jitter/bertogna_edf_comp.v ./analysis/global/jitter/bertogna_fp_theory.v ./analysis/global/jitter/interference_bound.v ./analysis/global/jitter/interference_bound_fp.v ./analysis/global/jitter/bertogna_edf_theory.v ./analysis/global/parallel/bertogna_fp_comp.v ./analysis/global/parallel/interference_bound_edf.v ./analysis/global/parallel/workload_bound.v ./analysis/global/parallel/bertogna_edf_comp.v ./analysis/global/parallel/bertogna_fp_theory.v ./analysis/global/parallel/interference_bound.v ./analysis/global/parallel/interference_bound_fp.v ./analysis/global/parallel/bertogna_edf_theory.v ./analysis/global/basic/bertogna_fp_comp.v ./analysis/global/basic/interference_bound_edf.v ./analysis/global/basic/workload_bound.v ./analysis/global/basic/bertogna_edf_comp.v ./analysis/global/basic/bertogna_fp_theory.v ./analysis/global/basic/interference_bound.v ./analysis/global/basic/interference_bound_fp.v ./analysis/global/basic/bertogna_edf_theory.v ./analysis/apa/bertogna_fp_comp.v ./analysis/apa/interference_bound_edf.v ./analysis/apa/workload_bound.v ./analysis/apa/bertogna_edf_comp.v ./analysis/apa/bertogna_fp_theory.v ./analysis/apa/interference_bound.v ./analysis/apa/interference_bound_fp.v ./analysis/apa/bertogna_edf_theory.v ./analysis/uni/susp/dynamic/oblivious/fp_rta.v ./analysis/uni/susp/dynamic/oblivious/reduction.v ./analysis/uni/jitter/workload_bound_fp.v ./analysis/uni/jitter/fp_rta_comp.v ./analysis/uni/jitter/fp_rta_theory.v ./analysis/uni/basic/workload_bound_fp.v ./analysis/uni/basic/fp_rta_comp.v ./analysis/uni/basic/fp_rta_theory.v ./model/suspension.v ./model/schedule/partitioned/schedulability.v ./model/schedule/partitioned/schedule.v ./model/schedule/global/workload.v ./model/schedule/global/schedulability.v ./model/schedule/global/jitter/interference_edf.v ./model/schedule/global/jitter/interference.v ./model/schedule/global/jitter/job.v ./model/schedule/global/jitter/constrained_deadlines.v ./model/schedule/global/jitter/schedule.v ./model/schedule/global/jitter/platform.v ./model/schedule/global/response_time.v ./model/schedule/global/basic/interference_edf.v ./model/schedule/global/basic/interference.v ./model/schedule/global/basic/constrained_deadlines.v ./model/schedule/global/basic/schedule.v ./model/schedule/global/basic/platform.v ./model/schedule/apa/interference_edf.v ./model/schedule/apa/interference.v ./model/schedule/apa/affinity.v ./model/schedule/apa/constrained_deadlines.v ./model/schedule/apa/platform.v ./model/schedule/uni/workload.v ./model/schedule/uni/transformation/construction.v ./model/schedule/uni/susp/suspension_intervals.v ./model/schedule/uni/susp/last_execution.v ./model/schedule/uni/susp/schedule.v ./model/schedule/uni/susp/platform.v ./model/schedule/uni/schedulability.v ./model/schedule/uni/jitter/workload.v ./model/schedule/uni/jitter/busy_interval.v ./model/schedule/uni/jitter/schedule.v ./model/schedule/uni/jitter/platform.v ./model/schedule/uni/jitter/service.v ./model/schedule/uni/schedule_of_task.v ./model/schedule/uni/response_time.v ./model/schedule/uni/schedule.v ./model/schedule/uni/basic/busy_interval.v ./model/schedule/uni/basic/platform.v ./model/schedule/uni/service.v ./model/arrival/jitter/arrival_sequence.v ./model/arrival/jitter/task_arrival.v ./model/arrival/jitter/job.v ./model/arrival/jitter/arrival_bounds.v ./model/arrival/basic/arrival_sequence.v ./model/arrival/basic/task.v ./model/arrival/basic/task_arrival.v ./model/arrival/basic/job.v ./model/arrival/basic/arrival_bounds.v ./model/priority.v ./model/time.v ./implementation/arrival_sequence.v ./implementation/task.v ./implementation/global/jitter/arrival_sequence.v ./implementation/global/jitter/task.v ./implementation/global/jitter/bertogna_edf_example.v ./implementation/global/jitter/job.v ./implementation/global/jitter/bertogna_fp_example.v ./implementation/global/jitter/schedule.v ./implementation/global/parallel/bertogna_edf_example.v ./implementation/global/parallel/bertogna_fp_example.v ./implementation/global/basic/bertogna_edf_example.v ./implementation/global/basic/bertogna_fp_example.v ./implementation/global/basic/schedule.v ./implementation/job.v ./implementation/apa/arrival_sequence.v ./implementation/apa/task.v ./implementation/apa/bertogna_edf_example.v ./implementation/apa/job.v ./implementation/apa/bertogna_fp_example.v ./implementation/apa/schedule.v ./implementation/uni/susp/dynamic/arrival_sequence.v ./implementation/uni/susp/dynamic/task.v ./implementation/uni/susp/dynamic/job.v ./implementation/uni/susp/dynamic/oblivious/fp_rta_example.v ./implementation/uni/susp/schedule.v ./implementation/uni/jitter/arrival_sequence.v ./implementation/uni/jitter/task.v ./implementation/uni/jitter/job.v ./implementation/uni/jitter/fp_rta_example.v ./implementation/uni/jitter/schedule.v ./implementation/uni/basic/fp_rta_example.v ./implementation/uni/basic/schedule.v -o Makefile
#
.DEFAULT_GOAL := all
@@ -190,7 +190,6 @@ VFILES:=util/ssromega.v\
model/schedule/uni/schedule_of_task.v\
model/schedule/uni/response_time.v\
model/schedule/uni/schedule.v\
- model/schedule/uni/basic/arrival_bounds.v\
model/schedule/uni/basic/busy_interval.v\
model/schedule/uni/basic/platform.v\
model/schedule/uni/service.v\
diff --git a/model/schedule/uni/basic/arrival_bounds.v b/model/schedule/uni/basic/arrival_bounds.v
deleted file mode 100644
index fc1517b576647f4d46a2784dfe9e5fd4d9c86802..0000000000000000000000000000000000000000
--- a/model/schedule/uni/basic/arrival_bounds.v
+++ /dev/null
@@ -1,217 +0,0 @@
-Require Import rt.util.all.
-Require Import rt.model.arrival.basic.arrival_sequence rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.task_arrival.
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path div.
-
-(* Properties of job arrival. *)
-Module ArrivalBounds.
-
- Import ArrivalSequence SporadicTaskset TaskArrival.
-
- Section Lemmas.
-
- Context {Task: eqType}.
- Variable task_period: Task -> time.
-
- Context {Job: eqType}.
- Variable job_cost: Job -> time.
- Variable job_task: Job -> Task.
-
- (* Consider any job arrival sequence that does not contain duplicate jobs. *)
- Variable arr_seq: arrival_sequence Job.
- Hypothesis H_arrival_sequence_is_a_set: arrival_sequence_is_a_set arr_seq.
-
- (* In this section, we prove an upper bound on the number of jobs that can arrive
- in any interval. *)
- Section BasicArrivalBound.
-
- (* Assume that jobs are sporadic. *)
- Hypothesis H_sporadic_tasks: sporadic_task_model task_period arr_seq job_task.
-
- (* Consider any time interval [t1, t2)... *)
- Variable t1 t2: time.
-
- (* ...and let tsk be any task with period > 0. *)
- Variable tsk: Task.
- Hypothesis H_period_gt_zero: task_period tsk > 0.
-
- (* Recall the jobs of tsk during [t1, t2), along with the number of arrivals. *)
- Let arriving_jobs := arrivals_of_task_between job_task arr_seq tsk t1 t2.
- Let num_arrivals := num_arrivals_of_task job_task arr_seq tsk t1 t2.
-
- (* We will establish an upper bound on the number of arriving jobs of tsk.
- Since the proof requires analyzing the distance between the first and last
- jobs, we begin with a case analysis to eliminate the special cases
- of 0 or 1 arriving job. *)
-
- (* Case 1: Assume that no jobs of tsk arrive in the interval. *)
- Section NoJobs.
-
- (* If there are no arriving jobs in [t1, t2), ...*)
- Hypothesis H_no_jobs: num_arrivals = 0.
-
- (* ...then the arrival bound trivially holds. *)
- Lemma sporadic_arrival_bound_no_jobs:
- num_arrivals <= div_ceil (t2 - t1) (task_period tsk).
- Proof.
- by rewrite H_no_jobs.
- Qed.
-
- End NoJobs.
-
- (* Case 2: Assume that a single job of tsk arrives in the interval. *)
- Section OneJob.
-
- (* First, note that because the interval is open at time t2,
- t2 must be larger than t1. *)
- Lemma sporadic_arrival_bound_more_than_one_point:
- num_arrivals > 0 ->
- t1 < t2.
- Proof.
- unfold num_arrivals, num_arrivals_of_task in *; intros ONE.
- rewrite -/arriving_jobs in ONE *.
- destruct arriving_jobs as [| j l] eqn:EQ; first by done.
- have IN: j \in arriving_jobs by rewrite EQ in_cons eq_refl orTb.
- rewrite mem_filter in IN; move: IN => /andP [_ ARR].
- rewrite mem_filter in ARR; move: ARR => /andP [GE ARR].
- apply JobIn_arrived in ARR.
- by apply leq_ltn_trans with (n := job_arrival j).
- Qed.
-
- (* Since the interval length is positive, if there is one job of tsk
- arriving during [t1, t2), ... *)
- Hypothesis H_no_jobs: num_arrivals = 1.
-
- (* ...then the arrival bound also holds. *)
- Lemma sporadic_arrival_bound_one_job:
- num_arrivals <= div_ceil (t2 - t1) (task_period tsk).
- Proof.
- rewrite H_no_jobs.
- rewrite ceil_neq0 // ltn_subRL addn0.
- apply sporadic_arrival_bound_more_than_one_point.
- by rewrite H_no_jobs.
- Qed.
-
- End OneJob.
-
- (* Case 3: There are at least two arriving jobs. *)
- Section AtLeastTwoJobs.
-
- (* Assume that there is at least one job of tsk arriving in [t1,t2). *)
- Hypothesis H_at_least_two_jobs: num_arrivals >= 2.
-
- (* We prove the arrival bound by contradiction. *)
- Section DerivingContradiction.
-
- (* Suppose that the number of arrivals is larger than the bound. *)
- Hypothesis H_many_arrivals: num_arrivals > div_ceil (t2 - t1) (task_period tsk).
-
- (* Consider the list of jobs ordered by arrival times. *)
- Let by_arrival_time (j j': JobIn arr_seq) := job_arrival j <= job_arrival j'.
- Let sorted_jobs := sort by_arrival_time arriving_jobs.
-
- (* Based on the notation for the n-th job in the sorted list of arrivals, ... *)
- Variable elem: JobIn arr_seq.
- Let nth_task := nth elem sorted_jobs.
-
- (* ...we identify the first and last jobs and their respective arrival times. *)
- Let j_first := nth_task 0.
- Let j_last := nth_task (num_arrivals.-1).
- Let a_first := job_arrival j_first.
- Let a_last := job_arrival j_last.
-
- (* Recall from model/task_arrival.v that the first and last
- jobs are separated by at least (num_arrivals - 1) periods. *)
- Remark sporadic_arrival_bound_distance_between_first_and_last:
- a_last >= a_first + (num_arrivals.-1) * task_period tsk.
- Proof.
- apply sorted_arrivals_distance_from_first_job; [by done | by done |].
- by rewrite -/num_arrivals; destruct num_arrivals.
- Qed.
-
- (* Due to the initial assumption that the number of arrivals is larger
- than the bound, it follows that the first and last jobs are separated
- by at least the length of the interval. *)
- Lemma sporadic_arrival_bound_entire_interval_in_between:
- a_first + t2 - t1 <= a_last.
- Proof.
- have DIST := sporadic_arrival_bound_distance_between_first_and_last.
- have MORE := sporadic_arrival_bound_more_than_one_point.
- rename H_many_arrivals into MANY, H_at_least_two_jobs into TWO.
- destruct num_arrivals; first by rewrite ltn0 in TWO.
- destruct n; first by rewrite ltnn in TWO.
- rewrite /= in DIST.
- apply leq_trans with (n := a_first + n.+1*task_period tsk); last by done.
- rewrite -addnBA; last by apply ltnW, MORE.
- rewrite leq_add2l.
- {
- unfold div_ceil in MANY.
- destruct (task_period tsk %| t2 - t1) eqn:DIV;
- first by rewrite ltnS leq_divLR in MANY.
- by rewrite ltnS ltn_divLR // in MANY; apply ltnW.
- }
- Qed.
-
- (* This implies that the last job arrives after t2. *)
- Lemma sporadic_arrival_bound_last_arrives_too_late:
- a_last >= t2.
- Proof.
- have NTH := sorted_arrivals_properties_of_nth job_task arr_seq tsk t1 t2 elem.
- have TOOFAR := sporadic_arrival_bound_entire_interval_in_between.
- apply leq_trans with (n := a_first + t2 - t1); last by done.
- apply leq_trans with (n := t1 + t2 - t1); first by rewrite addKn.
- rewrite leq_sub2r // leq_add2r.
- by feed (NTH 0); [ by apply leq_ltn_trans with (n := 1) | des].
- Qed.
-
- (* However, the last job is known to arrive in the interval [t1, t2).
- Contradiction! *)
- Lemma sporadic_arrival_bound_case_3_contradiction: False.
- Proof.
- have LATE := sporadic_arrival_bound_last_arrives_too_late.
- have NTH := sorted_arrivals_properties_of_nth job_task arr_seq
- tsk t1 t2 elem.
- rename H_at_least_two_jobs into TWO.
- rewrite -/num_arrivals in NTH.
- feed (NTH num_arrivals.-1); first by destruct num_arrivals.
- move: NTH => [/andP [_ BUG] _].
- by rewrite ltnNge LATE in BUG.
- Qed.
-
- End DerivingContradiction.
-
- (* Using the proof by contradiction above, we show that the arrival bound
- is correct for case 3 (i.e., at least two arriving jobs). *)
- Lemma sporadic_task_arrival_bound_at_least_two_jobs:
- num_arrivals <= div_ceil (t2 - t1) (task_period tsk).
- Proof.
- have CONTRA := sporadic_arrival_bound_case_3_contradiction.
- unfold num_arrivals, num_arrivals_of_task in *.
- rename H_at_least_two_jobs into TWO.
- set l := arrivals_of_task_between job_task arr_seq tsk t1 t2; fold l in TWO.
- apply contraT; rewrite -ltnNge; intro MANY; exfalso.
- have DUMMY: exists (j: JobIn arr_seq), True.
- {
- destruct l eqn:EQ; first by rewrite /= ltn0 in TWO.
- by exists j.
- } destruct DUMMY as [elem _].
- by apply CONTRA; last by apply elem.
- Qed.
-
- End AtLeastTwoJobs.
-
- (* From the case analysis we infer that the number of job arrivals of tsk
- can be upper-bounded using the length of the interval as follows. *)
- Theorem sporadic_task_arrival_bound:
- num_arrivals <= div_ceil (t2 - t1) (task_period tsk).
- Proof.
- destruct num_arrivals as [|n] eqn:CEIL;
- first by rewrite -CEIL; apply sporadic_arrival_bound_no_jobs.
- destruct n as [|num_arr]; rewrite -CEIL; first by apply sporadic_arrival_bound_one_job.
- by apply sporadic_task_arrival_bound_at_least_two_jobs; rewrite CEIL.
- Qed.
-
- End BasicArrivalBound.
-
- End Lemmas.
-
-End ArrivalBounds.
\ No newline at end of file
diff --git a/model/schedule/uni/schedule.v b/model/schedule/uni/schedule.v
index 8fd88e807ca38f14ef2c6bc19310cf11c1954c23..ce049caffef60d3a276e8edac1c3de6835b6db65 100644
--- a/model/schedule/uni/schedule.v
+++ b/model/schedule/uni/schedule.v
@@ -13,7 +13,6 @@ Module UniprocessorSchedule.
Section ScheduleDef.
Context {Job: eqType}.
- Variable job_cost: Job -> time.
(* Consider any job arrival sequence. *)
Variable arr_seq: arrival_sequence Job.