Equivalence of EDF Predicates

This MR connects the two ways with which one can specify that a schedule is an EDF schedule in PROSA: the EDF_schedule predicate and the respects_policy_at_preemption_point - given the EDF priority policy - predicate. We connect these two predicates by showing that they're equivalent. We then restate the optimality proof of EDF schedules using the proven equivalence.

Hi Laila, this branch is currently not merge-able. Please rebase this branch on top of the latest master branch. In particular, please drop the commits that were already merged as part of !109 (merged).

assigned to @bbb

CC: @sophie — FYI, we discussed this about a year ago; this is finally connecting the two definitions.

added 9 commits

• 8a2a67d1...c95b4984 - 7 commits from branch RT-PROOFS:master
• 1c0a8d7e - Add proof of equivalence of EDF definitions
• d5c56d27 - Add optimality of work-conserving policy compliant schedules

Compare with previous version

Thank you, Sophie. I think Laila has sort of disappeared due to class-work obligations, so someone else will have to wrap this up at some point. Right now, I don't have any time; maybe I can squeeze this in some time later in the month.

resolved all threads

resolved all threads

added 20 commits

• d5c56d27...39bd1a26 - 15 commits from branch RT-PROOFS:master
• 327967da - add proof of equivalence of EDF definitions
• 28cc501c - cleanup EDF equiv. proof
• 0efa008f - add a couple of small but useful behavior lemmas
• ab31d426 - revise EDF definition equiv. proof
• f4d24732 - remove superfluous lemmas and file

Compare with previous version

Laila is MIA. I'd like to get this MR out of the queue.

I've cleaned up, revised, and rebased this MR. @mmaida, @sbozhko please take a quick look and let me know if spot anything else that needs to be cleaned up before this goes it. Thanks.

added 1 commit

• 33081d4a - Improved proof

Compare with previous version

added 1 commit

• d4dd08a6 - Minor fix to avoid spelling errors

Compare with previous version

@sbozhko waiting for your ok

Thanks for the feedback. I'll take a look when I get a chance; if you have cycles; feel free to just push the patches yourself.

resolved all threads

resolved all threads

added 11 commits

• d4dd08a6...483d4633 - 3 commits from branch RT-PROOFS:master
• 0be2a8bf - add proof of equivalence of EDF definitions
• 3c9acf7d - cleanup EDF equiv. proof
• 53beb3d6 - add a couple of small but useful behavior lemmas
• 98ab9366 - revise EDF definition equiv. proof
• bd0ccc3f - remove superfluous lemmas and file
• a50c3636 - Improved proof
• ae832c2c - Minor fix to avoid spelling errors
• ed3445d3 - coding style and comment fixes

Compare with previous version

merged