August 2021 - Devel - lists.sel4.systems

Is the project port Minix 3 to run on seL4 already in work?
by christian.sagstetter＠googlemail.com 24 Aug '21

24 Aug '21

hello everyone, I would be interested in the project and wanted to know if it is already being worked on. best christian

3 3

Uses and description for seL4_CNode_Mutate?
by Mark Jones 23 Aug '21

23 Aug '21

This isn't a big issue, but I'm curious about how seL4_CNode_Mutate is intended to be used, and have found that the description in the seL4 reference manual doesn't seem to match the implementation. Is it for changing rights? The manual (Section 3.1.2) says: "seL4_CNode_Mutate() can move a capability similarly to seL4_CNode_Move() and also reduce its rights..." Section 3.1.4 also refers to the possibility to specify a new set of rights with an invocation of seL4_CNode_Mutate(). However, the summary of seL4_CNode_Mutate in Section 10.3.1.6 does not include a parameter that specifies any rights information, so it appears that it cannot actually be used in this way. Is it for changing badges? In Section 4.2.1, the manual says that "An endpoint capability with a zero badge ... can be badged with the seL4_CNode_Mutate() or seL4_CNode_Mint() invocations" There is a similar statement for Notifications in Section 5.1. But a comment in the (Haskell version of the) spec says "endpoint capabilities may not have their badges changed" when they are updated by a Mutate or Rotate operation. And the kernel seems to follow this: I added a test to sel4test to confirm that you get an illegal operation error if you try to badge an endpoint using Mutate. (Assuming I wrote the test correctly ...) Unless there are other arch-specific use cases, it looks like the only thing you can do with Mutate is to change the guard of a CNode capability. Even then, that is only possible if you are moving the capability at the same time. Of course, you could combine a mutate with a regular move to simulate an in-place update ... but you could also use an in-place mutate and a separate move to simulate the current behavior, without having to find an empty slot if you just wanted the in-place operation. One conclusion is that the manual's description of Mutate probably needs an update. But if nobody else has tripped over problems using it to create badged endpoints, then perhaps Mutate just isn't being used very much at all and could be removed altogether? A second thought is whether Mutate could be modified to perform an in-place update if the source and destination are the same (i.e., similar in some ways to how you specify a swap with Rotate)? Best wishes, Mark

4 5

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