On Thu, 2017-04-06 at 13:06 +0200, Juergen Gross wrote:
> On 06/04/17 12:59, Dario Faggioli wrote:
> > Maybe:
> > 
> > domain_scheduler()
> > vcpu_scheduler()
> > 
> > or
> > 
> > dom_scheduler()
> > vcpu_scheduler()
> > 
> > Or, also trading 'scheduler' for 'ops':
> > 
> > dom_ops()
> > vcpu_ops()
> 
> sched_ops_dom()
> sched_ops_vcpu()
> 
> or
> 
> sched_dom_ops()
> sched_vcpu_ops()
> 
Yeah, these too.

So, for now, I've resent using dom_scheduler() and vcpu_scheduler().

But I'm happy to change them to whatever and re-send again, as soon as
George tells me which one is his preferred solution. :-D

Thanks and Regards,
Dario
-- 
<<This happens because I choose it to happen!>> (Raistlin Majere)
-----------------------------------------------------------------
Dario Faggioli, Ph.D, http://about.me/dario.faggioli
Senior Software Engineer, Citrix Systems R&D Ltd., Cambridge (UK)