Transfer Schedulability for Ideal Uniprocessors

This module provides the mechanized result from the following paper:

• Willemsen et al., “Transfer Schedulability in Periodic Real-Time Systems”, EMSOFT 2025 / ACM TECS, 2025.
  DOI: 10.1145/3763236

Overview and Dependencies

Transfer schedulability is a concept that allows mimicking the behavior of some reference schedule in an online schedule such that no job finishes later in the online schedule than in the reference schedule. In this development, we define the exact transfer schedulability criterion and prove two sufficient conditions and one necessary condition. In particular, we are concerned solely with the conditions under which such a schedulability transfer is guaranteed. We do not concern ourselves with any particular mechanism for accomplishing such a transfer at runtime. The following line imports Prosa's utility library, which in turn pulls in the SSReflect tactics language that we use to construct proofs.

We build on Prosa's central modeling definitions and many auxiliary lemmas.

In particular, we restrict our focus exclusively to ideal uniprocessor schedules in the following.

System Model

We are now ready to introduce the general system model upon which our analysis rests.

We consider jobs that are characterized by arrival times and deadlines. No assumptions are made on how jobs relate (or whether they do so at all) and on how deadlines relate to arrival times. (We do not consider any "task" concept in this file.)

As already mentioned, we consider ideal uniprocessor schedules. To this end, let us recall Prosa's existing definition of this common assumption. (For convenience and to match Prosa convention, we will refer to the ideal uniprocessor state simply as PState.)

Next, we introduce the two key elements of the model. First, assume we are given a reference schedule, called ref_sched in the following. This is the schedule that we assume is being emulated.

Second, we consider a second online schedule called online_sched, which is the schedule to which schedulability is supposed to be transferred.

We need to consider two different job costs: the one planned for in the reference schedule, called ref_job_cost, and the one actually exhibited in the online schedule, called online_job_cost.

When we say that a job is complete in the reference schedule, it is a statement w.r.t. the reference cost job_cost_ref. Conversely, when we say that a job is complete in the online schedule, it is a statement w.r.t. the online cost job_cost_online. For ease of reference, we define respective local abbreviations. Syntax hint: The "@" notation allows us to explicitly specify parameters that are usually implicitly inferred, such as the job-cost parameter in our case here.

Well-Formedness of the Schedules

In order to prove the desired results, we need to place some mild assumptions on the reference and online schedules. The following hypotheses express these well-formedness requirements. First of all, we assume that the (possibly infinite) set of jobs to be scheduled is characterized by the arrival sequence, called arr_seq, which is a standard modeling element in Prosa. Note that arr_seq is a section variable and hence implicitly ∀-quantified. The results established in this file thus hold w.r.t. any arrival sequence (in which each job arrives at most once).

Next, we require that the reference schedule indeed contains only jobs that arrive in the system.

Additionally, we require the reference schedule to be well-formed: any job that executes must have arrived and not yet completed.

Finally, we also require that completed jobs don't execute past their completion in the online schedule.

Definition of Schedulability Transfer

By "transfer schedulability", we refer to the property that no job finishes later in the online schedule than in the reference schedule. That is, if a job j is finished at a given time t in the reference schedule, then the same job is also finished at time t in the online schedule.

As a corollary, we next observe that this notion trivially extends to deadlines. As before, we need to be careful to refer to the appropriate job-cost parameter.

We can now re-state the schedulability-transfer property in terms of job deadlines: Assuming that the schedulability_transferred property holds, a job meets its deadline in the online schedule if it meets its deadline in the reference schedule.

Setup for the Generic Argument

We are now ready to start establishing the desired results. Since we want to prove two variants of the sufficiency condition, one for online_job_cost and one for ref_job_cost, we are abstracting in the following from the specific job-cost parameter.

Let job_cost_bound denote an upper bound on the cost of each job in online_sched. Below, we are going to instantiate job_cost_bound once as online_job_cost and once as ref_job_cost, but technically it could be any bound in between the two extremes.

We require that job_cost_bound indeed upper-bounds the online cost of any job.

Conversely, we require that the reference cost ref_job_cost upper-bounds the job_cost_bound used in this section.

As a trivial corollary, by transitivity the reference cost also bounds the online cost.

The Remaining Job-Cost Bound

We next introduce one of the central elements of the proof: the remaining job-cost bound, which for a given job j and given time t relates the amount of service received by j up to time t in the online schedule to the generic upper bound given by job_cost_bound.

As the proofs must reason about remaining_cost_bound quite a bit, we require a few auxiliary lemmas related to this definition, which we introduce below. Most of these are common-sense facts that will be obvious to a human reader.

Basic Facts About the Remaining Job-Cost Bound

The remaining job-cost bound at a given time t can be split into the remaining cost at the next point in time t.+1 and the service received at time t itself.

We can trivially lift the preceding fact to entire intervals.

Furthermore, we can lift the preceding whole-interval observation to arbitrary sets of jobs. Notation hint: xpredT is the trivial dummy predicate that is always true, i.e., no jobs are being filtered here.

If we further know that, at each point in the interval, some job in the set of jobs under consideration is scheduled, then we can relate the remaining job-cost bound to the interval length. This is a crucial reasoning step, as it allows us to conclude that the remaining cost must be zero at time t2 if the interval length equals the total remaining cost (as it will in our proof below). Notation hint: uniq js means that js is indeed a set, i.e., technically a list without repetitions.

Relation to the Remaining Online Cost

As the purpose of the remaining job-cost bound is to upper-bound the leftover runtime of jobs in the online schedule, we introduce a few auxiliary lemmas relating the (true) remaining online cost to the (over-approximating) job-cost bound. As before, we introduce an intuitive alias to succinctly refer to the remaining online cost. The definition used here, remaining_cost, is a standard Prosa construct.

As intended, the remaining job-cost bound indeed upper-bounds the remaining online cost.

Furthermore, the remaining job-cost bound of any incomplete job is necessarily positive.

Conversely, if the total remaining job-cost bound of a set of jobs hits zero, then every job in the set is necessarily complete.

The Set of Critical Jobs

The second major element in the proof is the notion of the set of critical jobs at a given time t1 w.r.t. to a reference time t2. Intuitively, the critical jobs are those that must be scheduled immediately in order to avoid a deadline miss. Technically, based on the arrival sequence arr_seq, given an interval [t1, t2), we define the set of critical jobs to be those that

• are not finished at time t1 in the online schedule and
• are finished in the reference schedule at time t2.

Notation hint: [seq j <- some_sequence | filter_predicate_on j ] is MathComp's notation for a list comprehension, similarly to those encountered in for instance Haskell or Python.

Basic Facts About the Set of Critical Jobs

To reason about critical jobs, we establish a number of facts about them that will be fairly obvious to a human reader. To begin with, if a job is critical at a time t2 w.r.t. a reference time t3, then it is also critical at any earlier time t1 w.r.t. the same reference time.

If a job is critical at a time t1 w.r.t. a reference time t3 and no longer critical at a later time t2 (w.r.t. the same reference time), then it must have completed in the meantime.

We can thus express the set of critical jobs at a time t2 w.r.t. a reference time t3 as the set of critical jobs at an earlier time t1 (w.r.t. the same reference time) by filtering out all jobs that completed in the meantime.

Since the set of jobs is defined in terms of the arrival sequence (in which each job arrives at most once), the set of critical jobs is indeed a proper set (that is represented as a sequence without repeated elements).

We observe that the generic job-cost bound implies a lower bound on the earliest-possible completion time of any critical jobs at time zero. This lemma may appear somewhat contrived at first sight, but represents an important reasoning step to rule out a corner case at time zero.

Finally, we observe that the total remaining job-cost bound of a set of critical jobs is monotonically decreasing.

Definition of Slackless Intervals

The third and final major element of the proof is the concept of "slackless intervals," which we define next. Slackless intervals tie together the remaining job-cost bound and the notion of critical jobs. In the definition of a "slackless interval," the "slack" is computed based on the generic job-cost bound, since the online job cost is assumed to be unknown until after the job's completion (i.e., we seek to support also the non-clairvoyant setting). More precisely, we call a non-empty interval [t1, t2) slackless if the total remaining job-cost bound of the critical jobs at time t1 (w.r.t. reference time t2) is exactly equal to the interval length t2 - t1.

In fact, in our proof we require a stronger notion of slackless intervals: slackless intervals without "holes." To this end, we call an interval [t1, t2) contiguously slackless if [t1, t2) is slackless (and hence non-empty) and every suffix interval ending at t2 is also slackless. Notation hints:

• The notation 'I_(t2 - t1) is MathComp's notation for a bounded natural number, i.e., for the set {0, 1, 2, ..., t2 - t1 - 1}.
• The notation [∀ delta, some_predicate_on delta ] is conceptually the same as the standard (∀ delta, some_property_on delta), but defined on a finite type and hence in bool and not Prop, and therefore computable (which we'll need).

Technical comment: the definition is slightly redundant, because the ∀-quantified part covers also [t1, t2), but by requiring slackless_interval t1 t2 explicitly we avoid having to deal with empty intervals.

We are now ready to state the main property: To guarantee the transfer of schedulability, we define the following property, which forces critical jobs to be scheduled at the beginning of slackless intervals.

The Schedulability Transfer Criterion

The condition schedulability_transferred --- no job finishes later in the online schedule than in the reference schedule --- is simple and intuitive, but has one major downside: it can only be checked after the fact, that is, whether a schedule satisfies it becomes apparent only when it's already too late to do anything about a possible deadline violation. We therefore next introduce a definition equivalent to schedulability_transferred that can be checked before reaching a job's deadline, namely at the beginning of a slackless interval in which it is part of the critical jobs. In short, the criterion requires that a critical job is scheduled at the beginning of any slackless interval in the online schedule. Establishing that this definition is indeed equivalent to schedulability_transferred is the overall proof objective of this file.

In the remainder of this section, we assume the criterion to be satisfied.

The main proof establishing that transfer_schedulability_criterion is a sufficient condition for schedulability_transferred consists of three steps that lead to contradiction:

• First, assume that some job j finishes later in the online schedule than in the reference schedule, and let t2 denote a time such that j is complete in the reference schedule and incomplete in the online schedule.
• Second, we establish there exists a preceding contiguously slackless interval [t1, t2) and that j is a critical job at time t1 w.r.t. reference time t2.
• Third, we establish that any job that is critical at the start of the contiguously slackless interval is necessarily complete in the online schedule at the end of it, which contradicts the assumption that j is incomplete at time t2.

Of the three steps, the second step is by far the most challenging one. We consider it next.

Existence of a Contiguously Slackless Interval

In the second step of the overall proof strategy, the goal is to establish the existence of a contiguously slackless interval under two major assumptions: (1) the transfer_schedulability_criterion holds and (2) there exists a job that completes later in the online schedule than in the reference schedule. While this existence claim may not be so difficult for a human to "see," it is not so easy to formally establish this existence proof such that Rocq verifies it. We therefore first establish a number of supporting auxiliary lemmas.

Supporting Lemmas

If a job is complete in the reference schedule and not complete in the online schedule, it is by definition a critical job at the time.

No job is late at the start of the schedule, which rules out some corner cases.

Intervals of Non-Positive Slack

As a stepping stone towards finding slackless intervals, we introduce the related notion of an interval with non-positive slack. This notion relaxes the slackless interval's strict equality to an inequality. It thus over-approximates slackless intervals (i.e., every slackless interval has non-positive slack, but an interval with non-positive slack may not satisfy the slackless definition if there is in fact negative "slack").

Mirroring the step from slackless intervals to contiguously slackless intervals, we establish the notion of contiguously non-positive slack intervals, with the obvious interpretation: every suffix-interval must also have non-positive slack.

Facts about Intervals with Non-Positive Slack

Before moving on, we establish some further auxiliary lemmas covering various cases coming up in the main proofs below. First, before the start of a maximally contiguously non-positive slack interval, there is an interval with positive slack.

If a job is finished at a given time t2 in the reference schedule, but not in the online schedule, then there exists a non-empty contiguously non-positive slack interval [t1, t2) that either starts at time zero or is preceded by an interval with positive slack. NB: Note the comments in the proof --- this is a key step.

As a starting point, we establish that [t2 -1, t2) has non-positive slack.

We "upgrade" NPS2 to a contiguously non-positive slack interval. Since the interval contains only one point, this is conceptually trivial, but we need it as a witness for the below search via MathComp's ex_minn facility.

The following is a key step of the overall proof strategy: We search "backwards" in time from t2.-1 until we find the starting point of the maximally, contiguously non-positive slack interval ending at t2.

Finally, we do a case analysis on t1 =?= 0 to figure out the last disjunction of the existence claim: either t1 = 0, in which case the first case holds trivially, or t1 = t0.+1 > 0, in which case we show that [t0, t2) has positive slack.

Slackless Interval Existence Induction Step

In the following, we establish a key technical lemma, slackless_interval_step, which will later serve as the induction step in the main argument below. The lemma establishes that, if we have a slackless interval [t1, t2) and [t1 + 1, t2) has non-positive slack, then [t1 + 1, t2) is also a slackless interval. Intuitively, this will allow us to "grow" the contiguously slackless interval (the existence of which we seek to establish) via induction on the length of the interval. Since establishing slackless_interval_step is itself somewhat laborious, we reason by case analysis and break it up into smaller steps.

Case 1: The Critical Job Completes

The first case is characterized by the following added assumptions:

• there is a critical job j scheduled at time t1 and
• and j is complete at time t1 + 1.

To help establish slackless_interval_step in this case, we first observe that such a job's remaining cost bound is necessarily zero.

With the above helper lemma in place, we can establish slackless_interval_step's claim under the assumptions of the first case.

Case 2: The Critical Job Remains Incomplete

The second case covers the complementary situation:

• there is a critical job j scheduled at time t1 but
• j remains incomplete at time t1 + 1.

Induction Step by Case Analysis

From the transfer schedulability criterion H_ts_criterion, we have that there is indeed a critical job j scheduled at the beginning t1 of any given slackless interval. We proceed by case analysis on whether or not j completes at the next step t1 + 1, which results in exactly the two cases analyzed above.

Main Argument: Slackless Interval Existence

With all required helper lemmas in place, we can proceed to the main argument, which establishes that a late completion is necessarily preceded by a contiguously slackless interval. We first establish the main "upgrade lemma": if we have a slackless interval [t1, t2), and know that [t1, t2) is also a contiguously non-positive slack interval, then we can conclude that [t1, t2) is in fact also contiguously slackless.

With the "upgrade lemma" slackless_interval_continuation in place, we are finally ready to derive the existence of contiguously slackless intervals from a late completion. Note: This proof is commented more than usual to highlight the key reasoning steps.

Setup: job j is incomplete at time t2 in the online schedule, but complete in the reference schedule.

A: Recall that a contiguously non-positive slack interval exists before t2.

B: We will show that [t1, t2) is a contiguously slackless interval.

Showing that j is in critical_jobs t1 t2 is trivial and done here.

C: We recall that [t1, t2) has non-positive slack.

D: From the observation that [t1, t2) has non-positive slack, we infer that [t1, t2) is in fact slackless. This step needs to deal with a bunch of corner cases (e.g., at time zero).

E: Finally, the above "upgrade" lemma allows us to go from [t1, t2) being slackless to [t1, t2) being contiguously slackless.

All Critical Jobs Complete in a Contiguously Slackless Interval

The third step of the overall proof strategy is to show that all critical jobs are complete at the end of a contiguously slackless interval. We establish this key "stepping stone" in the following lemma. From the length of the proof and the absence of many additional supporting lemmas, it should be obvious that this step is much easier than the preceding one. Which makes intuitive sense since the "contiguously slackless" property is a very strong property, which is hard to establish but easy to exploit.

We are going to argue that the total remaining job-cost bound for the critical jobs across [t1, t2) is zero, and they all must have completed. What remains to be shown afterwards is that the remaining job-cost bound is indeed zero.

The main setup step: convert the fact that [t1, t2) is contiguously slackless into the property that at each point in the interval there is a critical job scheduled.

From the property that there is always a critical job scheduled, we can apply a helper lemma that lets us relate the interval length to the accumulated service.

The rest is simple arithmetic.

This marks the end of the generic argument for an abstract job_cost_bound. We will now close this section and establish the concrete results.

Main Results

Naturally, to derive any guarantees, the reference schedule needs to over-approximate the job costs encountered in the online schedule. We add this assumption now.

Sufficiency Theorem w.r.t. Online Job Costs

Using the generic argument for job_cost_bound := online_job_cost, we establish that transfer_schedulability_criterion is a sufficient condition for schedulability_transferred to hold.

By contradiction: suppose j is not complete in the online schedule at time t, but it is complete in the reference schedule.

Observe that online_job_cost trivially "bounds" online_job_cost.

There is necessarily a contiguously slackless interval [t1, t2).

That means that j is complete at time t2, which contradicts the initial assumption that j is incomplete at time t2.

As a straightforward corollary, and for the sake of completeness, we lift online_transfer_schedulability_criterion_sufficiency to the level of job deadlines.

Necessity Theorem w.r.t. Online Job Costs

For job_cost_bound := online_job_cost, we can also establish the reverse direction: transfer_schedulability_criterion online_job_cost is a necessary condition for schedulability_transferred, which establishes the equivalency of the two definitions for online job costs. As a stepping stone, we first establish a lemma that shows that, if there ever is a slackless interval in which none of the critical jobs is scheduled at the start of the interval, then some job must finish later in the online schedule than in the reference schedule.

Let's restate the claim in terms of has, which we can contradict more easily.

By contradiction: suppose that all critical jobs are complete at time t2.

As a stepping stone, we observe that an incomplete critical job necessarily exists if the total remaining cost bound is non-zero.

Hence we proceed to show that the total remaining job cost is non-zero at time t2.

In the following, we exploit the assumption that no critical job is scheduled at time t1 implies that the critical jobs collectively receive no service at that time. Before we can use that fact, though, we must first reshape the sum of remaining cost bounds to expose the collective service received at time t1 in the formula.

First, split the sum of remaining cost bounds into a sum of job costs and a sum of service received.

Next, split the service received into the service received up to (but not including) time t1 and the service received during [t1 + 1,t2). Note this leaves out the service received at time t1, which we know to be zero due to the assumption that no critical job is scheduled at time t1.

Observe that the sum of service_during in the goal matches the definition of service_of_jobs, for which there are useful lemmas in Prosa.

Rewrite the goal to expose that we need to show that the service received by the critical jobs during [t1 + 1, t2) is strictly less than t2 - t1.

Recall a basic fact about service_of_jobs on unit-speed uniprocessors: the total amount of service received in an interval is trivially upper-bounded by the interval length.

The goal then follows immediately from simple arithmetic.

From the preceding stepping stone, we can easily prove that schedulability_transferred implies transfer_schedulability_criterion online_job_cost.

Consider a slackless interval [t1, t2).

To prove the claim, it suffices to show that one of the critical jobs is scheduled at t1.

By contradiction: suppose there is no such job scheduled at t1.

From the stepping stone lemma, we have that some job finishes late as a result.

But this contradicts the precondition that no job finishes later than in the reference schedule.

Sufficiency Theorem w.r.t. Reference Job Costs

Using the generic argument for job_cost_bound := ref_job_cost, we establish that transfer_schedulability_criterion is a sufficient condition for schedulability_transferred to hold even if job costs are over-approximated.

By contradiction: suppose j is not complete in the online schedule at time t, but it is complete in the reference schedule.

Observe that ref_job_cost trivially "bounds" ref_job_cost.

There is necessarily a contiguously slackless interval [t1, t2).

That means that j is complete at time t2, which contradicts the initial assumption that j is incomplete at time t2.

For completeness' sake, we once more lift the sufficient condition to the level of job deadlines.

Without further restrictions, it is not possible to establish necessity for job_cost_bound := ref_job_cost.