# Library prosa.analysis.facts.transform.edf_opt

From mathcomp Require Import ssrnat ssrbool fintype.

Require Import prosa.model.readiness.basic.

Require Export prosa.model.schedule.edf.

Require Export prosa.analysis.definitions.schedulability.

Require Export prosa.analysis.transform.edf_trans.

Require Export prosa.analysis.facts.transform.swaps.

Require Export prosa.analysis.facts.readiness.basic.

Require Import prosa.model.readiness.basic.

Require Export prosa.model.schedule.edf.

Require Export prosa.analysis.definitions.schedulability.

Require Export prosa.analysis.transform.edf_trans.

Require Export prosa.analysis.facts.transform.swaps.

Require Export prosa.analysis.facts.readiness.basic.

This file contains the main argument of the EDF optimality proof,
starting with an analysis of the individual functions that drive
the piece-wise transformation of a given reference schedule in an
EDF schedule, and ending with 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.

We assume the classic (i.e., Liu & Layland) model of readiness
without jitter or self-suspensions, wherein pending jobs are
always ready.

#[local] Existing Instance basic_ready_instance.

For any given type of jobs...

...consider an ideal uniprocessor schedule...

...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.

Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.

Suppose we are given a job j1...

...and a point in time t1...

...at which j1 is scheduled...

...and that is before its deadline.

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.

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.

∃ 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).

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.

∃ 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.

∀ 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.

For convenience, since we often only require the lower bound on
the interval, we re-state it as a corollary.

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.

∀ 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.

∀ 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.

For any given type of jobs...

...consider an ideal uniprocessor schedule...

...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.

Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.

...and in which no scheduled job misses a deadline.

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.

We analyze make_edf_at applied to an arbitrary point in time,
which we denote t_edf in the following.

For brevity, let sched' denote the schedule obtained from
make_edf_at applied to sched at time t_edf.

First, we observe that in sched' jobs still don't execute past
completion.

Importantly, make_edf_at does not introduce any deadline
misses, which is a crucial step in the EDF optimality
argument.

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.

∀ 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.

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'.

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.

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.

Second, by the definition of sched', j_edf is scheduled in
sched at the time returned by find_swap_candidate.

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'.

job_deadline j_orig ≤ t' →

job_deadline j_edf ≤ job_deadline j'.

Lemma mea_guarantee_case_t'_before_deadline:

t' < job_deadline j_orig →

job_deadline j_edf ≤ job_deadline j'.

End GuaranteeCaseAnalysis.

t' < job_deadline j_orig →

job_deadline j_edf ≤ job_deadline j'.

End GuaranteeCaseAnalysis.

Finally, putting the preceding cases together, we obtain the
result that make_edf_at establishes EDF_at at time
t_edf.

We observe that make_edf_at maintains the property that jobs
must arrive to execute.

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.

Conversely, if a job is scheduled in sched, it is also
scheduled somewhere in sched' since make_edf_at does not lose
any jobs.

Next, we observe that if all jobs in sched come from a given
arrival sequence, then that's still the case in sched', too.

For given arrival sequence,...

...if all jobs in sched come from the arrival sequence,...

...then all jobs in sched' do, too.

Lemma mea_jobs_come_from_arrival_sequence:

jobs_come_from_arrival_sequence sched' arr_seq.

End ArrivalSequence.

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.

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.

In the following section, we establish properties of edf_transform_prefix.

For any given type of jobs...

...consider an ideal uniprocessor schedule...

...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.

Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.

...and in which no scheduled job misses a deadline.

Consider any point in time, denoted horizon, and...

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'.

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.

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.

∀ 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.

Conversely, if a job is scheduled in the original schedule, it is
also scheduled at some point in the transformed schedule.

Next, we note that edf_transform_prefix maintains the
property that all jobs stem from a given arrival sequence.

For any arrival sequence,...

...if all jobs in the original schedule come from the arrival sequence,...

...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.

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.

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.

For any given type of jobs...

...consider an ideal uniprocessor schedule...

...that is well-behaved...

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 →

identical_prefix (edf_transform_prefix sched h1) (edf_transform_prefix sched h2) h1.

End EDFPrefixInclusion.

Lemma edf_prefix_inclusion:

∀ h1 h2,

h1 ≤ h2 →

identical_prefix (edf_transform_prefix sched h1) (edf_transform_prefix sched h2) h1.

End EDFPrefixInclusion.

In the following section, we finally establish properties of the
overall EDF transformationedf_transform.

For any given type of jobs...

...consider an ideal uniprocessor schedule...

...that is well-behaved...

Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.

...and in which no scheduled job misses a deadline.

In the following, let sched_edf denote the EDF schedule obtained by
transforming the given reference schedule.

We begin with a simple lemma relating sched_edf to its definition that
allows us to easily look at any finite prefix of the EDF-transformed
scheduled.

From this, we move on to the defining property of the transformation: the
resulting schedule is actually an EDF schedule.

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.

Similarly, we observe that no job is scheduled prior to its arrival.

We next establish the second key property: in the transformed EDF
schedule, no scheduled job misses a deadline.

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'.

∀ 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'.

∀ 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.

For any arrival sequence,...

...if all jobs in the original schedule come from the arrival sequence,...

...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.

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.

We assume the classic (i.e., Liu & Layland) model of readiness
without jitter or self-suspensions, wherein pending jobs are
always ready.

#[local] Existing Instance basic_ready_instance.

For any given type of jobs...

... consider an arbitrary valid job arrival sequence ...

... and an ideal uniprocessor schedule...

... that corresponds to the given arrival sequence.

In the following, let equivalent_edf_schedule denote the schedule that
results from the EDF transformation.

Suppose no job scheduled in the given reference schedule misses a deadline.

Then the resulting EDF schedule is a valid schedule for the given
arrival sequence...

...and no scheduled job misses its deadline.

Theorem edf_schedule_meets_all_deadlines:

all_deadlines_met equivalent_edf_schedule.

End AllDeadlinesMet.

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.

Suppose no job that's part of the arrival sequence misses a deadline in
the given reference schedule.

Then no job that's part of the arrival sequence misses a deadline in the
EDF schedule, either.