Library rt.implementation.uni.jitter.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.jitter.schedule
rt.model.schedule.uni.jitter.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 UniprocessorScheduleWithJitter Platform Priority
ScheduleConstruction.
(* In this section, we implement a jitter-aware priority-based uniprocessor scheduler *)
Section Implementation.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_jitter: Job → time.
(* Let arr_seq be any job arrival sequence. *)
Variable arr_seq: arrival_sequence 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 job_jitter sched_prefix.
(* Consider the list of pending jobs with actual arrivals up to t. *)
Definition pending_jobs :=
[seq j <- actual_arrivals_up_to job_arrival job_jitter 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.
Variable job_jitter: 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.
(* Consider any JLDP policy that is reflexive, transitive and total. *)
Variable higher_eq_priority: JLDP_policy Job.
Hypothesis H_priority_is_reflexive: JLDP_is_reflexive higher_eq_priority.
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 job_jitter 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_execute_after_jitter:
jobs_execute_after_jitter job_arrival job_jitter 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 job_jitter arr_seq sched.
(* ... and respects the JLDP policy. *)
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 rt.model.arrival.basic.job rt.model.arrival.basic.arrival_sequence rt.model.priority.
Require Import rt.model.schedule.uni.jitter.schedule
rt.model.schedule.uni.jitter.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 UniprocessorScheduleWithJitter Platform Priority
ScheduleConstruction.
(* In this section, we implement a jitter-aware priority-based uniprocessor scheduler *)
Section Implementation.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_jitter: Job → time.
(* Let arr_seq be any job arrival sequence. *)
Variable arr_seq: arrival_sequence 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 job_jitter sched_prefix.
(* Consider the list of pending jobs with actual arrivals up to t. *)
Definition pending_jobs :=
[seq j <- actual_arrivals_up_to job_arrival job_jitter 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.
Variable job_jitter: 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.
(* Consider any JLDP policy that is reflexive, transitive and total. *)
Variable higher_eq_priority: JLDP_policy Job.
Hypothesis H_priority_is_reflexive: JLDP_is_reflexive higher_eq_priority.
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 job_jitter 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_execute_after_jitter:
jobs_execute_after_jitter job_arrival job_jitter 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 job_jitter arr_seq sched.
(* ... and respects the JLDP policy. *)
Theorem scheduler_respects_policy :
respects_JLDP_policy job_arrival job_cost job_jitter arr_seq sched higher_eq_priority.
End Proofs.
End ConcreteScheduler.