Hi,
The seL4/RISC-V port is now working on Spike (emulator), Rocket Chip (FPGA), and jor1k (online emulator). I've also written a recent blog post how to build/run the port with SOS project [1] from my repos).
The code is pretty much like the ARM port, and following the same bootstrapping procedure (more on this on my blog). MMU code provides 4KiB and 4MiB pages (like IA-32).
I'd like to ask if there are special requirements to upstream this work: * All libraries that are target-dependant. * seL4 microkernel. * Tools (elf loader, build system). * SOS project?
I understand it won't be an easy process because this work is the first "foreign" code that big, of course apart from formal verification. But it wouldn't hurt to ask.
[1] http://heshamelmatary.blogspot.co.uk/2015/07/howto-build-and-run-sel4-on-ris...
Best,
Nice!
On Fri, Aug 7, 2015 at 7:58 AM Hesham ALMatary heshamelmatary@gmail.com wrote:
Hi,
The seL4/RISC-V port is now working on Spike (emulator), Rocket Chip (FPGA), and jor1k (online emulator). I've also written a recent blog post how to build/run the port with SOS project [1] from my repos).
The code is pretty much like the ARM port, and following the same bootstrapping procedure (more on this on my blog). MMU code provides 4KiB and 4MiB pages (like IA-32).
I'd like to ask if there are special requirements to upstream this work:
- All libraries that are target-dependant.
- seL4 microkernel.
- Tools (elf loader, build system).
- SOS project?
I understand it won't be an easy process because this work is the first "foreign" code that big, of course apart from formal verification. But it wouldn't hurt to ask.
[1] http://heshamelmatary.blogspot.co.uk/2015/07/howto-build-and-run-sel4-on-ris...
Best,
Hesham
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
That’s great to hear!
It’s a bit hard to tell what exactly would need to be done to merge it, but if you create a pull request on github, we can look at the diffs in details, give feedback and discuss what else needs to be done.
Probably easiest to start with the kernel itself first, and then go through the other repos.
Cheers, Gerwin
On 8 Aug 2015, at 12:54 am, Hesham ALMatary heshamelmatary@gmail.com wrote:
Hi,
The seL4/RISC-V port is now working on Spike (emulator), Rocket Chip (FPGA), and jor1k (online emulator). I've also written a recent blog post how to build/run the port with SOS project [1] from my repos).
The code is pretty much like the ARM port, and following the same bootstrapping procedure (more on this on my blog). MMU code provides 4KiB and 4MiB pages (like IA-32).
I'd like to ask if there are special requirements to upstream this work:
- All libraries that are target-dependant.
- seL4 microkernel.
- Tools (elf loader, build system).
- SOS project?
I understand it won't be an easy process because this work is the first "foreign" code that big, of course apart from formal verification. But it wouldn't hurt to ask.
[1] http://heshamelmatary.blogspot.co.uk/2015/07/howto-build-and-run-sel4-on-ris...
Best,
Hesham
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
________________________________
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.
On Aug 8, 2015 12:02 AM, "Gerwin Klein" Gerwin.Klein@nicta.com.au wrote:
That’s great to hear!
It’s a bit hard to tell what exactly would need to be done to merge it,
but if you create a pull request on github, we can look at the diffs in details, give feedback and discuss what else needs to be done.
Probably easiest to start with the kernel itself first, and then go
through the other repos.
I would guess the pull request should be against experimental branches, right? Or maybe a totally new one?
Are there any coding style/format?
Best, Hesham
Cheers, Gerwin
On 8 Aug 2015, at 12:54 am, Hesham ALMatary heshamelmatary@gmail.com
wrote:
Hi,
The seL4/RISC-V port is now working on Spike (emulator), Rocket Chip (FPGA), and jor1k (online emulator). I've also written a recent blog post how to build/run the port with SOS project [1] from my repos).
The code is pretty much like the ARM port, and following the same bootstrapping procedure (more on this on my blog). MMU code provides 4KiB and 4MiB pages (like IA-32).
I'd like to ask if there are special requirements to upstream this work:
- All libraries that are target-dependant.
- seL4 microkernel.
- Tools (elf loader, build system).
- SOS project?
I understand it won't be an easy process because this work is the first "foreign" code that big, of course apart from formal verification. But it wouldn't hurt to ask.
[1]
http://heshamelmatary.blogspot.co.uk/2015/07/howto-build-and-run-sel4-on-ris...
Best,
Hesham
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
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.
On Sun 09-Aug-2015 5:29 AM, Hesham ALMatary wrote:
I would guess the pull request should be against experimental branches, right? Or maybe a totally new one?
This may be a little confusing but you probably want to do a pull request against the master branch. The experimental branch is for experimental kernel features that, if they were included in the master branch, would break verification. There are also features that present a different API.
A platform or architecture port should have no verification impact, and should not change the API, hence it is fine to go straight into the master branch.
Are there any coding style/format?
We have a couple of guidelines on style, but I realize we have not made these public. Until this is done the short summary is * For general style follow what you already see in the kernel * You can do 'make style' in the kernel directory to auto format using astyle * Stick to the 'verification subset' of C99 Again the 'verification subset' is not well defined. But a very short list of things you should not do (that you might want to do) * Take the address of a local variable * Use unions, goto, fall through switch statements * Use function pointers
If your willing to do a couple of iterations then just do your best and we can point out any additional style preferences on the pull request.
Adrian
________________________________
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.
-
Adrian Danis -
Gerwin Klein -
Hesham ALMatary -
Wink Saville