Simulation Interval for Periodic Schedulers

This module develops the results of Guidolin–Pina et al., “Minimal simulation interval for periodic task schedulers”, Journal of Systems Architecture 179 (2026), 103939.
DOI: 10.1016/j.sysarc.2026.103939 Theorem 1 concerns a bounded first idle point ending a repeating hyperperiod. Corollary 4.1 specializes this bound to constrained offsets. Lemma 4.7 transfers a finite deadline check to the entire schedule. Here we prove discrete-time versions of these statements. As a notable deviation from the paper, whereas Guidolin-Pina et al. reason about a class of "resettable deterministic schedulers" that asserts properties of state-based schedulers, we introduce here a different scheduler contract that better suits Prosa's schedule representation (which does not explicitly model the scheduler itself). A general JLFP result establishes the reset contract from deterministic, antisymmetric priorities preserved across hyperperiods, yielding a finite deadline-check corollary for JLFP schedules. The development concerns fully preemptive ideal uniprocessors. We reuse Prosa's periodic task, service, readiness, and deadline models.

System Model

Tasks have arbitrary offsets and relative deadlines, periodic arrivals, and fixed execution requirements.

Jobs of these tasks have arrival times and execution requirements. Each job's absolute is derived from its task's relative deadline via job_deadline_from_task_deadline.

The considered workload is a finite set of periodic tasks ...

... generating a valid infinite arrival sequence ...

... in which each task's first job arrives at its offset ...

... and consecutive jobs of each task are separated by exactly one period.

Simulation uses the task WCET for every job, ensuring that execution requirements repeat.

We assume that the system is not overloaded: the work arriving per hyperperiod fits in one hyperperiod of service. This is the integer formulation of the paper's utilization bound U ≤ 1, and permits both zero work and full utilization.

We use the basic Liu-and-Layland-style job readiness model, where every pending job is always ready to execute, including jobs whose deadlines have passed.

In the following, we analyze a given well-formed, work-conserving schedule of the workload on an ideal uniprocessor.

Importantly, we make no assumption on which scheduling policy was used to obtain sched and do not assume any particular preemption model.

Simulation Time Boundaries

We now identify the part of the schedule that a finite simulation must cover. The following definitions translate the paper's time conventions to Prosa's discrete time model and specify where to look for a no-carry-in instant that bounds a complete repeating hyperperiod. Following Definition 4.1 in the paper, the "onset of global periodicity" is the maximum of task_offset tsk + 1 - task_period tsk, with saturating subtraction and an empty maximum of zero. This translates the paper's strict inequality t > O - T; in particular, O = T requires t ≥ 1.

When every task's offset is strictly less than its period, i.e., when all tasks have constrained offsets, then this bound reduces to zero, yielding the horizon specialization of Corollary 4.1.

The search for a no-carry-in instant starts one hyperperiod after the arrival boundary. This is the first integer strictly after the paper's t0 + H, interpreting 0^- as the predecessor of zero.

The simulation horizon is the main bound of interest: the main claim established below is that a simulation must cover only the jobs that arrive prior to this horizon to establish schedulability for all jobs (up to infinity). It accounts for the initial transient through the no-carry-in search boundary as well as for the total amount of work carried out by the tasks in one hyperperiod.

The paper's "idle points" are exactly Prosa's no_carry_in times: every job arriving strictly before the instant has completed. This gives the scheduler an empty backlog before processing new arrivals. New jobs may arrive and execute at the idle point itself. The first no-carry-in instant at or after the search start identifies the earliest eligible boundary for the simulation.

Existence of a No-Carry-In Instant

With the system model and key definitions in place, we begin by observing that the first no-carry-in instant always exists before the simulation horizon because the system is (a) not overloaded and (b) work-conserving.

We next establish some auxiliary lemmas that we require for the subsequent proofs.

Matching Jobs Across Hyperperiods

To relate "matching" jobs across hyperperiods, we use Prosa's next_hyperperiod_job and prev_hyperperiod_job definitions. We establish some useful facts about these definitions in our specific context. As a stepping stone, we observe that jobs that arrive after the starting threshold for the no-carry-in instant search have indeed a predecessor that arrives exactly one hyperperiod earlier.

A job's "matching successor" indeed arrives during the next hyperperiod.

From the arrival boundary onward, there is a "matching predecessor" in the preceding hyperperiod for every later release.

For jobs that arrive after the start of periodicity, the "matching successor" and "matching predecessor" relationships cancel out.

Next, we establish two helper lemmas on the workload in intervals exactly one hyperperiod apart.

Relating Workload Across Hyperperiods

The total workload in a given interval is never less than the total workload in an interval of the same length exactly one hyperperiod later. This holds even during the initial transient.

Once arrivals repeat, the workload comparison becomes an equality.

Resettable Deterministic Schedulers

Guidolin–Pina et al. introduce a notion of "resettable deterministic schedulers" (RDS) to state their result in broad terms, independently of a specific scheduling policy such as FP or EDF. The essence of their definition is that such a scheduler must reset to a known internal state whenever it encounters a no-carry-in instant. They then argue that an RDS scheduler must necessarily produce a recurring schedule under the stated system model. In Prosa, we represent schedules directly, typically without reasoning about the scheduler that produces the schedule. Their definition does not translate directly to our setting. Instead, we explicitly require the schedule to exhibit a recurring pattern. First, a hyperperiod-sized interval is self-contained if it has a no-carry-instant on both ends, which implies that no workload "bleeds in or out" of the interval.

We say that execution repeats at time t in schedule sched (w.r.t. the workload's hyperperiod) if the "matching successor" job given by next_hyperperiod_job (if any) is scheduled at time t + hyperperiod ts. Similarly, if no job is scheduled at time t, then t + hyperperiod ts must also be idle.

No-carry-in instants give the scheduler matching reset states. This contract captures the consequence of resettable determinism needed here: corresponding arrivals produce matching execution over the following hyperperiod. This lets us propagate no-carry-in boundaries and establish indefinite repetition by induction over successive hyperperiods. We show further below in lemma jlfp_respects_hyperperiod_reset that JLFP policies satisfy this requirement under mild assumptions (antisymmetric job prioritization that agrees across hyperperiods).

The consequence of the RDS contract is that execution repeats forever after the initial transient, which we define here and establish below.

Self-Contained Hyperperiod Propagation

We next establish that, if the schedule repeats, then a self-contained hyperperiod begets a successive self-contained hyperperiod, thereby propagating the notion to infinity. As the first step, we note that the service received by matching jobs is equal at all points across successive hyperperiods, ...

... which trivially extends to the pending predicate.

We obtain the induction step for repeating self-contained hyperperiods.

Repeating Schedule

We now have the ingredients for a repeating schedule. To bring them together, we first need two no-carry-in instants one hyperperiod apart. Fortunately, finding the later instant also tells us that there are no carry-in jobs at the earlier one, either. The intuition, captured by the workload argument of Lemma 4.5 in the paper, is that any unfinished backlog at the earlier boundary would leave unfinished work one hyperperiod later as well.

With a self-contained hyperperiod in hand, we can now follow the schedule forward. The RDS contract gives us matching execution in the next hyperperiod, and the propagation lemma above tells us that this next hyperperiod is self-contained too. We can therefore apply the same reasoning again, carrying the repeating pattern forward.

Minimal Simulation Interval

We are now ready to put the pieces together and establish our version of Guidolin–Pina et al.'s Theorem 1. The first no-carry-in instant in our search lies within the simulation horizon. Looking back one hyperperiod gives us the other no-carry-in instant, so the interval between them is self-contained. From the start of this interval onward, the schedule follows the same pattern forever. For tasks with constrained offsets, constrained_offsets_periodicity lets us place the arrival boundary at zero. The horizon then simplifies to hyperperiod ts + (hyperperiod_workload ts - 1), giving the specialization in Corollary 4.1. Rocq's subtraction saturates at zero, so this bound also covers the corner case of task sets with zero workload.

Finite Deadline Check

Having found a repeating pattern, we can turn our attention to deadlines. We collect the jobs arriving up to and including a chosen horizon and check that each of them meets its deadline. These jobs will serve as our representatives for the rest of the schedule.

The repeating pattern explains why these representatives suffice. Theorem 1 places a complete repeating hyperperiod within our simulation horizon. Every later job has a matching predecessor one hyperperiod earlier, with the same execution requirement and relative deadline. Since matching jobs receive the same service at corresponding times, they also share the same deadline outcome. Stepping backward through these predecessors eventually brings us to a job covered by the finite check. This gives us the guarantee for the entire schedule, as stated in Lemma 4.7.

We follow the chain of matching predecessors by induction on arrival time, until we reach a job whose deadline has already been checked.

We can now compare the job with its predecessor: the repeating execution pattern gives them matching service through their respective deadlines.

RDS Contract for JLFP Priority Policies

So far, we have used the reset contract as an assumption. We now show how a job-level fixed-priority (JLFP) policy can provide this contract. The intuition is that, when corresponding jobs are pending and their priority order agrees, the scheduler makes corresponding choices. Starting from empty backlogs, we can follow these choices through a whole hyperperiod.

We begin with a JLFP policy, whose priority relation between jobs stays fixed as time passes. We include the scheduler's way of breaking priority ties in this relation too.

We consider fully preemptive jobs, so the scheduler can enforce the priority order at every instant, ...

... and assume that the schedule indeed complies with job priorities at all times.

To make the choice of job deterministic, we also ask that the order resolve priority ties uniquely among arriving jobs. This is the role of antisymmetry: together with policy compliance, it ensures that the same pending jobs force the same choice.

Finally, the priority order must agree across hyperperiods. When we replace jobs by their matching successors, their relative order, including the way ties are broken, stays the same. This lets us carry a scheduling decision from one hyperperiod to the next.

Let us first look at a single scheduling decision. Suppose execution has already matched up to this point in the two hyperperiods. The service and pending-job results above tell us that the chosen job's matching successor is pending too. The preserved priority order then puts this successor ahead of every competing choice. Prosa's jlfp_pending_highest_priority_job_is_scheduled lemma lets us conclude that the successor is indeed the job that runs. This gives us the next matching decision.

We can now build the matching execution of an entire hyperperiod, one decision at a time. Whenever a job runs, the lemma above gives us its matching successor in the next hyperperiod. Idle instants match as well: corresponding jobs have the same pending status, and work conservation makes the processor run whenever work is ready. Induction carries these two observations through the hyperperiod, establishing the reset contract.

With the reset contract established, we can apply the finite deadline check from the preceding section to our JLFP schedule. The jobs arriving up to and including the simulation horizon serve as representatives whose deadline guarantees extend to every later arrival.

Finally, we can express the same guarantee from the tasks' point of view. Since every arriving job meets its deadline, every task's releases meet their deadlines too. This connects our finite check to the usual notion of task-set schedulability.

Applicability to EDF, FP, FIFO, GEL, and ELF

The corollary jlfp_finite_deadline_check applies to fully preemptive EDF, FP, FIFO, GEL, and ELF schedules with consistent tie-breaking. In particular:

• The specialization tiebreaking_edf_finite_deadline_check in prosa.results.periodic.simulation.edf applies directly to EDF with task-ID and job-ID tie-breaking under valid_task_ids and valid_job_ids.
• Similarly, tiebreaking_fp_finite_deadline_check in prosa.results.periodic.simulation.fp applies to any task-level FP policy with task-ID and job-ID tie-breaking under valid_task_ids, valid_job_ids, and monotonic_job_ids. The latter constraint makes ties between jobs of the same task follow arrival order, preserving priorities across hyperperiods.
• The specialization tiebreaking_fifo_finite_deadline_check in prosa.results.periodic.simulation.fifo likewise applies directly to FIFO with task-ID and job-ID tie-breaking under the same ID validity constraints as required by EDF.
• Under the same assumptions, the specialization tiebreaking_gel_finite_deadline_check in prosa.results.periodic.simulation.gel also applies to GEL with task-derived priority points.
• Finally, tiebreaking_elf_finite_deadline_check in prosa.results.periodic.simulation.elf applies to ELF over any task-level FP policy with task-derived priority points, again with tie-breaking based on task and job IDs.