diff git a/Makefile b/Makefile
index 025787824816f202ceec9b935563dcadbdffbe69..3a828e16c87ad2c86f43488aeaa85eccf7915e2d 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/basic/workload_bound_fp.v ./analysis/uni/basic/fp_rta_comp.v ./analysis/uni/basic/fp_rta_theory.v ./model/arrival_sequence.v ./model/task.v ./model/task_arrival.v ./model/partitioned/schedulability.v ./model/partitioned/schedule.v ./model/priority.v ./model/global/workload.v ./model/global/schedulability.v ./model/global/jitter/interference_edf.v ./model/global/jitter/interference.v ./model/global/jitter/job.v ./model/global/jitter/constrained_deadlines.v ./model/global/jitter/schedule.v ./model/global/jitter/platform.v ./model/global/response_time.v ./model/global/basic/interference_edf.v ./model/global/basic/interference.v ./model/global/basic/constrained_deadlines.v ./model/global/basic/schedule.v ./model/global/basic/platform.v ./model/job.v ./model/time.v ./model/arrival_bounds.v ./model/apa/interference_edf.v ./model/apa/interference.v ./model/apa/affinity.v ./model/apa/constrained_deadlines.v ./model/apa/platform.v ./model/uni/workload.v ./model/uni/transformation/construction.v ./model/uni/schedulability.v ./model/uni/schedule_of_task.v ./model/uni/response_time.v ./model/uni/schedule.v ./model/uni/basic/arrival_bounds.v ./model/uni/basic/busy_interval.v ./model/uni/basic/platform.v ./model/uni/service.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/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/basic/workload_bound_fp.v ./analysis/uni/basic/fp_rta_comp.v ./analysis/uni/basic/fp_rta_theory.v ./model/arrival_sequence.v ./model/task.v ./model/task_arrival.v ./model/suspension.v ./model/partitioned/schedulability.v ./model/partitioned/schedule.v ./model/priority.v ./model/global/workload.v ./model/global/schedulability.v ./model/global/jitter/interference_edf.v ./model/global/jitter/interference.v ./model/global/jitter/job.v ./model/global/jitter/constrained_deadlines.v ./model/global/jitter/schedule.v ./model/global/jitter/platform.v ./model/global/response_time.v ./model/global/basic/interference_edf.v ./model/global/basic/interference.v ./model/global/basic/constrained_deadlines.v ./model/global/basic/schedule.v ./model/global/basic/platform.v ./model/job.v ./model/time.v ./model/arrival_bounds.v ./model/apa/interference_edf.v ./model/apa/interference.v ./model/apa/affinity.v ./model/apa/constrained_deadlines.v ./model/apa/platform.v ./model/uni/workload.v ./model/uni/transformation/construction.v ./model/uni/susp/suspension_intervals.v ./model/uni/susp/schedule.v ./model/uni/susp/platform.v ./model/uni/schedulability.v ./model/uni/schedule_of_task.v ./model/uni/response_time.v ./model/uni/schedule.v ./model/uni/basic/arrival_bounds.v ./model/uni/basic/busy_interval.v ./model/uni/basic/platform.v ./model/uni/service.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/basic/fp_rta_example.v ./implementation/uni/basic/schedule.v o Makefile
#
.DEFAULT_GOAL := all
@@ 145,12 +145,15 @@ VFILES:=util/ssromega.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/basic/workload_bound_fp.v\
analysis/uni/basic/fp_rta_comp.v\
analysis/uni/basic/fp_rta_theory.v\
model/arrival_sequence.v\
model/task.v\
model/task_arrival.v\
+ model/suspension.v\
model/partitioned/schedulability.v\
model/partitioned/schedule.v\
model/priority.v\
@@ 178,6 +181,9 @@ VFILES:=util/ssromega.v\
model/apa/platform.v\
model/uni/workload.v\
model/uni/transformation/construction.v\
+ model/uni/susp/suspension_intervals.v\
+ model/uni/susp/schedule.v\
+ model/uni/susp/platform.v\
model/uni/schedulability.v\
model/uni/schedule_of_task.v\
model/uni/response_time.v\
@@ 206,6 +212,11 @@ VFILES:=util/ssromega.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/basic/fp_rta_example.v\
implementation/uni/basic/schedule.v
diff git a/analysis/apa/bertogna_edf_comp.v b/analysis/apa/bertogna_edf_comp.v
index f0a777da4672957ec19d4308b527cad47b3dde5c..e57397b38a225a3a48d62c5354a96403a9ef6b52 100755
 a/analysis/apa/bertogna_edf_comp.v
+++ b/analysis/apa/bertogna_edf_comp.v
@@ 911,10 +911,10 @@ Module ResponseTimeIterationEDF.
(* ...and jobs are sequential. *)
Hypothesis H_sequential_jobs: sequential_jobs sched.
 (* Assume a workconserving APA scheduler that enforces EDF policy. *)
+ (* Assume a workconserving APA scheduler that respects EDF policy. *)
Hypothesis H_respects_affinity: respects_affinity job_task sched alpha.
Hypothesis H_work_conserving: apa_work_conserving job_cost job_task sched alpha.
 Hypothesis H_edf_policy: enforces_JLDP_policy_under_weak_APA job_cost job_task sched alpha (EDF job_deadline).
+ Hypothesis H_edf_policy: respects_JLFP_policy_under_weak_APA job_cost job_task sched alpha (EDF job_deadline).
(* To avoid a long list of parameters, we provide some local definitions. *)
Definition no_deadline_missed_by_task (tsk: sporadic_task) :=
diff git a/analysis/apa/bertogna_edf_theory.v b/analysis/apa/bertogna_edf_theory.v
index 7f2ba569f795fd02501e2b911912c7c5ddd2d756..f8d7b8ef55d85962877a759c2a4da4240d2e1167 100644
 a/analysis/apa/bertogna_edf_theory.v
+++ b/analysis/apa/bertogna_edf_theory.v
@@ 68,11 +68,11 @@ Module ResponseTimeAnalysisEDF.
completed_jobs_dont_execute job_cost sched.
(* Assume that the schedule is an workconserving APA schedule that
 enforces EDF priorities. *)
+ respects EDF priorities. *)
Hypothesis H_respects_affinity: respects_affinity job_task sched alpha.
Hypothesis H_work_conserving: apa_work_conserving job_cost job_task sched alpha.
Hypothesis H_edf_policy:
 enforces_JLDP_policy_under_weak_APA job_cost job_task sched alpha (EDF job_deadline).
+ respects_JLFP_policy_under_weak_APA job_cost job_task sched alpha (EDF job_deadline).
(* Let's define some local names to avoid passing many parameters. *)
Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
diff git a/analysis/apa/bertogna_fp_comp.v b/analysis/apa/bertogna_fp_comp.v
index b8a18df38d37f5529c442a9ba2e4eb50d6768264..7cc2ffb776067028515808d3d5a63523b37a2a42 100644
 a/analysis/apa/bertogna_fp_comp.v
+++ b/analysis/apa/bertogna_fp_comp.v
@@ 531,11 +531,11 @@ Module ResponseTimeIterationFP.
(* ...and jobs are sequential. *)
Hypothesis H_sequential_jobs: sequential_jobs sched.
 (* Assume a workconserving APA scheduler that enforces the FP policy. *)
+ (* Assume a workconserving APA scheduler that respects the FP policy. *)
Hypothesis H_respects_affinity: respects_affinity job_task sched alpha.
Hypothesis H_work_conserving: apa_work_conserving job_cost job_task sched alpha.
 Hypothesis H_enforces_FP_policy:
 enforces_FP_policy_under_weak_APA job_cost job_task sched alpha higher_priority.
+ Hypothesis H_respects_FP_policy:
+ respects_FP_policy_under_weak_APA job_cost job_task sched alpha higher_priority.
(* To avoid a long list of parameters, we provide some local definitions. *)
Let no_deadline_missed_by_task (tsk: sporadic_task) :=
diff git a/analysis/apa/bertogna_fp_theory.v b/analysis/apa/bertogna_fp_theory.v
index 4242943e0ba070e56038cc66254d9d4dcb9d45cc..e3634a59fe99af82de8d6d6846f5a6d6c3b69679 100644
 a/analysis/apa/bertogna_fp_theory.v
+++ b/analysis/apa/bertogna_fp_theory.v
@@ 72,11 +72,11 @@ Module ResponseTimeAnalysisFP.
Variable higher_eq_priority: FP_policy sporadic_task.
(* ... and assume that the schedule is an APA workconserving
 schedule that enforces this policy. *)
+ schedule that respects this policy. *)
Hypothesis H_respects_affinity: respects_affinity job_task sched alpha.
Hypothesis H_work_conserving: apa_work_conserving job_cost job_task sched alpha.
 Hypothesis H_enforces_FP_policy:
 enforces_FP_policy_under_weak_APA job_cost job_task sched alpha higher_eq_priority.
+ Hypothesis H_respects_FP_policy:
+ respects_FP_policy_under_weak_APA job_cost job_task sched alpha higher_eq_priority.
(* Let's define some local names to avoid passing many parameters. *)
Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
@@ 383,7 +383,7 @@ Module ResponseTimeAnalysisFP.
H_previous_jobs_of_tsk_completed into BEFOREok,
H_response_time_no_larger_than_deadline into NOMISS,
H_constrained_deadlines into RESTR,
 H_respects_affinity into APA, H_enforces_FP_policy into FP.
+ H_respects_affinity into APA, H_respects_FP_policy into FP.
unfold sporadic_task_model in *.
unfold x, X, total_interference, task_interference.
rewrite big_mkcond exchange_big big_distrl /= mul1n.
@@ 444,7 +444,7 @@ Module ResponseTimeAnalysisFP.
H_work_conserving into WORK,
H_response_time_no_larger_than_deadline into NOMISS,
H_constrained_deadlines into RESTR,
 H_enforces_FP_policy into FP,
+ H_respects_FP_policy into FP,
H_respects_affinity into APA, H_affinity_subset into SUB.
unfold sporadic_task_model in *.
unfold x, X, total_interference, task_interference.
@@ 512,7 +512,7 @@ Module ResponseTimeAnalysisFP.
H_valid_task_parameters into PARAMS,
H_previous_jobs_of_tsk_completed into BEFOREok,
H_sequential_jobs into SEQ, H_constrained_deadlines into CONSTR,
 H_enforces_FP_policy into FP.
+ H_respects_FP_policy into FP.
move => t /andP [GEt LTt] BACK.
move: WORK => WORK.
specialize (WORK j t BACK).
@@ 667,7 +667,7 @@ Module ResponseTimeAnalysisFP.
H_job_of_tsk into JOBtsk, H_affinity_subset into SUB,
H_sporadic_tasks into SPO, H_respects_affinity into APA,
H_constrained_deadlines into RESTR,
 H_sequential_jobs into SEQ, H_enforces_FP_policy into FP.
+ H_sequential_jobs into SEQ, H_respects_FP_policy into FP.
unfold sporadic_task_model in *.
move => delta /andP [HAS LT].
rewrite has_count in HAS.
diff git a/analysis/apa/interference_bound_edf.v b/analysis/apa/interference_bound_edf.v
index 913c5beb0ed38bfd5addf1559abe77949ffbd393..be081757655c6ca9b5c10eb3c3099917466bb037 100644
 a/analysis/apa/interference_bound_edf.v
+++ b/analysis/apa/interference_bound_edf.v
@@ 174,7 +174,7 @@ Module InterferenceBoundEDF.
(* Assume that the scheduler is a workconserving EDF scheduler. *)
Hypothesis H_work_conserving: apa_work_conserving job_cost job_task sched alpha.
Hypothesis H_edf_weak_APA_scheduler:
 enforces_JLDP_policy_under_weak_APA job_cost job_task sched alpha (EDF job_deadline).
+ respects_JLFP_policy_under_weak_APA job_cost job_task sched alpha (EDF job_deadline).
(* Let tsk_i be the task to be analyzed, ...*)
Variable tsk_i: sporadic_task.
diff git a/analysis/global/basic/bertogna_edf_comp.v b/analysis/global/basic/bertogna_edf_comp.v
index ad6f43082fa69e2771be297eab07409f7f3a23d8..de4d42c9772ad10af25431aba066929075ad755b 100755
 a/analysis/global/basic/bertogna_edf_comp.v
+++ b/analysis/global/basic/bertogna_edf_comp.v
@@ 900,7 +900,7 @@ Module ResponseTimeIterationEDF.
(* Assume a workconserving scheduler with EDF policy. *)
Hypothesis H_work_conserving: work_conserving job_cost sched.
 Hypothesis H_edf_policy: enforces_JLDP_policy job_cost sched (EDF job_deadline).
+ Hypothesis H_edf_policy: respects_JLFP_policy job_cost sched (EDF job_deadline).
Definition no_deadline_missed_by_task (tsk: sporadic_task) :=
task_misses_no_deadline job_cost job_deadline job_task sched tsk.
diff git a/analysis/global/basic/bertogna_edf_theory.v b/analysis/global/basic/bertogna_edf_theory.v
index 15e0e18b057828c9d5f026cf97556ccd0d61cfee..0b800f1afe6e2f5c56c1b914fe4e0c5466f408af 100644
 a/analysis/global/basic/bertogna_edf_theory.v
+++ b/analysis/global/basic/bertogna_edf_theory.v
@@ 69,7 +69,7 @@ Module ResponseTimeAnalysisEDF.
(* Assume that the schedule is a workconserving EDF schedule. *)
Hypothesis H_work_conserving: work_conserving job_cost sched.
 Hypothesis H_edf_policy: enforces_JLDP_policy job_cost sched (EDF job_deadline).
+ Hypothesis H_edf_policy: respects_JLFP_policy job_cost sched (EDF job_deadline).
(* Let's define some local names to avoid passing many parameters. *)
Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
diff git a/analysis/global/basic/bertogna_fp_comp.v b/analysis/global/basic/bertogna_fp_comp.v
index 6bc0e4d64a00e1b4eb14ce8d09339a89418f87d4..164a8dcbfaa5e88f4063e4bf43d53349ffadc3c3 100644
 a/analysis/global/basic/bertogna_fp_comp.v
+++ b/analysis/global/basic/bertogna_fp_comp.v
@@ 518,10 +518,10 @@ Module ResponseTimeIterationFP.
(* Also assume that jobs are sequential (as required by the workload bound). *)
Hypothesis H_sequential_jobs: sequential_jobs sched.
 (* Assume that the scheduler is workconserving and enforces the FP policy. *)
+ (* Assume that the scheduler is workconserving and respects the FP policy. *)
Hypothesis H_work_conserving: work_conserving job_cost sched.
 Hypothesis H_enforces_FP_policy:
 enforces_FP_policy job_cost job_task sched higher_priority.
+ Hypothesis H_respects_FP_policy:
+ respects_FP_policy job_cost job_task sched higher_priority.
Let no_deadline_missed_by_task (tsk: sporadic_task) :=
task_misses_no_deadline job_cost job_deadline job_task sched tsk.
diff git a/analysis/global/basic/bertogna_fp_theory.v b/analysis/global/basic/bertogna_fp_theory.v
index 822997f01543e3fe91ed317aa8af0ae337339c3d..aa5fca4c4bf31284a2eeaff03824641091961fcf 100644
 a/analysis/global/basic/bertogna_fp_theory.v
+++ b/analysis/global/basic/bertogna_fp_theory.v
@@ 71,10 +71,10 @@ Module ResponseTimeAnalysisFP.
Variable higher_eq_priority: FP_policy sporadic_task.
(* ... and assume that the schedule is a workconserving
 schedule that enforces this policy. *)
+ schedule that respects this policy. *)
Hypothesis H_work_conserving: work_conserving job_cost sched.
 Hypothesis H_enforces_FP_policy:
 enforces_FP_policy job_cost job_task sched higher_eq_priority.
+ Hypothesis H_respects_FP_policy:
+ respects_FP_policy job_cost job_task sched higher_eq_priority.
(* Let's define some local names to avoid passing many parameters. *)
Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
@@ 383,7 +383,7 @@ Module ResponseTimeAnalysisFP.
\sum_(tsk_k < hp_tasks) x tsk_k = X * num_cpus.
Proof.
have DIFFTASK := bertogna_fp_interference_by_different_tasks.
 rename H_work_conserving into WORK, H_enforces_FP_policy into FP,
+ rename H_work_conserving into WORK, H_respects_FP_policy into FP,
H_all_jobs_from_taskset into FROMTS, H_job_of_tsk into JOBtsk.
unfold sporadic_task_model in *.
unfold x, X, total_interference, task_interference.
@@ 436,7 +436,7 @@ Module ResponseTimeAnalysisFP.
H_response_time_no_larger_than_deadline into NOMISS,
H_constrained_deadlines into CONSTR,
H_sequential_jobs into SEQ,
 H_enforces_FP_policy into FP,
+ H_respects_FP_policy into FP,
H_hp_bounds_has_interfering_tasks into HASHP,
H_interfering_tasks_miss_no_deadlines into NOMISSHP.
unfold sporadic_task_model in *.
diff git a/analysis/global/basic/interference_bound_edf.v b/analysis/global/basic/interference_bound_edf.v
index 5923528dca82e6290d8d755a2a06377e963e9151..410628c5f6a7003c435af4cde0e4b2c29bba1ad6 100644
 a/analysis/global/basic/interference_bound_edf.v
+++ b/analysis/global/basic/interference_bound_edf.v
@@ 161,7 +161,7 @@ Module InterferenceBoundEDF.
(* Assume that the scheduler is a workconserving EDF scheduler. *)
Hypothesis H_work_conserving: work_conserving job_cost sched.
Hypothesis H_edf_scheduler:
 enforces_JLDP_policy job_cost sched (EDF job_deadline).
+ respects_JLFP_policy job_cost sched (EDF job_deadline).
(* Let tsk_i be the task to be analyzed, ...*)
Variable tsk_i: sporadic_task.
diff git a/analysis/global/jitter/bertogna_edf_comp.v b/analysis/global/jitter/bertogna_edf_comp.v
index 31701e5aa13fb812d3726cea523851099a466085..2c4fabe7098f3b0a6774ea8ec2ce0018246a1043 100755
 a/analysis/global/jitter/bertogna_edf_comp.v
+++ b/analysis/global/jitter/bertogna_edf_comp.v
@@ 987,7 +987,7 @@ Module ResponseTimeIterationEDF.
(* Assume that we have a workconserving EDF scheduler. *)
Hypothesis H_work_conserving: work_conserving job_cost job_jitter sched.
 Hypothesis H_edf_policy: enforces_JLDP_policy job_cost job_jitter sched (EDF job_deadline).
+ Hypothesis H_edf_policy: respects_JLFP_policy job_cost job_jitter sched (EDF job_deadline).
Let no_deadline_missed_by_task (tsk: sporadic_task) :=
task_misses_no_deadline job_cost job_deadline job_task sched tsk.
diff git a/analysis/global/jitter/bertogna_edf_theory.v b/analysis/global/jitter/bertogna_edf_theory.v
index 6a5542746dd44f12297f1d482efe233c3211cd05..ddea5fec08dc5b47aa0f48a9c86f4a06f0212323 100644
 a/analysis/global/jitter/bertogna_edf_theory.v
+++ b/analysis/global/jitter/bertogna_edf_theory.v
@@ 75,7 +75,7 @@ Module ResponseTimeAnalysisEDFJitter.
(* Assume that the schedule is a workconserving EDF schedule. *)
Hypothesis H_work_conserving: work_conserving job_cost job_jitter sched.
 Hypothesis H_edf_policy: enforces_JLDP_policy job_cost job_jitter sched (EDF job_deadline).
+ Hypothesis H_edf_policy: respects_JLFP_policy job_cost job_jitter sched (EDF job_deadline).
(* Let's define some local names to avoid passing many parameters. *)
Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
diff git a/analysis/global/jitter/bertogna_fp_comp.v b/analysis/global/jitter/bertogna_fp_comp.v
index 13b5b83f530ea19bdd0937f5401b2390089e56ed..12c0ff8e79bbf317411e12b9eb7eff8d86c86abd 100644
 a/analysis/global/jitter/bertogna_fp_comp.v
+++ b/analysis/global/jitter/bertogna_fp_comp.v
@@ 519,10 +519,10 @@ Module ResponseTimeIterationFP.
(* Also assume that jobs are sequential (as required by the workload bound). *)
Hypothesis H_sequential_jobs: sequential_jobs sched.
 (* Assume that the scheduler is workconserving and enforces the FP policy. *)
+ (* Assume that the scheduler is workconserving and respects the FP policy. *)
Hypothesis H_work_conserving: work_conserving job_cost job_jitter sched.
 Hypothesis H_enforces_FP_policy:
 enforces_FP_policy job_cost job_task job_jitter sched higher_priority.
+ Hypothesis H_respects_FP_policy:
+ respects_FP_policy job_cost job_task job_jitter sched higher_priority.
Let no_deadline_missed_by_task (tsk: sporadic_task) :=
task_misses_no_deadline job_cost job_deadline job_task sched tsk.
diff git a/analysis/global/jitter/bertogna_fp_theory.v b/analysis/global/jitter/bertogna_fp_theory.v
index 36bb1d68102990ea0cf33e5cb63f2dce42984384..790c26db631c90fbd493cb63fe7db84ad380b1ad 100644
 a/analysis/global/jitter/bertogna_fp_theory.v
+++ b/analysis/global/jitter/bertogna_fp_theory.v
@@ 76,10 +76,10 @@ Module ResponseTimeAnalysisFP.
(* Consider a given FP policy, ... *)
Variable higher_eq_priority: FP_policy sporadic_task.
 (* ...and assume that the schedule is workconserving and enforces this policy. *)
+ (* ...and assume that the schedule is workconserving and respects this policy. *)
Hypothesis H_work_conserving: work_conserving job_cost job_jitter sched.
 Hypothesis H_enforces_priority:
 enforces_FP_policy job_cost job_task job_jitter sched higher_eq_priority.
+ Hypothesis H_respects_priority:
+ respects_FP_policy job_cost job_task job_jitter sched higher_eq_priority.
(* Let's define some local names to avoid passing many parameters. *)
Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
@@ 416,7 +416,7 @@ Module ResponseTimeAnalysisFP.
H_work_conserving into WORK,
H_constrained_deadlines into CONSTR,
H_previous_jobs_of_tsk_completed into PREV,
 H_enforces_priority into FP,
+ H_respects_priority into FP,
H_response_time_no_larger_than_deadline into NOMISS.
unfold sporadic_task_model in *.
unfold x, X, total_interference, task_interference.
@@ 470,7 +470,7 @@ Module ResponseTimeAnalysisFP.
H_response_time_no_larger_than_deadline into NOMISS,
H_constrained_deadlines into CONSTR,
H_sequential_jobs into SEQ,
 H_enforces_priority into FP,
+ H_respects_priority into FP,
H_hp_bounds_has_interfering_tasks into HASHP,
H_interfering_tasks_miss_no_deadlines into NOMISSHP.
unfold sporadic_task_model, valid_sporadic_job_with_jitter, valid_sporadic_job in *.
diff git a/analysis/global/jitter/interference_bound_edf.v b/analysis/global/jitter/interference_bound_edf.v
index bc54baf3b1c5febf468fee366b86d6904c48c62f..b8cc8f2491a74b78b5376661159ad9dd9d526e1d 100644
 a/analysis/global/jitter/interference_bound_edf.v
+++ b/analysis/global/jitter/interference_bound_edf.v
@@ 163,7 +163,7 @@ Module InterferenceBoundEDFJitter.
(* Assume that we have a workconserving EDF scheduler. *)
Hypothesis H_work_conserving: work_conserving job_cost job_jitter sched.
 Hypothesis H_edf_policy: enforces_JLDP_policy job_cost job_jitter sched (EDF job_deadline).
+ Hypothesis H_edf_policy: respects_JLFP_policy job_cost job_jitter sched (EDF job_deadline).
(* Let tsk_i be the task to be analyzed, ...*)
Variable tsk_i: sporadic_task.
diff git a/analysis/global/parallel/bertogna_edf_comp.v b/analysis/global/parallel/bertogna_edf_comp.v
index 32c5f7898fb85b96a1802068c40e29c7fbefa8e2..b1a4a2d1300e6b7db79364299a2655365ab22eb0 100755
 a/analysis/global/parallel/bertogna_edf_comp.v
+++ b/analysis/global/parallel/bertogna_edf_comp.v
@@ 893,7 +893,7 @@ Module ResponseTimeIterationEDF.
(* Assume a workconserving scheduler with EDF policy. *)
Hypothesis H_work_conserving: work_conserving job_cost sched.
 Hypothesis H_edf_policy: enforces_JLDP_policy job_cost sched (EDF job_deadline).
+ Hypothesis H_edf_policy: respects_JLFP_policy job_cost sched (EDF job_deadline).
Definition no_deadline_missed_by_task (tsk: sporadic_task) :=
task_misses_no_deadline job_cost job_deadline job_task sched tsk.
diff git a/analysis/global/parallel/bertogna_edf_theory.v b/analysis/global/parallel/bertogna_edf_theory.v
index 564115fe0955ec088fabd44c12fe08a4ce141a8f..c0a44f9d5f59d070e0acb629725e585fcccbe0d3 100644
 a/analysis/global/parallel/bertogna_edf_theory.v
+++ b/analysis/global/parallel/bertogna_edf_theory.v
@@ 69,7 +69,7 @@ Module ResponseTimeAnalysisEDF.
(* Assume that the schedule is a workconserving EDF schedule. *)
Hypothesis H_work_conserving: work_conserving job_cost sched.
 Hypothesis H_edf_policy: enforces_JLDP_policy job_cost sched (EDF job_deadline).
+ Hypothesis H_edf_policy: respects_JLFP_policy job_cost sched (EDF job_deadline).
(* Let's define some local names to avoid passing many parameters. *)
Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
diff git a/analysis/global/parallel/bertogna_fp_comp.v b/analysis/global/parallel/bertogna_fp_comp.v
index b7fa67b9bd06082621918d7bd2e4748f84d699ca..ca8584bf9e1b27284285dd0aea88be5b8ae05b56 100644
 a/analysis/global/parallel/bertogna_fp_comp.v
+++ b/analysis/global/parallel/bertogna_fp_comp.v
@@ 505,10 +505,10 @@ unfold interference_bound_generic; simpl.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
 (* Assume that the scheduler is workconserving and enforces the FP policy. *)
+ (* Assume that the scheduler is workconserving and respects the FP policy. *)
Hypothesis H_work_conserving: work_conserving job_cost sched.
 Hypothesis H_enforces_FP_policy:
 enforces_FP_policy job_cost job_task sched higher_priority.
+ Hypothesis H_respects_FP_policy:
+ respects_FP_policy job_cost job_task sched higher_priority.
Let no_deadline_missed_by_task (tsk: sporadic_task) :=
task_misses_no_deadline job_cost job_deadline job_task sched tsk.
diff git a/analysis/global/parallel/bertogna_fp_theory.v b/analysis/global/parallel/bertogna_fp_theory.v
index c4ffa2d6f9bd4dedbefe370b468b788f4adebf36..e7eba2c09162004b1c9c370a2719df2562321cfc 100644
 a/analysis/global/parallel/bertogna_fp_theory.v
+++ b/analysis/global/parallel/bertogna_fp_theory.v
@@ 68,10 +68,10 @@ Module ResponseTimeAnalysisFP.
Variable higher_eq_priority: FP_policy sporadic_task.
(* ... and assume that the schedule is an APA workconserving
 schedule that enforces this policy. *)
+ schedule that respects this policy. *)
Hypothesis H_work_conserving: work_conserving job_cost sched.
 Hypothesis H_enforces_FP_policy:
 enforces_FP_policy job_cost job_task sched higher_eq_priority.
+ Hypothesis H_respects_FP_policy:
+ respects_FP_policy job_cost job_task sched higher_eq_priority.
(* Assume that there exists at least one processor. *)
Hypothesis H_at_least_one_cpu: num_cpus > 0.
@@ 267,11 +267,11 @@ Module ResponseTimeAnalysisFP.
H_sporadic_tasks into SPO,
H_work_conserving into WORK,
H_constrained_deadlines into RESTR,
 H_enforces_FP_policy into FP,
+ H_respects_FP_policy into FP,
H_previous_jobs_of_tsk_completed into BEFOREok,
H_response_time_no_larger_than_deadline into NOMISS.
 unfold sporadic_task_model, enforces_FP_policy,
 enforces_JLDP_policy, FP_to_JLDP in *.
+ unfold sporadic_task_model, respects_FP_policy,
+ respects_JLDP_policy, FP_to_JLDP in *.
unfold x, X, total_interference, task_interference.
rewrite big_mkcond exchange_big big_distrl /=.
rewrite [\sum_(_ <= _ < _  backlogged _ _ _ _) _]big_mkcond.
diff git a/analysis/global/parallel/interference_bound_edf.v b/analysis/global/parallel/interference_bound_edf.v
index 969aac4f8c4e5032fbf18ae53667dbfd0fb6793f..ff8ae33de74dfb3431c4c026df05662df2ea91ce 100644
 a/analysis/global/parallel/interference_bound_edf.v
+++ b/analysis/global/parallel/interference_bound_edf.v
@@ 158,7 +158,7 @@ Module InterferenceBoundEDF.
(* Assume that the scheduler is a workconserving EDF scheduler. *)
Hypothesis H_work_conserving: work_conserving job_cost sched.
Hypothesis H_edf_scheduler:
 enforces_JLDP_policy job_cost sched (EDF job_deadline).
+ respects_JLFP_policy job_cost sched (EDF job_deadline).
(* Let tsk_i be the task to be analyzed, ...*)
Variable tsk_i: sporadic_task.
diff git a/analysis/uni/basic/fp_rta_comp.v b/analysis/uni/basic/fp_rta_comp.v
index f3b98a2cb13dcdea5de84dd108a51f90a2f0ccf0..c40b00cad983e2b12105c4d2301238e460ae42ab 100644
 a/analysis/uni/basic/fp_rta_comp.v
+++ b/analysis/uni/basic/fp_rta_comp.v
@@ 288,10 +288,10 @@ Module ResponseTimeIterationFP.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
 (* Also assume that the scheduler is workconserving and enforces the FP policy. *)
+ (* Also assume that the scheduler is workconserving and respects the FP policy. *)
Hypothesis H_work_conserving: work_conserving job_cost sched.
 Hypothesis H_enforces_FP_policy:
 enforces_FP_policy job_cost job_task sched higher_eq_priority.
+ Hypothesis H_respects_FP_policy:
+ respects_FP_policy job_cost job_task sched higher_eq_priority.
(* For simplicity, let's define some local names. *)
Let no_deadline_missed_by_task :=
diff git a/analysis/uni/basic/fp_rta_theory.v b/analysis/uni/basic/fp_rta_theory.v
index 534fde6e2f29956426164540fbd227305ec6c98f..7503f2f7ea00bf41380da38c933a904593418269 100644
 a/analysis/uni/basic/fp_rta_theory.v
+++ b/analysis/uni/basic/fp_rta_theory.v
@@ 66,7 +66,7 @@ Module ResponseTimeAnalysisFP.
(* Next, assume that the schedule is a workconserving FP schedule. *)
Hypothesis H_work_conserving: work_conserving job_cost sched.
 Hypothesis H_enforces_fp_policy: enforces_FP_policy job_cost job_task sched higher_eq_priority.
+ Hypothesis H_respects_fp_policy: respects_FP_policy job_cost job_task sched higher_eq_priority.
(* Now we proceed with the analysis.
Let tsk be any task in ts that is to be analyzed. *)
@@ 92,13 +92,17 @@ Module ResponseTimeAnalysisFP.
Theorem uniprocessor_response_time_bound_fp:
response_time_bounded_by tsk R.
Proof.
+ rename H_response_time_is_fixed_point into FIX.
intros j JOBtsk.
 apply busy_interval_bounds_response_time with
 (job_task0 := job_task) (tsk0 := tsk)
 (higher_eq_priority0 := higher_eq_priority); try (by done).
+ have bla := busy_interval_bounds_response_time.
+ set prio := FP_to_JLFP job_task arr_seq higher_eq_priority.
+ apply busy_interval_bounds_response_time with (higher_eq_priority0 := prio); try (by done).
+  by intros x; apply H_priority_is_reflexive.
+  by intros x z y; apply H_priority_is_transitive.
apply fp_workload_bound_holds with (task_cost0 := task_cost)
(task_period0 := task_period) (task_deadline0 := task_deadline)
(job_deadline0 := job_deadline) (ts0 := ts); try (by done).
+ by rewrite JOBtsk.
Qed.
End ResponseTimeBound.
diff git a/analysis/uni/basic/workload_bound_fp.v b/analysis/uni/basic/workload_bound_fp.v
index cb64d4a145e3b78c1cd55c25545c751cfd740a6b..d535ecd206bf5941f386fcbf691765d7a8f9bb20 100644
 a/analysis/uni/basic/workload_bound_fp.v
+++ b/analysis/uni/basic/workload_bound_fp.v
@@ 187,7 +187,7 @@ Module WorkloadBoundFP.
(* First, let's define some local names for clarity. *)
Let hp_workload :=
 workload_of_higher_or_equal_priority job_cost job_task arr_seq higher_eq_priority tsk.
+ workload_of_higher_or_equal_priority_tasks job_cost job_task arr_seq higher_eq_priority tsk.
Let workload_bound :=
total_workload_bound_fp task_cost task_period higher_eq_priority ts tsk.
@@ 206,7 +206,7 @@ Module WorkloadBoundFP.
rename H_fixed_point into FIX, H_all_jobs_from_taskset into FROMTS,
H_valid_job_parameters into JOBPARAMS,
H_valid_task_parameters into PARAMS.
 unfold hp_workload, workload_of_higher_or_equal_priority,
+ unfold hp_workload, workload_of_higher_or_equal_priority_tasks,
valid_sporadic_job, valid_realtime_job,
valid_sporadic_taskset, is_valid_sporadic_task in *.
intro t.
diff git a/analysis/uni/susp/dynamic/oblivious/fp_rta.v b/analysis/uni/susp/dynamic/oblivious/fp_rta.v
new file mode 100644
index 0000000000000000000000000000000000000000..3765496bc1f00a5510ee294a3dc9ae4501e8ece9
 /dev/null
+++ b/analysis/uni/susp/dynamic/oblivious/fp_rta.v
@@ 0,0 +1,150 @@
+Require Import rt.util.all.
+Require Import rt.model.job rt.model.task rt.model.arrival_sequence
+ rt.model.priority rt.model.suspension rt.model.task_arrival.
+Require Import rt.model.uni.schedule rt.model.uni.schedulability.
+Require Import rt.model.uni.susp.suspension_intervals
+ rt.model.uni.susp.schedule rt.model.uni.susp.platform.
+Require Import rt.analysis.uni.basic.fp_rta_comp.
+Require Import rt.analysis.uni.susp.dynamic.oblivious.reduction.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+
+Module SuspensionObliviousFP.
+
+ Import Job TaskArrival SporadicTaskset Suspension Priority Schedulability
+ PlatformWithSuspensions SuspensionIntervals.
+ Export ResponseTimeIterationFP ReductionToBasicSchedule.
+
+ (* In this section, we formalize the suspensionoblivious RTA
+ for fixedpriority tasks under the dynamic selfsuspension model. *)
+ Section ReductionToBasicAnalysis.
+
+ Context {SporadicTask: eqType}.
+ Variable task_cost: SporadicTask > time.
+ Variable task_period: SporadicTask > time.
+ Variable task_deadline: SporadicTask > time.
+
+ Context {Job: eqType}.
+ Variable job_cost: Job > time.
+ Variable job_deadline: Job > time.
+ Variable job_task: Job > SporadicTask.
+
+ (* Let ts be any task set to be analyzed... *)
+ Variable ts: taskset_of SporadicTask.
+
+ (* ...such that tasks have valid parameters. *)
+ Hypothesis H_valid_task_parameters:
+ valid_sporadic_taskset task_cost task_period task_deadline ts.
+
+ (* Next, consider any job arrival sequence with no duplicate arrivals,... *)
+ Context {arr_seq: arrival_sequence Job}.
+ Hypothesis H_arrival_sequence_is_a_set: arrival_sequence_is_a_set arr_seq.
+
+ (* ...in which all jobs come from task set ts, ... *)
+ Hypothesis H_jobs_from_taskset: forall (j: JobIn arr_seq), job_task j \in ts.
+
+ (* ...have valid parameters,...*)
+ Hypothesis H_valid_job_parameters:
+ forall (j: JobIn arr_seq),
+ valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
+
+ (* ... and satisfy the sporadic task model.*)
+ Hypothesis H_sporadic_tasks: sporadic_task_model task_period arr_seq job_task.
+
+ (* Consider any FP policy that is reflexive, transitive and total, indicating
+ "higher or equal task priority". *)
+ Variable higher_eq_priority: FP_policy SporadicTask.
+ Hypothesis H_priority_is_reflexive: FP_is_reflexive higher_eq_priority.
+ Hypothesis H_priority_is_transitive: FP_is_transitive higher_eq_priority.
+ Hypothesis H_priority_is_total: FP_is_total_over_task_set higher_eq_priority ts.
+
+ (* Assume that the total suspension time of any job is bounded according
+ to the dynamic suspension model. *)
+ Variable next_suspension: job_suspension Job.
+ Variable task_suspension_bound: SporadicTask > time.
+ Hypothesis H_dynamic_suspensions:
+ dynamic_suspension_model job_cost job_task next_suspension task_suspension_bound.
+
+ (* Next, consider any suspensionaware schedule... *)
+ Variable sched: schedule arr_seq.
+
+ (* ...where jobs only execute after they arrive... *)
+ Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched.
+
+ (* ...and no longer than their execution costs. *)
+ Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
+
+ (* Also assume that the schedule is workconserving when there are nonsuspended jobs, ... *)
+ Hypothesis H_work_conserving: work_conserving job_cost next_suspension sched.
+
+ (* ...that the schedule respects job priority... *)
+ Hypothesis H_respects_priority:
+ respects_FP_policy job_cost job_task next_suspension sched higher_eq_priority.
+
+ (* ...and that suspended jobs are not allowed to be scheduled. *)
+ Hypothesis H_respects_self_suspensions:
+ respects_self_suspensions job_cost next_suspension sched.
+
+ (* Now we move to the schedulability analysis. *)
+ Section MainProof.
+
+ (* For simplicity, let's first define some local names. *)
+ Let task_is_schedulable := task_misses_no_deadline job_cost job_deadline job_task sched.
+
+ (* Now, consider the task costs inflated with suspension bounds... *)
+ Let inflated_cost := inflated_task_cost task_cost task_suspension_bound.
+
+ (* ...and assume that these costs are no larger than the deadline nor the period of each task. *)
+ Hypothesis H_inflated_cost_le_deadline_and_period:
+ forall tsk,
+ tsk \in ts >
+ inflated_cost tsk <= task_deadline tsk /\
+ inflated_cost tsk <= task_period tsk.
+
+ (* Next, recall the responsetime analysis for FP scheduling instantiated with
+ these inflated task costs. *)
+ Let claimed_to_be_schedulable :=
+ fp_schedulable inflated_cost task_period task_deadline higher_eq_priority.
+
+ (* Finally, we prove that if the suspensionoblivious schedulability test suceeds... *)
+ Hypothesis H_claimed_schedulable_by_suspension_oblivious_RTA:
+ claimed_to_be_schedulable ts.
+
+ (* ...then no task misses its deadline in the suspensionaware schedule.
+ The proof is a straightforward application of the following lemma from
+ reduction.v: suspension_oblivious_preserves_schedulability. *)
+ Theorem suspension_oblivious_fp_rta_implies_schedulability:
+ forall tsk,
+ tsk \in ts >
+ task_is_schedulable tsk.
+ Proof.
+ rename H_claimed_schedulable_by_suspension_oblivious_RTA into SCHED,
+ H_jobs_from_taskset into FROMTS, H_inflated_cost_le_deadline_and_period into LEdl.
+ intros tsk INts j JOBtsk.
+ apply suspension_oblivious_preserves_schedulability with
+ (higher_eq_priority0 := (FP_to_JLDP job_task arr_seq higher_eq_priority))
+ (next_suspension0 := next_suspension); try (by done).
+  by intros t x; apply H_priority_is_reflexive.
+  by intros t y x z; apply H_priority_is_transitive.
+  by intros t j1 j2; apply/orP; apply H_priority_is_total.
+ apply jobs_schedulable_by_fp_rta with (task_cost0 := inflated_cost) (ts0 := ts)
+ (task_period0 := task_period) (task_deadline0 := task_deadline) (job_task0 := job_task)
+ (higher_eq_priority0 := higher_eq_priority); try (by done).
+  by apply suspension_oblivious_task_parameters_remain_valid.
+  by apply suspension_oblivious_job_parameters_remain_valid with (ts0 := ts)
+ (task_period0 := task_period).
+  by apply sched_new_jobs_must_arrive_to_execute.
+  by apply sched_new_completed_jobs_dont_execute.
+  by apply sched_new_work_conserving.
+ {
+ intros j_low j_hp t; apply sched_new_respects_policy.
+  by intros t' x; apply H_priority_is_reflexive.
+  by intros t' j1 j2 j3; apply H_priority_is_transitive.
+  by intros t' j1 j2; apply/orP; apply H_priority_is_total.
+ }
+ Qed.
+
+ End MainProof.
+
+ End ReductionToBasicAnalysis.
+
+End SuspensionObliviousFP.
\ No newline at end of file
diff git a/analysis/uni/susp/dynamic/oblivious/reduction.v b/analysis/uni/susp/dynamic/oblivious/reduction.v
new file mode 100644
index 0000000000000000000000000000000000000000..e5f6844c87cc304de93671d58543a70d104f9ba2
 /dev/null
+++ b/analysis/uni/susp/dynamic/oblivious/reduction.v
@@ 0,0 +1,712 @@
+Require Import rt.util.all.
+Require Import rt.model.job rt.model.task rt.model.arrival_sequence
+ rt.model.priority rt.model.suspension.
+Require Import rt.model.uni.schedule rt.model.uni.schedulability.
+Require Import rt.model.uni.basic.platform.
+Require Import rt.model.uni.susp.suspension_intervals
+ rt.model.uni.susp.schedule rt.model.uni.susp.platform.
+Require Import rt.model.uni.transformation.construction.
+Require Import rt.implementation.uni.basic.schedule.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.
+
+Module ReductionToBasicSchedule.
+
+ Import Job SporadicTaskset Suspension Priority SuspensionIntervals
+ Schedulability ScheduleConstruction.
+
+ (* Recall the platform constraints for suspensionoblivious and suspensionaware schedules. *)
+ Module susp := ScheduleWithSuspensions.
+ Module susp_oblivious := Platform.
+ Module susp_aware := PlatformWithSuspensions.
+
+ (* In this section, we perform a reduction from a suspensionaware schedule
+ to a suspensionoblivious schedule, in which jobs have inflated execution costs. *)
+ Section Reduction.
+
+ Context {Task: eqType}.
+ Variable task_period: Task > time.
+ Variable task_deadline: Task > time.
+
+ Context {Job: eqType}.
+ Variable job_deadline: Job > time.
+ Variable job_task: Job > Task.
+
+ (* Let ts be any task set to be analyzed. *)
+ Variable ts: seq Task.
+
+ (* Next, consider any job arrival sequence... *)
+ Context {arr_seq: arrival_sequence Job}.
+
+ (* ...whose jobs come from task set ts. *)
+ Hypothesis H_jobs_from_taskset:
+ forall (j: JobIn arr_seq), job_task j \in ts.
+
+ (* Consider any JLDP policy that is reflexive, transitive and total, i.e., that
+ indicates "higher or equal priority". *)
+ Variable higher_eq_priority: JLDP_policy arr_seq.
+ Hypothesis H_priority_is_reflexive: JLDP_is_reflexive higher_eq_priority.
+ Hypothesis H_priority_is_transitive: JLDP_is_transitive higher_eq_priority.
+ Hypothesis H_priority_is_total: JLDP_is_total higher_eq_priority.
+
+ (* Consider the original job and task costs. *)
+ Variable original_job_cost: Job > time.
+ Variable original_task_cost: Task > time.
+
+ (* Assume that the maximum suspension time of any job is bounded according
+ to the dynamic suspension model. *)
+ Variable next_suspension: job_suspension Job.
+ Variable task_suspension_bound: Task > time.
+ Hypothesis H_dynamic_suspensions:
+ dynamic_suspension_model original_job_cost job_task next_suspension task_suspension_bound.
+
+ (* Next, consider any suspensionaware schedule where jobs have their original costs. *)
+ Variable sched_susp: schedule arr_seq.
+
+ (* Assume that jobs only execute after they arrive... *)
+ Hypothesis H_jobs_must_arrive_to_execute:
+ jobs_must_arrive_to_execute sched_susp.
+
+ (* ...and no longer than their execution costs. *)
+ Hypothesis H_completed_jobs_dont_execute:
+ completed_jobs_dont_execute original_job_cost sched_susp.
+
+ (* Also assume that the schedule is workconserving if there are nonsuspended jobs, ... *)
+ Hypothesis H_work_conserving:
+ susp_aware.work_conserving original_job_cost next_suspension sched_susp.
+
+ (* ...that the schedule respects job priority... *)
+ Hypothesis H_respects_priority:
+ susp_aware.respects_JLDP_policy original_job_cost next_suspension
+ sched_susp higher_eq_priority.
+
+ (* ...and that suspended jobs are not allowed to be scheduled. *)
+ Hypothesis H_respects_self_suspensions:
+ respects_self_suspensions original_job_cost next_suspension sched_susp.
+
+ (* Now we proceed with the reduction. First, we formalize the inflation of job and task costs. *)
+ Section CostInflation.
+
+ (* Recall the total suspension time of a job in the original schedule. *)
+ Let job_total_suspension :=
+ total_suspension original_job_cost next_suspension.
+
+ (* To inflate job costs, we just add the total suspension of the job. *)
+ Definition inflated_job_cost (j: Job) :=
+ original_job_cost j + job_total_suspension j.
+
+ (* Similarly, to inflate task costs, we just add its suspension bound. *)
+ Definition inflated_task_cost (tsk: Task) :=
+ original_task_cost tsk + task_suspension_bound tsk.
+
+ (* As shown next, this inflation produces job valid parameters. *)
+ Section NewParametersAreValid.
+
+ (* Recall the definition of valid sporadic jobs and tasks. *)
+ Let jobs_are_valid job_cost task_cost :=
+ forall (j: JobIn arr_seq),
+ valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
+ Let tasks_are_valid task_cost :=
+ valid_sporadic_taskset task_cost task_period task_deadline ts.
+
+ (* If the inflated task costs are no larger than the deadline nor period of each task, ... *)
+ Hypothesis H_inflated_cost_le_deadline_and_period:
+ forall tsk,
+ tsk \in ts >
+ inflated_task_cost tsk <= task_deadline tsk /\
+ inflated_task_cost tsk <= task_period tsk.
+
+ (* ...then we can prove that job parameters remain valid after the inflation. *)
+ Lemma suspension_oblivious_job_parameters_remain_valid:
+ jobs_are_valid original_job_cost original_task_cost >
+ jobs_are_valid inflated_job_cost inflated_task_cost.
+ Proof.
+ rename H_inflated_cost_le_deadline_and_period into LEdl,
+ H_dynamic_suspensions into DYN, H_jobs_from_taskset into FROMTS.
+ unfold jobs_are_valid, valid_sporadic_job, valid_realtime_job.
+ intros VALIDjob j; specialize (VALIDjob j); des.
+ split.
+ {
+ split;
+ first by apply leq_trans with (n := original_job_cost j);
+ last by apply leq_addr.
+ split; last by done.
+ rewrite /job_cost_le_deadline /inflated_job_cost.
+ feed (LEdl (job_task j)); [by done  move: LEdl => [LEdl _]].
+ apply leq_trans with (n := inflated_task_cost (job_task j));
+ last by rewrite VALIDjob1 LEdl.
+ by apply leq_add; last by apply DYN.
+ }
+ split; last by done.
+ by apply leq_add; last by apply DYN.
+ Qed.
+
+ (* The same applies for task parameters. *)
+ Lemma suspension_oblivious_task_parameters_remain_valid:
+ tasks_are_valid original_task_cost > tasks_are_valid inflated_task_cost.
+ Proof.
+ rename H_inflated_cost_le_deadline_and_period into LEdl.
+ unfold tasks_are_valid, valid_sporadic_taskset, is_valid_sporadic_task.
+ intros VALIDtask tsk IN; specialize (VALIDtask tsk IN); des.
+ split;
+ first by apply: (leq_trans VALIDtask); last by apply leq_addr.
+ specialize (LEdl tsk IN); move: LEdl => [LEdl LEp].
+ by repeat split.
+ Qed.
+
+ End NewParametersAreValid.
+
+ End CostInflation.
+
+ (* Now, we are going to generate a suspensionoblivious schedule with the inflated
+ job costs. For that, we always try to copy the original schedule, as long as that
+ doesn't break the priority enforcement in the generated schedule. *)
+
+ Section ScheduleConstruction.
+
+ (* In this section, we define the schedule construction function. *)
+ Section ConstructionStep.
+
+ (* For any time t, suppose that we have generated the schedule prefix in the
+ interval [0, t). Then, we must define what should be scheduled at time t. *)
+ Variable sched_prefix: schedule arr_seq.
+ Variable t: time.
+
+ (* First, consider the list of pending jobs at time t in the generated schedule, ... *)
+ Let job_is_pending := pending inflated_job_cost sched_prefix.
+ Definition pending_jobs :=
+ [seq j < jobs_arrived_up_to arr_seq t  job_is_pending j t].
+
+ (* ...which we sort by (decreasing) higherorequal priority. *)
+ Definition sorted_jobs := sort (higher_eq_priority t) pending_jobs.
+
+ (* From the sorted list, let's call j_hp one of the (possibly many) highestpriority jobs,
+ or None, in case there are no pending jobs. *)
+ Definition highest_priority_job := ohead sorted_jobs.
+
+ (* Then, we construct the schedule at time t as follows.
+ a) If there's a job scheduled in the original schedule at time t that is also a
+ highestpriority pending job in the generated schedule, copy this job.
+ b) Else, pick one of the highest priority pending jobs in the generated schedule. *)
+
+ Definition build_schedule : option (JobIn arr_seq) :=
+ (* If there is a highestpriority job j_hp in the generated schedule, ...*)
+ if highest_priority_job is Some j_hp then
+ (* ...and there is some job scheduled in the original schedule... *)
+ if (sched_susp t) is Some j_sched then
+ (* ...that is a highestpriority pending job,...*)
+ if job_is_pending j_sched t && higher_eq_priority t j_sched j_hp then
+ Some j_sched (* ...copy this scheduled job. *)
+ else
+ highest_priority_job (* In the remaining cases, just pick the *)
+ else highest_priority_job (* highestpriority job in the generated schedule. *)
+ else highest_priority_job.
+
+ End ConstructionStep.
+
+ (* Next, starting from the empty schedule, ...*)
+ Let empty_schedule : schedule arr_seq := fun t => None.
+
+ (* ...we use the recursive definition above to construct the suspensionoblivious schedule. *)
+ Definition sched_new := build_schedule_from_prefixes arr_seq build_schedule empty_schedule.
+
+ (* Then, by showing that the construction function depends only on the previous service, ... *)
+ Lemma sched_new_depends_only_on_service:
+ forall sched1 sched2 t,
+ (forall j, service sched1 j t = service sched2 j t) >
+ build_schedule sched1 t = build_schedule sched2 t.
+ Proof.
+ intros sched1 sched2 t ALL.
+ rewrite /build_schedule /highest_priority_job /sorted_jobs.
+ have SAME: pending_jobs sched1 t = pending_jobs sched2 t.
+ {
+ apply eq_in_filter.
+ intros j IN; apply JobIn_arrived in IN.
+ rewrite /arrived_before ltnS in IN.
+ rewrite /pending /has_arrived IN 2!andTb.
+ by rewrite /completed_by ALL.
+ }
+ have SAME': forall j,
+ pending inflated_job_cost sched1 j t = pending inflated_job_cost sched2 j t.
+ {
+ intros j; rewrite /pending.
+ case: (has_arrived j t); [rewrite 2!andTb  by done].
+ by rewrite /completed_by ALL.
+ }
+ rewrite SAME.
+ desf; try (by done).
+  by rewrite SAME' in Heq1.
+  by rewrite SAME' in Heq2.
+ Qed.
+
+ (* ...we infer that the generated schedule is indeed based on the construction function. *)
+ Corollary sched_new_uses_construction_function:
+ forall t,
+ sched_new t = build_schedule sched_new t.
+ Proof.
+ by ins; apply service_dependent_schedule_construction,
+ sched_new_depends_only_on_service.
+ Qed.
+
+ End ScheduleConstruction.
+
+ (* Next, we prove that the generated schedule is wellformed. *)
+ Section GeneratedScheduleIsValid.
+
+ (* First, we show that jobs do not execute before their arrival times... *)
+ Lemma sched_new_jobs_must_arrive_to_execute:
+ jobs_must_arrive_to_execute sched_new.
+ Proof.
+ move => j t /eqP SCHED.
+ rewrite sched_new_uses_construction_function in SCHED.
+ rewrite /build_schedule in SCHED.
+ destruct (highest_priority_job sched_new t) as [j_hp] eqn:HP; last by done.
+ have IN: has_arrived j_hp t.
+ {
+ suff IN: j_hp \in pending_jobs sched_new t.
+ by rewrite mem_filter in IN; move: IN => /andP [/andP [ARR _] _].
+ suff: j_hp \in sorted_jobs sched_new t by rewrite mem_sort.
+ rewrite /highest_priority_job in HP.
+ by destruct (sorted_jobs sched_new t);
+ last by move: HP; case => EQ; subst; rewrite in_cons eq_refl.
+ }
+ destruct (sched_susp t) eqn:SUSP; last by move: SCHED; case => EQ; subst.
+ move: SCHED; case: ifP; last by move => _; case => SAME; subst.
+ by move => /andP [/andP [ARR _] _]; case => SAME; subst.
+ Qed.
+
+ (* ...nor longer than their execution costs. *)
+ Lemma sched_new_completed_jobs_dont_execute:
+ completed_jobs_dont_execute inflated_job_cost sched_new.
+ Proof.
+ intros j t.
+ induction t;
+ first by rewrite /service /service_during big_geq //.
+ rewrite /service /service_during big_nat_recr //=.
+ rewrite leq_eqVlt in IHt; move: IHt => /orP [/eqP EQ  LT]; last first.
+ {
+ apply: leq_trans LT; rewrite addn1.
+ by apply leq_add; last by apply leq_b1.
+ }
+ rewrite [inflated_job_cost _]addn0; apply leq_add; first by rewrite EQ.
+ rewrite leqn0 eqb0 /scheduled_at.
+ rewrite sched_new_uses_construction_function.
+ rewrite /build_schedule.
+ destruct (highest_priority_job sched_new t) as [j_hp] eqn:HP; last by done.
+ rewrite /highest_priority_job in HP.
+ destruct (sched_susp t) eqn:SUSP.
+ {
+ case: ifP => [PEND  NOTPEND].
+ {
+ apply/eqP; case => SAME; subst.
+ move: PEND => /andP [PEND _].
+ by rewrite /pending /completed_by EQ eq_refl andbF in PEND.
+ }
+ {
+ apply/eqP; case => SAME; subst.
+ suff IN: j \in sorted_jobs sched_new t.
+ {
+ rewrite mem_sort mem_filter in IN; move: IN => /andP [/andP [_ NOTCOMP] _].
+ by rewrite /completed_by EQ eq_refl in NOTCOMP.
+ }
+ destruct (sorted_jobs sched_new t); first by done.
+ by case: HP => SAME; subst; rewrite in_cons; apply/orP; left.
+ }
+ }
+ {
+ apply/eqP; case => SAME; subst.
+ suff IN: j \in sorted_jobs sched_new t.
+ {
+ rewrite mem_sort mem_filter in IN; move: IN => /andP [/andP [_ NOTCOMP] _].
+ by rewrite /completed_by EQ eq_refl in NOTCOMP.
+ }
+ destruct (sorted_jobs sched_new t); first by done.
+ by case: HP => SAME; subst; rewrite in_cons; apply/orP; left.
+ }
+ Qed.
+
+ (* In addition, we prove that the schedule is (suspensionoblivious) workconserving... *)
+ Lemma sched_new_work_conserving:
+ susp_oblivious.work_conserving inflated_job_cost sched_new.
+ Proof.
+ intros j t BACK.
+ move: BACK => /andP [/andP [ARR NOTCOMP] NOTSCHED].
+ rewrite /scheduled_at sched_new_uses_construction_function /build_schedule in NOTSCHED.
+ rewrite /scheduled_at sched_new_uses_construction_function /build_schedule.
+ destruct (highest_priority_job sched_new t) as [j_hp] eqn:HP.
+ {
+ destruct (sched_susp t) eqn:SUSP; last by exists j_hp.
+ by case: ifP => [_  _]; [exists j0  exists j_hp].
+ }
+ {
+ rewrite /highest_priority_job in HP.
+ have IN: j \in sorted_jobs sched_new t.
+ by rewrite mem_sort mem_filter /pending ARR NOTCOMP 2!andTb; apply JobIn_arrived.
+ by destruct (sorted_jobs sched_new t).
+ }
+ Qed.
+
+ (* ...and respects job priorities. *)
+ Lemma sched_new_respects_policy:
+ susp_oblivious.respects_JLDP_policy inflated_job_cost
+ sched_new higher_eq_priority.
+ Proof.
+ rename H_priority_is_transitive into TRANS, H_priority_is_total into TOTAL,
+ H_priority_is_reflexive into REFL.
+ move => j1 j2 t BACK /eqP SCHED.
+ move: BACK => /andP [/andP [ARR NOTCOMP] NOTSCHED].
+ rewrite /scheduled_at sched_new_uses_construction_function /build_schedule in NOTSCHED.
+ rewrite /scheduled_at sched_new_uses_construction_function /build_schedule in SCHED.
+ destruct (highest_priority_job sched_new t) as [j_hp] eqn:HP; last by done.
+ have ALL: forall j, j \in sorted_jobs sched_new t > higher_eq_priority t j_hp j.
+ {
+ intros j IN.
+ have SORT: sorted (higher_eq_priority t) (sorted_jobs sched_new t) by apply sort_sorted.
+ rewrite /highest_priority_job in HP.
+ destruct (sorted_jobs sched_new t) as [j0 l]; first by done.
+ simpl in *; case: HP => SAME; subst.
+ rewrite in_cons in IN; move: IN => /orP [/eqP SAME  IN]; subst; first by apply REFL.
+ apply order_path_min in SORT; last by done.
+ by move: SORT => /allP ALL; apply ALL.
+ }
+ have IN: j1 \in sorted_jobs sched_new t.
+ by rewrite mem_sort mem_filter /pending ARR NOTCOMP 2!andTb; apply JobIn_arrived.
+ rewrite /highest_priority_job in HP.
+ destruct (sched_susp t) eqn:SUSP;
+ last by case: SCHED => SAME; subst; apply ALL; last by done.
+ destruct (pending inflated_job_cost sched_new j t
+ && higher_eq_priority t j j_hp) eqn:PEND;
+ last by case: SCHED => SAME; subst; apply ALL.
+ move: PEND => /andP [PEND HPj]; case: SCHED => SAME; subst.
+ by apply: (TRANS _ j_hp); last by apply ALL.
+ Qed.
+
+ (* In addition, due to the copy step in the schedule construction, we show that in case
+ there are multiple highestpriority jobs, we pick the same job as in the original
+ schedule. *)
+ Lemma sched_new_breaks_ties:
+ forall j1 j2 t,
+ higher_eq_priority t j1 j2 >
+ higher_eq_priority t j2 j1 >
+ scheduled_at sched_susp j1 t >
+ pending inflated_job_cost sched_new j1 t >
+ scheduled_at sched_new j2 t >
+ j1 = j2.
+ Proof.
+ move => j1 j2 t HP1 HP2 /eqP SCHEDs PEND /eqP SCHEDn.
+ rewrite sched_new_uses_construction_function /build_schedule in SCHEDn.
+ destruct (highest_priority_job sched_new t) as [j_hp] eqn:HP; last by done.
+ destruct (sched_susp t) eqn:SUSP; last by done.
+ case: SCHEDs => SAME; subst.
+ rewrite PEND andTb in SCHEDn.
+ move: SCHEDn; case: ifP => HP'; case => SAME; subst; first by done.
+ by rewrite HP1 in HP'.
+ Qed.
+
+ (* To reason about schedulability, we now prove that the generated schedule
+ preserves the service received by each job. *)
+ Section Service.
+
+ (* Recall the definitions of suspended job, cumulative service and
+ cumulative suspension time in the suspensionaware schedule. *)
+ Let job_suspended_at (sched: schedule arr_seq) :=
+ suspended_at original_job_cost next_suspension sched.
+ Let job_cumulative_suspension :=
+ cumulative_suspension original_job_cost next_suspension sched_susp.
+ Let job_service_with_suspensions := service sched_susp.
+
+ (* Also recall the definition of cumulative service in the generated schedule. *)
+ Let job_service_without_suspensions := service sched_new.
+
+ (* We are going to prove that for any job j, at any time t, the service received by j
+ in the generated schedule (without suspensions) is no larger than the sum of the
+ cumulative service plus suspension time in the original schedule (with suspensions).
+ The proof follows by induction on time. Since the base case is trivial, we focus
+ on the inductive step. *)
+ Section InductiveStep.
+
+ (* Assume that the claim we want to prove holds for the interval [0, t). *)
+ Variable t: time.
+ Hypothesis H_induction_hypothesis:
+ forall (j: JobIn arr_seq),
+ job_service_without_suspensions j t <=
+ job_service_with_suspensions j t + job_cumulative_suspension j t.
+
+ (* Now, let j be any job in arrival sequence. We are going to prove that the claim
+ continues to hold for job j in the interval [0, t + 1). *)
+ Variable j: JobIn arr_seq.
+
+ (* If j has not arrived by time t, then the proof is trivial, ... *)
+ Lemma reduction_inductive_step_not_arrived:
+ ~~ has_arrived j t >
+ job_service_without_suspensions j t.+1 <=
+ job_service_with_suspensions j t.+1 + job_cumulative_suspension j t.+1.
+ Proof.
+ rewrite ltnNge; intro NOTARR.
+ rewrite /job_service_without_suspensions /job_service_with_suspensions
+ /service /service_during.
+ rewrite cumulative_service_before_job_arrival_zero //.
+ by apply sched_new_jobs_must_arrive_to_execute.
+ Qed.
+
+ (* ...so let's assume instead that j has arrived by time t. *)
+ Hypothesis H_j_has_arrived: has_arrived j t.
+
+ (* We begin by performing a case analysis on whether j has completed in the
+ suspensionaware schedule. *)
+ Section CompletedInSuspensionAwareSchedule.
+
+ (* Case 1) If j has completed by time t in the suspensionaware schedule, ... *)
+ Hypothesis H_j_has_completed:
+ completed_by original_job_cost sched_susp j t.
+
+ (* ...then it follows from the induction hypothesis that the service
+ received by j is preserved up in the interval [0, t + 1). *)
+ Lemma reduction_inductive_step_case1_completed:
+ job_service_without_suspensions j t.+1 <=
+ job_service_with_suspensions j t.+1 + job_cumulative_suspension j t.+1.
+ Proof.
+ rename H_j_has_completed into COMP, H_induction_hypothesis into IH.
+ apply leq_trans with (n := original_job_cost j +
+ total_suspension original_job_cost next_suspension j).
+ {
+ by apply leq_trans with (n := inflated_job_cost j);
+ first by apply cumulative_service_le_job_cost,
+ sched_new_completed_jobs_dont_execute.
+ }
+ have SERVs: job_service_with_suspensions j t.+1 = original_job_cost j.
+ {
+ by apply/eqP; apply completion_monotonic with (t0 := t).
+ } rewrite SERVs; clear SERVs.
+ rewrite leq_add2l.
+ apply completion_monotonic with (t' := t.+1) in COMP; try (by done).
+ rewrite /job_cumulative_suspension.
+ by rewrite > cumulative_suspension_eq_total_suspension with
+ (job_cost := original_job_cost).
+ Qed.
+
+ End CompletedInSuspensionAwareSchedule.
+
+ (* Next, consider the complementary case. *)
+ Section PendingInSuspensionAwareSchedule.
+
+ (* Case 2) Since job j has arrived by time t, let's assume that j has not completed
+ by time t in the suspensionaware schedule, i.e., j is still pending. *)
+ Hypothesis H_j_is_pending:
+ ~~ completed_by original_job_cost sched_susp j t.
+
+ (* Since we know from the induction hypothesis that the service received by j is
+ preserved in the interval [0, t), now we only have to consider the state of job j
+ at time t in both schedules. That is, we need to prove the following property:
+
+ scheduled_at sched_new j t <=
+ job_suspended_at sched_susp j t + scheduled_at sched_susp j t. *)
+
+ (* If j is not scheduled in the suspensionoblivious schedule, then the claim follows. *)
+ Lemma reduction_inductive_step_not_scheduled_in_new:
+ ~~ scheduled_at sched_new j t >
+ scheduled_at sched_new j t <=
+ job_suspended_at sched_susp j t + scheduled_at sched_susp j t.
+ Proof.
+ by case: scheduled_at.
+ Qed.
+
+ (* Likewise, if j is scheduled in the suspensionaware schedule, then the claim is also
+ trivial. *)
+ Lemma reduction_inductive_step_scheduled_in_susp:
+ scheduled_at sched_susp j t >
+ scheduled_at sched_new j t <=
+ job_suspended_at sched_susp j t + scheduled_at sched_susp j t.
+ Proof.
+ by move >; case: scheduled_at; [by apply leq_addl  by rewrite addn1].
+ Qed.
+
+ (* Having proved the simple cases, let's now move to the harder case. *)
+ Section NotScheduledInSuspensionAware.
+
+ (* Assume that j is scheduled in the suspensionoblivious schedule, but
+ not in the suspensionaware schedule. *)
+ Hypothesis H_j_scheduled_in_new: scheduled_at sched_new j t.
+ Hypothesis H_j_not_scheduled_in_susp: ~~ scheduled_at sched_susp j t.
+
+ (* It remains to show that j is suspended at time t in the suspensionaware schedule.
+ We are going to prove that by contradiction. *)
+ Section ProofByContradiction.
+
+ (* Assume that j it not suspended at time t in the suspensionaware schedule, ... *)
+ Hypothesis H_j_is_not_suspended: ~~ job_suspended_at sched_susp j t.
+
+ (* ...which implies that j is backlogged at time t in the suspensionaware schedule. *)
+ Lemma reduction_inductive_step_j_is_backlogged:
+ susp.backlogged original_job_cost next_suspension sched_susp j t.
+ Proof.
+ by repeat (apply/andP; split).
+ Qed.
+
+ (* By work conservation, there must be a scheduled job with higher or equal
+ priority in the suspensionaware schedule. *)
+ Lemma reduction_inductive_step_exists_hep_job:
+ exists j_hp, scheduled_at sched_susp j_hp t /\ higher_eq_priority t j_hp j.
+ Proof.
+ rename H_work_conserving into WORKs, H_respects_priority into PRIOs.
+ have BACKs := reduction_inductive_step_j_is_backlogged.
+ move: (BACKs) => BACKs'; apply WORKs in BACKs.
+ by move: BACKs => [j_hp SCHEDhp]; exists j_hp; split; last by apply PRIOs.
+ Qed.
+
+ (* Let j_hp be this job with higherorequal priority. *)
+ Variable j_hp: JobIn arr_seq.
+ Hypothesis H_j_hp_is_scheduled: scheduled_at sched_susp j_hp t.
+ Hypothesis H_higher_or_equal_priority: higher_eq_priority t j_hp j.
+
+ (* First, note that j and j_hp cannot be the same job, since j is not scheduled
+ in the suspensionaware schedule at time t. Moreover, since the generated
+ schedule breaks ties when there are multiple highestpriority jobs (by copying
+ the original schedule), it follows that the higherpriority job j_hp must have
+ completed earlier in the suspensionoblivious schedule. *)
+ Lemma reduction_inductive_step_j_hp_completed_in_new:
+ completed_by inflated_job_cost sched_new j_hp t.
+ Proof.
+ rename H_j_not_scheduled_in_susp into NOTSCHEDs, H_j_scheduled_in_new into SCHEDn.
+ move: H_j_hp_is_scheduled (H_j_hp_is_scheduled) => SCHEDhp PENDhp.
+ apply scheduled_implies_pending with (job_cost := original_job_cost) in PENDhp;
+ try (by done).
+ move: PENDhp => /andP [ARRhp _].
+ apply contraT; intro NOTCOMPhp.
+ have PENDhp: pending inflated_job_cost sched_new j_hp t by apply/andP; split.
+ destruct (boolP (scheduled_at sched_new j_hp t)) as [SCHEDhp'  NOTSCHEDhp'].
+ {
+ have SAME: j = j_hp by apply only_one_job_scheduled with (j1 := j) in SCHEDhp'.
+ by subst; rewrite SCHEDhp in NOTSCHEDs.
+ }
+ have BACKhp: backlogged inflated_job_cost sched_new j_hp t by apply/andP.
+ have HP': higher_eq_priority t j j_hp by apply sched_new_respects_policy.
+ apply sched_new_breaks_ties in HP'; try (by done).
+ by subst; rewrite SCHEDn in NOTSCHEDhp'.
+ Qed.
+
+ (* However, recall from the induction hypothesis how the service in the two schedules
+ are related. From that, we can conclude that j_hp must have completed in the
+ suspensionaware schedule as well, ... *)
+ Lemma reduction_inductive_step_j_hp_completed_in_susp:
+ completed_by original_job_cost sched_susp j_hp t.
+ Proof.
+ have COMPNEW := reduction_inductive_step_j_hp_completed_in_new.
+ rename H_induction_hypothesis into IHt.
+ rewrite /completed_by eqn_leq; apply/andP; split;
+ first by apply cumulative_service_le_job_cost.
+ rewrite (leq_add2r (total_suspension original_job_cost next_suspension j_hp)).
+ rewrite /(inflated_job_cost _).
+ apply leq_trans with (n := job_service_without_suspensions j_hp t);
+ first by apply eq_leq; symmetry; apply/eqP; apply COMPNEW.
+ apply: (leq_trans (IHt j_hp)).
+ by rewrite leq_add2l; apply cumulative_suspension_le_total_suspension.
+ Qed.
+
+ (* ...which of course is a contradiction, since we assumed that j_hp was scheduled
+ in the the suspensionaware schedule at time t. *)
+ Lemma reduction_inductive_step_contradiction: False.
+ Proof.
+ have COMPhp' := reduction_inductive_step_j_hp_completed_in_susp.
+ rename H_j_hp_is_scheduled into SCHEDhp.
+ apply completed_implies_not_scheduled in COMPhp'; try (by done).
+ by rewrite SCHEDhp in COMPhp'.
+ Qed.
+
+ End ProofByContradiction.
+
+ End NotScheduledInSuspensionAware.
+
+ (* From the lemmas above, we infer that the claim to be proven holds if job j
+ is pending in the suspensionaware schedule. *)
+ Lemma reduction_inductive_step_case2_pending:
+ job_service_without_suspensions j t.+1 <=
+ job_service_with_suspensions j t.+1 + job_cumulative_suspension j t.+1.
+ Proof.
+ have CONTRA := reduction_inductive_step_contradiction.
+ have HP := reduction_inductive_step_exists_hep_job.
+ rename H_induction_hypothesis into IHt.
+ rewrite /job_service_without_suspensions /job_service_with_suspensions
+ /job_cumulative_suspension /cumulative_suspension
+ /cumulative_suspension_during /service /service_during /service_at.
+ rewrite !big_nat_recr //=.
+ rewrite addnA [scheduled_at sched_susp _ _ + _]addnC !addnA addnA.
+ apply leq_add; first by apply IHt.
+ destruct (boolP (scheduled_at sched_new j t)) as [SCHEDn ]; last by done.
+ destruct (boolP (scheduled_at sched_susp j t)) as [SCHEDs  NOTSCHEDs];
+ [by apply leq_addl  rewrite addn0].
+ apply eq_leq; symmetry; apply/eqP; rewrite eqb1.
+ apply contraT; intro NOTSUSP.
+ specialize (HP NOTSCHEDs NOTSUSP); specialize (CONTRA SCHEDn NOTSCHEDs NOTSUSP).
+ move: HP => [j_hp [SCHEDhp HP]].
+ by exfalso; apply CONTRA with (j_hp := j_hp).
+ Qed.
+
+ End PendingInSuspensionAwareSchedule.
+
+ End InductiveStep.
+
+ (* Using the proof by induction, we show that the service received by any
+ job j at any time t is preserved in the suspensionaware schedule. *)
+ Theorem suspension_oblivious_preserves_service:
+ forall j t,
+ job_service_without_suspensions j t <= job_service_with_suspensions j t
+ + job_cumulative_suspension j t.
+ Proof.
+ have CASE1 := reduction_inductive_step_case1_completed.
+ have CASE2 := reduction_inductive_step_case2_pending.
+ move => j t; move: t j.
+ induction t;
+ first by ins; rewrite /job_service_without_suspensions/service/service_during big_geq.
+ intros j.
+ destruct (boolP (has_arrived j t)) as [ARR  NOTARR];
+ last by apply reduction_inductive_step_not_arrived.
+ destruct (boolP (completed_by original_job_cost sched_susp j t)) as [COMP  NOTCOMP];
+ first by apply CASE1.
+ by apply CASE2.
+ Qed.
+
+ (* As a corollary, we show that if a job has completed in the suspensionoblivious
+ schedule, it must have completed in the suspensionaware schedule as well. *)
+ Corollary suspension_oblivious_preserves_completion:
+ forall j t,
+ completed_by inflated_job_cost sched_new j t >
+ completed_by original_job_cost sched_susp j t.
+ Proof.
+ have COMP := sched_new_completed_jobs_dont_execute.
+ have SERV := suspension_oblivious_preserves_service.
+ intros j t COMPLETED.
+ rewrite /completed_by eqn_leq; apply/andP; split;
+ first by apply cumulative_service_le_job_cost.
+ rewrite (leq_add2r (total_suspension original_job_cost next_suspension j)).
+ rewrite /(inflated_job_cost j).
+ move: COMPLETED => /eqP EQ; rewrite EQ.
+ apply: (leq_trans (SERV _ _)); rewrite leq_add2l.
+ by apply cumulative_suspension_le_total_suspension.
+ Qed.
+
+ End Service.
+
+ End GeneratedScheduleIsValid.
+
+
+ (* To conclude, based on the definition of schedulability, ...*)
+ Let schedulable_without_suspensions :=
+ job_misses_no_deadline inflated_job_cost job_deadline sched_new.
+ Let schedulable_with_suspensions :=
+ job_misses_no_deadline original_job_cost job_deadline sched_susp.
+
+ (* ...we prove that if no job misses a deadline in the suspensionoblivious schedule, ... *)
+ Hypothesis H_schedulable_without_suspensions:
+ forall j, schedulable_without_suspensions j.
+
+ (* ...then no job misses a deadline in the suspensionaware schedule. *)
+ Corollary suspension_oblivious_preserves_schedulability:
+ forall j, schedulable_with_suspensions j.
+ Proof.
+ rename H_schedulable_without_suspensions into SCHED.
+ by intros j; apply suspension_oblivious_preserves_completion, SCHED.
+ Qed.
+
+ End Reduction.
+
+End ReductionToBasicSchedule.
\ No newline at end of file
diff git a/implementation/apa/bertogna_edf_example.v b/implementation/apa/bertogna_edf_example.v
index 98defcb390cef535c77ab30a6c7aeaf1a75c2b49..8894ba101488b51f291b7334209b06775d8a0faf 100644
 a/implementation/apa/bertogna_edf_example.v
+++ b/implementation/apa/bertogna_edf_example.v
@@ 133,7 +133,8 @@ Module ResponseTimeAnalysisEDF.
Let arr_seq := periodic_arrival_sequence ts.
(* Let sched be the weak APA EDF scheduler. *)
 Let sched := scheduler job_cost job_task num_cpus arr_seq task_affinity (EDF job_deadline).
+ Let sched := scheduler job_cost job_task num_cpus arr_seq task_affinity
+ (JLFP_to_JLDP arr_seq (EDF job_deadline)).
(* Recall the definition of deadline miss. *)
Let no_deadline_missed_by :=
@@ 166,12 +167,12 @@ Module ResponseTimeAnalysisEDF.
 by apply scheduler_respects_affinity.
 apply scheduler_apa_work_conserving; try (by done).
 by apply periodic_arrivals_is_a_set.
  by apply EDF_is_transitive.
  by apply EDF_is_total.
  apply scheduler_enforces_policy.
+  by intro t; apply EDF_is_transitive.
+  by intro t; apply EDF_is_total.
+  apply scheduler_respects_policy.
 by apply periodic_arrivals_is_a_set.
  by apply EDF_is_transitive.
  by apply EDF_is_total.
+  by intro t; apply EDF_is_transitive.
+  by intro t; apply EDF_is_total.
 by apply schedulability_test_succeeds.
 by apply IN.
Qed.
diff git a/implementation/apa/bertogna_fp_example.v b/implementation/apa/bertogna_fp_example.v
index 4896677a6a63afc5cd35ab0d4d3dce1c79250f5a..5968f7c2d77821f03b79baa09e20e004934ea2c6 100644
 a/implementation/apa/bertogna_fp_example.v
+++ b/implementation/apa/bertogna_fp_example.v
@@ 89,7 +89,7 @@ Module ResponseTimeAnalysisFP.
(* Assume ratemonotonic priorities. *)
Let higher_priority : JLDP_policy arr_seq :=
 (FP_to_JLDP job_task (RM task_period)).
+ (FP_to_JLDP job_task arr_seq (RM task_period)).
Section FactsAboutPriorityOrder.
@@ 257,7 +257,7 @@ Module ResponseTimeAnalysisFP.
unfold FP_to_JLDP; intros t x y; apply/orP.
by apply priority_is_total; rewrite periodic_arrivals_all_jobs_from_taskset.
}
  apply scheduler_enforces_policy.
+  apply scheduler_respects_policy.
 by apply periodic_arrivals_is_a_set.
 by ins; apply RM_is_transitive.
{
diff git a/implementation/apa/schedule.v b/implementation/apa/schedule.v
index 7ae8f5a5c1e5c4661135ca756fff76de7c933b8d..0a498fe2d3650c47a7ff2e9e621ac6fa63b92a1a 100644
 a/implementation/apa/schedule.v
+++ b/implementation/apa/schedule.v
@@ 492,7 +492,7 @@ Module ConcreteScheduler.
}
Qed.
 (* Next, we prove that the mapping enforces priority. *)
+ (* Next, we prove that the mapping respects priority. *)
Lemma scheduler_priority :
forall j j_hp cpu t,
backlogged job_cost sched j t >
@@ 733,11 +733,11 @@ Module ConcreteScheduler.
by rewrite scheduler_scheduled_on.
Qed.
 (* ... and enforces the JLDP policy under weak APA scheduling. *)
 Theorem scheduler_enforces_policy :
 enforces_JLDP_policy_under_weak_APA job_cost job_task sched alpha higher_eq_priority.
+ (* ... and respects the JLDP policy under weak APA scheduling. *)
+ Theorem scheduler_respects_policy :
+ respects_JLDP_policy_under_weak_APA job_cost job_task sched alpha higher_eq_priority.
Proof.
 unfold enforces_JLDP_policy_under_weak_APA.
+ unfold respects_JLDP_policy_under_weak_APA.
intros j j_hp cpu t BACK SCHED ALPHA.
rewrite scheduler_scheduled_on in SCHED.
apply scheduler_priority with (cpu := cpu); try by done.
diff git a/implementation/global/basic/bertogna_edf_example.v b/implementation/global/basic/bertogna_edf_example.v
index 59dfd508c6dcc34c9746b9519aaacaffe2b138c6..3f7e31eaf006c77e160c69c11a06ed9ad83c4e6e 100644
 a/implementation/global/basic/bertogna_edf_example.v
+++ b/implementation/global/basic/bertogna_edf_example.v
@@ 89,7 +89,8 @@ Module ResponseTimeAnalysisEDF.
Let arr_seq := periodic_arrival_sequence ts.
(* Let sched be the workconserving EDF scheduler. *)
 Let sched := scheduler job_cost num_cpus arr_seq (EDF job_deadline).
+ Let sched := scheduler job_cost num_cpus arr_seq
+ (JLFP_to_JLDP arr_seq (EDF job_deadline)).
(* Recall the definition of deadline miss. *)
Let no_deadline_missed_by :=
@@ 118,9 +119,9 @@ Module ResponseTimeAnalysisEDF.
 by apply periodic_arrivals_is_a_set.
 by apply scheduler_sequential_jobs, periodic_arrivals_is_a_set.
 by apply scheduler_work_conserving.
  apply scheduler_enforces_policy.
  by apply EDF_is_transitive.
  by apply EDF_is_total.
+  apply scheduler_respects_policy.
+  by intro t; apply EDF_is_transitive.
+  by intro t; apply EDF_is_total.
 by apply schedulability_test_succeeds.
 by apply IN.
Qed.
diff git a/implementation/global/basic/bertogna_fp_example.v b/implementation/global/basic/bertogna_fp_example.v
index c4efb676a85d1b05b8db933335a56f22a41d3e49..3ee7d7911871640b6a08dc2c8049238eabc605e2 100644
 a/implementation/global/basic/bertogna_fp_example.v
+++ b/implementation/global/basic/bertogna_fp_example.v
@@ 104,7 +104,7 @@ Module ResponseTimeAnalysisFP.
(* Assume ratemonotonic priorities. *)
Let higher_priority : JLDP_policy arr_seq :=
 (FP_to_JLDP job_task (RM task_period)).
+ (FP_to_JLDP job_task arr_seq (RM task_period)).
Section FactsAboutPriorityOrder.
@@ 160,7 +160,7 @@ Module ResponseTimeAnalysisFP.
 by apply periodic_arrivals_is_a_set.
 by apply scheduler_sequential_jobs, periodic_arrivals_is_a_set.
 by apply scheduler_work_conserving.
  apply scheduler_enforces_policy.
+  apply scheduler_respects_policy.
 by intros t; apply RM_is_transitive.
{
unfold FP_to_JLDP; intros t x y; apply/orP.
diff git a/implementation/global/basic/schedule.v b/implementation/global/basic/schedule.v
index 42e1c00e3f3247050a8d4c369cd35766c12b0832..3bdb47448fe9bfb85df69adcfbd6bec68b789492 100644
 a/implementation/global/basic/schedule.v
+++ b/implementation/global/basic/schedule.v
@@ 322,11 +322,11 @@ Module ConcreteScheduler.
by apply nth_or_none_size_some in NTH; apply ltnW.
Qed.
 (* ... and enforces the JLDP policy. *)
 Theorem scheduler_enforces_policy :
 enforces_JLDP_policy job_cost sched higher_eq_priority.
+ (* ... and respects the JLDP policy. *)
+ Theorem scheduler_respects_policy :
+ respects_JLDP_policy job_cost sched higher_eq_priority.
Proof.
 unfold enforces_JLDP_policy; intros j j_hp t BACK SCHED.
+ unfold respects_JLDP_policy; intros j j_hp t BACK SCHED.
set jobs := sorted_pending_jobs job_cost num_cpus arr_seq higher_eq_priority sched t.
apply scheduler_nth_or_none_backlogged in BACK.
destruct BACK as [cpu_out [SOME GE]].
diff git a/implementation/global/jitter/bertogna_edf_example.v b/implementation/global/jitter/bertogna_edf_example.v
index 384b64c0b8e9e1ae84042641f0d83f5de8bf4bd9..e58e64a219aedc983f5eb29741c57b227dcb9660 100644
 a/implementation/global/jitter/bertogna_edf_example.v
+++ b/implementation/global/jitter/bertogna_edf_example.v
@@ 92,7 +92,8 @@ Module ResponseTimeAnalysisEDF.
Let arr_seq := periodic_arrival_sequence ts.
(* Let sched be the workconserving EDF scheduler. *)
 Let sched := scheduler job_cost job_jitter num_cpus arr_seq (EDF job_deadline).
+ Let sched := scheduler job_cost job_jitter num_cpus arr_seq
+ (JLFP_to_JLDP arr_seq (EDF job_deadline)).
(* Recall the definition of deadline miss. *)
Let no_deadline_missed_by :=
@@ 122,9 +123,9 @@ Module ResponseTimeAnalysisEDF.
 by apply periodic_arrivals_is_a_set.
 by apply scheduler_sequential_jobs, periodic_arrivals_is_a_set.
 by apply scheduler_work_conserving.
  apply scheduler_enforces_policy.
  by apply EDF_is_transitive.
  by apply EDF_is_total.
+  apply scheduler_respects_policy.
+  by intros t; apply EDF_is_transitive.
+  by intros t; apply EDF_is_total.
 by apply schedulability_test_succeeds.
 by apply IN.
Qed.
diff git a/implementation/global/jitter/bertogna_fp_example.v b/implementation/global/jitter/bertogna_fp_example.v
index 023dc7bd9f7ffd82a2f0c9003a55192f68614b73..1dcf113a982f2711bb2c393928823e84386feba1 100644
 a/implementation/global/jitter/bertogna_fp_example.v
+++ b/implementation/global/jitter/bertogna_fp_example.v
@@ 107,7 +107,7 @@ Module ResponseTimeAnalysisFP.
(* Assume ratemonotonic priorities. *)
Let higher_priority : JLDP_policy arr_seq :=
 (FP_to_JLDP job_task (RM task_period)).
+ (FP_to_JLDP job_task arr_seq (RM task_period)).
Section FactsAboutPriorityOrder.
@@ 164,7 +164,7 @@ Module ResponseTimeAnalysisFP.
 by apply periodic_arrivals_is_a_set.
 by apply scheduler_sequential_jobs, periodic_arrivals_is_a_set.
 by apply scheduler_work_conserving.
  apply scheduler_enforces_policy.
+  apply scheduler_respects_policy.
 by intros t; apply RM_is_transitive.
{
unfold FP_to_JLDP; intros t x y; apply/orP.
diff git a/implementation/global/jitter/schedule.v b/implementation/global/jitter/schedule.v
index 692ac58666526ca9f28decfd5f3ad19fbcc940d3..4ff3541e0b310872268942f56fea96134e347738 100644
 a/implementation/global/jitter/schedule.v
+++ b/implementation/global/jitter/schedule.v
@@ 324,11 +324,11 @@ Module ConcreteScheduler.
by apply nth_or_none_size_some in NTH; apply ltnW.
Qed.
 (* ... and enforces the JLDP policy. *)
 Theorem scheduler_enforces_policy :
 enforces_JLDP_policy job_cost job_jitter sched higher_eq_priority.
+ (* ... and respects the JLDP policy. *)
+ Theorem scheduler_respects_policy :
+ respects_JLDP_policy job_cost job_jitter sched higher_eq_priority.
Proof.
 unfold enforces_JLDP_policy; intros j j_hp t BACK SCHED.
+ unfold respects_JLDP_policy; intros j j_hp t BACK SCHED.
set jobs := sorted_pending_jobs job_cost job_jitter num_cpus arr_seq higher_eq_priority sched t.
apply scheduler_nth_or_none_backlogged in BACK.
destruct BACK as [cpu_out [SOME GE]].
diff git a/implementation/global/parallel/bertogna_edf_example.v b/implementation/global/parallel/bertogna_edf_example.v
index 4ef7a4c07cad040641d4a76ef5dd04b548adc300..9ecd24764c184d3fa7855d5a047376505f6ecf69 100644
 a/implementation/global/parallel/bertogna_edf_example.v
+++ b/implementation/global/parallel/bertogna_edf_example.v
@@ 96,7 +96,8 @@ Module ResponseTimeAnalysisEDF.
Let arr_seq := periodic_arrival_sequence ts.
(* Let sched be the workconserving EDF scheduler. *)
 Let sched := scheduler job_cost num_cpus arr_seq (EDF job_deadline).
+ Let sched := scheduler job_cost num_cpus arr_seq
+ (JLFP_to_JLDP arr_seq (EDF job_deadline)).
(* Recall the definition of deadline miss. *)
Let no_deadline_missed_by :=
@@ 112,7 +113,8 @@ Module ResponseTimeAnalysisEDF.
have VALID := periodic_arrivals_valid_job_parameters ts ts_has_valid_parameters.
have TSVALID := ts_has_valid_parameters.
unfold valid_sporadic_job, valid_realtime_job in *; des.
 apply taskset_schedulable_by_edf_rta with (task_cost := task_cost) (task_period := task_period) (task_deadline := task_deadline) (ts0 := ts).
+ apply taskset_schedulable_by_edf_rta with (task_cost := task_cost)
+ (task_period := task_period) (task_deadline := task_deadline) (ts0 := ts).
 by apply ts_has_valid_parameters.
 by apply ts_has_constrained_deadlines.
 by apply periodic_arrivals_all_jobs_from_taskset.
@@ 124,9 +126,9 @@ Module ResponseTimeAnalysisEDF.
 by specialize (VALID j'); des.
 by apply periodic_arrivals_is_a_set.
 by apply scheduler_work_conserving.
  apply scheduler_enforces_policy.
  by apply EDF_is_transitive.
  by apply EDF_is_total.
+  apply scheduler_respects_policy.
+  by intro t; apply EDF_is_transitive.
+  by intro t; apply EDF_is_total.
 by apply schedulability_test_succeeds.
 by apply IN.
Qed.
diff git a/implementation/global/parallel/bertogna_fp_example.v b/implementation/global/parallel/bertogna_fp_example.v
index 4681aa4e8acab76366e167028437164f30c671a7..519e19e0728ecd1f39efa5de04cd2041ec540b3c 100644
 a/implementation/global/parallel/bertogna_fp_example.v
+++ b/implementation/global/parallel/bertogna_fp_example.v
@@ 126,7 +126,7 @@ Module ResponseTimeAnalysisFP.
(* Assume ratemonotonic priorities. *)
Let higher_priority : JLDP_policy arr_seq :=
 (FP_to_JLDP job_task (RM task_period)).
+ (FP_to_JLDP job_task arr_seq (RM task_period)).
Section FactsAboutPriorityOrder.
@@ 181,7 +181,7 @@ Module ResponseTimeAnalysisFP.
 by specialize (VALID j'); des.
 by apply periodic_arrivals_is_a_set.
 by apply scheduler_work_conserving.
  apply scheduler_enforces_policy.
+  apply scheduler_respects_policy.
 by intros t; apply RM_is_transitive.
{
unfold FP_to_JLDP; intros t x y; apply/orP.
diff git a/implementation/uni/basic/fp_rta_example.v b/implementation/uni/basic/fp_rta_example.v
index ec7917992f0adebcd3b934de0fe80060b0115fb7..4d6b43d7bfe042e2aa1c2cf5ecbaad7ad5c49af7 100644
 a/implementation/uni/basic/fp_rta_example.v
+++ b/implementation/uni/basic/fp_rta_example.v
@@ 1,7 +1,6 @@
Require Import rt.util.all.
Require Import rt.model.job rt.model.task rt.model.priority.
Require Import rt.model.uni.schedule rt.model.uni.schedulability.
Require Import rt.model.global.basic.platform.
Require Import rt.analysis.uni.basic.workload_bound_fp
rt.analysis.uni.basic.fp_rta_comp.
Require Import rt.implementation.job rt.implementation.task
@@ 12,7 +11,7 @@ From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
Module ResponseTimeAnalysisFP.
Import Job UniprocessorSchedule SporadicTaskset Priority Schedulability
 Platform WorkloadBoundFP ResponseTimeIterationFP.
+ WorkloadBoundFP ResponseTimeIterationFP.
Import ConcreteJob ConcreteTask ConcreteArrivalSequence ConcreteScheduler.
(* In this section, we run the FP RTA on a simple task set to show that the theorems
@@ 107,15 +106,15 @@ Module ResponseTimeAnalysisFP.
Let arr_seq := periodic_arrival_sequence ts.
(* Assume ratemonotonic priorities... *)
 Let higher_eq_priority : JLDP_policy arr_seq := (FP_to_JLDP job_task (RM task_period)).
+ Let higher_eq_priority : JLDP_policy arr_seq := (FP_to_JLDP job_task arr_seq (RM task_period)).
(* ... and recall that this priority assignment is total. *)
Fact priority_is_total:
forall t, total (higher_eq_priority t).
Proof.
 rewrite /higher_eq_priority /FP_to_JLDP /RM.
+ rewrite /higher_eq_priority /FP_to_JLDP /RM /FP_to_JLFP.
intros t x y; apply/orP.
 elim LEQ: (_ <= _); first by left.
+ case LEQ: (_ <= _); first by left.
apply negbT in LEQ; rewrite ltnNge in LEQ.
by right; apply ltnW.
Qed.
@@ 148,7 +147,7 @@ Module ResponseTimeAnalysisFP.
 by apply scheduler_jobs_must_arrive_to_execute.
 by apply scheduler_completed_jobs_dont_execute; intro j'; specialize (VALID j'); des.
 by apply scheduler_work_conserving.
  apply scheduler_enforces_policy.
+  apply scheduler_respects_policy.
 by intros t; apply RM_is_transitive.
 by apply priority_is_total.
 by apply schedulability_test_succeeds.
diff git a/implementation/uni/basic/schedule.v b/implementation/uni/basic/schedule.v
index bebaa1982c5721cda9b6a7f4c621e30c9b8625ea..b62d93354430e2840ffc9c117e2e78a0270ee5d8 100644
 a/implementation/uni/basic/schedule.v
+++ b/implementation/uni/basic/schedule.v
@@ 245,11 +245,11 @@ Module ConcreteScheduler.
by apply JobIn_arrived; move: PEND => /andP [ARR _].
Qed.
 (* ... and enforces the JLDP policy. *)
 Theorem scheduler_enforces_policy :
 enforces_JLDP_policy job_cost sched higher_eq_priority.
+ (* ... and respects the JLDP policy. *)
+ Theorem scheduler_respects_policy :
+ respects_JLDP_policy job_cost sched higher_eq_priority.
Proof.
 unfold enforces_JLDP_policy; move => j j_hp t BACK /eqP SCHED.
+ unfold respects_JLDP_policy; move => j j_hp t BACK /eqP SCHED.
move: (SCHED) => OHEAD.
rewrite scheduler_picks_first_job in OHEAD.
set jobs := sorted_pending_jobs job_cost arr_seq higher_eq_priority sched t in OHEAD.
diff git a/implementation/uni/susp/dynamic/arrival_sequence.v b/implementation/uni/susp/dynamic/arrival_sequence.v
new file mode 100644
index 0000000000000000000000000000000000000000..455520090718fe4fc47a72c82a4871b0d1e1a81c
 /dev/null
+++ b/implementation/uni/susp/dynamic/arrival_sequence.v
@@ 0,0 +1,110 @@
+Require Import rt.util.all.
+Require Import rt.model.arrival_sequence rt.model.task rt.model.task_arrival rt.model.job.
+Require Import rt.implementation.uni.susp.dynamic.task
+ rt.implementation.uni.susp.dynamic.job.
+From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq div.
+
+Module ConcreteArrivalSequence.
+
+ Import Job ArrivalSequence ConcreteTask ConcreteJob SporadicTaskset TaskArrival.
+
+ Section PeriodicArrivals.
+
+ Variable ts: concrete_taskset.
+
+ (* At any time t, we release Some job of tsk if t is a multiple of the period,
+ otherwise we release None. *)
+ Definition add_job (t: time) (tsk: concrete_task) :=
+ if task_period tsk % t then
+ Some (Build_concrete_job (t %/ task_period tsk) (task_cost tsk) (task_deadline tsk) tsk)
+ else
+ None.
+
+ (* The arrival sequence at any time t is simply the partial map of add_job. *)
+ Definition periodic_arrival_sequence (t: time) := pmap (add_job t) ts.
+
+ End PeriodicArrivals.
+
+ Section Proofs.
+
+ (* Let ts be any concrete task set with valid parameters. *)
+ Variable ts: concrete_taskset.
+ Hypothesis H_valid_task_parameters:
+ valid_sporadic_taskset task_cost task_period task_deadline ts.
+
+ (* Regarding the periodic arrival sequence built from ts, we prove that...*)
+ Let arr_seq := periodic_arrival_sequence ts.
+
+ (* ... every job comes from the task set, ... *)
+ Theorem periodic_arrivals_all_jobs_from_taskset:
+ forall (j: JobIn arr_seq),
+ job_task (job_of_job_in j) \in ts. (* TODO: fix coercion *)
+ Proof.
+ intros j.
+ destruct j as [j arr ARRj]; simpl.
+ unfold arr_seq, arrives_at, periodic_arrival_sequence in *.
+ rewrite mem_pmap in ARRj.
+ move: ARRj => /mapP ARRj; destruct ARRj as [tsk IN SOME].
+ by unfold add_job in *; desf.
+ Qed.
+
+ (* ..., jobs have valid parameters, ... *)
+ Theorem periodic_arrivals_valid_job_parameters:
+ forall (j: JobIn arr_seq),
+ valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
+ Proof.
+ rename H_valid_task_parameters into PARAMS.
+ unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
+ intros j; destruct j as [j arr ARRj]; simpl.
+ unfold arrives_at, arr_seq, periodic_arrival_sequence in ARRj.
+ rewrite mem_pmap in ARRj; move: ARRj => /mapP [tsk IN SOME].
+ unfold add_job in SOME; desf.
+ specialize (PARAMS tsk IN); des.
+ unfold valid_sporadic_job, valid_realtime_job, job_cost_positive.
+ by repeat split; try (by done); apply leqnn.
+ Qed.
+
+ (* ... job arrivals satisfy the sporadic task model, ... *)
+ Theorem periodic_arrivals_are_sporadic:
+ sporadic_task_model task_period arr_seq job_task.
+ Proof.
+ unfold sporadic_task_model; move => j j' /eqP DIFF SAMEtsk LE.
+ destruct j as [j arr ARR], j' as [j' arr' ARR']; simpl in *.
+ rewrite eqE /= /jobin_eqdef negb_and /= in DIFF.
+ unfold arrives_at, arr_seq, periodic_arrival_sequence in *.
+ rewrite 2!mem_pmap in ARR ARR'.
+ move: ARR ARR' => /mapP [tsk_j INj SOMEj] /mapP [tsk_j' INj' SOMEj'].
+ unfold add_job in SOMEj, SOMEj'; desf; simpl in *;
+ move: Heq0 Heq => /dvdnP [k DIV] /dvdnP [k' DIV'].
+ {
+ rewrite DIV DIV' mulSnr.
+ rewrite leq_eqVlt in LE; move: LE => /orP [/eqP EQ  LESS].
+ {
+ exfalso; move: DIFF => /negP DIFF; apply DIFF.
+ by subst; rewrite EQ.
+ }
+ subst; rewrite leq_mul2r; apply/orP; right.
+ by rewrite ltn_mul2r in LESS; move: LESS => /andP [_ LT].
+ }
+ {
+ assert (LT: arr < arr'). by rewrite ltn_neqAle; apply/andP.
+ clear LE DIFF; subst tsk_j' arr arr'.
+ rewrite ltn_mul2r in LT; move: LT => /andP [_ LT].
+ by apply leq_trans with (n := k.+1 * task_period tsk_j);
+ [by rewrite mulSnr  by rewrite leq_mul2r; apply/orP; right].
+ }
+ Qed.
+
+ (* ... and the arrival sequence has no duplicate jobs. *)
+ Theorem periodic_arrivals_is_a_set:
+ arrival_sequence_is_a_set arr_seq.
+ Proof.
+ intros t.
+ unfold arr_seq, periodic_arrival_sequence.
+ apply (pmap_uniq) with (g := job_task); last by destruct ts.
+ by unfold add_job, ocancel; intro tsk; desf.
+ Qed.
+
+ End Proofs.
+
+End ConcreteArrivalSequence.
\ No newline at end of file
diff git a/implementation/uni/susp/dynamic/job.v b/implementation/uni/susp/dynamic/job.v
new file mode 100644
index 0000000000000000000000000000000000000000..77057332dd452a339dfed002f18ae75a1331c881
 /dev/null
+++ b/implementation/uni/susp/dynamic/job.v
@@ 0,0 +1,58 @@
+Require Import rt.util.all.
+Require Import rt.implementation.uni.susp.dynamic.task.
+From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq.
+
+Module ConcreteJob.
+
+ Import ConcreteTask.
+
+ Section Defs.
+
+ (* Definition of a concrete task. *)
+ Record concrete_job :=
+ {
+ job_id: nat;
+ job_cost: nat;
+ job_deadline: nat;
+ job_task: concrete_task_eqType
+ }.
+
+ (* To make it compatible with ssreflect, we define a decidable
+ equality for concrete jobs. *)
+ Definition job_eqdef (j1 j2: concrete_job) :=
+ (job_id j1 == job_id j2) &&
+ (job_cost j1 == job_cost j2) &&
+ (job_deadline j1 == job_deadline j2) &&
+ (job_task j1 == job_task j2).
+
+ (* Next, we prove that job_eqdef is indeed an equality, ... *)
+ Lemma eqn_job : Equality.axiom job_eqdef.
+ Proof.
+ unfold Equality.axiom; intros x y.
+ destruct (job_eqdef x y) eqn:EQ.
+ {
+ apply ReflectT; unfold job_eqdef in *.
+ move: EQ => /andP [/andP [/andP [/eqP ID /eqP COST] /eqP DL] /eqP TASK].
+ by destruct x, y; simpl in *; subst.
+ }
+ {
+ apply ReflectF.
+ unfold job_eqdef, not in *; intro BUG.
+ apply negbT in EQ; rewrite negb_and in EQ.
+ destruct x, y.
+ rewrite negb_and in EQ.
+ move: EQ => /orP [EQ  /eqP TASK]; last by apply TASK; inversion BUG.
+ move: EQ => /orP [EQ  /eqP DL]; last by apply DL; inversion BUG.
+ rewrite negb_and in EQ.
+ move: EQ => /orP [/eqP ID  /eqP COST]; last by apply COST; inversion BUG.
+ by apply ID; inversion BUG.
+ }
+ Qed.
+
+ (* ..., which allows instantiating the canonical structure. *)
+ Canonical concrete_job_eqMixin := EqMixin eqn_job.
+ Canonical concrete_job_eqType := Eval hnf in EqType concrete_job concrete_job_eqMixin.
+
+ End Defs.
+
+End ConcreteJob.
\ No newline at end of file
diff git a/implementation/uni/susp/dynamic/oblivious/fp_rta_example.v b/implementation/uni/susp/dynamic/oblivious/fp_rta_example.v
new file mode 100644
index 0000000000000000000000000000000000000000..38c3a9ddb593d3793176d996ce4747c45ce80bd5
 /dev/null
+++ b/implementation/uni/susp/dynamic/oblivious/fp_rta_example.v
@@ 0,0 +1,183 @@
+Require Import rt.util.all.
+Require Import rt.model.job rt.model.task rt.model.priority.
+Require Import rt.model.uni.schedule rt.model.uni.schedulability.
+Require Import rt.model.uni.susp.suspension_intervals.
+Require Import rt.analysis.uni.basic.workload_bound_fp.
+Require Import rt.analysis.uni.susp.dynamic.oblivious.fp_rta.
+Require Import rt.implementation.uni.susp.dynamic.job
+ rt.implementation.uni.susp.dynamic.task
+ rt.implementation.uni.susp.dynamic.arrival_sequence.
+Require Import rt.implementation.uni.susp.schedule.
+From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
+
+Module ResponseTimeAnalysisFP.
+
+ Import Job UniprocessorSchedule SporadicTaskset Priority Schedulability
+ SuspensionIntervals SuspensionObliviousFP WorkloadBoundFP.
+ Import ConcreteJob ConcreteTask ConcreteArrivalSequence ConcreteScheduler.
+
+ (* In this section, we run the suspensionoblivious FP RTA on a simple task set
+ to show that the theorems contain no contradictory assumptions. *)
+ Section ExampleRTA.
+
+ Let tsk1 := { task_id := 1; task_cost := 1; task_period := 5;
+ task_deadline := 5; task_suspension_bound := 1 }.
+ Let tsk2 := { task_id := 2; task_cost := 1; task_period := 5;
+ task_deadline := 5; task_suspension_bound := 0}.
+ Let tsk3 := { task_id := 3; task_cost := 1; task_period := 6;
+ task_deadline := 6; task_suspension_bound := 1}.
+
+ (* Let ts be a task set containing these three tasks, ... *)
+ Program Let ts := Build_set [:: tsk1; tsk2; tsk3] _.
+
+ (* ...which can be shown to have valid parameters. *)
+ Fact ts_has_valid_parameters:
+ valid_sporadic_taskset task_cost task_period task_deadline ts.
+ Proof.
+ intros tsk IN.
+ repeat (move: IN => /orP [/eqP EQ  IN]; subst; compute); by done.
+ Qed.
+
+ (* Now let's inflate the task costs with the suspensionbounds. *)
+ Let inflated_cost := inflated_task_cost task_cost task_suspension_bound.
+
+ (* After the inflation, note that the task costs are no larger than deadlines and periods. *)
+ Fact inflated_cost_le_deadline_and_period:
+ forall tsk,
+ tsk \in ts >
+ inflated_cost tsk <= task_deadline tsk /\
+ inflated_cost tsk <= task_period tsk.
+ Proof.
+ intros tsk IN.
+ repeat (move: IN => /orP [/eqP EQ  IN]; subst; compute); by done.
+ Qed.
+
+ (* Next, recall the FP RTA schedulability test using RM as the FP policy
+ and the inflated task costs. *)
+ Let RTA_claimed_bounds :=
+ fp_claimed_bounds inflated_cost task_period task_deadline (RM task_period).
+ Let schedulability_test :=
+ fp_schedulable inflated_cost task_period task_deadline (RM task_period).
+
+ (* First, we show that the schedulability test returns the following bounds, ... *)
+ Fact RTA_yields_these_bounds :
+ RTA_claimed_bounds ts = Some [:: (tsk1, 3); (tsk2, 3); (tsk3, 5)].
+ Proof.
+ rewrite /RTA_claimed_bounds /fp_claimed_bounds /inflated_cost /inflated_task_cost.
+ set RESP := [seq _  tsk < ts].
+ suff EQ: RESP = [:: (tsk1, Some 3); (tsk2, Some 3); (tsk3, Some 5)] by rewrite EQ; compute.
+ rewrite /RESP /ts /=; do 2 f_equal.
+ {
+ rewrite /per_task_rta /= addn1.
+ have WORK: total_workload_bound_fp inflated_cost task_period (RM task_period)
+ [:: tsk1; tsk2; tsk3] tsk1 2 = 3.
+ {
+ by compute; rewrite unlock; compute.
+ }
+ rewrite !WORK /=; clear WORK.
+ have WORK: total_workload_bound_fp inflated_cost task_period (RM task_period)
+ [:: tsk1; tsk2; tsk3] tsk1 3 = 3.
+ {
+ by compute; rewrite unlock; compute.
+ }
+ by rewrite !WORK /=.
+ }
+ f_equal.
+ {
+ rewrite /per_task_rta /= addn0.
+ have WORK: total_workload_bound_fp inflated_cost task_period (RM task_period)
+ [:: tsk1; tsk2; tsk3] tsk2 1 = 3.
+ {
+ by compute; rewrite unlock; compute.
+ }
+ rewrite !WORK /=; clear WORK.
+ have WORK: total_workload_bound_fp inflated_cost task_period (RM task_period)
+ [:: tsk1; tsk2; tsk3] tsk2 3 = 3.
+ {
+ by compute; rewrite unlock; compute.
+ }
+ by rewrite !WORK /=.
+ }
+ do 2 f_equal.
+ {
+ rewrite /per_task_rta /= addn1.
+ have WORK: total_workload_bound_fp inflated_cost task_period (RM task_period)
+ [:: tsk1; tsk2; tsk3] tsk3 2 = 5.
+ {
+ by compute; rewrite unlock; compute.
+ }
+ rewrite !WORK /=; clear WORK.
+ have WORK: total_workload_bound_fp inflated_cost task_period (RM task_period)
+ [:: tsk1; tsk2; tsk3] tsk3 5 = 5.
+ {
+ by compute; rewrite unlock; compute.
+ }
+ by rewrite !WORK /=; clear WORK.
+ }
+ Qed.
+
+ (* ...so the schedulability test indeed returns true. *)
+ Fact schedulability_test_succeeds :
+ schedulability_test ts = true.
+ Proof.
+ rewrite /schedulability_test /fp_schedulable /RTA_claimed_bounds.
+ by rewrite RTA_yields_these_bounds.
+ Qed.
+
+ (* Now, let's show that the task set is schedulable. *)
+
+ (* Let arr_seq be the periodic arrival sequence from ts... *)
+ Let arr_seq := periodic_arrival_sequence ts.
+
+ (* ...where jobs have total suspension times that are no larger than
+ the suspension bound of their tasks. *)
+ Variable next_suspension: job_suspension concrete_job_eqType.
+ Hypothesis H_dynamic_suspensions:
+ dynamic_suspension_model job_cost job_task next_suspension task_suspension_bound.
+
+ (* Also assume ratemonotonic priorities. *)
+ Let higher_eq_priority : JLDP_policy arr_seq := (FP_to_JLDP job_task arr_seq (RM task_period)).
+
+ (* Next, let sched be the suspensionaware RM schedule with those job suspension times. *)
+ Let sched := scheduler job_cost arr_seq next_suspension higher_eq_priority.
+
+ (* To conclude, based on the definition of deadline miss,... *)
+ Let no_deadline_missed_by :=
+ task_misses_no_deadline job_cost job_deadline job_task sched.
+
+ (* ...we use the result of the suspensionoblivious FP RTA to conclude that
+ no task misses its deadline. *)
+ Corollary ts_is_schedulable:
+ forall tsk,
+ tsk \in ts >
+ no_deadline_missed_by tsk.
+ Proof.
+ intros tsk IN.
+ have VALID := periodic_arrivals_valid_job_parameters ts ts_has_valid_parameters.
+ have TSVALID := ts_has_valid_parameters.
+ unfold valid_sporadic_job, valid_realtime_job in *; des.
+ apply suspension_oblivious_fp_rta_implies_schedulability with (task_cost := task_cost)
+ (task_period := task_period) (task_deadline := task_deadline) (ts0 := ts)
+ (higher_eq_priority0 := RM task_period) (next_suspension0 := next_suspension)
+ (task_suspension_bound := task_suspension_bound); try (by done).
+  by apply periodic_arrivals_is_a_set.
+  by apply periodic_arrivals_all_jobs_from_taskset.
+  by apply periodic_arrivals_are_sporadic.
+  by apply RM_is_reflexive.
+  by apply RM_is_transitive.
+  by intros tsk_a tsk_b INa INb; apply/orP; apply leq_total.
+
+  by apply scheduler_jobs_must_arrive_to_execute.
+  by apply scheduler_completed_jobs_dont_execute; intro j'; specialize (VALID j'); des.
+  by apply scheduler_work_conserving.
+  apply scheduler_respects_policy.
+  by intros t; apply RM_is_transitive.
+  by intros _ j1 j2; apply leq_total.
+  by apply scheduler_respects_self_suspensions.
+  by apply inflated_cost_le_deadline_and_period.
+  by apply schedulability_test_succeeds.
+ Qed.
+
+ End ExampleRTA.
+
+End ResponseTimeAnalysisFP.
\ No newline at end of file
diff git a/implementation/uni/susp/dynamic/task.v b/implementation/uni/susp/dynamic/task.v
new file mode 100644
index 0000000000000000000000000000000000000000..f6805378c55b50efb7d67ab39a025c07c7e9012e
 /dev/null
+++ b/implementation/uni/susp/dynamic/task.v
@@ 0,0 +1,70 @@
+Require Import rt.util.all.
+Require Import rt.model.task.
+From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq.
+
+Module ConcreteTask.
+
+ Import SporadicTaskset.
+
+ Section Defs.
+
+ (* Definition of a concrete task. *)
+ Record concrete_task :=
+ {
+ task_id: nat; (* for uniqueness *)
+ task_cost: nat;
+ task_period: nat;
+ task_deadline: nat;
+ task_suspension_bound: nat
+ }.
+
+ (* To make it compatible with ssreflect, we define a decidable
+ equality for concrete tasks. *)
+ Definition task_eqdef (t1 t2: concrete_task) :=
+ (task_id t1 == task_id t2) &&
+ (task_cost t1 == task_cost t2) &&
+ (task_period t1 == task_period t2) &&
+ (task_deadline t1 == task_deadline t2) &&
+ (task_suspension_bound t1 == task_suspension_bound t2).
+
+ (* Next, we prove that task_eqdef is indeed an equality, ... *)
+ Lemma eqn_task : Equality.axiom task_eqdef.
+ Proof.
+ unfold Equality.axiom; intros x y.
+ destruct (task_eqdef x y) eqn:EQ.
+ {
+ apply ReflectT.
+ unfold task_eqdef in *.
+ move: EQ => /andP [/andP [/andP [/andP [/eqP ID /eqP COST] /eqP PERIOD] /eqP DL] /eqP SUSP].
+ by destruct x, y; simpl in *; subst.
+ }
+ {
+ apply ReflectF.
+ unfold task_eqdef, not in *; intro BUG.
+ apply negbT in EQ; rewrite negb_and in EQ.
+ destruct x, y.
+ rewrite negb_and in EQ.
+ move: EQ => /orP [/orP [EQ  /eqP DL]  /eqP SUSP]; last by apply SUSP; inversion BUG.
+ rewrite negb_and in EQ.
+ move: EQ => /orP [EQ  /eqP DL]; last by apply DL; inversion BUG.
+ rewrite negb_and in EQ.
+ move: EQ => /orP [/eqP ID  /eqP PERIOD]; last by apply PERIOD; inversion BUG.
+ by apply ID; inversion BUG.
+ by apply DL; inversion BUG.
+ }
+ Qed.
+
+ (* ..., which allows instantiating the canonical structure. *)
+ Canonical concrete_task_eqMixin := EqMixin eqn_task.
+ Canonical concrete_task_eqType := Eval hnf in EqType concrete_task concrete_task_eqMixin.
+
+ End Defs.
+
+ Section ConcreteTaskset.
+
+ Definition concrete_taskset :=
+ taskset_of concrete_task_eqType.
+
+ End ConcreteTaskset.
+
+End ConcreteTask.
\ No newline at end of file
diff git a/implementation/uni/susp/schedule.v b/implementation/uni/susp/schedule.v
new file mode 100644
index 0000000000000000000000000000000000000000..6debae9a846fca1d554eaaf8d85ff0808f2bf4f4
 /dev/null
+++ b/implementation/uni/susp/schedule.v
@@ 0,0 +1,256 @@
+Require Import rt.util.all.
+Require Import rt.model.job rt.model.arrival_sequence rt.model.priority.
+Require Import rt.model.uni.schedule.
+Require Import rt.model.uni.susp.platform.
+Require Import rt.model.uni.transformation.construction.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop seq path.
+
+Module ConcreteScheduler.
+
+ Import Job ArrivalSequence UniprocessorSchedule PlatformWithSuspensions Priority
+ ScheduleConstruction.
+
+ (* In this section, we implement a prioritybased uniprocessor scheduler *)
+ Section Implementation.
+
+ Context {Job: eqType}.
+ Variable job_cost: Job > time.
+
+ (* Let arr_seq be any job arrival sequence...*)
+ Variable arr_seq: arrival_sequence Job.
+
+ (* ...that is subject to job suspensions. *)
+ Variable next_suspension: job_suspension Job.
+
+ (* Also, assume that a JLDP policy is given. *)
+ Variable higher_eq_priority: JLDP_policy arr_seq.
+
+ (* Next, we show how to recursively construct the schedule. *)
+ Section ScheduleConstruction.
+
+ (* For any time t, suppose that we have generated the schedule prefix in the
+ interval [0, t). Then, we must define what should be scheduled at time t. *)
+ Variable sched_prefix: schedule arr_seq.
+ Variable t: time.
+
+ (* For simplicity, let's use some local names. *)
+ Let is_pending := pending job_cost sched_prefix.
+ Let is_suspended :=
+ suspended_at job_cost next_suspension sched_prefix.
+
+ (* Consider the list of pending, nonsuspended jobs at time t. *)
+ Definition pending_jobs :=
+ [seq j < jobs_arrived_up_to arr_seq t  is_pending j t && ~~ is_suspended j t].
+
+ (* Then, we sort this list by priority... *)
+ Definition sorted_jobs := sort (higher_eq_priority t) pending_jobs.
+
+ (* ...and pick the highestpriority job. *)
+ Definition highest_priority_job := ohead sorted_jobs.
+
+ End ScheduleConstruction.
+
+ (* Starting from the empty schedule, the final schedule is obtained by iteratively
+ picking the highestpriority job. *)
+ Let empty_schedule : schedule arr_seq := fun t => None.
+ Definition scheduler :=
+ build_schedule_from_prefixes arr_seq highest_priority_job empty_schedule.
+
+ (* Then, by showing that the construction function depends only on the prefix, ... *)
+ Lemma scheduler_depends_only_on_prefix:
+ forall sched1 sched2 t,
+ (forall t0, t0 < t > sched1 t0 = sched2 t0) >
+ highest_priority_job sched1 t = highest_priority_job sched2 t.
+ Proof.
+ intros sched1 sched2 t ALL.
+ rewrite /highest_priority_job /sorted_jobs.
+ suff SAME: pending_jobs sched1 t = pending_jobs sched2 t by rewrite SAME.
+ apply eq_in_filter.
+ intros j IN; apply JobIn_arrived in IN.
+ rewrite /arrived_before ltnS in IN.
+ rewrite /pending /has_arrived IN 2!andTb.
+ have COMP: completed_by job_cost sched1 j t =
+ completed_by job_cost sched2 j t.
+ {
+ rewrite /completed_by.
+ rewrite /completed_by; f_equal.
+ apply eq_big_nat; move => i /= LTi.
+ by rewrite /service_at /scheduled_at ALL.
+ }
+ rewrite COMP; do 2 f_equal.
+ rewrite /suspended_at; f_equal; first by rewrite COMP.
+ have EX: [exists t0: 'I_t, scheduled_at sched1 j t0] =
+ [exists t0: 'I_t, scheduled_at sched2 j t0].
+ {
+ apply/idP/idP.
+ {
+ move => /existsP [t0 SCHED].
+ by apply/existsP; exists t0; rewrite /scheduled_at ALL.
+ }
+ {
+ move => /existsP [t0 SCHED].
+ by apply/existsP; exists t0; rewrite /scheduled_at ALL.
+ }
+ }
+ have BEG: time_after_last_execution sched1 j t =
+ time_after_last_execution sched2 j t.
+ {
+ rewrite /time_after_last_execution EX.
+ case: ifP => _; last by done.
+ f_equal; apply eq_bigl.
+ by intros t0; rewrite /scheduled_at ALL.
+ }
+ have SUSP: suspension_duration next_suspension sched1 j t =
+ suspension_duration next_suspension sched2 j t.
+ {
+ rewrite /suspension_duration BEG; f_equal.
+ rewrite /service /service_during big_nat_cond [in RHS]big_nat_cond.
+ apply congr_big; try (by done).
+ move => i /= /andP [LTi _].
+ rewrite /service_at /scheduled_at ALL //.
+ apply: (leq_trans LTi).
+ by apply last_execution_bounded_by_identity.
+ }
+ by rewrite BEG SUSP.
+ Qed.
+
+ (* ...we infer that the generated schedule is indeed based on the construction function. *)
+ Corollary scheduler_uses_construction_function:
+ forall t, scheduler t = highest_priority_job scheduler t.
+ Proof.
+ by ins; apply prefix_dependent_schedule_construction,
+ scheduler_depends_only_on_prefix.
+ Qed.
+
+ End Implementation.
+
+ (* In this section, we prove the properties of the scheduler that are used
+ as hypotheses in the analyses. *)
+ Section Proofs.
+
+ Context {Job: eqType}.
+ Variable job_cost: Job > time.
+
+ (* Let arr_seq be any job arrival sequence with no duplicates... *)
+ Variable arr_seq: arrival_sequence Job.
+ Hypothesis H_arrival_sequence_is_a_set: arrival_sequence_is_a_set arr_seq.
+
+ (* ...that is subject to suspension times. *)
+ Variable next_suspension: job_suspension Job.
+
+ (* Consider any JLDP policy that is reflexive, transitive and total. *)
+ Variable higher_eq_priority: JLDP_policy arr_seq.
+ Hypothesis H_priority_is_reflexive: JLDP_is_reflexive higher_eq_priority.
+ Hypothesis H_priority_is_transitive: JLDP_is_transitive higher_eq_priority.
+ Hypothesis H_priority_is_total: JLDP_is_total higher_eq_priority.
+
+ (* Let sched denote our concrete scheduler implementation. *)
+ Let sched := scheduler job_cost arr_seq next_suspension higher_eq_priority.
+
+ (* To conclude, we prove the important properties of the scheduler implementation. *)
+
+ (* First, we show that jobs do not execute before they arrive...*)
+ Theorem scheduler_jobs_must_arrive_to_execute:
+ jobs_must_arrive_to_execute sched.
+ Proof.
+ unfold jobs_must_arrive_to_execute.
+ move => j t /eqP SCHED.
+ rewrite /sched scheduler_uses_construction_function in SCHED.
+ rewrite /highest_priority_job in SCHED.
+ set jobs := sorted_jobs _ _ _ _ _ _ in SCHED.
+ suff IN: j \in jobs.
+ {
+ rewrite mem_sort mem_filter in IN.
+ by move: IN => /andP [/andP [/andP [ARR _] _] _].
+ }
+ destruct jobs; first by done.
+ by case: SCHED => SAME; subst; rewrite in_cons eq_refl.
+ Qed.
+
+ (* ... nor after completion. *)
+ Theorem scheduler_completed_jobs_dont_execute:
+ completed_jobs_dont_execute job_cost sched.
+ Proof.
+ intros j t.
+ induction t;
+ first by rewrite /service /service_during big_geq //.
+ rewrite /service /service_during big_nat_recr //=.
+ rewrite leq_eqVlt in IHt; move: IHt => /orP [/eqP EQ  LT]; last first.
+ {
+ apply: leq_trans LT; rewrite addn1.
+ by apply leq_add; last by apply leq_b1.
+ }
+ rewrite [job_cost _]addn0; apply leq_add; first by rewrite EQ.
+ rewrite leqn0 eqb0 /scheduled_at.
+ rewrite /sched scheduler_uses_construction_function.
+ rewrite /highest_priority_job.
+ apply/eqP; intro HP.
+ set jobs := sorted_jobs _ _ _ _ _ _ in HP.
+ suff IN: j \in jobs.
+ {
+ rewrite mem_sort mem_filter in IN.
+ move: IN => /andP [/andP [/andP [_ NOTCOMP] _] _].
+ by rewrite /completed_by /sched EQ eq_refl in NOTCOMP.
+ }
+ destruct jobs; first by done.
+ by case: HP => SAME; subst; rewrite in_cons eq_refl.
+ Qed.
+
+ (* In addition, the scheduler is work conserving, ... *)
+ Theorem scheduler_work_conserving:
+ work_conserving job_cost next_suspension sched.
+ Proof.
+ intros j t BACK.
+ move: BACK => /andP [/andP [/andP [ARR NOTCOMP] NOTSCHED] NOTSUSP].
+ rewrite /scheduled_at /sched scheduler_uses_construction_function in NOTSCHED.
+ rewrite /scheduled_at /sched scheduler_uses_construction_function.
+ case HP: (highest_priority_job _ _ _ _ _ ) => [j_hp];
+ first by exists j_hp.
+ rewrite /highest_priority_job in HP.
+ set jobs := sorted_jobs _ _ _ _ _ _ in HP.
+ suff IN: j \in jobs by destruct jobs.
+ by rewrite mem_sort mem_filter /pending ARR NOTCOMP NOTSUSP /=; apply JobIn_arrived.
+ Qed.
+
+ (* ... respects the JLDP policy..., *)
+ Theorem scheduler_respects_policy :
+ respects_JLDP_policy job_cost next_suspension sched higher_eq_priority.
+ Proof.
+ rename H_priority_is_transitive into TRANS, H_priority_is_total into TOTAL.
+ move => j1 j2 t BACK /eqP SCHED.
+ move: BACK => /andP [/andP [/andP [ARR NOTCOMP] NOTSCHED] NOTSUSP].
+ rewrite /scheduled_at /sched scheduler_uses_construction_function in NOTSCHED.
+ rewrite /scheduled_at /sched scheduler_uses_construction_function in SCHED.
+ rewrite /highest_priority_job in SCHED NOTSCHED.
+ set jobs := sorted_jobs _ _ _ _ _ _ in SCHED NOTSCHED.
+ have IN: j1 \in jobs.
+ by rewrite mem_sort mem_filter /pending ARR NOTCOMP NOTSUSP /=; apply JobIn_arrived.
+ have SORT: sorted (higher_eq_priority t) jobs by apply sort_sorted.
+ destruct jobs as [j0 l]; first by done.
+ rewrite in_cons in IN; move: IN => /orP [/eqP EQ  IN];
+ first by subst; rewrite /= eq_refl in NOTSCHED.
+ case: SCHED => SAME; subst.
+ simpl in SORT; apply order_path_min in SORT; last by done.
+ by move: SORT => /allP ALL; apply ALL.
+ Qed.
+
+ (* ... and respects selfsuspensions. *)
+ Theorem scheduler_respects_self_suspensions:
+ respects_self_suspensions job_cost next_suspension sched.
+ Proof.
+ move => j t /eqP SCHED.
+ rewrite /scheduled_at /sched scheduler_uses_construction_function in SCHED.
+ rewrite /highest_priority_job in SCHED.
+ set jobs := sorted_jobs _ _ _ _ _ _ in SCHED.
+ have IN: j \in jobs.
+ {
+ destruct jobs; first by done.
+ by case: SCHED => SAME; subst; rewrite in_cons eq_refl.
+ }
+ rewrite mem_sort mem_filter in IN.
+ by move: IN => /andP [/andP [_ NOTSUSP] _]; apply/negP.
+ Qed.
+
+ End Proofs.
+
+End ConcreteScheduler.
\ No newline at end of file
diff git a/model/apa/constrained_deadlines.v b/model/apa/constrained_deadlines.v
index a1cea5476577f750b60e1d421b04c0c8994338ae..1812a7981d6710cf6fd880b88d0084811d39cc1d 100644
 a/model/apa/constrained_deadlines.v
+++ b/model/apa/constrained_deadlines.v
@@ 44,8 +44,8 @@ Module ConstrainedDeadlines.
Variable higher_eq_priority: JLDP_policy arr_seq.
Hypothesis H_work_conserving:
apa_work_conserving job_cost job_task sched alpha.
 Hypothesis H_enforces_JLDP_policy:
 enforces_JLDP_policy_under_weak_APA job_cost job_task sched alpha higher_eq_priority.
+ Hypothesis H_respects_JLDP_policy:
+ respects_JLDP_policy_under_weak_APA job_cost job_task sched alpha higher_eq_priority.
(* Consider task set ts. *)
Variable ts: taskset_of sporadic_task.
@@ 135,8 +135,8 @@ Module ConstrainedDeadlines.
(* Assume any workconserving prioritybased scheduler. *)
Variable higher_eq_priority: FP_policy sporadic_task.
Hypothesis H_work_conserving: apa_work_conserving job_cost job_task sched alpha.
 Hypothesis H_enforces_JLDP_policy:
 enforces_FP_policy_under_weak_APA job_cost job_task sched alpha higher_eq_priority.
+ Hypothesis H_respects_JLDP_policy:
+ respects_FP_policy_under_weak_APA job_cost job_task sched alpha higher_eq_priority.
(* Consider any task set ts. *)
Variable ts: taskset_of sporadic_task.
diff git a/model/apa/interference_edf.v b/model/apa/interference_edf.v
index fcd1ee9df640e7555ab679ff2f366e3ac1ed8612..36fd123383402be27d30b3ed1cde03e8043fe23a 100644
 a/model/apa/interference_edf.v
+++ b/model/apa/interference_edf.v
@@ 31,7 +31,7 @@ Module InterferenceEDF.
for EDF, i.e., if any job of tsk is backlogged, every processor
must be busy with jobs with no larger absolute deadline. *)
Hypothesis H_scheduler_uses_EDF:
 enforces_JLDP_policy_under_weak_APA job_cost job_task sched alpha (EDF job_deadline).
+ respects_JLFP_policy_under_weak_APA job_cost job_task sched alpha (EDF job_deadline).
(* Under EDF scheduling, a job only causes interference if its deadline
is not larger than the deadline of the analyzed job. *)
@@ 41,7 +41,7 @@ Module InterferenceEDF.
job_arrival j + job_deadline j <= job_arrival j' + job_deadline j'.
Proof.
rename H_scheduler_uses_EDF into PRIO.
 unfold enforces_JLDP_policy_under_weak_APA in *.
+ unfold respects_JLDP_policy_under_weak_APA in *.
intros j j' t1 t2 INTERF.
unfold job_interference in INTERF.
destruct ([exists t': 'I_t2,
@@ 52,7 +52,7 @@ Module InterferenceEDF.
scheduled_on sched j cpu t']]) eqn:EX.
{
move: EX => /existsP [t' /existsP [cpu /andP [/andP [/andP [LE BACK] CAN] SCHED]]].
 by eapply PRIO in SCHED; last by apply CAN.
+ by specialize (PRIO j' j cpu t' BACK SCHED CAN).
}
{
apply negbT in EX; rewrite negb_exists in EX; move: EX => /forallP ALL.
diff git a/model/apa/platform.v b/model/apa/platform.v
index d83856742516a30cc8d3e4b724c7e3da270dc240..1b4343506ca61c2846db0064dd9eed75beb8d3c5 100644
 a/model/apa/platform.v
+++ b/model/apa/platform.v
@@ 43,7 +43,7 @@ Module Platform.
exists j_other,
scheduled_on sched j_other cpu t.
 (* In a schedule that enforces affinities, a job is scheduled
+ (* In a schedule that respects affinities, a job is scheduled
only if its affinity allows it. *)
Definition respects_affinity :=
forall j cpu t,
@@ 52,16 +52,52 @@ Module Platform.
End Execution.
+ Section FP.
+
+ (* An FP policy ...*)
+ Variable higher_eq_priority: FP_policy sporadic_task.
+
+ (* ... is respected by a weak APA scheduler iff for any
+ backlogged job j, if there is another job j_hp
+ executing on j's affinity, then j_hp's task priority
+ must be as high as j's task priority. *)
+ Definition respects_FP_policy_under_weak_APA :=
+ forall (j j_hp: JobIn arr_seq) cpu t,
+ backlogged job_cost sched j t >
+ scheduled_on sched j_hp cpu t >
+ can_execute_on alpha (job_task j) cpu >
+ higher_eq_priority (job_task j_hp) (job_task j).
+
+ End FP.
+
+ Section JLFP.
+
+ (* A JLFP policy ...*)
+ Variable higher_eq_priority: JLFP_policy arr_seq.
+
+ (* ... is respected by a weak APA scheduler iff for
+ any backlogged job j, if there is another job j_hp
+ executing on j's affinity, then j_hp's priority
+ must be as high as j's priority. *)
+ Definition respects_JLFP_policy_under_weak_APA :=
+ forall (j j_hp: JobIn arr_seq) cpu t,
+ backlogged job_cost sched j t >
+ scheduled_on sched j_hp cpu t >
+ can_execute_on alpha (job_task j) cpu >
+ higher_eq_priority j_hp j.
+
+ End JLFP.
+
Section JLDP.
(* A JLFP/JLDP policy ...*)
Variable higher_eq_priority: JLDP_policy arr_seq.
 (* ... is enforced by a weak APA scheduler iff at any time t,
+ (* ... is respected by a weak APA scheduler iff at any time t,
for any backlogged job j, if there is another job j_hp
executing on j's affinity, then j_hp's priority must be
as high as j's priority. *)
 Definition enforces_JLDP_policy_under_weak_APA :=
+ Definition respects_JLDP_policy_under_weak_APA :=
forall (j j_hp: JobIn arr_seq) cpu t,
backlogged job_cost sched j t >
scheduled_on sched j_hp cpu t >
@@ 70,18 +106,6 @@ Module Platform.
End JLDP.
 Section FP.

 (* Given an FP policy, ...*)
 Variable higher_eq_priority: FP_policy sporadic_task.

 (* ... this policy is enforced by a weak APA scheduler iff
 the corresponding JLDP policy is enforced by the scheduler. *)
 Definition enforces_FP_policy_under_weak_APA :=
 enforces_JLDP_policy_under_weak_APA (FP_to_JLDP job_task higher_eq_priority).

 End FP.

End Properties.
End Platform.
\ No newline at end of file
diff git a/model/global/basic/constrained_deadlines.v b/model/global/basic/constrained_deadlines.v
index 67f4875aa862e78b232e619ddd593efd114de98a..cae2e3b1c5da21959182bcea60e4cceae6220603 100644
 a/model/global/basic/constrained_deadlines.v
+++ b/model/global/basic/constrained_deadlines.v
@@ 40,8 +40,8 @@ Module ConstrainedDeadlines.
(* Assume any workconserving prioritybased scheduler. *)
Variable higher_eq_priority: JLDP_policy arr_seq.
Hypothesis H_work_conserving: work_conserving job_cost sched.
 Hypothesis H_enforces_JLDP_policy:
 enforces_JLDP_policy job_cost sched higher_eq_priority.
+ Hypothesis H_respects_JLDP_policy:
+ respects_JLDP_policy job_cost sched higher_eq_priority.
(* Consider task set ts. *)
Variable ts: taskset_of sporadic_task.
@@ 127,7 +127,7 @@ Module ConstrainedDeadlines.
rename H_all_jobs_from_taskset into FROMTS,
H_sequential_jobs into SEQUENTIAL,
H_work_conserving into WORK,
 H_enforces_JLDP_policy into PRIO,
+ H_respects_JLDP_policy into PRIO,
H_j_backlogged into BACK,
H_job_of_tsk into JOBtsk,
H_valid_job_parameters into JOBPARAMS,
@@ 137,7 +137,7 @@ Module ConstrainedDeadlines.
H_jobs_must_arrive_to_execute into ARRIVE.
apply work_conserving_eq_work_conserving_count in WORK.
unfold valid_sporadic_job, valid_realtime_job,
 enforces_JLDP_policy, completed_jobs_dont_execute,
+ respects_JLDP_policy, completed_jobs_dont_execute,
sporadic_task_model, is_valid_sporadic_task,
jobs_of_same_task_dont_execute_in_parallel,
sequential_jobs in *.
@@ 200,8 +200,8 @@ Module ConstrainedDeadlines.
(* Assume any workconserving prioritybased scheduler. *)
Variable higher_eq_priority: FP_policy sporadic_task.
Hypothesis H_work_conserving: work_conserving job_cost sched.
 Hypothesis H_enforces_JLDP_policy:
 enforces_FP_policy job_cost job_task sched higher_eq_priority.
+ Hypothesis H_respects_JLDP_policy:
+ respects_FP_policy job_cost job_task sched higher_eq_priority.
(* Consider any task set ts. *)
Variable ts: taskset_of sporadic_task.
@@ 341,7 +341,7 @@ Module ConstrainedDeadlines.
rename H_all_jobs_from_taskset into FROMTS,
H_sequential_jobs into SEQUENTIAL,
H_work_conserving into WORK,
 H_enforces_JLDP_policy into PRIO,
+ H_respects_JLDP_policy into PRIO,
H_j_backlogged into BACK,
H_job_of_tsk into JOBtsk,
H_sporadic_tasks into SPO,
@@ 353,7 +353,7 @@ Module ConstrainedDeadlines.
H_jobs_must_arrive_to_execute into ARRIVE.
apply work_conserving_eq_work_conserving_count in WORK.
unfold valid_sporadic_job, valid_realtime_job,
 enforces_FP_policy, enforces_JLDP_policy, FP_to_JLDP,
+ respects_FP_policy, respects_JLDP_policy, FP_to_JLDP,
completed_jobs_dont_execute, sequential_jobs,
sporadic_task_model, is_valid_sporadic_task,
jobs_of_same_task_dont_execute_in_parallel,
diff git a/model/global/basic/interference_edf.v b/model/global/basic/interference_edf.v
index 7ff6c14e6fe6a3a94c321a909f03b15acc6b818c..385d36819fbfd90ae2718fc297d982c6078bbb04 100644
 a/model/global/basic/interference_edf.v
+++ b/model/global/basic/interference_edf.v
@@ 25,7 +25,7 @@ Module InterferenceEDF.
for EDF, i.e., if any job of tsk is backlogged, every processor
must be busy with jobs with no larger absolute deadline. *)
Hypothesis H_scheduler_uses_EDF:
 enforces_JLDP_policy job_cost sched (EDF job_deadline).
+ respects_JLFP_policy job_cost sched (EDF job_deadline).
(* Under EDF scheduling, a job only causes interference if its deadline
is not larger than the deadline of the analyzed job. *)
diff git a/model/global/basic/platform.v b/model/global/basic/platform.v
index a9e2a6e45313eac6ee7e0118607153a89927009d..281fd4ddafefef78d2a3efa21ef3c724070f8ef6 100644
 a/model/global/basic/platform.v
+++ b/model/global/basic/platform.v
@@ 45,15 +45,46 @@ Module Platform.
End Execution.
+ Section FP.
+
+ (* An FP policy ...*)
+ Variable higher_eq_priority: FP_policy sporadic_task.
+
+ (* ... is respected by the scheduler iff every scheduled
+ job has higher (or same) priority than (as) a backlogged job. *)
+ Definition respects_FP_policy :=
+ forall (j j_hp: JobIn arr_seq) t,
+ backlogged job_cost sched j t >
+ scheduled sched j_hp t >
+ higher_eq_priority (job_task j_hp) (job_task j).
+
+ End FP.
+
+ Section JLFP.
+
+ (* A JLFP policy ...*)
+ Variable higher_eq_priority: JLFP_policy arr_seq.
+
+ (* ... is respected by the scheduler iff at any time t,
+ a scheduled job has higher (or same) priority than (as)
+ a backlogged job. *)
+ Definition respects_JLFP_policy :=
+ forall (j j_hp: JobIn arr_seq) t,
+ backlogged job_cost sched j t >
+ scheduled sched j_hp t >
+ higher_eq_priority j_hp j.
+
+ End JLFP.
+
Section JLDP.
 (* A JLFP/JLDP policy ...*)
+ (* A JLDP policy ...*)
Variable higher_eq_priority: JLDP_policy arr_seq.
 (* ... is enforced by the scheduler iff at any time t,
+ (* ... is respected by the scheduler iff at any time t,
a scheduled job has higher (or same) priority than (as)
a backlogged job. *)
 Definition enforces_JLDP_policy :=
+ Definition respects_JLDP_policy :=
forall (j j_hp: JobIn arr_seq) t,
backlogged job_cost sched j t >
scheduled sched j_hp t >
@@ 61,18 +92,6 @@ Module Platform.
End JLDP.
 Section FP.

 (* Given an FP policy, ...*)
 Variable higher_eq_priority: FP_policy sporadic_task.

 (* ... this policy is enforced by the scheduler iff
 a corresponding JLDP policy is enforced by the scheduler. *)
 Definition enforces_FP_policy :=
 enforces_JLDP_policy (FP_to_JLDP job_task higher_eq_priority).

 End FP.

Section Lemmas.
(* Assume all jobs have valid parameters, ...*)
diff git a/model/global/jitter/constrained_deadlines.v b/model/global/jitter/constrained_deadlines.v
index 0e525386e818c8a5582c71be2f87dda85feae30c..892f587111bedb8d82e107553b60ce909689b75d 100644
 a/model/global/jitter/constrained_deadlines.v
+++ b/model/global/jitter/constrained_deadlines.v
@@ 42,8 +42,8 @@ Module ConstrainedDeadlines.
Variable higher_eq_priority: JLDP_policy arr_seq.
Hypothesis H_work_conserving:
work_conserving job_cost job_jitter sched.
 Hypothesis H_enforces_JLDP_policy:
 enforces_JLDP_policy job_cost job_jitter sched higher_eq_priority.
+ Hypothesis H_respects_JLDP_policy:
+ respects_JLDP_policy job_cost job_jitter sched higher_eq_priority.
(* Consider task set ts. *)
Variable ts: taskset_of sporadic_task.
@@ 134,7 +134,7 @@ Module ConstrainedDeadlines.
rename H_all_jobs_from_taskset into FROMTS,
H_sequential_jobs into SEQUENTIAL,
H_work_conserving into WORK,
 H_enforces_JLDP_policy into PRIO,
+ H_respects_JLDP_policy into PRIO,
H_j_backlogged into BACK,
H_job_of_tsk into JOBtsk,
H_valid_job_parameters into JOBPARAMS,
@@ 144,7 +144,7 @@ Module ConstrainedDeadlines.
H_jobs_execute_after_jitter into JITTER.
apply work_conserving_eq_work_conserving_count in WORK.
unfold valid_sporadic_job, valid_realtime_job,
 enforces_JLDP_policy, completed_jobs_dont_execute,
+ respects_JLDP_policy, completed_jobs_dont_execute,
sporadic_task_model, is_valid_sporadic_task,
jobs_of_same_task_dont_execute_in_parallel,
sequential_jobs in *.
@@ 209,8 +209,8 @@ Module ConstrainedDeadlines.
(* Assume any workconserving prioritybased scheduler. *)
Variable higher_eq_priority: FP_policy sporadic_task.
Hypothesis H_work_conserving: work_conserving job_cost job_jitter sched.
 Hypothesis H_enforces_JLDP_policy:
 enforces_FP_policy job_cost job_task job_jitter sched higher_eq_priority.
+ Hypothesis H_respects_JLDP_policy:
+ respects_FP_policy job_cost job_task job_jitter sched higher_eq_priority.
(* Consider any task set ts. *)
Variable ts: taskset_of sporadic_task.
@@ 359,7 +359,7 @@ Module ConstrainedDeadlines.
rename H_all_jobs_from_taskset into FROMTS,
H_sequential_jobs into SEQUENTIAL,
H_work_conserving into WORK,
 H_enforces_JLDP_policy into PRIO,
+ H_respects_JLDP_policy into PRIO,
H_j_backlogged into BACK,
H_job_of_tsk into JOBtsk,
H_sporadic_tasks into SPO,
@@ 371,7 +371,7 @@ Module ConstrainedDeadlines.
H_jobs_execute_after_jitter into JITTER.
apply work_conserving_eq_work_conserving_count in WORK.
unfold valid_sporadic_job, valid_realtime_job,
 enforces_FP_policy, enforces_JLDP_policy, FP_to_JLDP,
+ respects_FP_policy, respects_JLDP_policy, FP_to_JLDP,
completed_jobs_dont_execute, sequential_jobs,
sporadic_task_model, is_valid_sporadic_task,
jobs_of_same_task_dont_execute_in_parallel,
diff git a/model/global/jitter/interference_edf.v b/model/global/jitter/interference_edf.v
index 09ada9aa7415be2cd9c8d67e52dcc590f2195a1a..a96040b98ac140c25224205e2684ee3d0c754956 100644
 a/model/global/jitter/interference_edf.v
+++ b/model/global/jitter/interference_edf.v
@@ 28,7 +28,7 @@ Module InterferenceEDF.
for EDF, i.e., if any job of tsk is backlogged, every processor
must be busy with jobs with no larger absolute deadline. *)
Hypothesis H_scheduler_uses_EDF:
 enforces_JLDP_policy job_cost job_jitter sched (EDF job_deadline).
+ respects_JLFP_policy job_cost job_jitter sched (EDF job_deadline).
(* Under EDF scheduling, a job only causes interference if its deadline
is not larger than the deadline of the analyzed job. *)
diff git a/model/global/jitter/platform.v b/model/global/jitter/platform.v
index c956b1bcef67022b77cebf7ec0924f4afbebce5f..3bc1422eaffa8f4e79ca4735f3d53ddb057d1ec9 100644
 a/model/global/jitter/platform.v
+++ b/model/global/jitter/platform.v
@@ 48,34 +48,53 @@ Module Platform.
End Execution.
+ Section FP.
+
+ (* An FP policy ...*)
+ Variable higher_eq_priority: FP_policy sporadic_task.
+
+ (* ... is respected by the schedule iff every scheduled
+ job has higher (or same) priority than (as) a backlogged job. *)
+ Definition respects_FP_policy :=
+ forall (j j_hp: JobIn arr_seq) t,
+ backlogged job_cost job_jitter sched j t >
+ scheduled sched j_hp t >
+ higher_eq_priority (job_task j_hp) (job_task j).
+
+ End FP.
+
+ Section JLFP.
+
+ (* A JLFP policy ...*)
+ Variable higher_eq_priority: JLFP_policy arr_seq.
+
+ (* ... is respected by the schedule iff at any time t,
+ a scheduled job has higher (or same) priority than (as)
+ a backlogged job. *)
+ Definition respects_JLFP_policy :=
+ forall (j j_hp: JobIn arr_seq) t,
+ backlogged job_cost job_jitter sched j t >
+ scheduled sched j_hp t >
+ higher_eq_priority j_hp j.
+
+ End JLFP.
+
Section JLDP.
 (* A JLFP/JLDP policy ...*)
+ (* A JLDP policy ...*)
Variable higher_eq_priority: JLDP_policy arr_seq.
 (* ... is enforced by the scheduler iff at any time t,
+ (* ... is respected by the schedule iff at any time t,
a scheduled job has higher (or same) priority than (as)
a backlogged job. *)
 Definition enforces_JLDP_policy :=
+ Definition respects_JLDP_policy :=
forall (j j_hp: JobIn arr_seq) t,
backlogged job_cost job_jitter sched j t >
scheduled sched j_hp t >
higher_eq_priority t j_hp j.
End JLDP.

 Section FP.

 (* Given an FP policy, ...*)
 Variable higher_eq_priority: FP_policy sporadic_task.
 (* ... this policy is enforced by the scheduler iff
 a corresponding JLDP policy is enforced by the scheduler. *)
 Definition enforces_FP_policy :=
 enforces_JLDP_policy (FP_to_JLDP job_task higher_eq_priority).

 End FP.

Section Lemmas.
(* Assume all jobs have valid parameters, ...*)
diff git a/model/priority.v b/model/priority.v
index 9dc73ad24f2191a1de8ce17788c9cb2de68fe115..c2b5bb7e3089af0fd6495fbeb5667aae04feca72 100644
 a/model/priority.v
+++ b/model/priority.v
@@ 1,49 +1,56 @@
Require Import rt.util.all.
Require Import rt.model.task rt.model.job rt.model.arrival_sequence.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq.
Set Implicit Arguments.
(* Definitions of FP and JLFP/JLDP priority relations. *)
+(* Definitions of FP, JLFP and JLDP priority relations. *)
Module Priority.
Import SporadicTaskset ArrivalSequence.
Section PriorityDefs.
 Section JLDP.
+ Section FP.
+
+ (* Let Task denote any type of task. *)
+ Variable Task: eqType.
+
+ (* We define an FP policy as a relation between tasks. *)
+ Definition FP_policy := rel Task.
+
+ End FP.
+
+ Section JLFP.
(* Consider any job arrival sequence. *)
Context {Job: eqType}.
Variable arr_seq: arrival_sequence Job.
 (* We define a JLDP policy as a relation between jobs in the
 arrival sequence at each point in time.
 Although this definition doesn't specify how the policy was
 constructed (e.g., whether it depends on the schedule, on
 job parameters, etc.), it is as general as possible.
 Knowing the priority of the jobs is sufficient to make
 scheduling decisions. *)
 Definition JLDP_policy := time > JobIn arr_seq > JobIn arr_seq > bool.
+ (* We define a JLFP policy as a relation between jobs in the arrival sequence. *)
+ Definition JLFP_policy := rel (JobIn arr_seq).
 End JLDP.
+ End JLFP.
 Section FP.
+ Section JLDP.
 (* Let Task denote any type of task. *)
 Variable Task: eqType.
+ (* Consider any job arrival sequence. *)
+ Context {Job: eqType}.
+ Variable arr_seq: arrival_sequence Job.
+
+ (* We define a JLDP policy as a timedependent relation between jobs
+ in the arrival sequence.
+ Although this definition doesn't specify how the policy was constructed
+ (e.g., whether it depends on the schedule, on job parameters, etc.), it is
+ as general as possible. Knowing the priority of the jobs is sufficient
+ to make scheduling decisions. *)
+ Definition JLDP_policy := time > rel (JobIn arr_seq).
 (* We define an FP policy as a relation between tasks. *)
 Definition FP_policy := Task > Task > bool.
+ End JLDP.
 End FP.

End PriorityDefs.
 (* To avoid repeating definitions for JLDP and FP policies,
 we state everything in terms of JLDP policies.
 For that, we define a function that converts the relation
 between tasks to a relation between jobs. *)
 Section GeneralizeFP.
+ (* Since FP policies are also JLFP and JLDP policies, we define
+ next conversion functions to do the generalization. *)
+ Section Generalization.
(* Consider any arrival sequence of jobs spawned by tasks. *)
Context {Task: eqType}.
@@ 51,40 +58,20 @@ Module Priority.
Variable job_task: Job > Task.
Variable arr_seq: arrival_sequence Job.
 (* We convert FP to JLDP policies using the following function. *)
 Definition FP_to_JLDP (task_hp: FP_policy Task) : JLDP_policy arr_seq :=
 fun (t: time) (jhigh jlow: JobIn arr_seq) =>
+ (* We show how to convert FP to JLFP,... *)
+ Definition FP_to_JLFP (task_hp: FP_policy Task) : JLFP_policy arr_seq :=
+ fun (jhigh jlow: JobIn arr_seq) =>
task_hp (job_task jhigh) (job_task jlow).

 End GeneralizeFP.

 (* Next, we define properties of a JLDP policy. *)
 Section PropertiesJLDP.

 (* Consider any JLDP policy. *)
 Context {Job: eqType}.
 Context {arr_seq: arrival_sequence Job}.
 Variable job_priority: JLDP_policy arr_seq.

 (* Now we define the properties. *)
 (* Whether the JLDP policy is reflexive. *)
 Definition JLDP_is_reflexive :=
 forall t, reflexive (job_priority t).

 (* Whether the JLDP policy is irreflexive. *)
 Definition JLDP_is_irreflexive :=
 forall t, irreflexive (job_priority t).

 (* Whether the JLDP policy is transitive. *)
 Definition JLDP_is_transitive :=
 forall t, transitive (job_priority t).

 (* Whether the JLDP policy is total. *)
 Definition JLDP_is_total :=
 forall t, total (job_priority t).
+ (* ...FP to JLDP, ... *)
+ Definition FP_to_JLDP (task_hp: FP_policy Task) : JLDP_policy arr_seq :=
+ fun (t: time) => FP_to_JLFP task_hp.
 End PropertiesJLDP.
+ (* ...and JLFP to JLDP. *)
+ Definition JLFP_to_JLDP (job_hp: JLFP_policy arr_seq) : JLDP_policy arr_seq :=
+ fun (t: time) => job_hp.
+
+ End Generalization.
(* Next we define properties of an FP policy. *)
Section PropertiesFP.
@@ 114,7 +101,7 @@ Module Priority.
Section Antisymmetry.
(* Consider any task set ts. *)
 Variable ts: taskset_of Task.
+ Variable ts: seq Task.
(* First we define whether task set ts is totally ordered with
the priority. *)
@@ 130,6 +117,58 @@ Module Priority.
End PropertiesFP.
+ (* Next, we define properties of a JLFP policy. *)
+ Section PropertiesJLFP.
+
+ (* Consider any JLFP policy. *)
+ Context {Job: eqType}.
+ Context {arr_seq: arrival_sequence Job}.
+ Variable job_priority: JLFP_policy arr_seq.
+
+ (* Now we define the properties. *)
+
+ (* Whether the JLFP policy is reflexive. *)
+ Definition JLFP_is_reflexive := reflexive job_priority.
+
+ (* Whether the JLFP policy is irreflexive. *)
+ Definition JLFP_is_irreflexive := irreflexive job_priority.
+
+ (* Whether the JLFP policy is transitive. *)
+ Definition JLFP_is_transitive := transitive job_priority.
+
+ (* Whether the JLFP policy is total. *)
+ Definition JLFP_is_total := total job_priority.
+
+ End PropertiesJLFP.
+
+ (* Next, we define properties of a JLDP policy. *)
+ Section PropertiesJLDP.
+
+ (* Consider any JLDP policy. *)
+ Context {Job: eqType}.
+ Context {arr_seq: arrival_sequence Job}.
+ Variable job_priority: JLDP_policy arr_seq.
+
+ (* Now we define the properties. *)
+
+ (* Whether the JLDP policy is reflexive. *)
+ Definition JLDP_is_reflexive :=
+ forall t, reflexive (job_priority t).
+
+ (* Whether the JLDP policy is irreflexive. *)
+ Definition JLDP_is_irreflexive :=
+ forall t, irreflexive (job_priority t).
+
+ (* Whether the JLDP policy is transitive. *)
+ Definition JLDP_is_transitive :=
+ forall t, transitive (job_priority t).
+
+ (* Whether the JLDP policy is total. *)
+ Definition JLDP_is_total :=
+ forall t, total (job_priority t).
+
+ End PropertiesJLDP.
+
(* Next we define some known FP policies. *)
Section KnownFPPolicies.
@@ 183,61 +222,35 @@ Module Priority.
End KnownFPPolicies.
 (* Next, we define the notion of JLFP policies. *)
 Section JLFP.

 Context {sporadic_task: eqType}.
 Context {Job: eqType}.
 Context {num_cpus: nat}.
 Context {arr_seq: arrival_sequence Job}.

 Variable is_higher_priority: JLDP_policy arr_seq.

 (* We call a policy JLFP iff job priorities do not vary with time. *)
 Definition is_JLFP_policy :=
 forall j1 j2 t t',
 is_higher_priority t j1 j2 > is_higher_priority t' j1 j2.

 End JLFP.

(* In this section, we define known JLFP policies. *)
Section KnownJLFPPolicies.
Context {Job: eqType}.
 Variable arr_seq: arrival_sequence Job.
+ Context {arr_seq: arrival_sequence Job}.
Variable job_deadline: Job > time.
(* Earliest deadline first (EDF) orders jobs by absolute deadlines. *)
 Definition EDF (t: time) (j1 j2: JobIn arr_seq) :=
+ Definition EDF (j1 j2: JobIn arr_seq) :=
job_arrival j1 + job_deadline j1 <= job_arrival j2 + job_deadline j2.
Section Properties.
 (* EDF is a JLFP policy. *)
 Lemma edf_JLFP : is_JLFP_policy EDF.
 Proof.
 by unfold is_JLFP_policy, EDF.
 Qed.

(* EDF is reflexive. *)
 Lemma EDF_is_reflexive : JLDP_is_reflexive EDF.
+ Lemma EDF_is_reflexive : JLFP_is_reflexive EDF.
Proof.
 unfold JLDP_is_reflexive, reflexive.
 by intros t j; apply leqnn.
+ by intros j; apply leqnn.
Qed.
(* EDF is transitive. *)
 Lemma EDF_is_transitive : JLDP_is_transitive EDF.
+ Lemma EDF_is_transitive : JLFP_is_transitive EDF.
Proof.
 unfold JLDP_is_transitive, transitive.
 by intros t y x z; apply leq_trans.
+ by intros y x z; apply leq_trans.
Qed.
(* EDF is total. *)
 Lemma EDF_is_total : JLDP_is_total EDF.
+ Lemma EDF_is_total : JLFP_is_total EDF.
Proof.
 unfold JLDP_is_total, total, EDF.
 intros _ x y.
+ unfold EDF; intros x y.
by case (leqP (job_arrival x + job_deadline x)
(job_arrival y + job_deadline y));
[by rewrite orTb  by move/ltnW => >].
diff git a/model/suspension.v b/model/suspension.v
new file mode 100644
index 0000000000000000000000000000000000000000..d8d7090889c3036338825d7dab81291ed63decc2
 /dev/null
+++ b/model/suspension.v
@@ 0,0 +1,69 @@
+Require Import rt.util.all.
+Require Import rt.model.arrival_sequence.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq bigop.
+
+Module Suspension.
+
+ Import ArrivalSequence.
+
+ (* First, we define the actual job suspension times. *)
+ Section SuspensionTimes.
+
+ (* Consider any type of job. *)
+ Variable Job: eqType.
+
+ (* We define job suspension as a function that takes a job in the arrival
+ sequence and its current service and returns how long the job must
+ suspend next. *)
+ Definition job_suspension := Job > (* job *)
+ time > (* current service *)
+ time. (* duration of next suspension *)
+
+ End SuspensionTimes.
+
+ (* Next, we define the total suspension time incurred by a job. *)
+ Section TotalSuspensionTime.
+
+ Context {Job: eqType}.
+ Variable job_cost: Job > time.
+
+ (* Consider any job suspension function. *)
+ Variable next_suspension: job_suspension Job.
+
+ (* Let j be any job. *)
+ Variable j: Job.
+
+ (* We define the total suspension time incurred by job j as the cumulative
+ duration of each suspension point t in the interval [0, job_cost j). *)
+ Definition total_suspension :=
+ \sum_(0 <= t < job_cost j) (next_suspension j t).
+
+ End TotalSuspensionTime.
+
+ (* In this section, we define the dynamic selfsuspension model as an
+ upper bound on the total suspension times. *)
+ Section DynamicSuspensions.
+
+ Context {Task: eqType}.
+ Context {Job: eqType}.
+ Variable job_cost: Job > time.
+ Variable job_task: Job > Task.
+
+ (* Consider any job arrival sequence subject to job suspensions. *)
+ Variable next_suspension: job_suspension Job.
+
+ (* Recall the definition of total suspension time. *)
+ Let total_job_suspension := total_suspension job_cost next_suspension.
+
+ (* Next, assume that for each task a suspension bound is known. *)
+ Variable suspension_bound: Task > time.
+
+ (* Then, we say that the arrival sequence satisfies the dynamic
+ suspension model iff the total suspension time of each job is no
+ larger than the suspension bound of its task. *)
+ Definition dynamic_suspension_model :=
+ forall j, total_job_suspension j <= suspension_bound (job_task j).
+
+ End DynamicSuspensions.
+
+End Suspension.
\ No newline at end of file
diff git a/model/uni/basic/busy_interval.v b/model/uni/basic/busy_interval.v
index 4514e7b750aa4897c904cdcdd60e475edc768f75..af8241ab490f7586a41bcb0bbe1d64037abc2919 100644
 a/model/uni/basic/busy_interval.v
+++ b/model/uni/basic/busy_interval.v
@@ 19,28 +19,26 @@ Module BusyInterval.
Variable job_cost: Job > time.
Variable job_task: Job > Task.
 (* Assume any FP policy... *)
 Variable higher_eq_priority: FP_policy Task.

 (* ...and consider any uniprocessor schedule. *)
+ (* Consider any uniprocessor schedule, ... *)
Context {arr_seq: arrival_sequence Job}.
Variable sched: schedule arr_seq.
 (* Let tsk be the task to be analyzed. *)
 Variable tsk: Task.
+ (* ...along with a JLFP policy. *)
+ Variable higher_eq_priority: JLFP_policy arr_seq.
+
+ (* Let j be the job to be analyzed. *)
+ Variable j: JobIn arr_seq.
(* For simplicity, let's define some local names. *)
Let job_pending_at := pending job_cost sched.
Let job_scheduled_at := scheduled_at sched.
Let job_completed_by := completed_by job_cost sched.
 Let higher_or_equal_priority_job j_other :=
 higher_eq_priority (job_task j_other) tsk.
 (* We say that t is a quiet time for tsk iff every higherpriority
+ (* We say that t is a quiet time for j iff every higherpriority
job that arrived before t has completed by that time. *)
Definition quiet_time (t: time) :=
forall (j_hp: JobIn arr_seq),
 higher_or_equal_priority_job j_hp >
+ higher_eq_priority j_hp j >
arrived_before j_hp t >
job_completed_by j_hp t.
@@ 69,18 +67,13 @@ Module BusyInterval.
Section BasicLemmas.
(* Assume that the priority relation is reflexive. *)
 Hypothesis H_priority_is_reflexive:
 FP_is_reflexive higher_eq_priority.
+ Hypothesis H_priority_is_reflexive: JLFP_is_reflexive higher_eq_priority.
 (* Consider any busy interval [t1, t2). *)
+ (* Consider any busy interval [t1, t2)... *)
Variable t1 t2: time.
Hypothesis H_busy_interval: busy_interval t1 t2.
 (* Let j be any job of tsk... *)
 Variable j: JobIn arr_seq.
 Hypothesis H_job_of_tsk: job_task j = tsk.

 (* ...that is pending during the busy interval. *)
+ (* ...and assume that job j is pending during this busy interval. *)
Variable t: time.
Hypothesis H_during_interval: t1 <= t < t2.
Hypothesis H_job_is_pending: job_pending_at j t.
@@ 91,16 +84,14 @@ Module BusyInterval.
Lemma job_completes_within_busy_interval:
job_completed_by j t2.
Proof.
 rename H_priority_is_reflexive into REFL,
 H_busy_interval into BUSY, H_job_of_tsk into JOBtsk,
+ rename H_priority_is_reflexive into REFL, H_busy_interval into BUSY,
H_during_interval into INT, H_job_is_pending into PEND.
move: BUSY => [_ QUIET].
move: INT => /andP [_ LT2].
 apply QUIET;
 first by rewrite /higher_or_equal_priority_job JOBtsk REFL.
+ apply QUIET; first by apply REFL.
apply leq_ltn_trans with (n := t); last by done.
by move: PEND => /andP [ARR _].
 Qed.
+ Qed.
End CompletesDuringBusyInterval.
@@ 116,8 +107,7 @@ Module BusyInterval.
Lemma job_arrives_within_busy_interval:
t1 <= job_arrival j.
Proof.
 rename H_priority_is_reflexive into REFL,
 H_busy_interval into BUSY, H_job_of_tsk into JOBtsk,
+ rename H_priority_is_reflexive into REFL, H_busy_interval into BUSY,
H_during_interval into INT, H_job_is_pending into PEND.
apply contraT; rewrite ltnNge; intro LT1.
move: BUSY => [[_ [QUIET _]] _].
@@ 125,8 +115,7 @@ Module BusyInterval.
move: INT => /andP [LE _].
exfalso; apply NOTCOMP.
apply completion_monotonic with (t0 := t1); try (by done).
 by apply QUIET;
 first by rewrite /higher_or_equal_priority_job JOBtsk REFL.
+ by apply QUIET; first by apply REFL.
Qed.
End ArrivesDuringBusyInterval.
@@ 151,31 +140,29 @@ Module BusyInterval.
(* Then, we prove that there exists a job pending at time t2
that has higher or equal priority (with respect ot tsk). *)
Lemma not_quiet_implies_exists_pending_job:
 exists (j: JobIn arr_seq),
 arrived_between j t1 t2 /\
 higher_eq_priority (job_task j) tsk /\
 ~ job_completed_by j t2.
+ exists (j_hp: JobIn arr_seq),
+ arrived_between j_hp t1 t2 /\
+ higher_eq_priority j_hp j /\
+ ~ job_completed_by j_hp t2.
Proof.
rename H_quiet into QUIET, H_not_quiet into NOTQUIET.
 set hep := higher_eq_priority.
 destruct (has (fun j => (~~ job_completed_by j t2) && hep (job_task j) tsk)
+ destruct (has (fun j_hp => (~~ job_completed_by j_hp t2) && higher_eq_priority j_hp j)
(arrivals_between t1 t2)) eqn:COMP.
{
 move: COMP => /hasP [j ARR /andP [NOTCOMP HP]].
 exists j; repeat split; [  by done  by apply/negP].
+ move: COMP => /hasP [j_hp ARR /andP [NOTCOMP HP]].
+ exists j_hp; repeat split; [  by done  by apply/negP].
rewrite mem_filter in ARR; move: ARR => /andP [GE ARR].
by apply/andP; split; last by apply JobIn_arrived.
}
{
apply negbT in COMP; rewrite all_predC in COMP.
move: COMP => /allP COMP.
 exfalso; apply NOTQUIET; intros j HP ARR.
 destruct (ltnP (job_arrival j) t1) as [BEFORE  AFTER];
 first by specialize (QUIET j HP BEFORE); apply completion_monotonic with (t := t1).
 feed (COMP j);
+ exfalso; apply NOTQUIET; intros j_hp HP ARR.
+ destruct (ltnP (job_arrival j_hp) t1) as [BEFORE  AFTER];
+ first by specialize (QUIET j_hp HP BEFORE); apply completion_monotonic with (t := t1).
+ feed (COMP j_hp);
first by rewrite mem_filter; apply/andP; split; last by apply JobIn_arrived.
 unfold higher_or_equal_priority_job in *.
 by rewrite /= /hep HP andbT negbK in COMP.
+ by rewrite /= HP andbT negbK in COMP.
}
Qed.
@@ 240,52 +227,49 @@ Module BusyInterval.
(* In fact, we can infer a stronger property. *)
Section OnlyHigherOrEqualPriority.
 (* If the schedule enforces an FP policy that is transitive, ...*)
 Hypothesis H_fixed_priority:
 enforces_FP_policy job_cost job_task sched higher_eq_priority.
 Hypothesis H_priority_is_transitive:
 FP_is_transitive higher_eq_priority.
+ (* If the JLFP policy is transitive and is respected by the schedule, ...*)
+ Hypothesis H_priority_is_transitive: JLFP_is_transitive higher_eq_priority.
+ Hypothesis H_respects_policy: respects_JLFP_policy job_cost sched higher_eq_priority.
 (* ... then the processor is always busy with a job of higher
 or equal priority (with respect to tsk). *)
+ (* ... then the processor is always busy with a job of higher or equal priority. *)
Lemma not_quiet_implies_exists_scheduled_hp_job:
forall t,
t1 <= t < t2 >
exists j_hp,
arrived_between j_hp t1 t2 /\
 higher_eq_priority (job_task j_hp) tsk /\
+ higher_eq_priority j_hp j /\
job_scheduled_at j_hp t.
Proof.
have NOTIDLE := not_quiet_implies_not_idle.
unfold is_idle, FP_is_transitive, transitive in *.
rename H_not_quiet into NOTQUIET, H_quiet into QUIET, H_priority_is_transitive into TRANS,
 H_work_conserving into WORK, H_fixed_priority into FP.
+ H_work_conserving into WORK, H_respects_policy into PRIO.
move => t /andP [GEt LEt].
feed (NOTIDLE t); first by apply/andP; split; last by apply ltnW.
 destruct (sched t) eqn:SCHED; [clear NOTIDLE  by exfalso; apply NOTIDLE].
+ destruct (sched t) as [j_hp] eqn:SCHED; [clear NOTIDLE  by exfalso; apply NOTIDLE].
move: SCHED => /eqP SCHED.
 exists j.
 have HP: higher_eq_priority (job_task j) tsk.
+ exists j_hp.
+ have HP: higher_eq_priority j_hp j.
{
apply contraT; move => /negP NOTHP; exfalso.
feed (NOTQUIET t.+1); first by apply/andP; split.
apply NOTQUIET.
 unfold quiet_time, higher_or_equal_priority_job in *; intros j_hp HP ARR.
+ unfold quiet_time in *; intros j_hp' HP ARR.
apply contraT; move => /negP NOTCOMP'; exfalso.
 have BACK: backlogged job_cost sched j_hp t.
+ have BACK: backlogged job_cost sched j_hp' t.
{
apply/andP; split; last first.
{
apply/negP; intro SCHED'.
 apply only_one_job_scheduled with (j1 := j) in SCHED'; last by done.
 by subst j_hp; rewrite HP in NOTHP.
+ apply only_one_job_scheduled with (j1 := j_hp) in SCHED'; last by done.
+ by subst; rewrite HP in NOTHP.
}
apply/andP; split; first by done.
apply/negP; intro COMP; apply NOTCOMP'.
by apply completion_monotonic with (t0 := t).
}
 feed (FP j_hp j t BACK); first by done.
 by apply NOTHP, TRANS with (y := (job_task j_hp)).
+ feed (PRIO j_hp' j_hp t BACK); first by done.
+ by apply NOTHP, TRANS with (y := j_hp').
}
repeat split; [ by done  by done].
{
@@ 294,9 +278,8 @@ Module BusyInterval.
apply/andP; split;
last by apply leq_ltn_trans with (n := t); first by move: PENDING => /andP [ARR _].
apply contraT; rewrite ltnNge; intro LT; exfalso.
 feed (QUIET j); first by done.
 specialize (QUIET LT).
 have COMP: job_completed_by j t by apply completion_monotonic with (t0 := t1).
+ specialize (QUIET j_hp HP LT).
+ have COMP: job_completed_by j_hp t by apply completion_monotonic with (t0 := t1).
apply completed_implies_not_scheduled in COMP; last by done.
by move: COMP => /negP COMP; apply COMP.
}
@@ 321,25 +304,20 @@ Module BusyInterval.
(* Also assume a workconserving FP schedule, ... *)
Hypothesis H_work_conserving: work_conserving job_cost sched.
 Hypothesis H_enforces_fp_policy:
 enforces_FP_policy job_cost job_task sched higher_eq_priority.
+ Hypothesis H_respects_policy: respects_JLFP_policy job_cost sched higher_eq_priority.
(* ...in which the priority relation is reflexive and transitive. *)
 Hypothesis H_priority_is_reflexive: FP_is_reflexive higher_eq_priority.
 Hypothesis H_priority_is_transitive: FP_is_transitive higher_eq_priority.
+ Hypothesis H_priority_is_reflexive: JLFP_is_reflexive higher_eq_priority.
+ Hypothesis H_priority_is_transitive: JLFP_is_transitive higher_eq_priority.
(* Let's recall the notions of service and workload of tasks with higher or equal
priority (with respect to tsk). *)
Let hp_service :=
 service_of_higher_or_equal_priority sched job_task higher_eq_priority tsk.
+ service_of_higher_or_equal_priority_jobs sched higher_eq_priority j.
Let hp_workload :=
 workload_of_higher_or_equal_priority job_cost job_task arr_seq higher_eq_priority tsk.

 (* Now we begin the proof. Let j be any job of tsk. *)
 Variable j: JobIn arr_seq.
 Hypothesis H_job_of_tsk: job_task j = tsk.
+ workload_of_higher_or_equal_priority_jobs job_cost arr_seq higher_eq_priority j.
 (* In this section, we show that the busy interval is bounded. *)
+ (* Now we begin the proof. First, we show that the busy interval is bounded. *)
Section BoundingBusyInterval.
(* Suppose that job j is pending at time t_busy. *)
@@ 356,14 +334,13 @@ Module BusyInterval.
busy_interval_prefix t1 t_busy.+1 /\
t1 <= job_arrival j <= t_busy.
Proof.
 rename H_j_is_pending into PEND, H_job_of_tsk into JOBtsk,
 H_work_conserving into WORK, H_priority_is_reflexive into REFL,
 H_enforces_fp_policy into FP.
+ rename H_j_is_pending into PEND, H_respects_policy into PRIO,
+ H_work_conserving into WORK, H_priority_is_reflexive into REFL.
unfold busy_interval_prefix.
set dec_quiet :=
fun t => all
 (fun (j: JobIn arr_seq) =>
 higher_eq_priority (job_task j) tsk ==> (completed_by job_cost sched j t))
+ (fun (j_hp: JobIn arr_seq) =>
+ higher_eq_priority j_hp j ==> (completed_by job_cost sched j_hp t))
(jobs_arrived_before arr_seq t).
destruct ([exists t:'I_t_busy.+1, dec_quiet t]) eqn:EX.
{
@@ 382,8 +359,7 @@ Module BusyInterval.
{
apply/andP; split; last by move: PEND => /andP [ARR _].
apply contraT; rewrite ltnNge; intros BEFORE.
 unfold quiet_time, higher_or_equal_priority_job in *.
 feed (QUIET j); first by rewrite JOBtsk REFL.
+ feed (QUIET j); first by apply REFL.
specialize (QUIET BEFORE).
move: PEND => /andP [_ NOTCOMP].
apply completion_monotonic with (t' := t_busy) in QUIET;
@@ 462,13 +438,13 @@ Module BusyInterval.
feed_n 3 EXISTS; try (by done).
apply eq_trans with (y := \sum_(t1 <= t < t1 + delta) 1);
last by simpl_sum_const; rewrite addKn.
 unfold hp_service, service_of_higher_or_equal_priority, service_of_jobs.
+ unfold hp_service, service_of_higher_or_equal_priority_jobs, service_of_jobs.
rewrite exchange_big /=.
apply eq_big_nat; move => t /andP [GEt LTt].
move: PREFIX => [_ [QUIET _]].
have EX: exists j_hp : JobIn arr_seq,
arrived_between j_hp t1 (t1 + delta) /\
 higher_eq_priority (job_task j_hp) tsk /\
+ higher_eq_priority j_hp j /\
scheduled_at sched j_hp t.
{
apply EXISTS with (t1 := t1) (t2 := t1 + delta); try (by done);
@@ 480,7 +456,7 @@ Module BusyInterval.
 by rewrite filter_uniq //; apply JobIn_uniq.
 by rewrite mem_filter; apply/andP; split; last by apply JobIn_arrived.
rewrite HP big1; first by rewrite /service_at SCHED addn0.
 intros j' NEQ; destruct (higher_eq_priority (job_task j') tsk); last by done.
+ intros j' NEQ; destruct (higher_eq_priority j' j); last by done.
apply/eqP; rewrite eqb0; apply/negP; move => SCHED'.
move: NEQ => /eqP NEQ; apply NEQ.
by apply only_one_job_scheduled with (sched0 := sched) (t0 := t).
@@ 494,11 +470,11 @@ Module BusyInterval.
have PEND := not_quiet_implies_exists_pending_job
H_completed_jobs_dont_execute.
rename H_no_quiet_time into NOTQUIET,
 H_is_busy_prefix into PREFIX, H_enforces_fp_policy into FP.
+ H_is_busy_prefix into PREFIX, H_respects_policy into PRIO.
set l := jobs_arrived_between arr_seq t1 (t1 + delta).
set hep := higher_eq_priority.
 unfold hp_service, service_of_higher_or_equal_priority, service_of_jobs,
 hp_workload, workload_of_higher_or_equal_priority, workload_of_jobs.
+ unfold hp_service, service_of_higher_or_equal_priority_jobs, service_of_jobs,
+ hp_workload, workload_of_higher_or_equal_priority_jobs, workload_of_jobs.
fold arrivals_between l hep.
move: (PREFIX) => [_ [QUIET _]].
move: (NOTQUIET) => NOTQUIET'.
@@ 519,7 +495,7 @@ Module BusyInterval.
apply leq_add; last first.
{
apply leq_sum; intros j1 NEQ.
 destruct (higher_eq_priority (job_task j1) tsk); last by done.
+ destruct (higher_eq_priority j1 j); last by done.
by apply cumulative_service_le_job_cost.
}
rewrite ltn_neqAle; apply/andP; split; last by apply cumulative_service_le_job_cost.
@@ 553,8 +529,8 @@ Module BusyInterval.
set dec_quiet :=
fun t => all
 (fun (j: JobIn arr_seq) =>
 higher_eq_priority (job_task j) tsk ==> (completed_by job_cost sched j t))
+ (fun (j_hp: JobIn arr_seq) =>
+ higher_eq_priority j_hp j ==> (completed_by job_cost sched j_hp t))
(jobs_arrived_before arr_seq t).
destruct ([exists t2:'I_(t1 + delta).+1, (t2 > t1) && dec_quiet t2]) eqn:EX.
@@ 675,7 +651,6 @@ Module BusyInterval.
job_completed_by j (job_arrival j + delta).
Proof.
have BUSY := exists_busy_interval delta.
 rename H_job_of_tsk into JOBtsk.
destruct (job_cost j == 0) eqn:COST.
{
move: COST => /eqP COST.
diff git a/model/uni/basic/platform.v b/model/uni/basic/platform.v
index 7c8f1abe97f8b03ad0e11a3a65b3adb90e66d3b8..254f95339c98873a1a5a5e9209dda3ed240bbc25 100644
 a/model/uni/basic/platform.v
+++ b/model/uni/basic/platform.v
@@ 36,15 +36,47 @@ Module Platform.
End Execution.
+ (* Next, we define properties related to FP scheduling. *)
+ Section FP.
+
+ (* We say that an FP policy...*)
+ Variable higher_eq_priority: FP_policy sporadic_task.
+
+ (* ...is respected by the schedule iff a scheduled task has
+ higher (or same) priority than (as) any backlogged task. *)
+ Definition respects_FP_policy :=
+ forall (j j_hp: JobIn arr_seq) t,
+ backlogged job_cost sched j t >
+ scheduled_at sched j_hp t >
+ higher_eq_priority (job_task j_hp) (job_task j).
+
+ End FP.
+
+ (* Next, we define properties related to JLFP policies. *)
+ Section JLFP.
+
+ (* We say that a JLFP policy ...*)
+ Variable higher_eq_priority: JLFP_policy arr_seq.
+
+ (* ... is respected by the scheduler iff a scheduled job has
+ higher (or same) priority than (as) any backlogged job. *)
+ Definition respects_JLFP_policy :=
+ forall (j j_hp: JobIn arr_seq) t,
+ backlogged job_cost sched j t >
+ scheduled_at sched j_hp t >
+ higher_eq_priority j_hp j.
+
+ End JLFP.
+
(* Next, we define properties related to JLDP policies. *)
Section JLDP.
(* We say that a JLFP/JLDP policy ...*)
Variable higher_eq_priority: JLDP_policy arr_seq.
 (* ... is enforced by the scheduler iff at any time t, a scheduled job
+ (* ... is respected by the scheduler iff at any time t, a scheduled job
has higher (or same) priority than (as) any backlogged job. *)
 Definition enforces_JLDP_policy :=
+ Definition respects_JLDP_policy :=
forall (j j_hp: JobIn arr_seq) t,
backlogged job_cost sched j t >
scheduled_at sched j_hp t >
@@ 52,19 +84,6 @@ Module Platform.
End JLDP.
 (* Next, we define properties related to FP scheduling. *)
 Section FP.

 (* We say that an FP policy...*)
 Variable higher_eq_priority: FP_policy sporadic_task.

 (* ...is enforced by the scheduler iff the corresponding JLDP
 policy is enforced by the scheduler. *)
 Definition enforces_FP_policy :=
 enforces_JLDP_policy (FP_to_JLDP job_task higher_eq_priority).

 End FP.

End Properties.
(* In this section, we prove some lemmas about the processor platform. *)
diff git a/model/uni/service.v b/model/uni/service.v
index ad610b33222916c895ca538207922b729aa16483..9f4be4dbce5c0505f1f2ba618e375e9f7c7d0e47 100644
 a/model/uni/service.v
+++ b/model/uni/service.v
@@ 27,7 +27,7 @@ Module Service.
Section ServiceOfJobs.
(* Given any predicate over jobs, ...*)
 Variable P: Job > bool.
+ Variable P: JobIn arr_seq > bool.
(* ...we define the cumulative service received during [t1, t2)
by the jobs that satisfy this predicate. *)
@@ 36,8 +36,9 @@ Module Service.
End ServiceOfJobs.
 (* Next, we define the service received by tasks with higher or equal priority. *)
 Section PerPriorityLevel.
+ (* Then, we define the service received by tasks with higher or equal priority
+ under FP policies. *)
+ Section PerTaskPriority.
Context {Task: eqType}.
Variable job_task: Job > Task.
@@ 52,10 +53,29 @@ Module Service.
Let of_higher_or_equal_priority j := higher_eq_priority (job_task j) tsk.
(* ...we define the service received during [t1, t2) by jobs of higher or equal priority. *)
 Definition service_of_higher_or_equal_priority (t1 t2: time) :=
+ Definition service_of_higher_or_equal_priority_tasks (t1 t2: time) :=
+ service_of_jobs of_higher_or_equal_priority t1 t2.
+
+ End PerTaskPriority.
+
+ (* Next, we define the service received by jobs with higher or equal priority
+ under JLFP policies. *)
+ Section PerJobPriority.
+
+ (* Consider any JLDP policy. *)
+ Variable higher_eq_priority: JLFP_policy arr_seq.
+
+ (* Let j be the job to be analyzed. *)
+ Variable j: JobIn arr_seq.
+
+ (* Based on the definition of jobs of higher or equal priority, ... *)
+ Let of_higher_or_equal_priority j_hp := higher_eq_priority j_hp j.
+
+ (* ...we define the service received during [t1, t2) by jobs of higher or equal priority. *)
+ Definition service_of_higher_or_equal_priority_jobs (t1 t2: time) :=
service_of_jobs of_higher_or_equal_priority t1 t2.
 End PerPriorityLevel.
+ End PerJobPriority.
End Definitions.
diff git a/model/uni/susp/platform.v b/model/uni/susp/platform.v
new file mode 100644
index 0000000000000000000000000000000000000000..f645397e4d794f6e98bc3ef0efad9d4ba9c5876b
 /dev/null
+++ b/model/uni/susp/platform.v
@@ 0,0 +1,98 @@
+Require Import rt.util.all.
+Require Import rt.model.arrival_sequence rt.model.suspension
+ rt.model.priority.
+Require Import rt.model.uni.susp.schedule.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+
+Module PlatformWithSuspensions.
+
+ Export ScheduleWithSuspensions Priority.
+
+ Section Definitions.
+
+ Context {Task: eqType}.
+ Context {Job: eqType}.
+ Variable job_cost: Job > time.
+ Variable job_task: Job > Task.
+
+ (* Assume that job suspension times are given. *)
+ Variable next_suspension: job_suspension Job.
+
+ (* Consider any uniprocessor schedule. *)
+ Context {arr_seq: arrival_sequence Job}.
+ Variable sched: schedule arr_seq.
+
+ (* For simplicity, let's recall the definitions of pending, scheduled, and backlogged job.
+ Note that this notion of backlogged is specific for suspensionaware schedulers. *)
+ Let job_pending_at := pending job_cost sched.
+ Let job_scheduled_at := scheduled_at sched.
+ Let job_backlogged_at := backlogged job_cost next_suspension sched.
+
+ (* In this section, we define schedule constraints for suspensionaware schedules. *)
+ Section ScheduleConstraints.
+
+ (* First, we consider constraints related to execution. *)
+ Section Execution.
+
+ (* We say that a scheduler is workconserving iff whenever a job j
+ is backlogged, the processor is always busy with another job. *)
+ Definition work_conserving :=
+ forall j t,
+ job_backlogged_at j t >
+ exists j_other, job_scheduled_at j_other t.
+
+ End Execution.
+
+ (* Next, we consider constraints related to FP policies. *)
+ Section FP.
+
+ (* We say that an FP policy...*)
+ Variable higher_eq_priority: FP_policy Task.
+
+ (* ... is respected by the scheduler iff at any time t, a scheduled job
+ has higher (or same) priority than (as) any backlogged job. *)
+ Definition respects_FP_policy :=
+ forall (j j_hp: JobIn arr_seq) t,
+ job_backlogged_at j t >
+ job_scheduled_at j_hp t >
+ higher_eq_priority (job_task j_hp) (job_task j).
+
+ End FP.
+
+ (* Next, we consider constraints related to JLFP policies. *)
+ Section JLFP.
+
+ (* We say that a JLFP policy ...*)
+ Variable higher_eq_priority: JLFP_policy arr_seq.
+
+ (* ... is respected by the scheduler iff every scheduled job
+ has higher (or same) priority than (as) any backlogged job. *)
+ Definition respects_JLFP_policy :=
+ forall (j j_hp: JobIn arr_seq) t,
+ job_backlogged_at j t >
+ job_scheduled_at j_hp t >
+ higher_eq_priority j_hp j.
+
+ End JLFP.
+
+ (* Next, we consider constraints related to JLDP policies. *)
+ Section JLDP.
+
+ (* We say that a JLDP policy ...*)
+ Variable higher_eq_priority: JLDP_policy arr_seq.
+
+ (* ... is respected by the scheduler iff at any time t, a scheduled job
+ has higher (or same) priority than (as) any backlogged job. *)
+ Definition respects_JLDP_policy :=
+ forall (j j_hp: JobIn arr_seq) t,
+ job_backlogged_at j t >
+ job_scheduled_at j_hp t >
+ higher_eq_priority t j_hp j.
+
+ End JLDP.
+
+ End ScheduleConstraints.
+
+ End Definitions.
+
+End PlatformWithSuspensions.
\ No newline at end of file
diff git a/model/uni/susp/schedule.v b/model/uni/susp/schedule.v
new file mode 100644
index 0000000000000000000000000000000000000000..3d71b85463266ced21eef8568ce9518e001b2e50
 /dev/null
+++ b/model/uni/susp/schedule.v
@@ 0,0 +1,48 @@
+Require Import rt.util.all.
+Require Import rt.model.arrival_sequence rt.model.suspension
+ rt.model.priority.
+Require Import rt.model.uni.schedule.
+Require Import rt.model.uni.susp.suspension_intervals.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+
+Module ScheduleWithSuspensions.
+
+ Export UniprocessorSchedule SuspensionIntervals.
+
+ Section Definitions.
+
+ Context {Task: eqType}.
+ Context {Job: eqType}.
+ Variable job_cost: Job > time.
+
+ (* Assume that job suspension times are given. *)
+ Variable next_suspension: job_suspension Job.
+
+ (* Consider any uniprocessor schedule. *)
+ Context {arr_seq: arrival_sequence Job}.
+ Variable sched: schedule arr_seq.
+
+ (* Recall the predicates that denote whether a job is scheduled
+ and suspended. *)
+ Let job_pending_at := pending job_cost sched.
+ Let job_scheduled_at := scheduled_at sched.
+ Let job_suspended_at := suspended_at job_cost next_suspension sched.
+
+ (* First, we redefine the notion of backlogged job to account for suspensions. *)
+ Section BackloggedJob.
+
+ (* We say that job j...*)
+ Variable j: JobIn arr_seq.
+
+ (* ...is backlogged at time t iff it is pending and neither
+ scheduled nor suspended. *)
+ Definition backlogged (t: time) :=
+ job_pending_at j t
+ && ~~ job_scheduled_at j t
+ && ~~ job_suspended_at j t.
+
+ End BackloggedJob.
+
+ End Definitions.
+
+End ScheduleWithSuspensions.
\ No newline at end of file
diff git a/model/uni/susp/suspension_intervals.v b/model/uni/susp/suspension_intervals.v
new file mode 100644
index 0000000000000000000000000000000000000000..fdb361b1796c8e9f9d098baa8909f0a9909808a0
 /dev/null
+++ b/model/uni/susp/suspension_intervals.v
@@ 0,0 +1,820 @@
+Require Import rt.util.all.
+Require Import rt.model.job rt.model.arrival_sequence rt.model.suspension.
+Require Import rt.model.uni.schedule.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+
+Module SuspensionIntervals.
+
+ Export Job UniprocessorSchedule Suspension.
+
+ (* In this section we define job suspension intervals in a schedule. *)
+ Section DefiningSuspensionIntervals.
+
+ Context {Job: eqType}.
+ Variable job_cost: Job > time.
+
+ (* Consider any job suspension times... *)
+ Variable next_suspension: job_suspension Job.
+
+ (* ...and any uniprocessor schedule. *)
+ Context {arr_seq: arrival_sequence Job}.
+ Variable sched: schedule arr_seq.
+
+ (* For simplicity, let's define some local names. *)
+ Let job_scheduled_at := scheduled_at sched.
+ Let job_completed_by := completed_by job_cost sched.
+
+ (* In this section, we define when jobs may begin to suspend. *)
+ Section BeginningOfSuspension.
+
+ Section Defs.
+
+ (* Let j be any job in the arrival sequence. *)
+ Variable j: JobIn arr_seq.
+
+ (* Next, we will show how to find the most recent selfsuspension
+ incurred by job j in the interval [0, t], if exists.
+ As we will show next, that corresponds to the time after the most
+ recent execution of job in the interval [0, t). *)
+ Variable t: time.
+
+ (* Let scheduled_before denote whether job j was scheduled in the interval [0, t). *)
+ Let scheduled_before :=
+ [exists t0: 'I_t, job_scheduled_at j t0].
+
+ (* In case j was scheduled before, we define the last time in which j was scheduled. *)
+ Let last_time_scheduled :=
+ \max_(t_last < t  job_scheduled_at j t_last) t_last.
+
+ (* Then, the most recent selfsuspension of job j in the interval [0, t], if exists,
+ occurs:
+ (a) immediately after the last time in which job j was scheduled, or,
+ (b) if j was never scheduled, at the arrival time of j. *)
+ Definition time_after_last_execution :=
+ if scheduled_before then
+ last_time_scheduled + 1
+ else job_arrival j.
+
+ End Defs.
+
+ (* Next, we prove lemmas about the time following the last execution. *)
+ Section Lemmas.
+
+ (* Let j be any job in the arrival sequence. *)
+ Variable j: JobIn arr_seq.
+
+ (* In this section, we show that the time after the last execution occurs
+ no earlier than the arrival of the job. *)
+ Section JobHasArrived.
+
+ (* Assume that jobs do not execute before they arrived. *)
+ Hypothesis H_jobs_must_arrive_to_execute:
+ jobs_must_arrive_to_execute sched.
+
+ (* Then, the time following the last execution of job j in the
+ interval [0, t) occurs no earlier than the arrival of j. *)
+ Lemma last_execution_after_arrival:
+ forall t,
+ has_arrived j (time_after_last_execution j t).
+ Proof.
+ unfold time_after_last_execution, has_arrived; intros t.
+ case EX: [exists _, _]; last by done.
+ move: EX => /existsP [t0 SCHED].
+ apply leq_trans with (n := t0 + 1);
+ last by rewrite leq_add2r; apply leq_bigmax_cond.
+ apply leq_trans with (n := t0); last by rewrite addn1.
+ by apply H_jobs_must_arrive_to_execute.
+ Qed.
+
+ End JobHasArrived.
+
+ (* Next, we establish the monotonicity of the function. *)
+ Section Monotonicity.
+
+ (* Assume that jobs do not execute before they arrived. *)
+ Hypothesis H_jobs_must_arrive_to_execute:
+ jobs_must_arrive_to_execute sched.
+
+ (* Let t1 be any time no earlier than the arrival of job j. *)
+ Variable t1: time.
+ Hypothesis H_after_arrival: has_arrived j t1.
+
+ (* Then, (time_after_last_execution j) grows monotonically
+ after that point. *)
+ Lemma last_execution_monotonic:
+ forall t2,
+ t1 <= t2 >
+ time_after_last_execution j t1 <= time_after_last_execution j t2.
+ Proof.
+ rename H_jobs_must_arrive_to_execute into ARR.
+ intros t2 LE12.
+ rewrite /time_after_last_execution.
+ case EX1: [exists _, _].
+ {
+ move: EX1 => /existsP [t0 SCHED0].
+ have EX2: [exists t:'I_t2, job_scheduled_at j t].
+ {
+ have LT: t0 < t2 by apply: (leq_trans _ LE12).
+ by apply/existsP; exists (Ordinal LT).
+ }
+ rewrite EX2 2!addn1.
+ set m1 := \max_(_ < t1  _)_.
+ have LTm1: m1 < t2.
+ {
+ apply: (leq_trans _ LE12).
+ by apply bigmax_ltn_ord with (i0 := t0).
+ }
+ apply leq_ltn_trans with (n := Ordinal LTm1); first by done.
+ by apply leq_bigmax_cond, (bigmax_pred _ _ t0).
+ }
+ {
+ case EX2: [exists _, _]; last by done.
+ move: EX2 => /existsP [t0 SCHED0].
+ set m2 := \max_(_ < t2  _)_.
+ rewrite addn1 ltnW // ltnS.
+ have SCHED2: scheduled_at sched j m2 by apply (bigmax_pred _ _ t0).
+ by apply ARR in SCHED2.
+ }
+ Qed.
+
+ End Monotonicity.
+
+ (* Next, we prove that the function is idempotent. *)
+ Section Idempotence.
+
+ (* Assume that jobs do not execute before they arrived. *)
+ Hypothesis H_jobs_must_arrive_to_execute:
+ jobs_must_arrive_to_execute sched.
+
+ (* Then, we prove that the time following the last execution of
+ job j is an idempotent function. *)
+ Lemma last_execution_idempotent:
+ forall t,
+ time_after_last_execution j (time_after_last_execution j t)
+ = time_after_last_execution j t.
+ Proof.
+ rename H_jobs_must_arrive_to_execute into ARR.
+ intros t.
+ rewrite {2 3}/time_after_last_execution.
+ case EX: [exists _,_].
+ {
+ move: EX => /existsP [t0 SCHED].
+ rewrite /time_after_last_execution.
+ set ex := [exists t0, _].
+ have EX': ex.
+ {
+ apply/existsP; rewrite addn1.
+ exists (Ordinal (ltnSn _)).
+ by apply bigmax_pred with (i0 := t0).
+ }
+ rewrite EX'; f_equal.
+ rewrite addn1; apply/eqP.
+ set m := \max_(_ < t  _)_.
+ have LT: m < m.+1 by done.
+ rewrite eqn_leq; apply/andP; split.
+ {
+ rewrite ltnS; apply bigmax_ltn_ord with (i0 := Ordinal LT).
+ by apply bigmax_pred with (i0 := t0).
+ }
+ {
+ apply leq_trans with (n := Ordinal LT); first by done.
+ by apply leq_bigmax_cond, bigmax_pred with (i0 := t0).
+ }
+ }
+ {
+ apply negbT in EX; rewrite negb_exists in EX.
+ move: EX => /forallP EX.
+ rewrite /time_after_last_execution.
+ set ex := [exists _, _].
+ suff EX': ex = false; first by rewrite EX'.
+ apply negbTE; rewrite negb_exists; apply/forallP.
+ intros x.
+ apply/negP; intro SCHED.
+ apply ARR in SCHED.
+ by apply leq_ltn_trans with (p := job_arrival j) in SCHED;
+ first by rewrite ltnn in SCHED.
+ }
+ Qed.
+
+ End Idempotence.
+
+ (* Next, we show that time_after_last_execution is bounded by the identity function. *)
+ Section BoundedByIdentity.
+
+ (* Let t be any time no earlier than the arrival of j. *)
+ Variable t: time.
+ Hypothesis H_after_arrival: has_arrived j t.
+
+ (* Then, the time following the last execution of job j in the interval [0, t)
+ occurs no later than time t. *)
+ Lemma last_execution_bounded_by_identity:
+ time_after_last_execution j t <= t.
+ Proof.
+ unfold time_after_last_execution.
+ case EX: [exists _, _]; last by done.
+ move: EX => /existsP [t0 SCHED].
+ by rewrite addn1; apply bigmax_ltn_ord with (i0 := t0).
+ Qed.
+
+ End BoundedByIdentity.
+
+ (* In this section, we show that if the service received by a job
+ remains the same, the time after last execution also doesn't change. *)
+ Section SameLastExecution.
+
+ (* Consider any time instants t and t'... *)
+ Variable t t': time.
+
+ (* ...in which job j has received the same amount of service. *)
+ Hypothesis H_same_service: service sched j t = service sched j t'.
+
+ (* Then, we prove that the times after last execution relative to
+ instants t and t' are exactly the same. *)
+ Lemma same_service_implies_same_last_execution:
+ time_after_last_execution j t = time_after_last_execution j t'.
+ Proof.
+ rename H_same_service into SERV.
+ have IFF := same_service_implies_scheduled_at_earlier_times
+ sched j t t' SERV.
+ rewrite /time_after_last_execution.
+ rewrite IFF; case EX2: [exists _, _]; [f_equal  by done].
+ have EX1: [exists x: 'I_t, job_scheduled_at j x] by rewrite IFF.
+ clear IFF.
+ move: t t' SERV EX1 EX2 => t1 t2; clear t t'.
+ wlog: t1 t2 / t1 <= t2 => [EQ SERV EX1 EX2  LE].
+ by case/orP: (leq_total t1 t2); ins; [symmetry]; apply EQ.
+
+ set m1 := \max_(t < t1  job_scheduled_at j t) t.
+ set m2 := \max_(t < t2  job_scheduled_at j t) t.
+ move => SERV /existsP [t1' SCHED1'] /existsP [t2' SCHED2'].
+ apply/eqP; rewrite eqn_leq; apply/andP; split.
+ {
+ have WID := big_ord_widen_cond t2
+ (fun x => job_scheduled_at j x) (fun x => x).
+ rewrite /m1 /m2 {}WID //.
+ rewrite big_mkcond [\max_(t < t2  _) _]big_mkcond.
+ apply leq_big_max; intros i _.
+ case AND: (_ && _); last by done.
+ by move: AND => /andP [SCHED _]; rewrite SCHED.
+ }
+ {
+ destruct (leqP t2 m1) as [GEm1  LTm1].
+ {
+ apply leq_trans with (n := t2); last by done.
+ by apply ltnW, bigmax_ltn_ord with (i0 := t2').
+ }
+ destruct (ltnP m2 t1) as [LTm2  GEm2].
+ {
+ apply leq_trans with (n := Ordinal LTm2); first by done.
+ by apply leq_bigmax_cond, bigmax_pred with (i0 := t2').
+ }
+ have LTm2: m2 < t2 by apply bigmax_ltn_ord with (i0 := t2').
+ have SCHEDm2: job_scheduled_at j m2 by apply bigmax_pred with (i0 := t2').
+ exfalso; move: SERV => /eqP SERV.
+ rewrite [_ == _]negbK in SERV.
+ move: SERV => /negP SERV; apply SERV; clear SERV.
+ rewrite neq_ltn; apply/orP; left.
+ rewrite /service /service_during.
+ rewrite > big_cat_nat with (n := m2) (p := t2);
+ [simpl  by done  by apply ltnW].
+ rewrite addn1; apply leq_add; first by apply extend_sum.
+ destruct t2; first by rewrite ltn0 in LTm1.
+ rewrite big_nat_recl; last by done.
+ by rewrite /service_at /job_scheduled_at SCHEDm2.
+ }
+ Qed.
+
+ End SameLastExecution.
+
+ (* In this section, we show that the service received by a job
+ does not change since the last execution. *)
+ Section SameService.
+
+ (* Assume that jobs do not execute before they arrived. *)
+ Hypothesis H_jobs_must_arrive_to_execute:
+ jobs_must_arrive_to_execute sched.
+
+ (* Then, we prove that, for any time t, the service received by job j
+ before (time_after_last_execution j t) is the same as the service
+ by j before time t. *)
+ Lemma same_service_since_last_execution:
+ forall t,
+ service sched j (time_after_last_execution j t) = service sched j t.
+ Proof.
+ intros t; rewrite /time_after_last_execution.
+ case EX: [exists _, _].
+ {
+ move: EX => /existsP [t0 SCHED0].
+ set m := \max_(_ < _  _) _; rewrite addn1.
+ have LTt: m < t by apply: (bigmax_ltn_ord _ _ t0).
+ rewrite leq_eqVlt in LTt.
+ move: LTt => /orP [/eqP EQ  LTt]; first by rewrite EQ.
+ rewrite {2}/service/service_during.
+ rewrite > big_cat_nat with (n := m.+1);
+ [simpl  by done  by apply ltnW].
+ rewrite [X in _ + X]big_nat_cond [X in _ + X]big1 ?addn0 //.
+ move => i /andP [/andP [GTi LTi] _].
+ apply/eqP; rewrite eqb0; apply/negP; intro BUG.
+ have LEi: (Ordinal LTi) <= m by apply leq_bigmax_cond.
+ by apply (leq_ltn_trans LEi) in GTi; rewrite ltnn in GTi.
+ }
+ {
+ apply negbT in EX; rewrite negb_exists in EX.
+ move: EX => /forallP ALL.
+ rewrite /service /service_during.
+ rewrite ignore_service_before_arrival // big_geq //.
+ rewrite big_nat_cond big1 //; move => i /andP [/= LTi _].
+ by apply/eqP; rewrite eqb0; apply (ALL (Ordinal LTi)).
+ }
+ Qed.
+
+ End SameService.
+
+ (* In this section, we show that for any smaller value of service, we can
+ always find the last execution that corresponds to that service. *)
+ Section ExistsIntermediateExecution.
+
+ (* Assume that jobs do not execute before they arrived. *)
+ Hypothesis H_jobs_must_arrive_to_execute:
+ jobs_must_arrive_to_execute sched.
+
+ (* Assume that job j has completed by time t. *)
+ Variable t: time.
+ Hypothesis H_j_has_completed: completed_by job_cost sched j t.
+
+ (* Then, for any value of service less than the cost of j, ...*)
+ Variable s: time.
+ Hypothesis H_less_than_cost: s < job_cost j.
+
+ (* ...there exists a last execution where the service received
+ by job j equals s. *)
+ Lemma exists_last_execution_with_smaller_service:
+ exists t0,
+ service sched j (time_after_last_execution j t0) = s.
+ Proof.
+ have SAME := same_service_since_last_execution.
+ rename H_jobs_must_arrive_to_execute into ARR.
+ move: H_j_has_completed => /eqP COMP.
+ feed (exists_intermediate_point (service sched j));
+ first by apply service_is_a_step_function.
+ move => EX; feed (EX (job_arrival j) t).
+ {
+ feed (cumulative_service_implies_scheduled sched j 0 t);
+ first by apply leq_ltn_trans with (n := s);
+ last by rewrite /(service _ _ _) COMP.
+ move => [t' [/= LTt SCHED]].
+ apply leq_trans with (n := t'); last by apply ltnW.
+ by apply ARR in SCHED.
+ }
+ feed (EX s).
+ {
+ apply/andP; split; last by rewrite COMP.
+ rewrite /service /service_during.
+ by rewrite ignore_service_before_arrival // big_geq.
+ }
+ move: EX => [x_mid [_ SERV]]; exists x_mid.
+ by rewrite SERV SAME.
+ Qed.
+
+ End ExistsIntermediateExecution.
+
+ End Lemmas.
+
+ End BeginningOfSuspension.
+
+ (* Having identified the time after last execution, we now define
+ whether jobs are suspended. *)
+ Section JobSuspension.
+
+ (* Let j be any job in the arrival sequence. *)
+ Variable j: JobIn arr_seq.
+
+ Section DefiningSuspension.
+
+ (* We are going to define whether job j is suspended at time t. *)
+ Variable t: time.
+
+ (* First, we define the (potential) begin of the latest self suspension as the
+ time following the last execution of job j in the interval [0, t).
+ (Note that suspension_start can return time t itself.) *)
+ Let suspension_start := time_after_last_execution j t.
+
+ (* Next, using the service received by j in the interval [0, suspension_start), ... *)
+ Let current_service := service sched j suspension_start.
+
+ (* ... we recall the duration of the suspension expected for job j after having
+ received that amount of service. *)
+ Definition suspension_duration := next_suspension j current_service.
+
+ (* Then, we say that job j is suspended at time t iff j has not completed
+ by time t and t lies in the latest suspension interval. *)
+ Definition suspended_at :=
+ ~~ completed_by job_cost sched j t &&
+ (suspension_start <= t < suspension_start + suspension_duration).
+
+ End DefiningSuspension.
+
+ (* Based on the notion of suspension, we also define the cumulative
+ suspension time of job j in any interval [t1, t2)... *)
+ Definition cumulative_suspension_during (t1 t2: time) :=
+ \sum_(t1 <= t < t2) (suspended_at t).
+
+ (* ...and the cumulative suspension time in any interval [0, t). *)
+ Definition cumulative_suspension (t: time) := cumulative_suspension_during 0 t.
+
+ End JobSuspension.
+
+ (* Next, we define whether the schedule respects selfsuspensions. *)
+ Section SuspensionAwareSchedule.
+
+ (* We say that the schedule respects selfsuspensions iff suspended
+ jobs are never scheduled. *)
+ Definition respects_self_suspensions :=
+ forall j t,
+ job_scheduled_at j t > ~ suspended_at j t.
+
+ End SuspensionAwareSchedule.
+
+ (* In this section, we prove several results related to job suspensions. *)
+ Section Lemmas.
+
+ (* First, we prove that at any time within any suspension interval,
+ a job is always suspended. *)
+ Section InsideSuspensionInterval.
+
+ (* Assume that jobs do not execute before they arrive... *)
+ Hypothesis H_jobs_must_arrive_to_execute:
+ jobs_must_arrive_to_execute sched.
+
+ (* ...and nor after completion. *)
+ Hypothesis H_completed_jobs_dont_execute:
+ completed_jobs_dont_execute job_cost sched.
+
+ (* Assume that the schedule respects selfsuspensions. *)
+ Hypothesis H_respects_self_suspensions: respects_self_suspensions.
+
+ (* Let j be any job in the arrival sequence. *)
+ Variable j: JobIn arr_seq.
+
+ (* Consider any time t after the arrival of j... *)
+ Variable t: time.
+ Hypothesis H_has_arrived: has_arrived j t.
+
+ (* ...and recall the latest suspension interval of job j relative to time t. *)
+ Let suspension_start := time_after_last_execution j t.
+ Let duration := suspension_duration j t.
+
+ (* First, we analyze the service received during a suspension interval. *)
+ Section SameService.
+
+ (* Let t_in be any time in the suspension interval relative to time t. *)
+ Variable t_in: time.
+ Hypothesis H_within_suspension_interval:
+ suspension_start <= t_in <= suspension_start + duration.
+
+ (* Then, we show that the service received before time t_in
+ equals the service received before the beginning of the
+ latest suspension interval (if exists). *)
+ Lemma same_service_in_suspension_interval:
+ service sched j t_in = service sched j suspension_start.
+ Proof.
+ rename H_within_suspension_interval into BETWEEN,
+ H_respects_self_suspensions into SUSP, t_in into i.
+ generalize dependent i.
+ suff SAME:
+ forall delta,
+ delta <= duration >
+ service sched j (suspension_start + delta) =
+ service sched j suspension_start.
+ {
+ move => i /andP [GE LT].
+ feed (SAME (isuspension_start)); first by rewrite leq_subLR.
+ by rewrite addnBA // addKn in SAME.
+ }
+ induction delta; first by rewrite addn0.
+ intros LT.
+ feed IHdelta; first by apply ltnW.
+ rewrite addnS [service _ _ suspension_start]addn0.
+ rewrite /service /service_during big_nat_recr //=.
+ f_equal; first by done.
+ apply/eqP; rewrite eqb0; apply/negP; intro SCHED.
+ move: (SCHED) => SCHED'.
+ apply SUSP in SCHED; apply SCHED; clear SCHED.
+ rewrite /suspended_at /suspension_duration.
+ case: (boolP (completed_by _ _ _ _)) => [COMP  NOTCOMP];
+ first by apply completed_implies_not_scheduled in COMP;
+ first by rewrite SCHED' in COMP.
+ rewrite andTb (same_service_implies_same_last_execution _ _ suspension_start) //.
+ rewrite /suspension_start last_execution_idempotent //.
+ apply/andP; split; first by apply leq_addr.
+ by rewrite ltn_add2l.
+ Qed.
+
+ End SameService.
+
+ (* Next, we infer that the job is suspended at all times during
+ the suspension interval. *)
+ Section JobSuspendedAtAllTimes.
+
+ (* Let t_in be any time before the completion of job j. *)
+ Variable t_in: time.
+ Hypothesis H_not_completed: ~~ job_completed_by j t_in.
+
+ (* If t_in lies in the suspension interval relative to time t, ...*)
+ Hypothesis H_within_suspension_interval:
+ suspension_start <= t_in < suspension_start + duration.
+
+ (* ...then job j is suspended at time t_in. More precisely, the suspension
+ interval relative to time t_in is included in the suspension interval
+ relative to time t. *)
+ Lemma suspended_in_suspension_interval:
+ suspended_at j t_in.
+ Proof.
+ rename H_within_suspension_interval into BETWEEN.
+ move: BETWEEN => /andP [GE LT].
+ have ARR: has_arrived j t_in.
+ {
+ by apply leq_trans with (n := suspension_start);
+ first by apply last_execution_after_arrival.
+ }
+ apply/andP; split; first by done.
+ apply/andP; split;
+ first by apply last_execution_bounded_by_identity.
+ apply (leq_trans LT).
+ have SAME: time_after_last_execution j t = time_after_last_execution j t_in.
+ {
+ set b := _ _ t.
+ rewrite [_ _ t_in](same_service_implies_same_last_execution _ _ b);
+ first by rewrite last_execution_idempotent.
+ apply same_service_in_suspension_interval.
+ by apply/andP; split; last by apply ltnW.
+ }
+ rewrite /suspension_start SAME leq_add2l.
+ by rewrite /duration /suspension_duration SAME.
+ Qed.
+
+ End JobSuspendedAtAllTimes.
+
+ End InsideSuspensionInterval.
+
+ (* Next, we prove lemmas about the state of a suspended job. *)
+ Section StateOfSuspendedJob.
+
+ (* Assume that jobs do not execute before they arrived. *)
+ Hypothesis H_jobs_must_arrive_to_execute:
+ jobs_must_arrive_to_execute sched.
+
+ (* Let j be any job in the arrival sequence. *)
+ Variable j: JobIn arr_seq.
+
+ (* Assume that j is suspended at time t. *)
+ Variable t: time.
+ Hypothesis H_j_is_suspended: suspended_at j t.
+
+ (* First, we show that j must have arrived by time t. *)
+ Lemma suspended_implies_arrived: has_arrived j t.
+ Proof.
+ rename H_j_is_suspended into SUSP.
+ move: SUSP => /andP [_ SUSP].
+ rewrite [_ && _]negbK in SUSP; move: SUSP => /negP SUSP.
+ rewrite /has_arrived leqNgt; apply/negP; intro LT.
+ apply SUSP; clear SUSP.
+ rewrite negb_and; apply/orP; left.
+ rewrite ltnNge.
+ apply: (leq_trans LT); clear LT.
+ rewrite /time_after_last_execution.
+ case EX: [exists _, _]; last by apply leqnn.
+ set t' := \max_(_ < _  _)_.
+ move: EX => /existsP [t0 EX].
+ apply bigmax_pred in EX; rewrite /t' /job_scheduled_at in EX.
+ apply leq_trans with (n := t'); last by apply leq_addr.
+ rewrite leqNgt; apply/negP; intro LT.
+ have NOTSCHED: ~~ scheduled_at sched j t'.
+ {
+ rewrite eqb0; apply/eqP.
+ by apply service_before_job_arrival_zero; first by done.
+ }
+ by rewrite EX in NOTSCHED.
+ Qed.
+
+ (* By the definition of suspension, it also follows that j cannot
+ have completed by time t. *)
+ Corollary suspended_implies_not_completed:
+ ~~ completed_by job_cost sched j t.
+ Proof.
+ by move: H_j_is_suspended => /andP [NOTCOMP _].
+ Qed.
+
+ End StateOfSuspendedJob.
+
+ (* Next, we establish a bound on the cumulative suspension time of any job. *)
+ Section BoundOnCumulativeSuspension.
+
+ (* Assume that jobs do not execute before they arrive... *)
+ Hypothesis H_jobs_must_arrive_to_execute:
+ jobs_must_arrive_to_execute sched.
+
+ (* ...and nor after completion. *)
+ Hypothesis H_completed_jobs_dont_execute:
+ completed_jobs_dont_execute job_cost sched.
+
+ (* Assume that the schedule respects selfsuspensions. *)
+ Hypothesis H_respects_self_suspensions: respects_self_suspensions.
+
+ (* Let j be any job in the arrival sequence. *)
+ Variable j: JobIn arr_seq.
+
+ (* Recall the total suspension of job j as given by the dynamic suspension model. *)
+ Let cumulative_suspension_of_j :=
+ cumulative_suspension_during j.
+ Let total_suspension_of_j :=
+ total_suspension job_cost next_suspension j.
+
+ (* We prove that the cumulative suspension time of job j in any
+ interval is upperbounded by the total suspension time. *)
+ Lemma cumulative_suspension_le_total_suspension:
+ forall t1 t2,
+ cumulative_suspension_of_j t1 t2 <= total_suspension_of_j.
+ Proof.
+ unfold cumulative_suspension_of_j, cumulative_suspension_during,
+ total_suspension_of_j, total_suspension.
+ intros t1 t2.
+ apply leq_trans with (n := \sum_(0 <= s < job_cost j)
+ \sum_(t1 <= t < t2  service sched j t == s) suspended_at j t).
+ {
+ rewrite (exchange_big_dep_nat (fun x => true)) //=.
+ apply leq_sum; intros s _.
+ destruct (boolP (suspended_at j s)) as [SUSP  NOTSUSP]; last by done.
+ rewrite (big_rem (service sched j s)); first by rewrite eq_refl.
+ rewrite mem_index_iota; apply/andP; split; first by done.
+ rewrite ltn_neqAle; apply/andP; split; last by apply cumulative_service_le_job_cost.
+ by apply suspended_implies_not_completed in SUSP.
+ }
+ {
+ apply leq_sum_nat; move => s /andP [_ LT] _.
+ destruct (boolP [exists t: 'I_t2, (t >= t1) && (service sched j t == s)]) as [EX  ALL];
+ last first.
+ {
+ rewrite negb_exists in ALL; move: ALL => /forallP ALL.
+ rewrite big_nat_cond big1 //.
+ move => i /andP [/andP [GEi LTi] SERV].
+ by specialize (ALL (Ordinal LTi)); rewrite /= SERV GEi andbT in ALL.
+ }
+ move: EX => /existsP [t' /andP [GE' /eqP SERV]].
+ unfold suspended_at, suspension_duration.
+ set b := time_after_last_execution j.
+ set n := next_suspension j s.
+ apply leq_trans with (n := \sum_(t1 <= t < t2  b t' <= t < b t' + n) 1).
+ {
+ rewrite big_mkcond [\sum_(_ <= _ < _  b t' <= _ < _) _]big_mkcond /=.
+ apply leq_sum_nat; intros t LEt _.
+ case: (boolP (completed_by _ _ _ _)) => [COMP  NOTCOMP];
+ [by case (_ == _)  simpl].
+ case EQ: (service _ _ _ == _); last by done.
+ move: EQ => /eqP EQ. rewrite /n EQ.
+ case INT: (_ <= _ < _); last by done.
+ apply eq_leq; symmetry; apply/eqP; rewrite eqb1.
+ move: INT => /andP [GEt LTt].
+ rewrite (same_service_in_suspension_interval _ _ _ _ t') //.
+ {
+ rewrite /b [b t'](same_service_implies_same_last_execution _ _ t);
+ last by rewrite SERV EQ.
+ by apply/andP; split.
+ }
+ {
+ rewrite /suspension_duration /b.
+ rewrite [b t'](same_service_implies_same_last_execution _ _ t);
+ last by rewrite SERV EQ.
+ by apply/andP; split; last by apply ltnW.
+ }
+ }
+ apply leq_trans with (n := \sum_(b t' <= t < b t' + n) 1);
+ last by simpl_sum_const; rewrite addKn.
+ by apply leq_sum1_smaller_range; move => i [LE LE']; split.
+ }
+ Qed.
+
+ End BoundOnCumulativeSuspension.
+
+ (* Next, we show that when a job completes, it must have suspended
+ as long as the total suspension time. *)
+ Section SuspendsForTotalSuspension.
+
+ (* Assume that jobs do not execute before they arrive... *)
+ Hypothesis H_jobs_must_arrive_to_execute:
+ jobs_must_arrive_to_execute sched.
+
+ (* ...and nor after completion. *)
+ Hypothesis H_completed_jobs_dont_execute:
+ completed_jobs_dont_execute job_cost sched.
+
+ (* Assume that the schedule respects selfsuspensions. *)
+ Hypothesis H_respects_self_suspensions: respects_self_suspensions.
+
+ (* Let j be any job in the arrival sequence. *)
+ Variable j: JobIn arr_seq.
+
+ (* Assume that j has completed by time t. *)
+ Variable t: time.
+ Hypothesis H_j_has_completed: completed_by job_cost sched j t.
+
+ (* Then, we prove that the cumulative suspension time must be
+ exactly equal to the total suspension time of the job. *)
+ Lemma cumulative_suspension_eq_total_suspension:
+ cumulative_suspension j t = total_suspension job_cost next_suspension j.
+ Proof.
+ rename H_j_has_completed into COMP, H_jobs_must_arrive_to_execute into ARR.
+ have EARLIER := exists_last_execution_with_smaller_service j ARR t COMP.
+ apply/eqP; rewrite eqn_leq; apply/andP; split;
+ first by apply cumulative_suspension_le_total_suspension.
+ rewrite /total_suspension /cumulative_suspension /cumulative_suspension_during.
+ move: COMP => /eqP COMP.
+ apply leq_trans with (n := \sum_(0 <= s < job_cost j)
+ \sum_(0 <= t0 < t  service sched j t0 == s) suspended_at j t0);
+ last first.
+ {
+ rewrite (exchange_big_dep_nat (fun x => true)) //=.
+ apply leq_sum_nat; move => t0 /andP [_ LT] _.
+ case (boolP [exists s: 'I_(job_cost j), service sched j t0 == s]) => [EX  ALL].
+ {
+ move: EX => /existsP [s /eqP EQs].
+ rewrite big_mkcond /=.
+ rewrite (bigD1_seq (nat_of_ord s)); [simpl   by apply iota_uniq];
+ last by rewrite mem_index_iota; apply/andP;split; last by apply ltn_ord.
+ rewrite EQs eq_refl big1; first by rewrite addn0.
+ by move => i /negbTE NEQ; rewrite eq_sym NEQ.
+ }
+ {
+ rewrite big_nat_cond big1; first by done.
+ move => i /andP [/andP [_ LTi] /eqP SERV].
+ rewrite negb_exists in ALL; move: ALL => /forallP ALL.
+ by specialize (ALL (Ordinal LTi)); rewrite /= SERV eq_refl in ALL.
+ }
+ }
+ {
+ apply leq_sum_nat; move => s /andP [_ LTs] _.
+ rewrite /suspended_at /suspension_duration.
+ set b := time_after_last_execution j.
+ set n := next_suspension j.
+
+ move: (EARLIER s LTs) => [t' EQ'].
+ apply leq_trans with (n := \sum_(0 <= t0 < t  (service sched j t0 == s) &&
+ (b t' <= t0 < b t' + n (service sched j (b t')))) 1); last first.
+ {
+ rewrite big_mkcond [\sum_(_ <= _ < _  _ == s)_]big_mkcond.
+ apply leq_sum_nat; move => i /andP [_ LTi] _.
+ case EQi: (service sched j i == s); [rewrite andTb  by rewrite andFb].
+ case LE: (_ <= _ <= _); last by done.
+ rewrite lt0n eqb0 negbK.
+ apply suspended_in_suspension_interval with (t := t'); try (by done).
+ rewrite neq_ltn; apply/orP; left.
+ by apply: (leq_ltn_trans _ LTs); apply eq_leq; apply/eqP.
+ }
+ {
+ apply leq_trans with (n := \sum_(b t' <= t0 < b t' + n (service sched j (b t')) 
+ (0 <= t0 < t) && (service sched j t0 == s)) 1).
+ {
+ apply leq_trans with (n := \sum_(b t' <= t0 < b t' + n (service sched j (b t'))) 1);
+ first by simpl_sum_const; rewrite addKn EQ'.
+ rewrite [in X in _ <= X]big_mkcond /=.
+ apply leq_sum_nat; move => i /andP [LEi GTi] _.
+ apply eq_leq; symmetry; apply/eqP; rewrite eqb1.
+ apply/andP; split.
+ {
+ have SUSPi: suspended_at j i.
+ {
+ apply: (suspended_in_suspension_interval _ _ _ _ t');
+ try (by done); last by apply/andP; split.
+ rewrite neq_ltn; apply/orP; left.
+ rewrite (same_service_in_suspension_interval _ _ _ _ t') //;
+ first by rewrite EQ'.
+ by apply/andP; split; last by apply ltnW.
+ }
+ apply contraT; rewrite leqNgt; intro LE.
+ apply suspended_implies_not_completed in SUSPi.
+ exfalso; move: SUSPi => /negP COMPi; apply COMPi.
+ apply completion_monotonic with (t0 := t); try (by done).
+ by apply/eqP.
+ }
+ {
+ rewrite EQ'; apply/eqP.
+ apply same_service_in_suspension_interval; try (by done).
+ by apply/andP; split; last by apply ltnW.
+ }
+ }
+ {
+ apply leq_sum1_smaller_range.
+ by move => i [LEb /andP [LE EQs]]; split;
+ last by apply/andP; split.
+ }
+ }
+ }
+ Qed.
+
+ End SuspendsForTotalSuspension.
+
+ End Lemmas.
+
+ End DefiningSuspensionIntervals.
+
+End SuspensionIntervals.
\ No newline at end of file
diff git a/model/uni/transformation/construction.v b/model/uni/transformation/construction.v
index 6ce3298c2b302a5897c83a7c00c004427eae7506..e02560dbe52cda2227fce4dac8ee0af9aeaa8ac2 100644
 a/model/uni/transformation/construction.v
+++ b/model/uni/transformation/construction.v
@@ 69,42 +69,79 @@ Module ScheduleConstruction.
}
Qed.
 (* If the generation function only depends on the service
+ Section ServiceDependent.
+
+ (* If the generation function only depends on the service
received by jobs during the schedule prefix, ...*)
 Hypothesis H_depends_only_on_service:
 forall sched1 sched2 t,
 (forall j, service sched1 j t = service sched2 j t) >
 build_schedule sched1 t = build_schedule sched2 t.
+ Hypothesis H_depends_only_on_service:
+ forall sched1 sched2 t,
+ (forall j, service sched1 j t = service sched2 j t) >
+ build_schedule sched1 t = build_schedule sched2 t.
 (* ...then we can prove that the final schedule, at any time t,
+ (* ...then we can prove that the final schedule, at any time t,
is exactly the result of the construction function. *)
 Lemma prefix_construction_uses_function:
 forall t,
 sched t = build_schedule sched t.
 Proof.
 intros t.
 feed (prefix_construction_same_prefix t t); [by done  intros EQ].
 rewrite {}EQ.
 induction t as [t IH] using strong_ind.
 destruct t.
 {
 rewrite /= /update_schedule eq_refl.
 apply H_depends_only_on_service.
 by intros j; rewrite /service /service_during big_geq // big_geq //.
 }
 {
 rewrite /= /update_schedule eq_refl.
 apply H_depends_only_on_service.
 intros j; rewrite /service /service_during.
 rewrite big_nat_recr //= big_nat_recr //=; f_equal.
 apply eq_big_nat; move => i /= LT.
 rewrite /service_at /scheduled_at.
 by rewrite prefix_construction_same_prefix; last by apply ltnW.
 }
 Qed.

+ Lemma service_dependent_schedule_construction:
+ forall t,
+ sched t = build_schedule sched t.
+ Proof.
+ intros t.
+ feed (prefix_construction_same_prefix t t); [by done  intros EQ].
+ rewrite {}EQ.
+ induction t as [t IH] using strong_ind.
+ destruct t.
+ {
+ rewrite /= /update_schedule eq_refl.
+ apply H_depends_only_on_service.
+ by intros j; rewrite /service /service_during big_geq // big_geq //.
+ }
+ {
+ rewrite /= /update_schedule eq_refl.
+ apply H_depends_only_on_service.
+ intros j; rewrite /service /service_during.
+ rewrite big_nat_recr //= big_nat_recr //=; f_equal.
+ apply eq_big_nat; move => i /= LT.
+ rewrite /service_at /scheduled_at.
+ by rewrite prefix_construction_same_prefix; last by apply ltnW.
+ }
+ Qed.
+
+ End ServiceDependent.
+
+ Section PrefixDependent.
+
+ (* If the generation function only depends on the schedule prefix, ... *)
+ Hypothesis H_depends_only_on_prefix:
+ forall (sched1 sched2: schedule arr_seq) t,
+ (forall t0, t0 < t > sched1 t0 = sched2 t0) >
+ build_schedule sched1 t = build_schedule sched2 t.
+
+ (* ...then we can prove that the final schedule, at any time t,
+ is exactly the result of the construction function. *)
+ Lemma prefix_dependent_schedule_construction:
+ forall t, sched t = build_schedule sched t.
+ Proof.
+ intros t.
+ feed (prefix_construction_same_prefix t t); [by done  intros EQ].
+ rewrite {}EQ.
+ induction t using strong_ind.
+ destruct t.
+ {
+ rewrite /= /update_schedule eq_refl.
+ apply H_depends_only_on_prefix.
+ by intros t; rewrite ltn0.
+ }
+ {
+ rewrite /= /update_schedule eq_refl.
+ apply H_depends_only_on_prefix.
+ intros t0 LT.
+ by rewrite prefix_construction_same_prefix.
+ }
+ Qed.
+
+ End PrefixDependent.
+
End Lemmas.

+
End ConstructionFromPrefixes.
End ScheduleConstruction.
\ No newline at end of file
diff git a/model/uni/workload.v b/model/uni/workload.v
index 69e0823d1f91a8fd5bc4982e7138dcc6d1df18d0..30d195b5ad505a737163aec96fc5f494ec84696c 100644
 a/model/uni/workload.v
+++ b/model/uni/workload.v
@@ 7,7 +7,6 @@ Module Workload.
Import Time ArrivalSequence Priority.

(* In this section, we define the notion of workload for sets of jobs. *)
Section WorkloadDefs.
@@ 26,7 +25,7 @@ Module Workload.
Section WorkloadOfJobs.
(* Given any predicate over Jobs, ... *)
 Variable pred: Job > bool.
+ Variable pred: JobIn arr_seq > bool.
(* ...we define the total workload of the jobs released during [t1, t2)
that satisfy such a predicate. *)
@@ 35,8 +34,9 @@ Module Workload.
End WorkloadOfJobs.
 (*Next, we define the workload of tasks with higher or equal priority. *)
 Section PerPriorityLevel.
+ (* Then, we define the workload of tasks with higher or equal priority
+ under FP policies. *)
+ Section PerTaskPriority.
(* Consider any FP policy that indicates whether a task has
higher or equal priority. *)
@@ 52,11 +52,33 @@ Module Workload.
(* Then, we define the workload of higher or equal priority requested
in the interval [t1, t2) as the workload of all the jobs of
higherorequalpriority tasks released in that interval. *)
 Definition workload_of_higher_or_equal_priority (t1 t2: time) :=
+ Definition workload_of_higher_or_equal_priority_tasks (t1 t2: time) :=
workload_of_jobs of_higher_or_equal_priority t1 t2.
 End PerPriorityLevel.
+ End PerTaskPriority.
+
+ (* Then, we define the workload of jobs with higher or equal priority
+ under JLFP policies. *)
+ Section PerJobPriority.
+
+ (* Consider any JLFP policy that indicates whether a job has
+ higher or equal priority. *)
+ Variable higher_eq_priority: JLFP_policy arr_seq.
+
+ (* Let j be the job to be analyzed. *)
+ Variable j: JobIn arr_seq.
+
+ (* Recall the notion of a job of higher or equal priority. *)
+ Let of_higher_or_equal_priority j_hp := higher_eq_priority j_hp j.
+
+ (* Then, we define the workload of higher or equal priority requested
+ in the interval [t1, t2) as the workload of all the jobs of
+ higherorequal priority released in that interval. *)
+ Definition workload_of_higher_or_equal_priority_jobs (t1 t2: time) :=
+ workload_of_jobs of_higher_or_equal_priority t1 t2.
+ End PerJobPriority.
+
End WorkloadDefs.
End Workload.
\ No newline at end of file