Library rt.restructuring.analysis.transform.facts.edf_opt
This file contains the main argument of the EDF optimality proof,
starting with an analysis of the individual functions that drive
the "EDF-ication" of a given reference schedule and ending with
the proofs of individual properties of the obtained EDF
schedule.
We start by analyzing the helper function [find_swap_candidate],
which is a problem-specific wrapper around [search_arg].
Section FindSwapCandidateFacts.
(* For any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
(* ...consider an ideal uniprocessor schedule... *)
Variable sched: schedule (ideal.processor_state Job).
(* ...that is well-behaved (i.e., in which jobs execute only after
having arrived and only if they are not yet complete). *)
Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
(* Suppose we are given a job [j1]... *)
Variable j1: Job.
(* ...and a point in time [t1]... *)
Variable t1: instant.
(* ...at which [j1] is scheduled... *)
Hypothesis H_not_idle: scheduled_at sched j1 t1.
(* ...and that is before its deadline. *)
Hypothesis H_deadline_not_missed: t1 < job_deadline j1.
(* First, we observe that under these assumptions the processor
state at time [t1] is "relevant" according to the notion of
relevance underlying the EDF transformation, namely
[relevant_pstate]. *)
Lemma t1_relevant: relevant_pstate t1 (sched t1).
(* Since [t1] is relevant, we conclude that a search for a relevant
state succeeds (if nothing else, it finds [t1]). *)
Lemma fsc_search_successful:
∃ t, search_arg sched (relevant_pstate t1) earlier_deadline t1 (job_deadline j1) = Some t.
(* For rewriting purposes, we observe that the [search_arg]
operation within [find_swap_candidate] yields the final result of
[find_swap_candidate]. *)
Corollary fsc_search_result:
search_arg sched (relevant_pstate t1) earlier_deadline t1 (job_deadline j1) = Some (find_swap_candidate sched t1 j1).
(* There is a job that is scheduled at the time that
[find_swap_candidate] returns, and that job arrives no later than
at time [t1]. *)
Lemma fsc_not_idle:
∃ j', (scheduled_at sched j' (find_swap_candidate sched t1 j1))
∧ job_arrival j' ≤ t1.
(* Since we are considering a uniprocessor model, only one job is
scheduled at a time. Hence once we know that a job is scheduled
at the time that [find_swap_candidate] returns, we can conclude
that it arrives not later than at time t1. *)
Corollary fsc_found_job_arrival:
∀ j2,
scheduled_at sched j2 (find_swap_candidate sched t1 j1) →
job_arrival j2 ≤ t1.
(* We observe that [find_swap_candidate] returns a value within a
known finite interval. *)
Lemma fsc_range:
t1 ≤ find_swap_candidate sched t1 j1 < job_deadline j1.
(* For convenience, since we often only require the lower bound on
the interval, we re-state it as a corollary. *)
Corollary fsc_range1:
t1 ≤ find_swap_candidate sched t1 j1.
(* The following lemma is a key step of the overall proof: the job
scheduled at the time found by [find_swap_candidate] has the
property that it has a deadline that is no later than that of any
other job in the window given by time [t1] and the deadline of
the job scheduled at time [t1]. *)
Lemma fsc_found_job_deadline:
∀ j2,
scheduled_at sched j2 (find_swap_candidate sched t1 j1) →
∀ j t,
t1 ≤ t < job_deadline j1 →
scheduled_at sched j t →
job_arrival j ≤ t1 →
job_deadline j2 ≤ job_deadline j.
(* As a special case of the above lemma, we observe that the job
scheduled at the time given by [find_swap_candidate] in
particular has a deadline no later than the job scheduled at time
[t1]. *)
Corollary fsc_no_later_deadline:
∀ j2,
scheduled_at sched j2 (find_swap_candidate sched t1 j1) →
job_deadline j2 ≤ job_deadline j1.
End FindSwapCandidateFacts.
(* For any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
(* ...consider an ideal uniprocessor schedule... *)
Variable sched: schedule (ideal.processor_state Job).
(* ...that is well-behaved (i.e., in which jobs execute only after
having arrived and only if they are not yet complete). *)
Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
(* Suppose we are given a job [j1]... *)
Variable j1: Job.
(* ...and a point in time [t1]... *)
Variable t1: instant.
(* ...at which [j1] is scheduled... *)
Hypothesis H_not_idle: scheduled_at sched j1 t1.
(* ...and that is before its deadline. *)
Hypothesis H_deadline_not_missed: t1 < job_deadline j1.
(* First, we observe that under these assumptions the processor
state at time [t1] is "relevant" according to the notion of
relevance underlying the EDF transformation, namely
[relevant_pstate]. *)
Lemma t1_relevant: relevant_pstate t1 (sched t1).
(* Since [t1] is relevant, we conclude that a search for a relevant
state succeeds (if nothing else, it finds [t1]). *)
Lemma fsc_search_successful:
∃ t, search_arg sched (relevant_pstate t1) earlier_deadline t1 (job_deadline j1) = Some t.
(* For rewriting purposes, we observe that the [search_arg]
operation within [find_swap_candidate] yields the final result of
[find_swap_candidate]. *)
Corollary fsc_search_result:
search_arg sched (relevant_pstate t1) earlier_deadline t1 (job_deadline j1) = Some (find_swap_candidate sched t1 j1).
(* There is a job that is scheduled at the time that
[find_swap_candidate] returns, and that job arrives no later than
at time [t1]. *)
Lemma fsc_not_idle:
∃ j', (scheduled_at sched j' (find_swap_candidate sched t1 j1))
∧ job_arrival j' ≤ t1.
(* Since we are considering a uniprocessor model, only one job is
scheduled at a time. Hence once we know that a job is scheduled
at the time that [find_swap_candidate] returns, we can conclude
that it arrives not later than at time t1. *)
Corollary fsc_found_job_arrival:
∀ j2,
scheduled_at sched j2 (find_swap_candidate sched t1 j1) →
job_arrival j2 ≤ t1.
(* We observe that [find_swap_candidate] returns a value within a
known finite interval. *)
Lemma fsc_range:
t1 ≤ find_swap_candidate sched t1 j1 < job_deadline j1.
(* For convenience, since we often only require the lower bound on
the interval, we re-state it as a corollary. *)
Corollary fsc_range1:
t1 ≤ find_swap_candidate sched t1 j1.
(* The following lemma is a key step of the overall proof: the job
scheduled at the time found by [find_swap_candidate] has the
property that it has a deadline that is no later than that of any
other job in the window given by time [t1] and the deadline of
the job scheduled at time [t1]. *)
Lemma fsc_found_job_deadline:
∀ j2,
scheduled_at sched j2 (find_swap_candidate sched t1 j1) →
∀ j t,
t1 ≤ t < job_deadline j1 →
scheduled_at sched j t →
job_arrival j ≤ t1 →
job_deadline j2 ≤ job_deadline j.
(* As a special case of the above lemma, we observe that the job
scheduled at the time given by [find_swap_candidate] in
particular has a deadline no later than the job scheduled at time
[t1]. *)
Corollary fsc_no_later_deadline:
∀ j2,
scheduled_at sched j2 (find_swap_candidate sched t1 j1) →
job_deadline j2 ≤ job_deadline j1.
End FindSwapCandidateFacts.
In the next section, we analyze properties of [make_edf_at], which
we abbreviate as "mea" in the following.
Section MakeEDFAtFacts.
(* For any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
(* ...consider an ideal uniprocessor schedule... *)
Variable sched: schedule (ideal.processor_state Job).
(* ...that is well-behaved... *)
Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
(* ...and in which no scheduled job misses a deadline. *)
Hypothesis H_no_deadline_misses: all_deadlines_met sched.
(* Since we will require this fact repeatedly, we briefly observe
that, since no scheduled job misses its deadline, if a job is
scheduled at some time [t], then its deadline is later than
[t]. *)
Fact scheduled_job_in_sched_has_later_deadline:
∀ j t,
scheduled_at sched j t →
job_deadline j > t.
(* We analyze [make_edf_at] applied to an arbitrary point in time,
which we denote [t_edf] in the following. *)
Variable t_edf: instant.
(* For brevity, let [sched'] denote the schedule obtained from
[make_edf_at] applied to [sched] at time [t_edf]. *)
Let sched' := make_edf_at sched t_edf.
(* First, we observe that in [sched'] jobs still don't execute past
completion. *)
Lemma mea_completed_jobs:
completed_jobs_dont_execute sched'.
(* Importantly, [make_edf_at] does not introduce any deadline
misses, which is a crucial step in the EDF optimality
argument. *)
Lemma mea_no_deadline_misses:
all_deadlines_met sched'.
(* As a result, we may conclude that any job scheduled at a time t has a deadline later than t. *)
Corollary mea_scheduled_job_has_later_deadline:
∀ j t,
scheduled_at sched' j t →
job_deadline j > t.
(* Next comes a big step in the optimality proof: we observe that
[make_edf_at] indeed ensures that [EDF_at] holds at time [t_edf] in
sched'. As this is a larger argument, we proceed by case analysis and
first establish a couple of helper lemmas in the following section. *)
Section GuaranteeCaseAnalysis.
(* Let j_orig denote the job scheduled in sched at time t_edf, let j_edf
denote the job scheduled in sched' at time t_edf, and let j' denote any
job scheduled in sched' at some time t' after t_edf... *)
Variable j_orig j_edf j': Job.
Variable t': instant.
Hypothesis H_t_edf_le_t' : t_edf ≤ t'.
Hypothesis H_sched_orig: scheduled_at sched j_orig t_edf.
Hypothesis H_sched_edf: scheduled_at sched' j_edf t_edf.
Hypothesis H_sched': scheduled_at sched' j' t'.
(* ... and that arrives before time t_edf. *)
Hypothesis H_arrival_j' : job_arrival j' ≤ t_edf.
(* We begin by observing three simple facts that will be used repeatedly in
the case analysis. *)
(* First, the deadline of j_orig is later than t_edf. *)
Fact mea_guarantee_dl_orig: t_edf < job_deadline j_orig.
(* Second, by the definition of sched', j_edf is scheduled in sched at the time
returned by [find_swap_candidate]. *)
Fact mea_guarantee_fsc_is_j_edf: sched (find_swap_candidate sched t_edf j_orig) = Some j_edf.
(* Third, the deadline of j_edf is no later than the deadline of j_orig. *)
Fact mea_guarantee_deadlines: job_deadline j_edf ≤ job_deadline j_orig.
(* With the setup in place, we are now ready to begin the case analysis. *)
(* First, we consider the simpler case where t' is no earlier than the
deadline of j_orig. This case is simpler because t' being no earlier
than j_orig's deadline implies that j' has deadline no earlier than
j_orig (since no scheduled job in sched misses a deadline), which in
turn has a deadline no earlier than j_edf. *)
Lemma mea_guarantee_case_t'_past_deadline:
job_deadline j_orig ≤ t' →
job_deadline j_edf ≤ job_deadline j'.
(* Next, we consider the more difficult case, where t' is before the
deadline of j_orig. *)
Lemma mea_guarantee_case_t'_before_deadline:
t' < job_deadline j_orig →
job_deadline j_edf ≤ job_deadline j'.
End GuaranteeCaseAnalysis.
(* Finally, putting the preceding case analysis together, we obtain the
result that [make_edf_at] establishes [EDF_at] at time [t_edf]. *)
Lemma make_edf_at_guarantee:
EDF_at sched' t_edf.
(* We observe that [make_edf_at] maintains the property that jobs must arrive
to execute. *)
Lemma mea_jobs_must_arrive:
jobs_must_arrive_to_execute sched'.
(* We connect the fact that a job is scheduled in [sched'] to the
fact that it must be scheduled somewhere in [sched], too, since
[make_edf_at] does not introduce any new jobs. *)
Lemma mea_job_scheduled:
∀ j t,
scheduled_at sched' j t →
∃ t', scheduled_at sched j t'.
(* Conversely, if a job is scheduled in [sched], it is also
scheduled somewhere in [sched'] since [make_edf_at] does not lose
any jobs. *)
Lemma mea_job_scheduled':
∀ j t,
scheduled_at sched j t →
∃ t', scheduled_at sched' j t'.
(* Next, we observe that if all jobs in [sched] come from a given
arrival sequence, then that's still the case in [sched'], too. *)
Section ArrivalSequence.
(* For given arrival sequence,... *)
Variable arr_seq: arrival_sequence Job.
(* ...if all jobs in [sched] come from the arrival sequence,... *)
Hypothesis H_from_arr_seq: jobs_come_from_arrival_sequence sched arr_seq.
(* ...then all jobs in [sched'] do, too. *)
Lemma mea_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched' arr_seq.
End ArrivalSequence.
(* For the final claim, assume that [EDF_at] already holds
everywhere prior to time [t_edf], i.e., that [sched] consists of
an EDF prefix. *)
Hypothesis H_EDF_prefix: ∀ t, t < t_edf → EDF_at sched t.
(* We establish a key property of [make_edf_at]: not only does it
ensure [EDF_at] at time [t_edf], it also maintains the fact that
the schedule has an EDF prefix prior to time [t_edf]. In other
words, it grows the EDF prefix by one time unit. *)
Lemma mea_EDF_widen:
∀ t, t ≤ t_edf → EDF_at sched' t.
End MakeEDFAtFacts.
(* For any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
(* ...consider an ideal uniprocessor schedule... *)
Variable sched: schedule (ideal.processor_state Job).
(* ...that is well-behaved... *)
Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
(* ...and in which no scheduled job misses a deadline. *)
Hypothesis H_no_deadline_misses: all_deadlines_met sched.
(* Since we will require this fact repeatedly, we briefly observe
that, since no scheduled job misses its deadline, if a job is
scheduled at some time [t], then its deadline is later than
[t]. *)
Fact scheduled_job_in_sched_has_later_deadline:
∀ j t,
scheduled_at sched j t →
job_deadline j > t.
(* We analyze [make_edf_at] applied to an arbitrary point in time,
which we denote [t_edf] in the following. *)
Variable t_edf: instant.
(* For brevity, let [sched'] denote the schedule obtained from
[make_edf_at] applied to [sched] at time [t_edf]. *)
Let sched' := make_edf_at sched t_edf.
(* First, we observe that in [sched'] jobs still don't execute past
completion. *)
Lemma mea_completed_jobs:
completed_jobs_dont_execute sched'.
(* Importantly, [make_edf_at] does not introduce any deadline
misses, which is a crucial step in the EDF optimality
argument. *)
Lemma mea_no_deadline_misses:
all_deadlines_met sched'.
(* As a result, we may conclude that any job scheduled at a time t has a deadline later than t. *)
Corollary mea_scheduled_job_has_later_deadline:
∀ j t,
scheduled_at sched' j t →
job_deadline j > t.
(* Next comes a big step in the optimality proof: we observe that
[make_edf_at] indeed ensures that [EDF_at] holds at time [t_edf] in
sched'. As this is a larger argument, we proceed by case analysis and
first establish a couple of helper lemmas in the following section. *)
Section GuaranteeCaseAnalysis.
(* Let j_orig denote the job scheduled in sched at time t_edf, let j_edf
denote the job scheduled in sched' at time t_edf, and let j' denote any
job scheduled in sched' at some time t' after t_edf... *)
Variable j_orig j_edf j': Job.
Variable t': instant.
Hypothesis H_t_edf_le_t' : t_edf ≤ t'.
Hypothesis H_sched_orig: scheduled_at sched j_orig t_edf.
Hypothesis H_sched_edf: scheduled_at sched' j_edf t_edf.
Hypothesis H_sched': scheduled_at sched' j' t'.
(* ... and that arrives before time t_edf. *)
Hypothesis H_arrival_j' : job_arrival j' ≤ t_edf.
(* We begin by observing three simple facts that will be used repeatedly in
the case analysis. *)
(* First, the deadline of j_orig is later than t_edf. *)
Fact mea_guarantee_dl_orig: t_edf < job_deadline j_orig.
(* Second, by the definition of sched', j_edf is scheduled in sched at the time
returned by [find_swap_candidate]. *)
Fact mea_guarantee_fsc_is_j_edf: sched (find_swap_candidate sched t_edf j_orig) = Some j_edf.
(* Third, the deadline of j_edf is no later than the deadline of j_orig. *)
Fact mea_guarantee_deadlines: job_deadline j_edf ≤ job_deadline j_orig.
(* With the setup in place, we are now ready to begin the case analysis. *)
(* First, we consider the simpler case where t' is no earlier than the
deadline of j_orig. This case is simpler because t' being no earlier
than j_orig's deadline implies that j' has deadline no earlier than
j_orig (since no scheduled job in sched misses a deadline), which in
turn has a deadline no earlier than j_edf. *)
Lemma mea_guarantee_case_t'_past_deadline:
job_deadline j_orig ≤ t' →
job_deadline j_edf ≤ job_deadline j'.
(* Next, we consider the more difficult case, where t' is before the
deadline of j_orig. *)
Lemma mea_guarantee_case_t'_before_deadline:
t' < job_deadline j_orig →
job_deadline j_edf ≤ job_deadline j'.
End GuaranteeCaseAnalysis.
(* Finally, putting the preceding case analysis together, we obtain the
result that [make_edf_at] establishes [EDF_at] at time [t_edf]. *)
Lemma make_edf_at_guarantee:
EDF_at sched' t_edf.
(* We observe that [make_edf_at] maintains the property that jobs must arrive
to execute. *)
Lemma mea_jobs_must_arrive:
jobs_must_arrive_to_execute sched'.
(* We connect the fact that a job is scheduled in [sched'] to the
fact that it must be scheduled somewhere in [sched], too, since
[make_edf_at] does not introduce any new jobs. *)
Lemma mea_job_scheduled:
∀ j t,
scheduled_at sched' j t →
∃ t', scheduled_at sched j t'.
(* Conversely, if a job is scheduled in [sched], it is also
scheduled somewhere in [sched'] since [make_edf_at] does not lose
any jobs. *)
Lemma mea_job_scheduled':
∀ j t,
scheduled_at sched j t →
∃ t', scheduled_at sched' j t'.
(* Next, we observe that if all jobs in [sched] come from a given
arrival sequence, then that's still the case in [sched'], too. *)
Section ArrivalSequence.
(* For given arrival sequence,... *)
Variable arr_seq: arrival_sequence Job.
(* ...if all jobs in [sched] come from the arrival sequence,... *)
Hypothesis H_from_arr_seq: jobs_come_from_arrival_sequence sched arr_seq.
(* ...then all jobs in [sched'] do, too. *)
Lemma mea_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched' arr_seq.
End ArrivalSequence.
(* For the final claim, assume that [EDF_at] already holds
everywhere prior to time [t_edf], i.e., that [sched] consists of
an EDF prefix. *)
Hypothesis H_EDF_prefix: ∀ t, t < t_edf → EDF_at sched t.
(* We establish a key property of [make_edf_at]: not only does it
ensure [EDF_at] at time [t_edf], it also maintains the fact that
the schedule has an EDF prefix prior to time [t_edf]. In other
words, it grows the EDF prefix by one time unit. *)
Lemma mea_EDF_widen:
∀ t, t ≤ t_edf → EDF_at sched' t.
End MakeEDFAtFacts.
In the following section, we establish properties of [edf_transform_prefix].
Section EDFPrefixFacts.
(* For any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
(* ...consider an ideal uniprocessor schedule... *)
Variable sched: schedule (ideal.processor_state Job).
(* ...that is well-behaved... *)
Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
(* ...and in which no scheduled job misses a deadline. *)
Hypothesis H_no_deadline_misses: all_deadlines_met sched.
(* Consider any point in time, denoted [horizon], and... *)
Variable horizon: instant.
(* ...let [sched'] denote the schedule obtained by EDF-ifying
[sched] up to the horizon. *)
Let sched' := edf_transform_prefix sched horizon.
(* To start, we observe that [sched'] is still well-behaved and
without deadline misses. *)
Lemma edf_prefix_well_formedness:
completed_jobs_dont_execute sched'
∧
jobs_must_arrive_to_execute sched'
∧
all_deadlines_met sched'.
(* Because it is needed frequently, we extract the second clause of
the above conjunction as a corollary. *)
Corollary edf_prefix_jobs_must_arrive:
jobs_must_arrive_to_execute sched'.
(* We similarly observe that the absence of deadline misses implies
that any scheduled job must have a deadline at a time later then
when it is scheduled. *)
Corollary edf_prefix_scheduled_job_has_later_deadline:
∀ j t,
scheduled_at sched' j t →
job_deadline j > t.
(* Since no jobs are lost or added to the schedule by
[edf_transform_prefix], we if a job is scheduled in the
transformed schedule, then it is also scheduled at some point in
the original schedule. *)
Lemma edf_prefix_job_scheduled:
∀ j t,
scheduled_at sched' j t →
∃ t', scheduled_at sched j t'.
(* Conversely, if a job is scheduled in the original schedule, it is
also scheduled at some point in the transformed schedule. *)
Lemma edf_prefix_job_scheduled':
∀ j t,
scheduled_at sched j t →
∃ t', scheduled_at sched' j t'.
(* Next, we note that [edf_transform_prefix] maintains the
property that all jobs stem from a given arrival sequence. *)
Section ArrivalSequence.
(* For any arrival sequence,... *)
Variable arr_seq: arrival_sequence Job.
(* ...if all jobs in the original schedule come from the arrival sequence,... *)
Hypothesis H_from_arr_seq: jobs_come_from_arrival_sequence sched arr_seq.
(* ...then all jobs in the transformed schedule still come from
the same arrival sequence. *)
Lemma edf_prefix_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched' arr_seq.
End ArrivalSequence.
(* We establish the key property of [edf_transform_prefix]: that it indeed
ensures that the resulting schedule ensures the EDF invariant up to the
given [horizon]. *)
Lemma edf_prefix_guarantee:
∀ t,
t < horizon →
EDF_at sched' t.
End EDFPrefixFacts.
(* Finally, we observe that [edf_transform_prefix] is prefix-stable, which
allows us to replace an earlier horizon with a later horizon. Note: this is
in a separate section because we need [edf_prefix_jobs_must_arrive]
generalized for any schedule. *)
Section EDFPrefixInclusion.
(* For any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
(* ...consider an ideal uniprocessor schedule... *)
Variable sched: schedule (ideal.processor_state Job).
(* ...that is well-behaved... *)
Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
(* ...and in which no scheduled job misses a deadline. *)
Hypothesis H_no_deadline_misses: all_deadlines_met sched.
Lemma edf_prefix_inclusion:
∀ h1 h2,
h1 ≤ h2 →
∀ t,
t < h1 →
(edf_transform_prefix sched h1) t = (edf_transform_prefix sched h2) t.
End EDFPrefixInclusion.
(* For any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
(* ...consider an ideal uniprocessor schedule... *)
Variable sched: schedule (ideal.processor_state Job).
(* ...that is well-behaved... *)
Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
(* ...and in which no scheduled job misses a deadline. *)
Hypothesis H_no_deadline_misses: all_deadlines_met sched.
(* Consider any point in time, denoted [horizon], and... *)
Variable horizon: instant.
(* ...let [sched'] denote the schedule obtained by EDF-ifying
[sched] up to the horizon. *)
Let sched' := edf_transform_prefix sched horizon.
(* To start, we observe that [sched'] is still well-behaved and
without deadline misses. *)
Lemma edf_prefix_well_formedness:
completed_jobs_dont_execute sched'
∧
jobs_must_arrive_to_execute sched'
∧
all_deadlines_met sched'.
(* Because it is needed frequently, we extract the second clause of
the above conjunction as a corollary. *)
Corollary edf_prefix_jobs_must_arrive:
jobs_must_arrive_to_execute sched'.
(* We similarly observe that the absence of deadline misses implies
that any scheduled job must have a deadline at a time later then
when it is scheduled. *)
Corollary edf_prefix_scheduled_job_has_later_deadline:
∀ j t,
scheduled_at sched' j t →
job_deadline j > t.
(* Since no jobs are lost or added to the schedule by
[edf_transform_prefix], we if a job is scheduled in the
transformed schedule, then it is also scheduled at some point in
the original schedule. *)
Lemma edf_prefix_job_scheduled:
∀ j t,
scheduled_at sched' j t →
∃ t', scheduled_at sched j t'.
(* Conversely, if a job is scheduled in the original schedule, it is
also scheduled at some point in the transformed schedule. *)
Lemma edf_prefix_job_scheduled':
∀ j t,
scheduled_at sched j t →
∃ t', scheduled_at sched' j t'.
(* Next, we note that [edf_transform_prefix] maintains the
property that all jobs stem from a given arrival sequence. *)
Section ArrivalSequence.
(* For any arrival sequence,... *)
Variable arr_seq: arrival_sequence Job.
(* ...if all jobs in the original schedule come from the arrival sequence,... *)
Hypothesis H_from_arr_seq: jobs_come_from_arrival_sequence sched arr_seq.
(* ...then all jobs in the transformed schedule still come from
the same arrival sequence. *)
Lemma edf_prefix_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched' arr_seq.
End ArrivalSequence.
(* We establish the key property of [edf_transform_prefix]: that it indeed
ensures that the resulting schedule ensures the EDF invariant up to the
given [horizon]. *)
Lemma edf_prefix_guarantee:
∀ t,
t < horizon →
EDF_at sched' t.
End EDFPrefixFacts.
(* Finally, we observe that [edf_transform_prefix] is prefix-stable, which
allows us to replace an earlier horizon with a later horizon. Note: this is
in a separate section because we need [edf_prefix_jobs_must_arrive]
generalized for any schedule. *)
Section EDFPrefixInclusion.
(* For any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
(* ...consider an ideal uniprocessor schedule... *)
Variable sched: schedule (ideal.processor_state Job).
(* ...that is well-behaved... *)
Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
(* ...and in which no scheduled job misses a deadline. *)
Hypothesis H_no_deadline_misses: all_deadlines_met sched.
Lemma edf_prefix_inclusion:
∀ h1 h2,
h1 ≤ h2 →
∀ t,
t < h1 →
(edf_transform_prefix sched h1) t = (edf_transform_prefix sched h2) t.
End EDFPrefixInclusion.
In the following section, we finally establish properties of the overall
EDF-ication operation [edf_transform].
Section EDFTransformFacts.
(* For any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
(* ...consider an ideal uniprocessor schedule... *)
Variable sched: schedule (ideal.processor_state Job).
(* ...that is well-behaved... *)
Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
(* ...and in which no scheduled job misses a deadline. *)
Hypothesis H_no_deadline_misses: all_deadlines_met sched.
(* In the following, let [sched_edf] denote the EDF schedule obtained by
transforming the given reference schedule. *)
Let sched_edf := edf_transform sched.
(* We begin with the first key property: the resulting schedule is actually
an EDF schedule. *)
Theorem edf_transform_ensures_edf:
is_EDF_schedule sched_edf.
(* Next, we observe that completed jobs still don't execute in the resulting
EDF schedule. This observation is needed to establish that the resulting
EDF schedule is valid. *)
Lemma edf_transform_completed_jobs_dont_execute:
completed_jobs_dont_execute sched_edf.
(* Similarly, we observe that no job is scheduled prior to its arrival. *)
Lemma edf_transform_jobs_must_arrive:
jobs_must_arrive_to_execute sched_edf.
(* We next establish the second key property: in the transformed EDF
schedule, no scheduled job misses a deadline. *)
Theorem edf_transform_deadlines_met:
all_deadlines_met sched_edf.
(* We observe that no new jobs are introduced: any job scheduled in the EDF
schedule were also present in the reference schedule. *)
Lemma edf_transform_job_scheduled:
∀ j t, scheduled_at sched_edf j t → ∃ t', scheduled_at sched j t'.
(* Conversely, we observe that no jobs are lost: any job scheduled in the
reference schedule is also present in the EDF schedule. *)
Lemma edf_transform_job_scheduled':
∀ j t, scheduled_at sched j t → ∃ t', scheduled_at sched_edf j t'.
(* Next, we note that [edf_transform] maintains the property that all jobs
stem from a given arrival sequence. *)
Section ArrivalSequence.
(* For any arrival sequence,... *)
Variable arr_seq: arrival_sequence Job.
(* ...if all jobs in the original schedule come from the arrival sequence,... *)
Hypothesis H_from_arr_seq: jobs_come_from_arrival_sequence sched arr_seq.
(* ...then all jobs in the transformed EDF schedule still come from the
same arrival sequence. *)
Lemma edf_transform_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched_edf arr_seq.
End ArrivalSequence.
End EDFTransformFacts.
(* For any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
(* ...consider an ideal uniprocessor schedule... *)
Variable sched: schedule (ideal.processor_state Job).
(* ...that is well-behaved... *)
Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
(* ...and in which no scheduled job misses a deadline. *)
Hypothesis H_no_deadline_misses: all_deadlines_met sched.
(* In the following, let [sched_edf] denote the EDF schedule obtained by
transforming the given reference schedule. *)
Let sched_edf := edf_transform sched.
(* We begin with the first key property: the resulting schedule is actually
an EDF schedule. *)
Theorem edf_transform_ensures_edf:
is_EDF_schedule sched_edf.
(* Next, we observe that completed jobs still don't execute in the resulting
EDF schedule. This observation is needed to establish that the resulting
EDF schedule is valid. *)
Lemma edf_transform_completed_jobs_dont_execute:
completed_jobs_dont_execute sched_edf.
(* Similarly, we observe that no job is scheduled prior to its arrival. *)
Lemma edf_transform_jobs_must_arrive:
jobs_must_arrive_to_execute sched_edf.
(* We next establish the second key property: in the transformed EDF
schedule, no scheduled job misses a deadline. *)
Theorem edf_transform_deadlines_met:
all_deadlines_met sched_edf.
(* We observe that no new jobs are introduced: any job scheduled in the EDF
schedule were also present in the reference schedule. *)
Lemma edf_transform_job_scheduled:
∀ j t, scheduled_at sched_edf j t → ∃ t', scheduled_at sched j t'.
(* Conversely, we observe that no jobs are lost: any job scheduled in the
reference schedule is also present in the EDF schedule. *)
Lemma edf_transform_job_scheduled':
∀ j t, scheduled_at sched j t → ∃ t', scheduled_at sched_edf j t'.
(* Next, we note that [edf_transform] maintains the property that all jobs
stem from a given arrival sequence. *)
Section ArrivalSequence.
(* For any arrival sequence,... *)
Variable arr_seq: arrival_sequence Job.
(* ...if all jobs in the original schedule come from the arrival sequence,... *)
Hypothesis H_from_arr_seq: jobs_come_from_arrival_sequence sched arr_seq.
(* ...then all jobs in the transformed EDF schedule still come from the
same arrival sequence. *)
Lemma edf_transform_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched_edf arr_seq.
End ArrivalSequence.
End EDFTransformFacts.
Finally, we state the theorems that jointly make up the EDF optimality claim.
Section Optimality.
(* For any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
(* ... consider an arbitrary valid job arrival sequence ... *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arr_seq_valid: valid_arrival_sequence arr_seq.
(* ... and an ideal uniprocessor schedule... *)
Variable sched: schedule (ideal.processor_state Job).
(* ... that corresponds to the given arrival sequence. *)
Hypothesis H_sched_valid: valid_schedule sched arr_seq.
(* In the following, let [equivalent_edf_schedule] denote the schedule that
results from the EDF transformation. *)
Let equivalent_edf_schedule := edf_transform sched.
Section AllDeadlinesMet.
(* Suppose no job scheduled in the given reference schedule misses a deadline. *)
Hypothesis H_no_deadline_misses: all_deadlines_met sched.
(* Then the resulting EDF schedule is a valid schedule for the given
arrival sequence... *)
Theorem edf_schedule_is_valid:
valid_schedule equivalent_edf_schedule arr_seq.
(* ...and no scheduled job misses its deadline. *)
Theorem edf_schedule_meets_all_deadlines:
all_deadlines_met equivalent_edf_schedule.
End AllDeadlinesMet.
(* Next, we strengthen the above "no deadline misses" claim by relating it
not just to all scheduled jobs, but to all jobs in the given arrival
sequence. *)
Section AllDeadlinesOfArrivalsMet.
(* Suppose no job that's part of the arrival sequence misses a deadline in
the given reference schedule. *)
Hypothesis H_no_deadline_misses_of_arrivals: all_deadlines_of_arrivals_met arr_seq sched.
(* Then no job that's part of the arrival sequence misses a deadline in the
EDF schedule, either. *)
Theorem edf_schedule_meets_all_deadlines_wrt_arrivals:
all_deadlines_of_arrivals_met arr_seq equivalent_edf_schedule.
End AllDeadlinesOfArrivalsMet.
End Optimality.
(* For any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
(* ... consider an arbitrary valid job arrival sequence ... *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arr_seq_valid: valid_arrival_sequence arr_seq.
(* ... and an ideal uniprocessor schedule... *)
Variable sched: schedule (ideal.processor_state Job).
(* ... that corresponds to the given arrival sequence. *)
Hypothesis H_sched_valid: valid_schedule sched arr_seq.
(* In the following, let [equivalent_edf_schedule] denote the schedule that
results from the EDF transformation. *)
Let equivalent_edf_schedule := edf_transform sched.
Section AllDeadlinesMet.
(* Suppose no job scheduled in the given reference schedule misses a deadline. *)
Hypothesis H_no_deadline_misses: all_deadlines_met sched.
(* Then the resulting EDF schedule is a valid schedule for the given
arrival sequence... *)
Theorem edf_schedule_is_valid:
valid_schedule equivalent_edf_schedule arr_seq.
(* ...and no scheduled job misses its deadline. *)
Theorem edf_schedule_meets_all_deadlines:
all_deadlines_met equivalent_edf_schedule.
End AllDeadlinesMet.
(* Next, we strengthen the above "no deadline misses" claim by relating it
not just to all scheduled jobs, but to all jobs in the given arrival
sequence. *)
Section AllDeadlinesOfArrivalsMet.
(* Suppose no job that's part of the arrival sequence misses a deadline in
the given reference schedule. *)
Hypothesis H_no_deadline_misses_of_arrivals: all_deadlines_of_arrivals_met arr_seq sched.
(* Then no job that's part of the arrival sequence misses a deadline in the
EDF schedule, either. *)
Theorem edf_schedule_meets_all_deadlines_wrt_arrivals:
all_deadlines_of_arrivals_met arr_seq equivalent_edf_schedule.
End AllDeadlinesOfArrivalsMet.
End Optimality.