[seL4] Re: Thread Scheduling Domains

Apologies for the necro, since it's been 10 days, but can I get clarification on this? Thanks! :D On Fri, Jul 22, 2022 at 7:51 AM June Tate-Gans (ジューン) wrote:

On that note, what kinds of information leak is this domain scheduling supposed to provide vs. everything all in one domain? The documentation for seL4 alludes to "certain" kinds of information leakage, but knowing exactly what might better explain how and when to use this kernel feature.

On Thu, Jul 21, 2022 at 5:44 PM Gerwin Klein wrote:

...

Hi June,

yes, if you're using the static domain scheduler, then that file needs to be overridden with the schedule you want.

Depending on what you're trying to do, the domain scheduler might not be the right tool for the job. It really is fully compile-time static.

Cheers, Gerwin

...

On 22 Jul 2022, at 01:35, June Tate-Gans (ジューン) via Devel wrote:

Hey folks,

So Sam and I are at the point now where we're attempting to get our untrusted user threads running in a different scheduling domain, and it's not exactly clear how this is supposed to work in terms of enabling more than one domain in the kernel.

So far, I've set KernelNumDomains to 2 in the easy-settings.cmake for our project, but unless I provide a separate implementation of kernel/config/default_domain.c by overriding KernelDomainSchedule, the resulting kernel will only think it has one domain and only ever schedule domain 0 for execution.

Are we expected to override the default_domain.c file with our own in the project, like sel4test seems to do?

Thanks!

-- June Tate-Gans Software Engineer _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems

-- June Tate-Gans Software Engineer Techlead, Kata OS / AmbiML, Cerebra Hardware

-- June Tate-Gans Software Engineer Techlead, Kata OS / AmbiML, Cerebra Hardware