Library prosa.analysis.facts.transform.swaps

In this file, we establish invariants about schedules in which two allocations have been swapped, as for instance it is done in the classic EDF optimality proof.

For any given type of jobs...

... any given type of processor states:

...consider any given reference schedule.

Suppose we are given two specific times t1 and t2.

In the following, let sched' denote the schedule in which the allocations at t1 and t2 have been swapped.

First, we note that the trivial case where t1 == t2 is not interesting because then the two schedules are identical.

In this trivial case, the amount of service received hence is obviously always identical.

In any case, the two schedules do not differ at non-swapped times.

By definition, if a job is scheduled at t2 in the original schedule, then it is found at t1 in the new schedule.

Similarly, a job scheduled at t1 in the original schedule is scheduled at t2 after the swap.

If a job is scheduled at any time not involved in the swap, then it remains scheduled at that time in the new schedule.

To make case analysis more convenient, we summarize the preceding three lemmas as a disjunction.

From this, we can easily conclude that no jobs have appeared out of thin air: if a job scheduled at some time in the new schedule, then it was also scheduled at some time in the original schedule.

Mirroring swap_job_scheduled_cases above, we also state a disjunction for case analysis under the premise that a job is scheduled in the original schedule.

Thus, we can conclude that no jobs are lost: if a job is scheduled at some point in the original schedule, then it is also scheduled at some point in the new schedule.

In the following, we lift the above basic invariants to statements about invariants about the cumulative amount of service received. To avoid dealing with symmetric cases, assume in the following that t1 and t2 are ordered.

As another trivial invariant, we observe that nothing has changed before time t1.

Similarly, nothing has changed after time t2.

Thus, we observe that, before t1, the two schedules are identical with regard to the service received by any job because they are identical.

Likewise, we observe that, *after* t2, the swapped schedule again does not differ with regard to the service received by any job.

Finally, we note that, trivially, jobs that are not involved in the swap receive invariant service.

In the following section, we observe that, if the original schedule satisfies certain properties, then so does the new scheduled obtained by swapping the allocations at times t1 and t2.

For any given type of jobs...

... any given type of processor states:

...consider any given reference schedule.

Suppose we are given two specific times t1 and t2...

...such that t1 is no later than t2.

We let sched' denote the schedule in which the allocations at t1 and t2 have been swapped.

First, we observe that if jobs never accumulate more service than required, then that's still the case after the swap.

From the above service bound, we conclude that, if if completed jobs don't execute in the original schedule, then that's still the case after the swap, assuming an ideal unit-service model (i.e., scheduled jobs receive exactly one unit of service).

Suppose all jobs in the original schedule come from some arrival sequence...

...then that's still the case in the new schedule.

In the next section, we consider a special case of swaps: namely, when the job moved earlier has an earlier deadline than the job being moved to a later allocation, assuming that the former has not yet missed its deadline, which is the core transformation of the classic EDF optimality proof.

For any given type of jobs with costs and deadlines...

... any given type of processor states...

...consider a given reference schedule...

...in which complete jobs don't execute...

...and scheduled jobs always receive service.

Suppose we are given two specific times t1 and t2...

...that are ordered.

Further, assume that, if there are jobs scheduled at times t1 and t2, then they either have the same deadline or violate EDF, ...

...and that we don't move idle times or deadline misses earlier, i.e., if t1 is not an idle time, then neither is t2 and whatever job is scheduled at time t2 has not yet missed its deadline.

Consider the schedule obtained from swapping the allocations at times t1 and t2.

The key property of this transformation is that, for any job that meets its deadline in the original schedule, we have not introduced any deadline misses, which we establish by considering a number of different cases.

Consider any job...

... that meets its deadline in the original schedule.

First we observe that jobs that are not involved in the swap still meet their deadlines.

Next, we observe that a swap is unproblematic for the job scheduled at time t2.

Finally, we observe is also unproblematic for the job that is moved to a later allocation.

From the above case analysis, we conclude that no deadline misses are introduced in the schedule obtained from swapping the allocations at times t1 and t2.