Library rt.model.schedule.global.transformation.construction
Require Import rt.util.all.
Require Import rt.model.arrival.basic.arrival_sequence.
Require Import rt.model.schedule.global.basic.schedule.
Module ScheduleConstruction.
Import ArrivalSequence Schedule.
(* 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.
(* Let num_cpus denote the number of processors. *)
Variable num_cpus: nat.
(* Assume we are given a function that takes an existing schedule prefix [0, t)
and returns what should be scheduled at time t on each processor. *)
Variable build_schedule:
schedule Job num_cpus → schedule Job num_cpus.
(* Then, starting from a base schedule, ... *)
Variable base_sched: schedule Job num_cpus.
(* ...we can update individual times using the build_schedule function, ... *)
Definition update_schedule (prev_sched: schedule Job num_cpus)
(t_next: time) : schedule Job num_cpus :=
fun (cpu: processor num_cpus) t ⇒
if t == t_next then
build_schedule prev_sched cpu t
else prev_sched cpu t.
(* ...which recursively generates schedule prefixes up to time t_max. *)
Fixpoint schedule_prefix (t_max: time) : schedule Job num_cpus :=
if t_max is t_prev.+1 then
update_schedule (schedule_prefix t_prev) t_prev.+1
else
update_schedule base_sched 0.
(* Based on the schedule prefixes, we construct a complete schedule. *)
Definition build_schedule_from_prefixes := fun cpu t ⇒ schedule_prefix t cpu 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:
∀ t t_max cpu,
t ≤ t_max →
schedule_prefix t_max cpu t = sched cpu t.
Section ServiceDependent.
(* If the generation function only depends on the service
received by jobs during the schedule prefix, ...*)
Hypothesis H_depends_only_on_service:
∀ sched1 sched2 cpu t,
(∀ j, service sched1 j t = service sched2 j t) →
build_schedule sched1 cpu t = build_schedule sched2 cpu t.
(* ...then we can prove that the final schedule, at any time t,
is exactly the result of the construction function. *)
Lemma service_dependent_schedule_construction:
∀ cpu t,
sched cpu t = build_schedule sched cpu t.
End ServiceDependent.
Section PrefixDependent.
(* If the generation function only depends on the schedule prefix, ... *)
Hypothesis H_depends_only_on_prefix:
∀ (sched1 sched2: schedule Job num_cpus) cpu t,
(∀ t0 cpu, t0 < t → sched1 cpu t0 = sched2 cpu t0) →
build_schedule sched1 cpu t = build_schedule sched2 cpu 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:
∀ cpu t, sched cpu t = build_schedule sched cpu t.
End PrefixDependent.
End Lemmas.
End ConstructionFromPrefixes.
End ScheduleConstruction.
Require Import rt.model.arrival.basic.arrival_sequence.
Require Import rt.model.schedule.global.basic.schedule.
Module ScheduleConstruction.
Import ArrivalSequence Schedule.
(* 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.
(* Let num_cpus denote the number of processors. *)
Variable num_cpus: nat.
(* Assume we are given a function that takes an existing schedule prefix [0, t)
and returns what should be scheduled at time t on each processor. *)
Variable build_schedule:
schedule Job num_cpus → schedule Job num_cpus.
(* Then, starting from a base schedule, ... *)
Variable base_sched: schedule Job num_cpus.
(* ...we can update individual times using the build_schedule function, ... *)
Definition update_schedule (prev_sched: schedule Job num_cpus)
(t_next: time) : schedule Job num_cpus :=
fun (cpu: processor num_cpus) t ⇒
if t == t_next then
build_schedule prev_sched cpu t
else prev_sched cpu t.
(* ...which recursively generates schedule prefixes up to time t_max. *)
Fixpoint schedule_prefix (t_max: time) : schedule Job num_cpus :=
if t_max is t_prev.+1 then
update_schedule (schedule_prefix t_prev) t_prev.+1
else
update_schedule base_sched 0.
(* Based on the schedule prefixes, we construct a complete schedule. *)
Definition build_schedule_from_prefixes := fun cpu t ⇒ schedule_prefix t cpu 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:
∀ t t_max cpu,
t ≤ t_max →
schedule_prefix t_max cpu t = sched cpu t.
Section ServiceDependent.
(* If the generation function only depends on the service
received by jobs during the schedule prefix, ...*)
Hypothesis H_depends_only_on_service:
∀ sched1 sched2 cpu t,
(∀ j, service sched1 j t = service sched2 j t) →
build_schedule sched1 cpu t = build_schedule sched2 cpu t.
(* ...then we can prove that the final schedule, at any time t,
is exactly the result of the construction function. *)
Lemma service_dependent_schedule_construction:
∀ cpu t,
sched cpu t = build_schedule sched cpu t.
End ServiceDependent.
Section PrefixDependent.
(* If the generation function only depends on the schedule prefix, ... *)
Hypothesis H_depends_only_on_prefix:
∀ (sched1 sched2: schedule Job num_cpus) cpu t,
(∀ t0 cpu, t0 < t → sched1 cpu t0 = sched2 cpu t0) →
build_schedule sched1 cpu t = build_schedule sched2 cpu 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:
∀ cpu t, sched cpu t = build_schedule sched cpu t.
End PrefixDependent.
End Lemmas.
End ConstructionFromPrefixes.
End ScheduleConstruction.