August 2021 - Devel - lists.sel4.systems

Failure on a CAmkES-VM with more than 150MB RAM
by hamed_ganji＠aut.ac.ir 06 Aug '21

06 Aug '21

Hello, I have a problem on booting a CAmkES-VM with more than 150MB RAM. The following error appears when I set [vm0.guest_ram_mb = 256] in the camkes file of the minimal example of CAmkES-VM and boot the produced image on both QEMU and real hardware system: ------------------------------------------------------------ ... vka_alloc_object_at_maybe_dev@object.h:64 Failed to allocate object of size 4096, error 1 alloc_bios_memory@acpi.c:119 Failed to allocate frame for bios addr 0xe0000 main_continued@main.c:871 [Cond failed: error] Failed to init guest boot structure ------------------------------------------------------------ Please find the full output of the booting process in attachment file. I also examined the effect of other parameters like [vm0.simple_untyped23_pool] and [vm0.heap_size] but no difference was found. Any help/hint would be very appreciated. Best regards, Hamed Ganji

1 0

Where does rumprun mount /
by Ellis 04 Aug '21

04 Aug '21

Hello, I have been messing around with sel4 rumprun and I have been trying to put files onto the file system. Where does rumprun mount the root / ? Sincerely, Ellis

1 0

Operating Systems built on top of seL4
by Sidhartha Agrawal 02 Aug '21

02 Aug '21

Hello sel4-devs, I am a first-year graduate student at the University of British Columbia at their Systopia Lab <https://systopia.cs.ubc.ca/> working on operating systems research. My advisor is Prof. Margo Seltzer <https://www.seltzer.com/margo>. In a past life, I have worked as a software engineer at Oracle and Arista Networks. My research is on General Purpose Isolation Mechanism in the OS. We ask whether we really need to have N different isolation mechanisms or whether instead, we could develop a framework in which all these different mechanisms represent points on a continuum. Here is a write-up <https://sid-agrawal.ca/#research-projects> with some more details. I am using seL4 as the microkernel base to build my research idea. At this stage, I am not looking in to the formal verification aspect of seL4, but that might change once I have a better idea about the type of mechanism I want to build. I would also like to keep the changes in the kernel to be minimum and try to demonstrate my ideas using user space processes. I have tried out the tutorials on the seL4 website. Currently, I am wading through the different helper libraries in seL4/seL4_libs <https://github.com/seL4/seL4_libs>. As someone who is just starting with seL4 ecosystem, I had a few high-level questions: - Are there are example OSes built with seL4, which would be a good place to look at? Specifically, I am looking for components such as basic versions of a process-server, vm-server, pager, file-systems server. - I came across refOS <https://github.com/seL4/refos>, but wasn't sure if it is still being maintained. - Another option was Genode <https://genode.org/documentation/general-overview/index>. This seemed to be maintained by another community and has many layers of abstractions since it supports multiple kernel backends. I am looking forward to engaging with this community, learning about seL4 and making meaningful contributions. Best, Sid sid-agrawal.ca

8 28

Sel4 rumprun has issues compiling
by Vortex 01 Aug '21

01 Aug '21

Hello, I would like to bring this issue to the attention of the community. Sel4’s fork of the rumprun unikernel no longer compiles. Due to the usage of Werror flag, the compiler produces repeated warnings which in turn creates errors. It seems like the rump kernel was tested on an older version of gcc and because it is older, raises warnings and causes the build to fail on newer compilers. This is a similar issue to https://github.com/rumpkernel/rumprun/issues/82 I have tested rumprun in the sel4 docker container. My build logs are also attached to this email. Thank you for taking attention to this issue. Sincerely, Ellis

3 3