Library prosa.classic.implementation.global.jitter.schedule
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.jitter.arrival_sequence prosa.classic.model.priority.
Require Import prosa.classic.model.schedule.global.jitter.schedule
prosa.classic.model.schedule.global.jitter.platform.
Require Import prosa.classic.model.schedule.global.transformation.construction.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop seq path.
Module ConcreteScheduler.
Import ArrivalSequenceWithJitter ScheduleWithJitter Platform Priority ScheduleConstruction.
Section Implementation.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_jitter: Job → time.
Variable num_cpus: nat.
Variable arr_seq: arrival_sequence Job.
Variable higher_eq_priority: JLDP_policy Job.
Section ScheduleConstruction.
Variable sched_prefix: schedule Job num_cpus.
Variable cpu: processor num_cpus.
Variable t: time.
Let is_pending := pending job_arrival job_cost job_jitter sched_prefix.
Let actual_arrivals := actual_arrivals_up_to job_arrival job_jitter arr_seq.
Definition pending_jobs :=
[seq j <- actual_arrivals t | is_pending j t].
Definition sorted_pending_jobs :=
sort (higher_eq_priority t) pending_jobs.
Definition nth_highest_priority_job :=
nth_or_none sorted_pending_jobs cpu.
End ScheduleConstruction.
Let empty_schedule : schedule Job num_cpus := fun cpu t ⇒ None.
Definition scheduler :=
build_schedule_from_prefixes num_cpus nth_highest_priority_job empty_schedule.
Lemma scheduler_depends_only_on_prefix:
∀ sched1 sched2 cpu t,
(∀ t0 cpu0, t0 < t → sched1 cpu0 t0 = sched2 cpu0 t0) →
nth_highest_priority_job sched1 cpu t = nth_highest_priority_job sched2 cpu t.
Corollary scheduler_uses_construction_function:
∀ t cpu, scheduler cpu t = nth_highest_priority_job scheduler cpu t.
End Implementation.
Section Proofs.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_jitter: Job → time.
Variable num_cpus: nat.
Hypothesis H_at_least_one_cpu: num_cpus > 0.
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_arrival_sequence_is_a_set: arrival_sequence_is_a_set arr_seq.
Variable higher_eq_priority: JLDP_policy Job.
Hypothesis H_priority_transitive: JLDP_is_transitive higher_eq_priority.
Hypothesis H_priority_total: ∀ t, total (higher_eq_priority t).
Let sched := scheduler job_arrival job_cost job_jitter num_cpus arr_seq higher_eq_priority.
Section HelperLemmas.
Let sorted_jobs :=
sorted_pending_jobs job_arrival job_cost job_jitter num_cpus arr_seq higher_eq_priority sched.
Corollary scheduler_nth_or_none_mapping :
∀ t cpu,
sched cpu t = nth_or_none (sorted_jobs t) cpu.
Lemma scheduler_nth_or_none_backlogged :
∀ j t,
arrives_in arr_seq j →
backlogged job_arrival job_cost job_jitter sched j t →
∃ i,
nth_or_none (sorted_jobs t) i = Some j ∧ i ≥ num_cpus.
End HelperLemmas.
Lemma scheduler_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
Theorem scheduler_jobs_execute_after_jitter:
jobs_execute_after_jitter job_arrival job_jitter sched.
Theorem scheduler_sequential_jobs: sequential_jobs sched.
Theorem scheduler_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Theorem scheduler_work_conserving:
work_conserving job_arrival job_cost job_jitter arr_seq sched.
Theorem scheduler_respects_policy :
respects_JLDP_policy job_arrival job_cost job_jitter arr_seq sched higher_eq_priority.
End Proofs.
End ConcreteScheduler.
Require Import prosa.classic.model.arrival.jitter.arrival_sequence prosa.classic.model.priority.
Require Import prosa.classic.model.schedule.global.jitter.schedule
prosa.classic.model.schedule.global.jitter.platform.
Require Import prosa.classic.model.schedule.global.transformation.construction.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop seq path.
Module ConcreteScheduler.
Import ArrivalSequenceWithJitter ScheduleWithJitter Platform Priority ScheduleConstruction.
Section Implementation.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_jitter: Job → time.
Variable num_cpus: nat.
Variable arr_seq: arrival_sequence Job.
Variable higher_eq_priority: JLDP_policy Job.
Section ScheduleConstruction.
Variable sched_prefix: schedule Job num_cpus.
Variable cpu: processor num_cpus.
Variable t: time.
Let is_pending := pending job_arrival job_cost job_jitter sched_prefix.
Let actual_arrivals := actual_arrivals_up_to job_arrival job_jitter arr_seq.
Definition pending_jobs :=
[seq j <- actual_arrivals t | is_pending j t].
Definition sorted_pending_jobs :=
sort (higher_eq_priority t) pending_jobs.
Definition nth_highest_priority_job :=
nth_or_none sorted_pending_jobs cpu.
End ScheduleConstruction.
Let empty_schedule : schedule Job num_cpus := fun cpu t ⇒ None.
Definition scheduler :=
build_schedule_from_prefixes num_cpus nth_highest_priority_job empty_schedule.
Lemma scheduler_depends_only_on_prefix:
∀ sched1 sched2 cpu t,
(∀ t0 cpu0, t0 < t → sched1 cpu0 t0 = sched2 cpu0 t0) →
nth_highest_priority_job sched1 cpu t = nth_highest_priority_job sched2 cpu t.
Corollary scheduler_uses_construction_function:
∀ t cpu, scheduler cpu t = nth_highest_priority_job scheduler cpu t.
End Implementation.
Section Proofs.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_jitter: Job → time.
Variable num_cpus: nat.
Hypothesis H_at_least_one_cpu: num_cpus > 0.
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_arrival_sequence_is_a_set: arrival_sequence_is_a_set arr_seq.
Variable higher_eq_priority: JLDP_policy Job.
Hypothesis H_priority_transitive: JLDP_is_transitive higher_eq_priority.
Hypothesis H_priority_total: ∀ t, total (higher_eq_priority t).
Let sched := scheduler job_arrival job_cost job_jitter num_cpus arr_seq higher_eq_priority.
Section HelperLemmas.
Let sorted_jobs :=
sorted_pending_jobs job_arrival job_cost job_jitter num_cpus arr_seq higher_eq_priority sched.
Corollary scheduler_nth_or_none_mapping :
∀ t cpu,
sched cpu t = nth_or_none (sorted_jobs t) cpu.
Lemma scheduler_nth_or_none_backlogged :
∀ j t,
arrives_in arr_seq j →
backlogged job_arrival job_cost job_jitter sched j t →
∃ i,
nth_or_none (sorted_jobs t) i = Some j ∧ i ≥ num_cpus.
End HelperLemmas.
Lemma scheduler_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
Theorem scheduler_jobs_execute_after_jitter:
jobs_execute_after_jitter job_arrival job_jitter sched.
Theorem scheduler_sequential_jobs: sequential_jobs sched.
Theorem scheduler_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Theorem scheduler_work_conserving:
work_conserving job_arrival job_cost job_jitter arr_seq sched.
Theorem scheduler_respects_policy :
respects_JLDP_policy job_arrival job_cost job_jitter arr_seq sched higher_eq_priority.
End Proofs.
End ConcreteScheduler.