Library rt.implementation.uni.basic.schedule
Require Import rt.util.all.
Require Import rt.model.arrival.basic.job rt.model.arrival.basic.arrival_sequence rt.model.priority.
Require Import rt.model.schedule.uni.schedule.
Require Import rt.model.schedule.uni.basic.platform.
Require Import rt.model.schedule.uni.transformation.construction.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop seq path.
Module ConcreteScheduler.
Import Job ArrivalSequence UniprocessorSchedule Platform Priority ScheduleConstruction.
(* In this section, we implement a priority-based uniprocessor scheduler *)
Section Implementation.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
(* Let arr_seq be any job arrival sequence with consistent arrivals.*)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
(* Assume a JLDP policy is given. *)
Variable higher_eq_priority: JLDP_policy Job.
(* Next, we show how to recursively construct the schedule. *)
Section ScheduleConstruction.
(* For any time t, suppose that we have generated the schedule prefix in the
interval 0, t). Then, we must define what should be scheduled at time t. *)
Variable sched_prefix: schedule Job.
Variable t: time.
(* For simplicity, let's use some local names. *)
Let is_pending := pending job_arrival job_cost sched_prefix.
(* Consider the list of pending jobs at time t. *)
Definition pending_jobs :=
[seq j <- jobs_arrived_up_to arr_seq t | is_pending j t].
(* To make the scheduling decision, we just pick one of the highest-priority jobs
that are pending (if it exists). *)
Definition highest_priority_job :=
seq_min (higher_eq_priority t) pending_jobs.
End ScheduleConstruction.
(* Starting from the empty schedule, the final schedule is obtained by iteratively
picking the highest-priority job. *)
Let empty_schedule : schedule Job := fun t ⇒ None.
Definition scheduler :=
build_schedule_from_prefixes highest_priority_job empty_schedule.
(* Then, by showing that the construction function depends only on the prefix, ... *)
Lemma scheduler_depends_only_on_prefix:
∀ sched1 sched2 t,
(∀ t0, t0 < t → sched1 t0 = sched2 t0) →
highest_priority_job sched1 t = highest_priority_job sched2 t.
(* ...we infer that the generated schedule is indeed based on the construction function. *)
Corollary scheduler_uses_construction_function:
∀ t, scheduler t = highest_priority_job scheduler t.
End Implementation.
(* In this section, we prove the properties of the scheduler that are used
as hypotheses in the analyses. *)
Section Proofs.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
(* Let arr_seq be any job arrival sequence with consistent, duplicate-free arrivals. *)
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.
(* Consider any JLDP policy that is transitive and total. *)
Variable higher_eq_priority: JLDP_policy Job.
Hypothesis H_priority_is_transitive: ∀ t, transitive (higher_eq_priority t).
Hypothesis H_priority_is_total: ∀ t, total (higher_eq_priority t).
(* Let sched denote our concrete scheduler implementation. *)
Let sched := scheduler job_arrival job_cost arr_seq higher_eq_priority.
(* To conclude, we prove the important properties of the scheduler implementation. *)
(* First, we show that scheduled jobs come from the arrival sequence. *)
Lemma scheduler_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
(* Next, we show that jobs do not execute before they arrive...*)
Theorem scheduler_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
(* ... nor after completion. *)
Theorem scheduler_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* In addition, the scheduler is work conserving, ... *)
Theorem scheduler_work_conserving:
work_conserving job_arrival job_cost arr_seq sched.
(* ...and respects the JLDP policy. *)
Theorem scheduler_respects_policy :
respects_JLDP_policy job_arrival job_cost arr_seq sched higher_eq_priority.
End Proofs.
End ConcreteScheduler.
Require Import rt.model.arrival.basic.job rt.model.arrival.basic.arrival_sequence rt.model.priority.
Require Import rt.model.schedule.uni.schedule.
Require Import rt.model.schedule.uni.basic.platform.
Require Import rt.model.schedule.uni.transformation.construction.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop seq path.
Module ConcreteScheduler.
Import Job ArrivalSequence UniprocessorSchedule Platform Priority ScheduleConstruction.
(* In this section, we implement a priority-based uniprocessor scheduler *)
Section Implementation.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
(* Let arr_seq be any job arrival sequence with consistent arrivals.*)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
(* Assume a JLDP policy is given. *)
Variable higher_eq_priority: JLDP_policy Job.
(* Next, we show how to recursively construct the schedule. *)
Section ScheduleConstruction.
(* For any time t, suppose that we have generated the schedule prefix in the
interval 0, t). Then, we must define what should be scheduled at time t. *)
Variable sched_prefix: schedule Job.
Variable t: time.
(* For simplicity, let's use some local names. *)
Let is_pending := pending job_arrival job_cost sched_prefix.
(* Consider the list of pending jobs at time t. *)
Definition pending_jobs :=
[seq j <- jobs_arrived_up_to arr_seq t | is_pending j t].
(* To make the scheduling decision, we just pick one of the highest-priority jobs
that are pending (if it exists). *)
Definition highest_priority_job :=
seq_min (higher_eq_priority t) pending_jobs.
End ScheduleConstruction.
(* Starting from the empty schedule, the final schedule is obtained by iteratively
picking the highest-priority job. *)
Let empty_schedule : schedule Job := fun t ⇒ None.
Definition scheduler :=
build_schedule_from_prefixes highest_priority_job empty_schedule.
(* Then, by showing that the construction function depends only on the prefix, ... *)
Lemma scheduler_depends_only_on_prefix:
∀ sched1 sched2 t,
(∀ t0, t0 < t → sched1 t0 = sched2 t0) →
highest_priority_job sched1 t = highest_priority_job sched2 t.
(* ...we infer that the generated schedule is indeed based on the construction function. *)
Corollary scheduler_uses_construction_function:
∀ t, scheduler t = highest_priority_job scheduler t.
End Implementation.
(* In this section, we prove the properties of the scheduler that are used
as hypotheses in the analyses. *)
Section Proofs.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
(* Let arr_seq be any job arrival sequence with consistent, duplicate-free arrivals. *)
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.
(* Consider any JLDP policy that is transitive and total. *)
Variable higher_eq_priority: JLDP_policy Job.
Hypothesis H_priority_is_transitive: ∀ t, transitive (higher_eq_priority t).
Hypothesis H_priority_is_total: ∀ t, total (higher_eq_priority t).
(* Let sched denote our concrete scheduler implementation. *)
Let sched := scheduler job_arrival job_cost arr_seq higher_eq_priority.
(* To conclude, we prove the important properties of the scheduler implementation. *)
(* First, we show that scheduled jobs come from the arrival sequence. *)
Lemma scheduler_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
(* Next, we show that jobs do not execute before they arrive...*)
Theorem scheduler_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
(* ... nor after completion. *)
Theorem scheduler_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* In addition, the scheduler is work conserving, ... *)
Theorem scheduler_work_conserving:
work_conserving job_arrival job_cost arr_seq sched.
(* ...and respects the JLDP policy. *)
Theorem scheduler_respects_policy :
respects_JLDP_policy job_arrival job_cost arr_seq sched higher_eq_priority.
End Proofs.
End ConcreteScheduler.