# Library prosa.analysis.facts.transform.wc_correctness

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

Require Export prosa.model.schedule.work_conserving.

Require Import prosa.model.readiness.basic.

Require Export prosa.analysis.facts.model.ideal.schedule.

Require Export prosa.analysis.transform.wc_trans.

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

Require Export prosa.analysis.definitions.schedulability.

Require Export prosa.util.list.

Require Export prosa.model.schedule.work_conserving.

Require Import prosa.model.readiness.basic.

Require Export prosa.analysis.facts.model.ideal.schedule.

Require Export prosa.analysis.transform.wc_trans.

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

Require Export prosa.analysis.definitions.schedulability.

Require Export prosa.util.list.

# Correctness of the work-conservation transformation

This file contains the main argument of the work-conservation proof, starting with an analysis of the individual functions that drive the work-conservation transformation of a given reference schedule and ending with the proofs of individual properties of the obtained work-conserving schedule.
We assume ideal uni-processor schedules.

#[local] Existing Instance ideal.processor_state.

We assume the basic (i.e., Liu & Layland)
readiness model under which any pending job is ready.

#[local] Existing Instance basic_ready_instance.

Consider any type of jobs with arrival times, costs, and deadlines...

Context {Job : JobType}.

Context `{JobArrival Job}.

Context `{JobCost Job}.

Context `{JobDeadline Job}.

Context `{JobArrival Job}.

Context `{JobCost Job}.

Context `{JobDeadline Job}.

...and an arbitrary arrival sequence.

We introduce the notion of work-conservation at a
given time t. The definition is based on the concept of readiness
of a job, and states that the presence of a ready job implies that
the processor is not idle.

Definition is_work_conserving_at sched t :=

(∃ j, arrives_in arr_seq j ∧ job_ready sched j t) →

∃ j, sched t = Some j.

(∃ j, arrives_in arr_seq j ∧ job_ready sched j t) →

∃ j, sched t = Some j.

First, we prove some useful properties about the most fundamental
operation of the work-conservation transformation: swapping two processor
states t1 and fsc, with fsc being a valid swap candidate of t1.

Consider an ideal uniprocessor schedule...

...in which jobs must be ready to execute.

Consider an arbitrary time instant t1.

...and sched' as the schedule resulting from the swap.

First, we show that, in any case, the result of the search will yield an
instant that is in the future (or, in case of failure, equal to t1).

Also, we show that the search will not yield jobs that arrive later than the
given reference time.

Lemma fsc_respects_has_arrived:

∀ j t,

sched (find_swap_candidate arr_seq sched t) == Some j →

has_arrived j t.

∀ j t,

sched (find_swap_candidate arr_seq sched t) == Some j →

has_arrived j t.

Next, we extend the previous lemma by stating that no job in the transformed
schedule is scheduled before its arrival.

Finally we show that, in the transformed schedule, jobs are scheduled
only if they are ready.

Lemma fsc_jobs_must_be_ready_to_execute:

jobs_must_be_ready_to_execute sched'.

End JobsMustBeReadyFindSwapCandidate.

jobs_must_be_ready_to_execute sched'.

End JobsMustBeReadyFindSwapCandidate.

In the following section, we put our attention on the point-wise
transformation performed at each point in time prior to the horizon.

Consider an ideal uniprocessor schedule...

...and take an arbitrary point in time...

...we define sched' as the resulting schedule after one point-wise transformation.

We start by proving that the point-wise transformation can only lead
to higher service for a job at a given time. This is true because we
swap only idle processor states with ones in which a job is scheduled.

Next, we show that any ready job in the transformed schedule must be ready also in
the original one, since the transformation can only lead to higher service.

Lemma mwa_ready_job_also_ready_in_original_schedule:

∀ j t, job_ready sched' j t → job_ready sched j t.

∀ j t, job_ready sched' j t → job_ready sched j t.

Since the search for a swap candidate is performed until the latest deadline
among all the jobs arrived before the reference time, we need to show that the computed
deadline is indeed the latest.

Lemma max_dl_is_greatest_dl:

∀ j t,

arrives_in arr_seq j →

job_arrival j ≤ t →

job_deadline j ≤ max_deadline_for_jobs_arrived_before arr_seq t.

∀ j t,

arrives_in arr_seq j →

job_arrival j ≤ t →

job_deadline j ≤ max_deadline_for_jobs_arrived_before arr_seq t.

Next, we want to show that, if a job arriving from the arrival
sequence is ready at some instant, then the point-wise transformation
is guaranteed to find a job to swap with. We will proceed by doing a case
analysis, and show that it is impossible that a swap candidate is not found.

We need to assume that, in the original schedule, all the deadlines of
the jobs coming from the arrival sequence are met, in order to be sure that
a ready job will be eventually scheduled.

Next, we define search_result as the result of the search for a swap candidate.
In order to take the first result, it is sufficient to define the ordering function
as a constant false.

Definition order (_ _ : nat) := false.

Definition search_result := search_arg sched (relevant_pstate t) order t max_dl.

Definition search_result := search_arg sched (relevant_pstate t) order t max_dl.

First, we consider the case in which the procedure finds a job to swap with.

Assuming that the processor is idle at time t...

...let t_swap be a time instant found by the search procedure.

We show that, since the search only yields relevant processor states, a job is found.

Lemma make_wc_at_case_result_found:

∃ j: Job,

swapped sched t t_swap t = Some j.

End MakeWCAtFindsReadyJobs_CaseResultFound.

∃ j: Job,

swapped sched t t_swap t = Some j.

End MakeWCAtFindsReadyJobs_CaseResultFound.

Conversely, we prove that assuming that the search yields no
result brings to a contradiction.

Consider a job that arrives in the arrival sequence, and assume that
it is ready at time t in the transformed schedule.

Variable j: Job.

Hypothesis H_arrives_in: arrives_in arr_seq j.

Hypothesis H_job_ready_sched': job_ready sched' j t.

Hypothesis H_arrives_in: arrives_in arr_seq j.

Hypothesis H_job_ready_sched': job_ready sched' j t.

Moreover, assume the search for a swap candidate yields nothing.

First, note that, since nothing was found, it means there is no relevant
processor state between t and max_dl.

On the other hand, since we know that there is no relevant state between t and max_dl,
then it must be the case that j is never scheduled in this period, and hence gets no
service.

Combining the previous lemmas, we can deduce that j misses its deadline.

The fact that j misses its deadline contradicts the fact that all deadlines
of jobs coming from the arrival sequence are met. We have a contradiction.

Next, we show that make_wc_at always manages to establish the work-conservation property
at the given time. Using the above case analysis, we can conclude that the presence of a
ready job always leads to a valid swap.

Lemma mwa_finds_ready_jobs:

all_deadlines_of_arrivals_met arr_seq sched →

is_work_conserving_at sched' t.

End MakeWCAtFindsReadyJobs.

all_deadlines_of_arrivals_met arr_seq sched →

is_work_conserving_at sched' t.

End MakeWCAtFindsReadyJobs.

Next we prove that, given a schedule that respects the work-conservation property until t-1,
applying the point-wise transformation at time t will extend the property until t.

Lemma mwa_establishes_wc:

all_deadlines_of_arrivals_met arr_seq sched →

(∀ t_l, t_l < t → is_work_conserving_at sched t_l) →

∀ t_l, t_l ≤ t → is_work_conserving_at sched' t_l.

all_deadlines_of_arrivals_met arr_seq sched →

(∀ t_l, t_l < t → is_work_conserving_at sched t_l) →

∀ t_l, t_l ≤ t → is_work_conserving_at sched' t_l.

We now show that the point-wise transformation does not introduce any new job
that does not come from the arrival sequence.

Lemma mwa_jobs_come_from_arrival_sequence:

jobs_come_from_arrival_sequence sched arr_seq →

jobs_come_from_arrival_sequence sched' arr_seq.

jobs_come_from_arrival_sequence sched arr_seq →

jobs_come_from_arrival_sequence sched' arr_seq.

We also show that the point-wise transformation does not schedule jobs in instants
in which they are not ready.

Lemma mwa_jobs_must_be_ready_to_execute:

jobs_must_be_ready_to_execute sched →

jobs_must_be_ready_to_execute sched'.

jobs_must_be_ready_to_execute sched →

jobs_must_be_ready_to_execute sched'.

Finally, we show that the point-wise transformation does not introduce deadline misses.

Lemma mwa_all_deadlines_of_arrivals_met:

all_deadlines_of_arrivals_met arr_seq sched →

all_deadlines_of_arrivals_met arr_seq sched'.

End MakeWCAtFacts.

all_deadlines_of_arrivals_met arr_seq sched →

all_deadlines_of_arrivals_met arr_seq sched'.

End MakeWCAtFacts.

In the following section, we proceed by proving some useful properties respected by
the partial schedule obtained by applying the work-conservation transformation up to
an arbitrary horizon.

Consider an ideal uniprocessor schedule.

We start by proving that the transformation performed with two different horizons
will yield two schedules that are identical until the earlier horizon.

Consider two horizons...

...and assume w.l.o.g. that they are ordered...

...we define two schedules, resulting from the transformation
performed, respectively, until the first and the second horizon.

Let sched1 := wc_transform_prefix arr_seq sched h1.

Let sched2 := wc_transform_prefix arr_seq sched h2.

Let sched2 := wc_transform_prefix arr_seq sched h2.

Then, we show that the two schedules are guaranteed to be equal until the
earlier horizon.

Next, we show that repeating the point-wise transformation up to a given horizon
does not introduce any deadline miss.

Assuming that all deadlines of jobs coming from the arrival sequence are met...

...let us define sched' as the schedule resulting from the
full work-conservation transformation. Note that, if the schedule is sampled at time
t, the transformation is performed until t+1.

Consider a job from the arrival sequence.

We show that, in the transformed schedule, the service of the job
is always greater or equal than in the original one, at any given time.

Finally, it follows directly that the transformed schedule cannot introduce
a deadline miss for any job from the arrival sequence.

Next, consider a given time, used as horizon for the transformation...

We prove that sched' will never introduce jobs not coming from the
arrival sequence.

Lemma wc_prefix_jobs_come_from_arrival_sequence:

jobs_come_from_arrival_sequence sched arr_seq →

jobs_come_from_arrival_sequence sched' arr_seq.

jobs_come_from_arrival_sequence sched arr_seq →

jobs_come_from_arrival_sequence sched' arr_seq.

Similarly, we can show that sched' will only schedule jobs if they are
ready.

Lemma wc_prefix_jobs_must_be_ready_to_execute:

jobs_must_be_ready_to_execute sched →

jobs_must_be_ready_to_execute sched'.

End PrefixFacts.

End AuxiliaryLemmasWorkConservingTransformation.

jobs_must_be_ready_to_execute sched →

jobs_must_be_ready_to_execute sched'.

End PrefixFacts.

End AuxiliaryLemmasWorkConservingTransformation.

Finally, we can leverage all the previous results to prove statements about the full
work-conservation transformation.

We assume the basic (i.e., Liu & Layland)
readiness model under which any pending job is ready.

#[local] Existing Instance basic_ready_instance.

Consider any type of jobs with arrival times, costs, and deadlines...

Context {Job : JobType}.

Context `{JobArrival Job}.

Context `{JobCost Job}.

Context `{JobDeadline Job}.

Context `{JobArrival Job}.

Context `{JobCost Job}.

Context `{JobDeadline Job}.

...an arbitrary valid arrival sequence...

...and an ideal uniprocessor schedule...

...in which jobs come from the arrival sequence, and must be ready to execute...

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

Let us call sched_wc the schedule obtained after applying the work-conservation transformation.

First, we show that any scheduled job still comes from the arrival sequence.

Similarly, jobs are only scheduled if they are ready.

Also, no deadline misses are introduced.

Finally, we can show that the transformation leads to a schedule in which
the processor is not idle if a job is ready.

Lemma wc_is_work_conserving_at:

∀ j t,

job_ready sched_wc j t →

arrives_in arr_seq j →

∃ j', sched_wc t = Some j'.

∀ j t,

job_ready sched_wc j t →

arrives_in arr_seq j →

∃ j', sched_wc t = Some j'.

We can easily extend the previous lemma to obtain the definition
of a work-conserving schedule.

Ultimately, we can show that the work-conservation transformation maintains
all the properties of validity, does not introduce new deadline misses, and
establishes the work-conservation property.