On Tue, May 19, 2015 at 2:40 PM, <krste(a)berkeley.edu> wrote:
Congrats on the GSoC acceptance!
From a quick review of the seL4, I'd guess you'd want to
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).
The current seL4 ports (ARM and IA32) are mapping the kernel itself
during bootstrap/elfload, hence the microkenel is working under
virtual env. As a starting point, I followed such an implementation
and made the kernel working in S-mode right from the start. But I
agree it makes more sense to have the microkernel working in M-mode
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.
>>>>> On Thu, 14 May 2015 16:31:49 +0100, Hesham ALMatary
| 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  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 ). The project will extensively make use of the
| newly published privileged spec  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
|  http://sel4.systems/
|  http://riscv.org/download.html#tab_spec_privileged_isa