Ideal Uniprocessor Scheduler Implementation
This MR introduces the first part of refactored Prosa's implementation folder, namely a generic function for computing valid work-conserving uniprocessor schedules for given priority policies, readiness models, and preemption policies.
This will be useful for future assumption-free instantiations of analyses in Prosa.
@mmaida @sbozhko: please review. In particular, please check out the two new readiness model classes nonclairvoyant_readiness and valid_nonpreemptive_readiness.
Merge request reports
Activity
added 16 commits
-
89e03467...7d507ed0 - 7 commits from branch
master - 967c6d07 - make --only-classic skip prosa.implementation module
- 953b38b7 - update ack config
- 6739de4f - add function to generate uniprocessor schedules
- 87f6ec3c - generalize notion of jobs_backlogged_at
- 93b40629 - add trivial replace_at definition rewriting lemma
- a77c7c71 - additional minor lemmas on job arrivals
- e236efb1 - add notion of a shared identical schedule prefix
- e1426920 - add readiness properties and facts on backlogged
- ab281cb8 - add implementation of ideal uniprocessor scheduler
Toggle commit list-
89e03467...7d507ed0 - 7 commits from branch
I broke up the implementation into three layers: a fully generic scheduler, a preemption-aware scheduler for ideal uniprocessors, and finally a priority-aware scheduler on top. The lemmas are now structured accordingly, which makes it more clear what the actual assumptions / dependencies are.