From 8c68c87a7f90d9819d75a09900ed52ff823a3d3e Mon Sep 17 00:00:00 2001
From: Felipe Cerqueira <felipec@mpi-sws.org>
Date: Thu, 6 Oct 2016 14:28:45 +0200
Subject: [PATCH] Add schedule construction based on prefixes
---
Makefile | 3 +-
model/uni/transformation/construction.v | 110 ++++++++++++++++++++++++
2 files changed, 112 insertions(+), 1 deletion(-)
create mode 100644 model/uni/transformation/construction.v
diff --git a/Makefile b/Makefile
index 98fe29ec8..9514d0ecc 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/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/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/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
#
.DEFAULT_GOAL := all
@@ -176,6 +176,7 @@ VFILES:=util/ssromega.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\
diff --git a/model/uni/transformation/construction.v b/model/uni/transformation/construction.v
new file mode 100644
index 000000000..290c05b92
--- /dev/null
+++ b/model/uni/transformation/construction.v
@@ -0,0 +1,110 @@
+Require Import rt.util.all.
+Require Import rt.model.job rt.model.arrival_sequence.
+Require Import rt.model.uni.schedule.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop seq path finfun.
+
+Module ScheduleConstruction.
+
+ Import Job ArrivalSequence UniprocessorSchedule.
+
+ (* In this section, we construct a schedule recursively by augmenting prefixes. *)
+ Section ConstructionFromPrefixes.
+
+ Context {Job: eqType}.
+
+ (* Let arr_seq be any arrival sequence.*)
+ Variable arr_seq: arrival_sequence Job.
+
+ (* Assume we are given a function that takes an existing schedule prefix
+ up to interval [0, t) and returns what should be scheduled at time t. *)
+ Variable build_schedule:
+ schedule arr_seq -> time -> option (JobIn arr_seq).
+
+ (* Then, starting from the empty schedule as a base, ... *)
+ Definition empty_schedule : schedule arr_seq := fun t => None.
+
+ (* ...we can update individual times using the build_schedule function, ... *)
+ Definition update_schedule (prev_sched: schedule arr_seq)
+ (t_next: time) : schedule arr_seq :=
+ fun t =>
+ if t == t_next then
+ build_schedule prev_sched t
+ else prev_sched t.
+
+ (* ...which recursively generates schedule prefixes up to time t_max. *)
+ Fixpoint schedule_prefix (t_max: time) : schedule arr_seq :=
+ if t_max is t_prev.+1 then
+ update_schedule (schedule_prefix t_prev) t_prev.+1
+ else
+ update_schedule empty_schedule 0.
+
+ (* Based on the schedule prefixes, we construct a complete schedule. *)
+ Definition build_schedule_from_prefixes := fun t => schedule_prefix t t.
+
+ (* In this section, we prove some lemmas about the construction. *)
+ Section Lemmas.
+
+ (* Let sched be the generated schedule. *)
+ Let sched := build_schedule_from_prefixes.
+
+ (* First, we show that the scheduler preserves its prefixes. *)
+ Lemma prefix_construction_same_prefix:
+ forall t t_max,
+ t <= t_max ->
+ schedule_prefix t_max t = sched t.
+ Proof.
+ intros t t_max LEt.
+ induction t_max;
+ first by rewrite leqn0 in LEt; move: LEt => /eqP EQ; subst.
+ rewrite leq_eqVlt in LEt.
+ move: LEt => /orP [/eqP EQ | LESS]; first by subst.
+ {
+ feed IHt_max; first by done.
+ unfold schedule_prefix, update_schedule at 1.
+ assert (FALSE: t == t_max.+1 = false).
+ {
+ by apply negbTE; rewrite neq_ltn LESS orTb.
+ } rewrite FALSE.
+ by rewrite -IHt_max.
+ }
+ Qed.
+
+ (* 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.
+
+ (* ...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.
+
+ End Lemmas.
+
+ End ConstructionFromPrefixes.
+
+End ScheduleConstruction.
\ No newline at end of file
--
GitLab