seL4 as a hypervisor running a linux guest and a RToS(or native sel4 applications) on ARM
Hello, I'm trying to form an understanding of what one can do with seL4 and how much work is involved in doing it. I am currently under the impression that seL4 could act as a hypervisor and run a linux guest. But I have not found easily accessible instructions for how to do this (ARM targets are most interesting, the Raspberry Pi preferably as it is cheap and ubiquitously available). Did anyone here set up such a seL4 as hypervisor for linux guest and document the procedure? I would be very thankful for links. If such a setup is doable, can you still run some native seL4 code on the "hypervisor" then? Thank you very much /JS
I don't believe raspberry pi is supported for virtualization. I followed
the instructions on https://github.com/SEL4PROJ/camkes-arm-vm/blob/
master/README.md to get it working on the TK1. Wasn't too hard.
On Jan 26, 2018 4:48 AM, "Joel Svensson"
Hello,
I'm trying to form an understanding of what one can do with seL4 and how much work is involved in doing it.
I am currently under the impression that seL4 could act as a hypervisor and run a linux guest. But I have not found easily accessible instructions for how to do this (ARM targets are most interesting, the Raspberry Pi preferably as it is cheap and ubiquitously available). Did anyone here set up such a seL4 as hypervisor for linux guest and document the procedure? I would be very thankful for links. If such a setup is doable, can you still run some native seL4 code on the "hypervisor" then?
Thank you very much /JS
_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Thank you very much Mike,
I think I have seen that what is missing on the PI is virtualized GIC
(VGIC/GICv2, RPI2/RPI3). The XVisor Pi port seems to do without it,
probably by implementing similar functionality itself (somehow).
Are there any plans in the pipeline to implement similar functionality on
the sel4-arm code tree (would it be possible)?
Thanks for pointing out the camkes-arm-vm gitrepo!
With the missing VGIC/GICv2 is there any point in even trying to adapt the
instructions in the camkes-arm-vm repo? I am guessing, no. But if I am
wrong and someone has been working in this direction, please let me know.
Thanks a lot and best regards
On Fri, Jan 26, 2018 at 3:12 PM, Mike Clark
I don't believe raspberry pi is supported for virtualization. I followed the instructions on https://github.com/SEL4PROJ/camkes-arm-vm/blob/master/ README.md to get it working on the TK1. Wasn't too hard.
On Jan 26, 2018 4:48 AM, "Joel Svensson"
wrote: Hello,
I'm trying to form an understanding of what one can do with seL4 and how much work is involved in doing it.
I am currently under the impression that seL4 could act as a hypervisor and run a linux guest. But I have not found easily accessible instructions for how to do this (ARM targets are most interesting, the Raspberry Pi preferably as it is cheap and ubiquitously available). Did anyone here set up such a seL4 as hypervisor for linux guest and document the procedure? I would be very thankful for links. If such a setup is doable, can you still run some native seL4 code on the "hypervisor" then?
Thank you very much /JS
_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
participants (2)
-
Joel Svensson
-
Mike Clark