EDF optimality proof should derive from its weaker version

In file analysis/edf/optimality.v

assigned to @bbb

And while we're at it, the top-level file should make it clear that the result is specific to the ideal uniprocessor and basic readiness models.

Actually, after looking at this, this is not so easy and not worth the hassle.

It's not straightforward to derive the high-level strong optimality result (EDF_optimality) from the high-level weak EDF optimality result (weak_EDF_optimality) because the conclusion of the weak theorem does not expose that edf_sched was obtained with edf_transform (i.e., it just states that there exists some EDF schedule without divulging how it was obtained).

Without the knowledge that edf_sched = edf_transform any_sched it is not possible to use edf_schedule_is_valid or edf_schedule_meets_all_deadlines_wrt_arrivals, as these are claims about edf_transform specifically and not just any EDF schedule.

The point of the high-level claim is to be a "pretty" summary that matches what's in the literature, so exposing this "implementation detail" would be quite inelegant. As both theorems have very short proofs relying exclusively on shared, also-rather-high-level lemmas in edf_opt, I don't see much value in forcing the suggested dependency.

So instead of understanding the strong result as a strengthening of the weak result, both can be seen as consequences of the lemmas established in edf_opt.

(I'll still make the schedule and readiness model explicit, though.)

closed

mentioned in commit bbefcd16

mentioned in merge request !56 (merged)

Clear!