Library rt.implementation.uni.susp.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.susp.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 PlatformWithSuspensions 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 consistent job arrival sequence...*)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
(* ...that is subject to job suspensions. *)
Variable next_suspension: job_suspension Job.
(* Also, assume that 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.
Let is_suspended :=
suspended_at job_arrival job_cost next_suspension sched_prefix.
(* Consider the list of pending, non-suspended jobs at time t. *)
Definition pending_jobs :=
[seq j <- jobs_arrived_up_to arr_seq t | is_pending j t && ~~ is_suspended 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.
(* Assume 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_no_duplicate_arrivals: arrival_sequence_is_a_set arr_seq.
(* ...that is subject to suspension times. *)
Variable next_suspension: job_suspension Job.
(* Consider any JLDP policy that is reflexive, transitive and total. *)
Variable higher_eq_priority: JLDP_policy Job.
Hypothesis H_priority_is_transitive: JLDP_is_transitive higher_eq_priority.
Hypothesis H_priority_is_total: JLDP_is_total arr_seq higher_eq_priority.
(* Let sched denote our concrete scheduler implementation. *)
Let sched := scheduler job_arrival job_cost arr_seq next_suspension 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 next_suspension arr_seq sched.
(* ... respects the JLDP policy..., *)
Theorem scheduler_respects_policy :
respects_JLDP_policy job_arrival job_cost next_suspension arr_seq sched higher_eq_priority.
(* ... and respects self-suspensions. *)
Theorem scheduler_respects_self_suspensions:
respects_self_suspensions job_arrival job_cost next_suspension sched.
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.susp.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 PlatformWithSuspensions 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 consistent job arrival sequence...*)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
(* ...that is subject to job suspensions. *)
Variable next_suspension: job_suspension Job.
(* Also, assume that 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.
Let is_suspended :=
suspended_at job_arrival job_cost next_suspension sched_prefix.
(* Consider the list of pending, non-suspended jobs at time t. *)
Definition pending_jobs :=
[seq j <- jobs_arrived_up_to arr_seq t | is_pending j t && ~~ is_suspended 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.
(* Assume 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_no_duplicate_arrivals: arrival_sequence_is_a_set arr_seq.
(* ...that is subject to suspension times. *)
Variable next_suspension: job_suspension Job.
(* Consider any JLDP policy that is reflexive, transitive and total. *)
Variable higher_eq_priority: JLDP_policy Job.
Hypothesis H_priority_is_transitive: JLDP_is_transitive higher_eq_priority.
Hypothesis H_priority_is_total: JLDP_is_total arr_seq higher_eq_priority.
(* Let sched denote our concrete scheduler implementation. *)
Let sched := scheduler job_arrival job_cost arr_seq next_suspension 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 next_suspension arr_seq sched.
(* ... respects the JLDP policy..., *)
Theorem scheduler_respects_policy :
respects_JLDP_policy job_arrival job_cost next_suspension arr_seq sched higher_eq_priority.
(* ... and respects self-suspensions. *)
Theorem scheduler_respects_self_suspensions:
respects_self_suspensions job_arrival job_cost next_suspension sched.
End Proofs.
End ConcreteScheduler.