Devel August 2021

devel@sel4.systems

28 participants
21 discussions

bingup the new platform not in Linux repository
by niewei1899＠163.com 20 Aug '21

20 Aug '21

about portint doc：(https://docs.sel4.systems/projects/sel4/porting) “You may need to add device nodes depending on what Linux uses and what is required by seL4. For example, in the port of the Rockpro64 a memory node and an extra timer node were needed so these had to be defined manually.” how can I get the required by seL4? have any doc about it?

1 0

smp camkes
by David Lorentz 19 Aug '21

19 Aug '21

Hi, I've been trying to extend one of the tutorial / example projects to run on more than one core with no success. After reading the camkes manual https://docs.sel4.systems/projects/camkes/manual.html#thread-cpu-affinity I assumed that you need to set core affinities for different components in your camkes file and set the KernelMaxNumNodes to a number greater than one. I tried this with the adder sample (as below) with no luck. Can anyone point me to some information on how to get smp to work, what hardware is supported and the like? configuration { adder.affinity = 1; client.affinity = 0; } Thanks David

1 0

VM support for iMX8MM/MQ dev boards
by Zippy Manaic 18 Aug '21

18 Aug '21

Hi, I have been attempting to follow some breadcrumbs to get vm_minimal app running on an IMX8 dev board. I am attempting to follow the commits by Sylvain but I think there may be a missing push to seL4/camkes-vm. Are there any plans to more formally support iMX8 platforms for VM development on seL4? Assuming I manage to get vm_minimal running on iMX8 what would be the odds of getting 2 VMs running on iMX8? Are there known limitations to the current CAmkES VM implementation that would cause me problems? Thanks, Zippy

1 0

seL4 Kernel: ARMv8.2 support
by Jorge Pereira 17 Aug '21

17 Aug '21

Hi all, Is the seL4 Kernel (with VE enabled) supporting versions of ARMv8 (e.g. ARMv8.2) other than the original one - v8.0? We'd like to port seL4 for a board that features ARMv8.2 CPUs. Is there any foreseeable roadblock? Thanks.

1 0

[Tutorial] Should the tutorial of seL4 be updated?
by Zheng Wenxin 10 Aug '21

10 Aug '21

It seems that the tutorial "CAmkES VM: Cross VM Connectors" has something missing. The part "Add modules to the guest" says that "There is a library in projects/camkes/vm-linux/camkes-linux-artifacts/camkes-linux-apps/camkes-connector-apps/libs containing Linux system call wrappers ...". But no folder named camkes/vm-linux and in camkes-vm-linux/camkes-linux-artifacts/camkes-linux-apps/camkes-connector-apps, no folder named libs. Is the tutorial should be updated?

1 0

seL4 how to access el3 secure world on ARM platfrom
by yadong.li 07 Aug '21

07 Aug '21

Hi： We want to create component driver who need to access ARM el3 secure world to read/write hardware register. But I found that seL4 did not offer capability to call smc function for component of native world. Which cap that already existed can offer the syscall or create new smc cap ? Is there some plan to support it ? Thank you very much.

2 1

some unexpected phenomenon about scheduling
by yadong.li 07 Aug '21

07 Aug '21

Hi: Recently, I found some unexpected phenomenon about scheduling on our project. My environment as follows: I run linux guest on seL4, Linux guest has 8 vcpu on 8 Arm PE from core0 ~ core7. WFI is not trap, seL4 is master kernel not mcs kernel I think seL4 idle task will not be run on core1, it will always run vcpu task. But the truth is the idle task will be run. I found when the maintenance and timer interrupt of Linux guest came, it will switch to idle, Because above interrupts handle will call handleFault, the sendIPC will set the ksCurThread(vcpu task) block on send, and the ksReadyQueuesL1Bitmap is empty. The idle task wille be run. But the recv task maybe run on core0, now core1 is in idle, is it reasonable? Thank you very much

2 1

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

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel August 2021