Commit 843c6ffc authored by Felipe Cerqueira's avatar Felipe Cerqueira

Major commit: Suspension-Oblivious Analysis

- Add generic definition of job suspension based on the cumulative service
- Define the dynamic suspension model (based on task suspension bounds)
- Add suspension semantics for uniprocessor schedules
- Formalize reduction from suspension-aware schedule to suspension-oblivious
  schedule by inflating costs (works with JLDP policies and non-unique priorities)
- Formalize suspension-oblivious FP RTA using the reduction
- Add implementation of a concrete suspension-aware scheduler
- Test suspension-oblivious FP RTA with an actual task set
- Add simpler definition for JLFP policies
- Generalize busy interval lemmas from FP to JLFP scheduling
parent cecba062
......@@ -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
......
......@@ -911,10 +911,10 @@ Module ResponseTimeIterationEDF.
(* ...and jobs are sequential. *)
Hypothesis H_sequential_jobs: sequential_jobs sched.
(* Assume a work-conserving APA scheduler that enforces EDF policy. *)
(* Assume a work-conserving 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) :=
......
......@@ -68,11 +68,11 @@ Module ResponseTimeAnalysisEDF.
completed_jobs_dont_execute job_cost sched.
(* Assume that the schedule is an work-conserving 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) :=
......
......@@ -531,11 +531,11 @@ Module ResponseTimeIterationFP.
(* ...and jobs are sequential. *)
Hypothesis H_sequential_jobs: sequential_jobs sched.
(* Assume a work-conserving APA scheduler that enforces the FP policy. *)
(* Assume a work-conserving 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) :=
......
......@@ -72,11 +72,11 @@ Module ResponseTimeAnalysisFP.
Variable higher_eq_priority: FP_policy sporadic_task.
(* ... and assume that the schedule is an APA work-conserving
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.
......
......@@ -174,7 +174,7 @@ Module InterferenceBoundEDF.
(* Assume that the scheduler is a work-conserving 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.
......
......@@ -900,7 +900,7 @@ Module ResponseTimeIterationEDF.
(* Assume a work-conserving 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.
......
......@@ -69,7 +69,7 @@ Module ResponseTimeAnalysisEDF.
(* Assume that the schedule is a work-conserving 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) :=
......
......@@ -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 work-conserving and enforces the FP policy. *)
(* Assume that the scheduler is work-conserving 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.
......
......@@ -71,10 +71,10 @@ Module ResponseTimeAnalysisFP.
Variable higher_eq_priority: FP_policy sporadic_task.
(* ... and assume that the schedule is a work-conserving
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 *.
......
......@@ -161,7 +161,7 @@ Module InterferenceBoundEDF.
(* Assume that the scheduler is a work-conserving 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.
......
......@@ -987,7 +987,7 @@ Module ResponseTimeIterationEDF.
(* Assume that we have a work-conserving 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.
......
......@@ -75,7 +75,7 @@ Module ResponseTimeAnalysisEDFJitter.
(* Assume that the schedule is a work-conserving 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) :=
......
......@@ -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 work-conserving and enforces the FP policy. *)
(* Assume that the scheduler is work-conserving 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.
......
......@@ -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 work-conserving and enforces this policy. *)
(* ...and assume that the schedule is work-conserving 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 *.
......
......@@ -163,7 +163,7 @@ Module InterferenceBoundEDFJitter.
(* Assume that we have a work-conserving 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.
......
......@@ -893,7 +893,7 @@ Module ResponseTimeIterationEDF.
(* Assume a work-conserving 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.
......
......@@ -69,7 +69,7 @@ Module ResponseTimeAnalysisEDF.
(* Assume that the schedule is a work-conserving 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) :=
......
......@@ -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 work-conserving and enforces the FP policy. *)
(* Assume that the scheduler is work-conserving 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.
......
......@@ -68,10 +68,10 @@ Module ResponseTimeAnalysisFP.
Variable higher_eq_priority: FP_policy sporadic_task.
(* ... and assume that the schedule is an APA work-conserving
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.
......
......@@ -158,7 +158,7 @@ Module InterferenceBoundEDF.
(* Assume that the scheduler is a work-conserving 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.
......
......@@ -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 work-conserving and enforces the FP policy. *)
(* Also assume that the scheduler is work-conserving 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 :=
......
......@@ -66,7 +66,7 @@ Module ResponseTimeAnalysisFP.
(* Next, assume that the schedule is a work-conserving 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.
......
......@@ -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.
......
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 suspension-oblivious RTA
for fixed-priority tasks under the dynamic self-suspension 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 suspension-aware 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 work-conserving when there are non-suspended 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 response-time 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 suspension-oblivious schedulability test suceeds... *)
Hypothesis H_claimed_schedulable_by_suspension_oblivious_RTA:
claimed_to_be_schedulable ts.
(* ...then no task misses its deadline in the suspension-aware 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
This diff is collapsed.
......@@ -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.
......