WIP: add general notion of "job readiness"

This adds a new generic parameter job_ready that determines whether a given job is ready at a given time in a given schedule. For different workload models (e.g., release jitter, self-suspensions, shared resources, etc.), appropriate definitions of job_ready can be provided. This allows us to define work-conservation and priority-compliance in a general way, which is needed to fully address #12 (closed).

As an example, I've defined job_ready for the workload model with release jitter (and without self-suspensions).

This is just a sketch; what do you think?

CC: @sbozhko @sophie @mlesourd @proux

added 1 commit

• 6f596446 - add basic readiness definition

Compare with previous version

Looks good to me! One small thing: I feel like a valid schedule should mention that only ready jobs execute, so maybe the notion of backlogged could remain where it was (with the consequence that schedule would then depend on ready).

One more thing: I feel the readiness folder would fit better in model but I guess at this point I need to come up with a rational explanation as to why I want some things in behavior and others in model ;-) So far, my motivation is to keep behavior as small as possible.

I'll be away for the week, as far as I am concerned you can merge this.

Thanks for your comments. I fully agree that valid schedules should really impose a constraint on ready jobs. Making that change, however, breaks a bunch of things in existing proofs, which is why I skipped it in the initial draft. :-)

I also see your point that the specific instantiations of job_ready are a better fit for the model folder.

Would it be possible to merge this without relying on the idle-cores branch?

It does not depend on the idle-cores branch. It does, however, require substantial proof fixes in the EDF optimality argument since it changes the notion of "valid schedule" in rather substantial ways. I'm working on that, but it's not yet complete.

This, by the way, highlights that we really need to get the basic definitions "right" before porting the bulk of the proofs, because it's quite painful to have to go back and redo these proofs.

OK noted.

And I agree that we should make sure we got the behavior and model right before we start porting analyses.

I'll close this merge request and share my current — still incomplete — second version of this pull request, so you can take a look at the core definitions and changes. Except for the broken (admitted) EDF argument, everything works.

closed

resolved all threads

mentioned in merge request !39 (merged)