> Date: Sat, 5 Mar 2022 19:15:05 +1100 > From: Kent Mcleod <[email protected]> > Subject: [seL4] Re: I Have some questions about the domain mechanism > in the seL4 > To: [email protected] > Cc: devel <[email protected]> > Message-ID: > <CA+-ozWdgMgBin34WBUoVL+uHSNfU=e852ekpgrngz5j7+ny...@mail.gmail.com> > Content-Type: text/plain; charset="UTF-8" > >> On Sat, Mar 5, 2022 at 6:11 PM 603644559--- via Devel >> <[email protected]> wrote: >> >> For some reason, i m learning the scheduling module in seL4. I have read the >> manual and the source code, and i have already read the answer in the link >> https://lists.sel4.systems/hyperkitty/list/[email protected]/thread/VYRTG3I2UDXJ2IAAQDKRJXH2AUA6SNAZ/ >> But i still do not know the purpose of adding the domain mechanism in seL4, >> Can anyone explain what kind of requirement led to the design of the domain >> mechanism? >> Please explain it more specifically, and it would be best if there were >> relevant documents and papers on the domain mechanism. > > It was added in order to enable the completion of the info-flow proofs. > >> From the infoflow proof paper > (https://trustworthy.systems/publications/nicta_full_text/6464.pdf) > where it is called the partition scheduler: > "Similarly, the original seL4 scheduler, before partition > scheduling was implemented, was known not to enforce > isolation. We could not prove information flow security until > we had fully and correctly specified the partition scheduler > in the updated abstract specification. Proving information > flow security then required us to show that the scheduler’s > choice about which partition to schedule next can never be > affected by any other partition, as one would expect."
Hello! It was my understanding that seL4 used to not have an in-kernel scheduler, and scheduling was up to the root task. How did that work? And why was the choice made to add the MCS features? Basically, why the change from having scheduling in the kernel vs. in userspace? It’s probably more convenient, especially since most operating systems are used to having scheduling in the kernel itself (so easier for people to think about). There are probably more technical reasons too. What are those? _______________________________________________ Devel mailing list -- [email protected] To unsubscribe send an email to [email protected]
