Project Milestone: Preemption Model Compliance
As discussed, here's the next milestone / mini-project.
Context
In Prosa, we usually assume whatever context necessary for a proof in an axiomatic style (i.e., with variables and hypotheses). This is a good idea in many ways (stays close to how papers are written, keeps arguments independent of "implementation details"), but comes with one big risk: we could accidentally be making inconsistent, contradicting assumptions.
To avoid this in a provable way (and also for some future projects), we need concrete implementations of everything assumed that show the assumptions of the main theorems to be fulfillable in a (largely) assumption-free context (which implies that they are contradiction-free, i.e., we show the type of the proof term to be inhabited by giving a concrete specimen that shows all premises to be inhabited). These concrete implementations are to be found in prosa.implementation
. (Currently, there's not much there yet, since we lost most implementations in the "great refactoring"; there are more implementations in prosa.classic
, but those are not so relevant for us right now.)
The main implementation right now is a generic routine for generating ideal uniprocessor schedules for a given arrival sequence.
For this to be useful, we need to show that it satisfies all common assumptions (e.g., the produced schedules are valid, comply with the priority policy, etc.). A bunch of relevant lemmas and theorems are already there:
- prosa.implementation.facts.generic_schedule
- prosa.implementation.facts.ideal_uni.preemption_aware
- prosa.implementation.facts.ideal_uni.prio_aware
However, there is one major omission: there's currently no proof that the generated uniprocessor schedules are preemption-model compliant.
Goal
The goal of this project milestone is to add a theorem in prosa.implementation.facts.ideal_uni.preemption_aware
that establishes that np_uni_schedule
(➔ definition) to produce schedules that satisfy the preemption model semantics (➔ definition).
This result should then also be re-stated as a corollary for the priority-aware uni_schedule
(➔ definition) in prosa.implementation.facts.ideal_uni.prio_aware
.
Again, once you understand the context, this should be a self-contained mini-project with a well-contained scope.
Please ack that you've seen this and post any questions.