Hi all,
I'm Hesham ALMatary a computer science research student at the University of York. I am considering porting L4 microkernel variants to RISC-V [2] (for both my research and Google Summer of Code), and Fiasco.OC is one of these variants, but I want to extend the options here by asking about seL4.
Is this project would be: first applicable, and second of interest to you? And if yes, would you offer some help (guidance)? I am sending this message as suggested here [1] that I should contact you if I'm willing to port seL4 to a new platform.
[1] http://sel4.systems/GettingStarted/ [2] http://riscv.org/
Thanks,
I'm Hesham ALMatary a computer science research student at the University of York. I am considering porting L4 microkernel variants to RISC-V [2] (for both my research and Google Summer of Code), and Fiasco.OC is one of these variants, but I want to extend the options here by asking about seL4.
Is this project would be: first applicable, and second of interest to you? And if yes, would you offer some help (guidance)? I am sending this message as suggested here [1] that I should contact you if I'm willing to port seL4 to a new platform.
An architecture port is a bit of a bigger beast than a platform port ;-) I haven’t looked at RISC-V in detail, so don’t know what would be involved. But, generally speaking, a performant ISA port requires a good understanding of both kernel design and implementation as well as architecture.
We’re obviously interested in seeing seL4 used as widely as possible, and believe (with support of some solid facts) that seL4 is the leading microkernel that defines the state of the art. It is also much simpler than Fiasco.OC (about 1/3 of the SLOC size).
We’ll be happy to provide guidance (on the usual best-effort basis).
Gernot
________________________________
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Hi Hesham,
I would strongly consider seL4 over Fiasco for a few reasons: 1) Fiasco is written in C++ and I found it quit a challenge to read through due to overloaded functions - the control flow jumps between files a lot, and its not always clear which object you have during a static analysis. seL4 on the other hand, is pretty much straight C, and fairly well commented. 2) The code size (as Gernot mentioned) is much smaller in seL4, which makes it easier to comprehend in a short amount of time
But I suppose it really depends on what you intend to do with the kernel in the end. If the verification & proofs are important to you, then the choice is easy. If functionality and features are important, Fiasco probably has the advantage. If you want simple code that a student can read and do something useful with in a short time, my vote is for seL4.
Regards, Joel
On Thu, 12 Mar 2015 13:38:35 +0000, Hesham ALMatary heshamelmatary@gmail.com wrote: Hi all,
I'm Hesham ALMatary a computer science research student at the University of York. I am considering porting L4 microkernel variants to RISC-V [2] (for both my research and Google Summer of Code), and Fiasco.OC is one of these variants, but I want to extend the options here by asking about seL4.
Is this project would be: first applicable, and second of interest to you? And if yes, would you offer some help (guidance)? I am sending this message as suggested here [1] that I should contact you if I'm willing to port seL4 to a new platform.
[1] http://sel4.systems/GettingStarted/ [2] http://riscv.org/
Thanks, -- Hesham
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Considering we are developing both l4 variants and riscv cores, I would agree with Joel's recommendations. Start with sel4 and move to fiasco later if needed. On Mar 13, 2015 3:32 PM, "Joel Nider" joel@nider.org wrote:
Hi Hesham,
I would strongly consider seL4 over Fiasco for a few reasons:
- Fiasco is written in C++ and I found it quit a challenge to read
through due to overloaded functions - the control flow jumps between files a lot, and its not always clear which object you have during a static analysis. seL4 on the other hand, is pretty much straight C, and fairly well commented. 2) The code size (as Gernot mentioned) is much smaller in seL4, which makes it easier to comprehend in a short amount of time
But I suppose it really depends on what you intend to do with the kernel in the end. If the verification & proofs are important to you, then the choice is easy. If functionality and features are important, Fiasco probably has the advantage. If you want simple code that a student can read and do something useful with in a short time, my vote is for seL4. Regards, Joel
On Thu, 12 Mar 2015 13:38:35 +0000, Hesham ALMatary < heshamelmatary@gmail.com> wrote: Hi all,
I'm Hesham ALMatary a computer science research student at the University of York. I am considering porting L4 microkernel variants to RISC-V [2] (for both my research and Google Summer of Code), and Fiasco.OC is one of these variants, but I want to extend the options here by asking about seL4. Is this project would be: first applicable, and second of interest to you? And if yes, would you offer some help (guidance)? I am sending this message as suggested here [1] that I should contact you if I'm willing to port seL4 to a new platform. [1] http://sel4.systems/GettingStarted/ [2] http://riscv.org/
Thanks, -- Hesham
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Hi,
Thanks all for replying. You encouraged me to choose seL4 over Fiasco.OC.
On Fri, Mar 13, 2015 at 4:29 PM, Madhu (Macaque Labs) madhu@macaque.in wrote:
Considering we are developing both l4 variants and riscv cores, I would agree with Joel's recommendations. Start with sel4 and move to fiasco later if needed. On Mar 13, 2015 3:32 PM, "Joel Nider" joel@nider.org wrote:
Hi Hesham,
I would strongly consider seL4 over Fiasco for a few reasons:
- Fiasco is written in C++ and I found it quit a challenge to read
through due to overloaded functions - the control flow jumps between files a lot, and its not always clear which object you have during a static analysis. seL4 on the other hand, is pretty much straight C, and fairly well commented. 2) The code size (as Gernot mentioned) is much smaller in seL4, which makes it easier to comprehend in a short amount of time
But I suppose it really depends on what you intend to do with the kernel in the end. If the verification & proofs are important to you, then the choice is easy. If functionality and features are important, Fiasco probably has the advantage. If you want simple code that a student can read and do something useful with in a short time, my vote is for seL4. Regards, Joel
On Thu, 12 Mar 2015 13:38:35 +0000, Hesham ALMatary < heshamelmatary@gmail.com> wrote: Hi all,
I'm Hesham ALMatary a computer science research student at the University of York. I am considering porting L4 microkernel variants to RISC-V [2] (for both my research and Google Summer of Code), and Fiasco.OC is one of these variants, but I want to extend the options here by asking about seL4. Is this project would be: first applicable, and second of interest to you? And if yes, would you offer some help (guidance)? I am sending this message as suggested here [1] that I should contact you if I'm willing to port seL4 to a new platform. [1] http://sel4.systems/GettingStarted/ [2] http://riscv.org/
Thanks, -- Hesham
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
-
Gernot Heiser -
Hesham ALMatary -
Joel Nider -
Madhu (Macaque Labs)