Project milestone: show existence of "early" deadline violations
This project is more open-ended and less clearly defined than the "warm-up" projects so far. I expect that you'll have clarification questions, so don't hesitate to ask.
Context: In the classic periodic task model, tasks release a potentially infinite sequence of jobs, where the arrival times of consecutive jobs are separated by a fixed interval called the period of the task.
A fundamental property of periodic workloads is that, while the set of jobs can be infinite, schedulability can be determined by analyzing only a finite set of jobs at the beginning of the timeline, because afterwards the arrival sequence repeats cyclicly due to the fixed rhythm of job releases (the repeating cycle is called the hyperperiod and is the least-common multiple of all task periods). The existence of such a finite observation interval (OI) is exploited in many papers, but we currently don't have support for this reasoning technique in Prosa yet. This project is a stepping stone towards supporting OI-based proof strategies.
More specifically, suppose one has a proof P that all jobs that arrive in a finite OI at the beginning of the timeline cannot miss their deadlines. How can one conclude from this that no job anywhere can miss a deadline? In particular if there is an infinite number of jobs? The idea is the following:
- By contradiction: suppose P holds but some job j misses its deadline.
- If that job arrives in the OI, it contradicts premise P and we're done.
- Otherwise, if that job arrives after the OI, consider the execution costs of the jobs in the hyperperiod H in which j arrives.
- Because of the periodic release patterns, there exists a corresponding job in the OI to each job in H.
- "Transplant" the execution costs of the jobs in H to the corresponding jobs in the OI.
- Observe that as a result the corresponding job of j in the OI also misses its deadline.
- The existence of this schedule contradicts premise P, so we're done.
Steps 4 and 5 have recently been added to Prosa (by Vedant, another remote intern working with us this summer). The next milestone is to establish Step 6. For generality, we don't want to argue just about deadline misses, but about exceeding any given response-time threshold.
Goal: Show that, if there exists a schedule S in which some job j (arriving anywhere) exceeds a given response-time threshold R, then there also exists a schedule S' in which a job j' that arrives in the OI exhibits a response time exceeding R. The OI is given by the maximum offset among all tasks plus one hyperperiod.
For simplicity, assume fixed-priority scheduling.
Bonus: If you come across proofs related to Steps 4 and 5 that can be simplified, please do so.
To kick things off, please try to state the claim formally, within a suitable context.