preemption model cleanup
The preemption model is a rather large and complicated piece of the spec, and it seems to be in need of some cleanup.
-
There seem to be duplicated definitions that (at least superficially) seem to express the same idea:
schedule_respects_preemption_model
vs. not_preemptive_implies_scheduled -
The current definitions and layout of the spec mix two different aspects:
- (a) job behavior -- whether or not a given job is preemptable at a given point in its execution, plus the corresponding task-level parameters and specs
- (b) scheduler behavior -- properties of the schedule and its structure
Of course (a) and (b) need to agree, but I they are not the same thing and I think they should be kept more clearly apart. Maybe this is mostly a matter of better documentation, but for now it seems rather confusing and I don't yet have a good idea of what how this can and should be clarified.