Preemption model compliance

We show that the preemption-aware scheduler respects the preemption model semantics.

@bbb

unmarked as a Work In Progress

changed the description

added 1 commit

• 4826ce0d - Proved that np_uni_schedule respects the preemption model

Compare with previous version

added 1 commit

• 41112454 - Proved that np_uni_schedule respects the preemption model

Compare with previous version

Very nice, I see this was way too easy. :-)

If you're up for another project (time permitting, etc.), I'll pick something more juicy.

added 1 commit

• 9d537763 - proved priority compliance of uni_schedule

Compare with previous version

added 1 commit

• bfd52c7e - fix spelling

Compare with previous version

resolved all threads

@bbb I think this MR is also ready, no? Minus the rebasing of course.

added 13 commits

• bfd52c7e...c95b4984 - 7 commits from branch master
• 4bb21a62 - Add proof of equivalence of EDF definitions
• 91c75d04 - Add optimality of work-conserving policy compliant schedules
• 2377aa44 - added the np_respect_preemption_model lemma
• d4df78cb - Proved that np_uni_schedule respects the preemption model
• c669e93d - proved priority compliance of uni_schedule
• b55116a9 - fix spelling

Compare with previous version

resolved all threads

added 5 commits

• fd1d0c4e - proof state recorder: check expected interaction number
• 8e8aecc4 - proof state recorder: add --pause option
• f9260e7b - proof state recorder: fix double prompt detection
• 3c9b7fb8 - proof state recorder: handle multiple closing '}'
• 28778be4 - proof state recorder: don't trip over vernacular commands

Compare with previous version

added 3 commits

• 795b4d6f - proof state recorder: handle multiple closing '}'
• 02f34370 - proof state recorder: don't trip over vernacular commands
• dae7b9fe - proof state recorder: add more out-of-sync checks

Compare with previous version

resolved all threads

resolved all threads

closed