Add schedule construction based on prefixes

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\

model/uni/transformation/construction.v

+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