Have compound hypotheses for "reasonable schedule" and "reasonable workload"
In just about any theory, a couple of standard "sanity" assumptions show up:
- jobs don't execute before they are released
- jobs don't executer after they are finished
- jobs arrive only once
- job arrival times are consistent
Additionally, in the context of a task model, we also usually assume:
- there is a finite set of tasks
- all jobs in the arrival sequence stem from some task
- jobs don't execute for longer than their task's WCET
- jobs from the same task execute in FIFO order
Let's define some standard definitions to group these hypotheses into more succinct compound assumptions (i.e., definitions that are big conjunctions). This should help to substantially reduce the amount of boilerplate assumptions in the beginning of many files.
We could then also have a second level of even higher-level compound assumptions such as "preemptive sporadic tasks". For example, the "sporadic task model" encompasses the following assumptions:
- reasonable schedule
- reasonable workload
- sporadic arrivals
For example, I'd like to reduce the assumptions for RTA of fixed-priority preemptive scheduling of sporadic tasks to something like this:
- preemptive sporadic task model
- jobs are always preemptive
- schedule is work-conserving
- schedule follows FP policy [at preemption points]
Basically, let's aim to reduce the list of explicitly stated hypotheses to high-level concepts that one would also state in a paper (e.g., "fixed-priority", "preemptive", "sporadic tasks") and avoid explicitly listing too many low-level, detailed assumptions. Proofs can just split & extract whatever hypotheses they need from the compound assumptions.
By making these compound assumptions, we don't restrict generality --- individual analyses are still free to pick and choose whatever assumptions they need, but the vast majority of analyses making "standard assumptions" become a lot simpler.
Comments or thoughts?