From a quick review of the seL4, I'd guess you'd want to start by

>>>> On Thu, 14 May 2015 16:31:49 +0100, Hesham ALMatary <heshamelmatary(a)gmail.com&gt; said:

Hi Hesham, Is there any link we can check to follow up ? Kudos for the acceptance !

-Jorge Alberto Garcia On Tue, May 19, 2015 at 8:40 AM, <krste(a)berkeley.edu&gt; wrote: > > > Hi Hesham, > > Congrats on the GSoC acceptance! > > From a quick review of the seL4, I'd guess you'd want to start by > using M-mode for L4 microkernel, and run guest OS instances in S-mode. > M/S-modes should be enough to provide efficient basic VMM > functionality, provided there's some physical memory protection (which > we consider part of hardware platform spec). > > RISC-V uses M-mode to emulate missing hardware functionality (e.g., > misaligned memory access), so that might be a concern (have to audit > the emulation code). > > Look forward to hearing of your progress. > > Krste > > >>>>> On Thu, 14 May 2015 16:31:49 +0100, Hesham ALMatary > >>>>> <heshamelmatary(a)gmail.com&gt; said: > > | Hi all, I was fortunate enough to be accepted in this year's GSoC > | instance with "Porting seL4 to lowRISC" project for lowRISC > | organization. My name is Hesham, and I am a PhD student at the > | University of York and my mentor is Stefan Wallentowitz. > > | As the name of the project indicates, it's about porting the > | formally verified seL4 microkernel [1] to RISC-V/lowRISC > | platform. Initially, I'll work on getting the seL4 microkernel > | working on Spike simulator which currently supports both 32-bit and > | 64-bit modes. Then we can move to running it on real hardware > | (Rocket Chip [2]). The project will extensively make use of the > | newly published privileged spec [3] and will study how to utilize > | the current 4 RISC-V modes (though there's no implementation for > | hypervisor mode yet). Some of the user-level libraries/applications > | will also be nice to port. > > | I'd appreciate any comments or suggestion that may help with this > | project. > > | [1] http://sel4.systems/ [2] https://github.com/ucb-bar/rocket-chip > | [3] http://riscv.org/download.html#tab_spec_privileged_isa > > | Thanks, > | -- > | Hesham

Hi Hesham, Congrats on the GSoC acceptance!

From a quick review of the seL4, I'd guess you'd want to start by using M-mode for L4 microkernel, and run guest OS instances in S-mode. M/S-modes should be enough to provide efficient basic VMM functionality, provided there's some physical memory protection (which we consider part of hardware platform spec).

RISC-V uses M-mode to emulate missing hardware functionality (e.g., misaligned memory access), so that might be a concern (have to audit the emulation code). Look forward to hearing of your progress. Krste >>>>> On Thu, 14 May 2015 16:31:49 +0100, Hesham ALMatary <heshamelmatary(a)gmail.com&gt; said: | Hi all, I was fortunate enough to be accepted in this year's GSoC | instance with "Porting seL4 to lowRISC" project for lowRISC | organization. My name is Hesham, and I am a PhD student at the | University of York and my mentor is Stefan Wallentowitz. | As the name of the project indicates, it's about porting the | formally verified seL4 microkernel [1] to RISC-V/lowRISC | platform. Initially, I'll work on getting the seL4 microkernel | working on Spike simulator which currently supports both 32-bit and | 64-bit modes. Then we can move to running it on real hardware | (Rocket Chip [2]). The project will extensively make use of the | newly published privileged spec [3] and will study how to utilize | the current 4 RISC-V modes (though there's no implementation for | hypervisor mode yet). Some of the user-level libraries/applications | will also be nice to port. | I'd appreciate any comments or suggestion that may help with this | project. | [1] http://sel4.systems/ [2] https://github.com/ucb-bar/rocket-chip | [3] http://riscv.org/download.html#tab_spec_privileged_isa | Thanks, | -- | Hesham