Project Milestone: EDF Equivalency
As we're wrapping up the initial patch on EDF work-conservation, I wanted to quickly state the goal for the next milestone.
Context: As you've probably noticed, all the EDF results are stated in terms of a schedule predicate called EDF_schedule
. There is however a more general notion of "policy-compliant schedule" in Prosa expressed by the predicate respects_policy_at_preemption_point
in prosa.model.schedule.priority_driven
. Conceptually, the latter also specifies what an EDF schedule looks like when used in conjunction with the EDF
JLFP instance (i.e., the definition of the EDF priority function) in prosa.model.priority.edf
.
The reasons that there are two ways to specify "EDF" is partly historic (EDF_schedule
predates respects_policy_at_preemption_point
) and partly for teaching purposes (EDF_schedule
is arguably more intuitive / less abstract).
Goal: It is of course unsatisfactory to have two competing, formally unrelated notions of "EDF" in Prosa. We don't mind alternate definitions of the same concept, but alternative definitions should be connected by appropriate conversions and/or equivalence lemmas. So the goal for your next milestone is to prove that EDF_schedule
and respects_policy_at_preemption_point
are indeed equivalent in the case of
- fully preemptive jobs (this is essential),
- the basic readiness model, and
- ideal uniprocessor schedules.
That is, show forall sched, EDF_schedule sched <-> respects_policy_at_preemption_point sched
in the context of the EDF
JLFP policy and the basic readiness model.
I hope this makes sense. Please reply below if you have any questions or discuss your initial angle of attack. :-)