Library prosa.classic.implementation.apa.schedule
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.priority.
Require Import prosa.classic.model.arrival.basic.arrival_sequence prosa.classic.model.arrival.basic.task.
Require Import prosa.classic.model.schedule.global.basic.schedule.
Require Import prosa.classic.model.schedule.apa.affinity prosa.classic.model.schedule.apa.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 SporadicTaskset ArrivalSequence Schedule Platform Priority Affinity ScheduleConstruction.
Section Implementation.
Context {Job: eqType}.
Context {sporadic_task: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → sporadic_task.
Variable num_cpus: nat.
Variable arr_seq: arrival_sequence Job.
Variable alpha: task_affinity sporadic_task num_cpus.
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 sched_prefix.
Let actual_arrivals := jobs_arrived_up_to 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 should_be_scheduled (j: Job) p :=
let '(cpu, mapped_job) := p in
if mapped_job is Some j' then
(can_execute_on alpha (job_task j) cpu) &&
~~ (higher_eq_priority t j' j)
else
(can_execute_on alpha (job_task j) cpu).
Definition update_available_cpu allocation j :=
replace_first (should_be_scheduled j)
(set_pair_2nd (Some j))
allocation.
Let empty_mapping : seq (processor num_cpus × option Job) :=
(zip (enum (processor num_cpus)) (nseq num_cpus None)).
Definition schedule_jobs_from_list l :=
foldl update_available_cpu empty_mapping l.
Definition apa_schedule :=
pairs_to_function None (schedule_jobs_from_list 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 apa_schedule empty_schedule.
Lemma scheduler_depends_only_on_prefix:
∀ sched1 sched2 cpu t,
(∀ t0 cpu0, t0 < t → sched1 cpu0 t0 = sched2 cpu0 t0) →
apa_schedule sched1 cpu t = apa_schedule sched2 cpu t.
Corollary scheduler_uses_construction_function:
∀ t cpu, scheduler cpu t = apa_schedule scheduler cpu t.
End Implementation.
Section Proofs.
Context {Job: eqType}.
Context {sporadic_task: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → sporadic_task.
Variable num_cpus: nat.
Hypothesis H_at_least_one_cpu: num_cpus > 0.
Variable alpha: task_affinity sporadic_task num_cpus.
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_task num_cpus arr_seq alpha higher_eq_priority.
Section HelperLemmas.
Let schedule_jobs t l := schedule_jobs_from_list job_task num_cpus alpha higher_eq_priority t l.
Let schedule_pending_jobs t :=
schedule_jobs t (sorted_pending_jobs job_arrival job_cost num_cpus arr_seq
higher_eq_priority sched t).
Lemma scheduler_uniq_cpus :
∀ t l,
uniq (unzip1 (schedule_jobs t l)).
Lemma scheduler_job_in_mapping :
∀ l j t cpu,
(cpu, Some j) \in schedule_jobs t l → j \in l.
Lemma scheduler_mapping_respects_affinity :
∀ j t cpu,
(cpu, Some j) \in schedule_pending_jobs t →
can_execute_on alpha (job_task j) cpu.
Lemma scheduler_has_no_duplicate_jobs :
∀ j t cpu1 cpu2,
(cpu1, Some j) \in schedule_pending_jobs t →
(cpu2, Some j) \in schedule_pending_jobs t →
cpu1 = cpu2.
Lemma scheduler_scheduled_on :
∀ j cpu t,
scheduled_on sched j cpu t = ((cpu, Some j) \in schedule_pending_jobs t).
Lemma scheduler_has_cpus :
∀ cpu t l,
∃ x,
(cpu, x) \in schedule_jobs t l.
Lemma scheduler_mapping_is_work_conserving :
∀ j cpu t l,
j \in l →
sorted (higher_eq_priority t) l →
uniq l →
(∀ cpu, (cpu, Some j) \notin schedule_jobs t l) →
can_execute_on alpha (job_task j) cpu →
∃ j_other,
(cpu, Some j_other) \in schedule_jobs t l.
Lemma scheduler_priority :
∀ j j_hp cpu t,
arrives_in arr_seq j →
backlogged job_arrival job_cost sched j t →
can_execute_on alpha (job_task j) cpu →
scheduled_on sched j_hp cpu t →
higher_eq_priority t j_hp j.
End HelperLemmas.
Lemma scheduler_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
Theorem scheduler_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Theorem scheduler_sequential_jobs: sequential_jobs sched.
Theorem scheduler_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Theorem scheduler_apa_work_conserving:
apa_work_conserving job_arrival job_cost job_task arr_seq sched alpha.
Theorem scheduler_respects_affinity:
respects_affinity job_task sched alpha.
Theorem scheduler_respects_policy :
respects_JLDP_policy_under_weak_APA job_arrival job_cost job_task arr_seq
sched alpha higher_eq_priority.
End Proofs.
End ConcreteScheduler.
Require Import prosa.classic.model.priority.
Require Import prosa.classic.model.arrival.basic.arrival_sequence prosa.classic.model.arrival.basic.task.
Require Import prosa.classic.model.schedule.global.basic.schedule.
Require Import prosa.classic.model.schedule.apa.affinity prosa.classic.model.schedule.apa.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 SporadicTaskset ArrivalSequence Schedule Platform Priority Affinity ScheduleConstruction.
Section Implementation.
Context {Job: eqType}.
Context {sporadic_task: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → sporadic_task.
Variable num_cpus: nat.
Variable arr_seq: arrival_sequence Job.
Variable alpha: task_affinity sporadic_task num_cpus.
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 sched_prefix.
Let actual_arrivals := jobs_arrived_up_to 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 should_be_scheduled (j: Job) p :=
let '(cpu, mapped_job) := p in
if mapped_job is Some j' then
(can_execute_on alpha (job_task j) cpu) &&
~~ (higher_eq_priority t j' j)
else
(can_execute_on alpha (job_task j) cpu).
Definition update_available_cpu allocation j :=
replace_first (should_be_scheduled j)
(set_pair_2nd (Some j))
allocation.
Let empty_mapping : seq (processor num_cpus × option Job) :=
(zip (enum (processor num_cpus)) (nseq num_cpus None)).
Definition schedule_jobs_from_list l :=
foldl update_available_cpu empty_mapping l.
Definition apa_schedule :=
pairs_to_function None (schedule_jobs_from_list 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 apa_schedule empty_schedule.
Lemma scheduler_depends_only_on_prefix:
∀ sched1 sched2 cpu t,
(∀ t0 cpu0, t0 < t → sched1 cpu0 t0 = sched2 cpu0 t0) →
apa_schedule sched1 cpu t = apa_schedule sched2 cpu t.
Corollary scheduler_uses_construction_function:
∀ t cpu, scheduler cpu t = apa_schedule scheduler cpu t.
End Implementation.
Section Proofs.
Context {Job: eqType}.
Context {sporadic_task: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → sporadic_task.
Variable num_cpus: nat.
Hypothesis H_at_least_one_cpu: num_cpus > 0.
Variable alpha: task_affinity sporadic_task num_cpus.
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_task num_cpus arr_seq alpha higher_eq_priority.
Section HelperLemmas.
Let schedule_jobs t l := schedule_jobs_from_list job_task num_cpus alpha higher_eq_priority t l.
Let schedule_pending_jobs t :=
schedule_jobs t (sorted_pending_jobs job_arrival job_cost num_cpus arr_seq
higher_eq_priority sched t).
Lemma scheduler_uniq_cpus :
∀ t l,
uniq (unzip1 (schedule_jobs t l)).
Lemma scheduler_job_in_mapping :
∀ l j t cpu,
(cpu, Some j) \in schedule_jobs t l → j \in l.
Lemma scheduler_mapping_respects_affinity :
∀ j t cpu,
(cpu, Some j) \in schedule_pending_jobs t →
can_execute_on alpha (job_task j) cpu.
Lemma scheduler_has_no_duplicate_jobs :
∀ j t cpu1 cpu2,
(cpu1, Some j) \in schedule_pending_jobs t →
(cpu2, Some j) \in schedule_pending_jobs t →
cpu1 = cpu2.
Lemma scheduler_scheduled_on :
∀ j cpu t,
scheduled_on sched j cpu t = ((cpu, Some j) \in schedule_pending_jobs t).
Lemma scheduler_has_cpus :
∀ cpu t l,
∃ x,
(cpu, x) \in schedule_jobs t l.
Lemma scheduler_mapping_is_work_conserving :
∀ j cpu t l,
j \in l →
sorted (higher_eq_priority t) l →
uniq l →
(∀ cpu, (cpu, Some j) \notin schedule_jobs t l) →
can_execute_on alpha (job_task j) cpu →
∃ j_other,
(cpu, Some j_other) \in schedule_jobs t l.
Lemma scheduler_priority :
∀ j j_hp cpu t,
arrives_in arr_seq j →
backlogged job_arrival job_cost sched j t →
can_execute_on alpha (job_task j) cpu →
scheduled_on sched j_hp cpu t →
higher_eq_priority t j_hp j.
End HelperLemmas.
Lemma scheduler_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
Theorem scheduler_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Theorem scheduler_sequential_jobs: sequential_jobs sched.
Theorem scheduler_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Theorem scheduler_apa_work_conserving:
apa_work_conserving job_arrival job_cost job_task arr_seq sched alpha.
Theorem scheduler_respects_affinity:
respects_affinity job_task sched alpha.
Theorem scheduler_respects_policy :
respects_JLDP_policy_under_weak_APA job_arrival job_cost job_task arr_seq
sched alpha higher_eq_priority.
End Proofs.
End ConcreteScheduler.