WIP: expose number of idle cores

What do you think of this way of defining work-conservation in a way that transparently works for both uni- and multiprocessor platforms?

To me, this looks appealing. The only downside that I see is that in proofs one doesn't get to destruct the exists j_other right away (i.e., we'd need a few helper lemmas to establish that idle_in s == 0 implies exists j_other.

We could also keep both notions and establish equivalency of the two definitions (once for each processor model).

CC: @sbozhko @mlesourd @sophie

added 1 commit

• 42bbce7f - fix comment

Compare with previous version

resolved all threads

After discussing this a bit with Sergey today, we've come to realize that one major limitation of this approach is that it is insufficiently general to capture issues such as partitioned scheduling, APA scheduling, or heterogenous platforms, where only certain cores are relevant for a particular job/task. To avoid having to revisit this issue when we get to porting the existing APA results (at which point we'd have to change potentially quite a few proofs), it would be preferable to find a more general solution right away.

So what can we do? One option that I see is to instead augment the interface with a predicate, say, idle_core_available: PState -> Job -> bool that checks whether a core is available for a specific job.

For the uniprocessor models, this has obvious implementations. For the multiprocessor case, it would need to be made a generic parameter that can then represent either global scheduling, partitioned scheduling, or APA scheduling (or any other function that maps jobs to sets of acceptable cores).

What do you think? Any better ideas?

Thanks for the interesting discussion. I am not sure it is such a good idea to have a generic definition of work-conservation if this implies changing the definition of schedule. I would rather go for two definitions and an equivalence relation.

I'm not clear on what you specifically propose. Can you share an example?

If we don't have a common definition of "work conservation", I'm afraid that we'll end up again with a lot of copy&pasted definitions because "is there a core available this job can run on" plays into the central notion of "when does a job make progress in the worst case" and thus affects pretty much all analyses. I mean, this is exactly why we have a separate APA folder in the current version... otherwise, there are no differences to the global analysis.

So concretely, how should we express a notion of "work conservation" that works for both global scheduling and APA if we don't have a generic notion of "could this job run on this core"?

Thinking about this some more, the same issue is going to come up with priority-compliance... Somehow avoiding duplication without over-engineering is a tricky issue. Unfortunately, we really should resolve this sooner rather than later to avoid more pain down the road.

Alternative ideas very welcome...

My main concern is to not modify schedule unless we have a really good reason.

I'll see if I can come up with an alternative proposal.

I thought a bit about this problem and here is a proposal (just words, no Coq so far, sorry):

• We make resources explicit in the ProcessorState (which BTW should be called PlatformState); for the moment we can stick to uniform platforms and take a definition similar to that of processor in multiprocessor.v.
• In ProcessorState, we add one parameter to scheduled_in and service_in such that they reflect whether a job is scheduled on / receives service from a given resource.
• In the model part, we add a platform folder and several files that allow us to constrain how jobs can be scheduled on resources (APA, partitioned, uniprocessor) using the notion of task.
• From there we should be able to provide a generic notion of work-conservation.

Basically, this is a generalization of your proposal. Does that make sense?

In ProcessorState, we add one parameter to scheduled_in and service_in such that they reflect whether a job is scheduled on / receives service from a given resource.

Doesn't that make all uniprocessor code needlessly verbose? Basically, that means that we treat uniprocessors as a funny kind of multiprocessor. That's obviously not wrong, but it seems somewhat inelegant and undesirable.

I am not sure how much that would impact definitions and proofs for uniprocessor systems, basically it would add one useless parameter. I like this definition better than having in ProcessorState a function defining whether "a core is available for a specific job". This to me does not really fit in the behavior, and it is also a bit awkward for uniprocessor systems, isn't it?

To be maybe more precise, my "proposal" would identify which resource is providing service for a specific job, which I guess is needed for APA.

For uniprocessors, there's a trivial canonical implementation, so this never shows up in any significant way. It's a no-op, and importantly, it's syntactically invisible in any uniprocessor code. No useless parameters.

To me, it does not sound so unreasonable to have a function that reflects the presence of idleness in a processor state. We have a generic function parameter that indicates "whether a job is scheduled", a generic function parameter that indicates "how much service a job receives". Further, the type class even carries a proof term to document that only scheduled jobs receive service. What's so bad about having another generic function that indicates "whether there is an idle core relevant to a job"?

By the way, I don't think this should be "platform state" — we don't want to start shoving memory modules, network adapters, etc. in there as well, but arguably all that constitutes "a platform".

I feel uncomfortable having in ProcessorState information about what could have happened (as in "that job could have executed on that processor") rather that what actually happened ("that job did execute on that processor").

I guess one option would be to hide the added parameter in uniprocessor code by having simpler scheduled_in s j and service_in s j wrappers that reduce to exists resource, scheduled_in_new s j resource and sum_(...resource \in resources...) service_in_new s j resource.

Still, that's an extra layer that I really would like to avoid if possible.

I feel uncomfortable having in ProcessorState information about what could have happened (as in "that job could have executed on that processor") rather that what actually happened ("that job did execute on that processor").

Ok, fair point.

There's a simple solution, though: add a generic function that returns a set of resource => job mappings. Uniprocessor code can safely ignore this function, there exist trivial, canonical implementations for the uniprocessor world, and sophisticated scheduling models can make use of this added interface when required. In particular, we can implement a "is there an idle core that this job could have implemented on" policy on top of this interface.

In fact, we can implement scheduled_in also on top of this interface.

Question: what do you return for a processor in an overhead-aware model that's currently experiencing context-switch overhead? There's no obviously scheduled job, but the core is also not idle and available to others.

Sorry, I lost track of the discussion a bit.

Would the generic function you suggest be independent of time and schedule?

Again, from my perspective mappings are part of the model and not of the behavior. This is why I had proposed to make explicit in the behavior the actual resource on which a job is scheduled, which must respect its mapping.

I find the question about context switching interesting. I had implicitly assumed that overhead costs would be hidden inside the scheduling intervals: a job would be scheduled but receive no service. Is there a reason not to do this? In which case we would need an explicit notion of idle core.

Sorry, I lost track of the discussion a bit.

Yeah, I think this is several confusing issues rolled into one. I don't claim to have a perfect solution.

Would the generic function you suggest be independent of time and schedule?

Yes. It maps a processor state to something (either a boolean or a set/list of something TBD). Just like scheduled_in and service_in, neither of which depends on time or a specific schedule.

Again, from my perspective mappings are part of the model and not of the behavior. This is why I had proposed to make explicit in the behavior the actual resource on which a job is scheduled, which must respect its mapping.

Sorry for the confusion, that's not what I meant by "mapping". I don't mean the set of cores on which a task may execute. I mean the relation job-executes-on-core (= resource) in a particular processor state. Currently, scheduled_in can be thought of testing whether a given job is an element of this relation. Instead, we could just expose this relation directly and implement scheduled_in on top of it.

I had implicitly assumed that overhead costs would be hidden inside the scheduling intervals: a job would be scheduled but receive no service. Is there a reason not to do this?

Consider the context switch after a job j has completed (service sched j t = job_cost j). If completed jobs don't execute, then this job cannot remain scheduled.

In which case we would need an explicit notion of idle core.

In my understanding, the whole point of having an abstract interface for processor state, realized by a type class, is to hide such model-specific semantics. But yes, "idleness" / "core availability" is something that needs to be communicated to the higher levels to express work conservation.

OK, I understand better now what you meant.

So if I got this right, the conclusion would be:

• We make resources explicit;
• We add a third function in ProcessorState that expresses whether a job executes on a given resource;
• We add a fourth function in ProcessorState that expresses the number of idle resources --- wouldn't it make sense to express instead for each resource whether it is idle?

• We make resources explicit;

Yes, but I don't have a clear idea of what that should look like. The most simple solution I can think of is to say a "resource" (core?) is simply a (type alias of) nat: the core ID.

• We add a third function in ProcessorState that expresses whether a job executes on a given resource;

Mhh... maybe?

I don't want to add something like scheduled_in pstate job core_id.

• We add a fourth function in ProcessorState that expresses the number of idle resources

No, that was the starting point of the discussion, but that interface was deemed not general enough.

--- wouldn't it make sense to express instead for each resource whether it is idle?

The last discussion point was the following: add a single function in processor state that maps each processor state to a sequence of ("core id", "scheduled job (if any)", "amount of service received") tuples (one for each core, a uniprocessor generates a singleton list). On top of this, we can implement the necessary idle semantics, we can later implement APA semantics, and even scheduled_in and service_in.

But that comes with new challenges (some outlined above), it's not clear if this is sufficiently general in the long run, and it adds some complexity and indirection where none is needed (uniprocessor case).

I don't think we have a good solution yet. Fundamentally, none of this is relevant for the uniprocessor case, which we don't want to complicate, but the multiprocessor case fundamentally needs to reason about core identities in all variants but global scheduling.

So we have conflicting design goals, and no decent compromise yet.

It would help to see what the various options look like in Coq. Maxime and I will discuss this later today.

Ok, looking forward to see what you come up with.

Fundamentally, we need to express two things:

1. for work conservation: given a ready job j and a state s, does there exists a core in s on which j is eligible to execute but that is idle?

2. for priority compliance: given a ready job j and a state s, is there a job scheduled with lower priority on any of the cores on which j is eligible to execute?

If we can answer both questions, we're all set — we don't need to know more than that to express everything up to and including APA.

I have quickly prototyped what I understand in terms of changes to the definition of processor state from the current state of the discussion here.

Hi Maxime, thanks for the quick sketch! I think it captures the discussion well.

Sergey and I briefly discussed this — one possible concern is that service_at and scheduled_at get used in quite a few places (just grep for /service_at and /scheduled_at). Changing these is going to cause some amount of friction.

Also, we don't actually need service_in: Job -> Resource -> State -> nat for anything that I can tell.

So one alternative would be to keep service_in and scheduled_in as they are right now, and just add the following:

 Resource : finType;

 scheduled_on: Job -> Resource -> State -> bool;

 scheheduled_on_consistent :
   forall j r s, scheduled_in j s = [exists r, scheduled_on j r s];

This would allow the existing code to remain unchanged and simple, and we could rely on the more sophisticated, fine-grained interface where needed (and translate between the two).

If we do end up needing a more fine-grained, resource-aware service_in variant at some point, we could add it similarly without disturbing existing code.

Hi Maxime,

Since the whole discussion began only because we want to get a general notion of work conservation, I'd like to see how this works in your case.
Could you please add the notion of "work conserving schedule" to your prototype?

(meanwhile, I am also working on a prototype)

I have updated the resources branch with the definition of work conserving, it still lacks some comments but it looks quite natural.

Some proofs are broken by the changes but it doesn't look too hard to fix.

Thanks for the worked example!

I’d like to reiterate that I think an additive approach that doesn’t break existing proofs — where the simple scheduled_in and scheduled_at remain unchanged (and primitive, i.e., part of the type class) — is preferable. What we have now is, in my opinion, really quite good and attractively simple. It’s the result of long, fruitful discussions and I really, really like it. :-) Can we just keep it?

I also quite liked in your original proposal how the resource type is part of the type class, rather than a parameter of the type class. Making it a parameter forces every use of the type class to declare a resource type in context, no? By making the type it a member, it doesn’t even show up in uniprocessor-only files. I find that very attractive — one can stay blissfully unaware of the MP support if one doesn’t need it. Is there a specific reason why you changed this?

I will open a merge request to explain some of the choices made

I really, really like it. :-) Can we just keep it?

Lian, give the keyboard back to Björn!

Joke aside, Maxime and I tried out a new proposal (in the resources branch) that is still not perfect but probably closer to what you want. I like it in the sense that it makes resources explicit and it should not mess up existing proofs too much (to be discussed).

Closing this merge request as it has been superseded by !54 (merged). Thank you, Maxime!

closed