remove ideal uniprocessor assumption from priority-driven schedules

assigned to @mmaida

Ah, it depends on preemption_time, and that in turn destructs the schedule state to get at the scheduled job. We need a generic way to get to this, as I previously mentioned here and here.

Two ideas on how to get rid of the current preemption_time

We introduce a function that maps PState to a list js of scheduled jobs. Then we define preemption_time using the list, e.g. preemption_time := exists a preemptable job in js. For ideal uni, js = [] if the scheduler is Idle and js = [j] if the schedule is Some j
We parametrize preemption_time with a job. In this case the definition could be preemption_time := scheduled_at && job_preemptable

2 looks cleaner to me

We introduce a function that maps PState to a list js of scheduled jobs. Then we define preemption_time using the list, e.g. preemption_time := exists a preemptable job in js. For ideal uni, js = [] if the scheduler is Idle and js = [j] if the schedule is Some j

What about mapping each Core to an option Job as I suggested in my comment? Wouldn't that be cleaner? It seems like this could simplify the whole processor interface quite a bit.

Well, since we have Core then I agree. Never noticed this class

What if we have a multiprocessor (let's say with two cores C1 and C2).

j1 is scheduled at C1 and is preemptable at time t
j2 is scheduled at C2 and is not preemptable at time t

Now, is t a preemptive time? It is not so clear to me. Technically, at time t scheduler can decide what job to schedule next. However, suppose we have a job j3 that cannot be scheduled at C1, then information that "t is a preemption time" is irrelevant for job j3.

We can have something like partitioned schedule, where we would like to separate preemptions of one core from preemptions on other cores.

Sergey, yes, the situation gets quite a bit more complicated on multiprocessors. I think you are hitting on two somewhat separate issues here.

Under global scheduling, whether t should be a preemption time depends on whether we have a global scheduler with eager or lazy preemption semantics (discussed at length in my thesis). We don't have these concepts in Prosa (and no plans to get into this anytime soon). The naïve definition would be to say if there exists any core on which there is a preemptive job (or the core is idle), then it's a preemption time. This would correspond to eager preemption semantics, which is also what most practical systems in the wild implement (but not e.g. LITMUS^RT). I would be ok with hard-coding this variant for the time being.
Everything gets a lot more complicated once you have job placement constraints. If you have any notion that prevents certain jobs from running on certain cores (e.g., partitioned, clustered, APA, semi-partitioned), it fundamentally affects notions of priority-policy compliance, work conservation, preemption-model compliance, etc. This is definitely something we will have to tackle in Prosa at some time, but I would argue we are not quite ready for this at the moment. So I would table it for now.

Bottomline: While I can give you a long lecture on these issues "on paper", tricky details remain to be resolved to properly formalize the multiprocessor case. Hence I would argue in favor of adopting just a uniprocessor solution for now. Specifically, I wouldn't mind having a set of definitions and supporting lemmas that make sense only in the context of a uniprocessor_model.

mentioned in merge request !130 (merged)

marked this issue as related to #78 (closed)

mentioned in issue #78 (closed)

Could you please post a quick update on the current progress here? Sergey, if !171 (merged) gets merged, will it take care of this, too?

Nope, we still need to change this def

  Definition preemption_time (t : instant) :=
    if sched t is Some j then
      job_preemptable j (service sched j t)
    else true.

My assumption is that this will be easy to do with the definitions you are adding in !171 (merged). Please correct me if that's not the case.

If not, that's ok. I just don't want to duplicate work in !171 (merged) and here.

Tbh, I don't see a lot of stuff that can be reused here from !171 (merged).
However, I think the nature of changes is very similar to !171 (merged) (we basically do the same thing but to two different definitions).

Ok, thanks. I thought the key issue is to have a generic but computable version of "which job is scheduled at time t". Is this coming with !171 (merged)? If so, we should reuse it rather than coming up with a parallel definition here. Presumably any such definition is going to come with a bunch of lemmas, which I don't want to redevelop multiple times.

"which job is scheduled at time t"

Ah, this might help.

We can define the following predicate:

  (* TODO: come up with a name *)
  Definition "a job with property P is scheduled at time t" :=  
    exists j, scheduled_at sched j t /\ P j

Then priority_inversion is defined as follows:

  Definition priority_inversion (t : instant) :=   
    ~~ scheduled_at sched j t /\
    "a job with property (has_lower_priority) is scheduled at time t"

And for preemption_time it will be:

  Definition preemption_time (t : instant) :=
    "is idle" 
    \/ "a job with property (fun j => job_preemptable j (service sched j t)) is scheduled at time t"

I'll see if I can add this to !171 (merged) (or "factor out" it into a separate MR).

Great, factoring something like this out would be easiest to review. If you look at preemption_time above, it's important that we need to be able to do a case analysis covering the situation where no job exists that's scheduled. Checking whether it satisfies some P is trivial once you have it, so I think the key primitive is to have a computable function that yields the currently scheduled job or none (on a uniprocessor, not sure about the multiprocessor case).

mentioned in commit 02b69cfa

mentioned in merge request !276 (merged)

mentioned in commit d8c06273

closed with merge request !276 (merged)

remove ideal uniprocessor assumption from priority-driven schedules

Designs

Child items ...

Activity