October 2018 - Devel - lists.sel4.systems

seL4 test on x86
by Yevgeny Lavrov 30 Jan '25

30 Jan '25

Hello, I'm new to seL4 and I'm just doing it for learning purpose. I'm trying to run seL4 test suite or simple hello world task from seL4 tutorials on the real hardware. So far I had no problems compiling seL4 test suite and running via QEMU for both x32 and x64 platforms. However, when I try to run it on the actual hardware following Running on real hardware tutorial for x86 I end up with no output at all and no error msgs that can give me a clue on where something went wrong. After compiling seL4test for x86, I ended up with two images in sel4_dir/images/ folder. Copied them over to /boot/sel4/ folder and created a new GRUB2 entry that looks like this menuentry “seL4 test suite” --class os { load video insmod gzio insmod part_msdos insmod ext2 set root=’(hd0,msdos5)’ multiboot /boot/sel4/kernel-ia32-pc99 module /boot/sel4/sel4test-driver-image-ia32-pc99 } update grub, restart and select the new entry from GRUB menu. I end up with blinking cursor on the top-left side of the screen. Please advise.

4 3

Stuck during invalidate local TLB in Tx2
by Muneeswaran Rajendran 16 Oct '24

16 Oct '24

Hi seL4 Dev team, Can someone explain the reason (share the reference) to invalidate the local TLB during kernel vspace activation as part CPU initialisation. The Tx2 board stuck while performing this operation. As per my understanding both Tx1 and Tx2 are using same A57 core. so the TLB initialisation and invalidation remain same for Tx2 and should not stuck during invalidation.Please correct me if anything wrong here. I understand from that instruction (tlbi vmalle1) which is invalidating stage 1 entries associated to the current VMID. Also from arm mmu code the seL4 setting up (TCR_EL1) TCR register addressing space as 48bit, ASID as 16bit and page table setup 4k granular size. I am using MRS macro to dump the spsr_el1 and dspsr_el0 register to see the state of processor but its throwing synchronous exception. Do we have any other option to dump all the register content to see the state of processor like we have one in 'sel4debug_dump_registers' which is used in sel4test code. Regards, Muneeswaran R

3 4

Questions about Memory Management in seL4
by Daniel Wang 19 May '23

19 May '23

Hi all, Sorry to bother, I have some basic questions about seL4 memory management. Can someone help me? 1. where is the kernel’s address space? I know there are basically three methods: a) separate virtual address space, e.g. through changing page tables on entry into privileged mode to access b) physical space, e.g. through disable automatic hardware translation of virtual addresses on entry into privilege mode c) privilege region in each process’s virtual address space, e.g. through page table to map kernel address into use-mode process. My question is which of this is being used by seL4 microkernel? 2. Objects like CSpace, VSpace, CNode, TCB, Endpoint, etc. are called kernel objects, but it seems all dynamically allocated in thread running/creating time. Are those objects (e.g. Figure 3.3 in seL4 manual) in kernel space or in user space? 3. I read that after the kernel boot up, it passes all resources, untyped memory to the first thread. Are those untyped memory physical memory or virtual memory in a single page? The reason I ask is I’m learning the code of the UNSW AOS project (two of the assignment projects are implementing frame and papers). I’m confused that before the implementation of frames and pages what kind of memory is passed to the the first thread? I saw int AOS project, it uses ut_table_init(), ut_steal_mem(), I wonder what kind of memory it operates on? Thanks -Dan

5 4

Network lwip for imx6
by wong xuguo 11 Dec '18

11 Dec '18

Hi, I am a student fron Nanjing university, a fresh man of microkernel, specially, know very little about the seL4. Recently I accept a chellange about porting the lwip to sel4, on arch of imx6, does any one could give me a clue? I found the source of camkes does have this code, could I do something to port, to make the lwip work? What my aim is make a tcp echo server. Thank you for all of you help. Best regards from Xuguo Wang

4 4

Support for QNX-like booting from an XIP filesystem image
by Andrew Warkentin 08 Nov '18

08 Nov '18

For UX/RT <https://gitlab.com/uxrt/>, the seL4-based OS I am writing, I have patched seL4 to support for booting from an in-memory execute-in-place filesystem image that contains the kernel and all user-mode programs required to mount the root filesystem (similar to that of QNX, but with more of the functionality in the bootloader rather than the root server). The existing seL4 boot process may be OK for static embedded systems that are always cross-compiled, but UX/RT is going to be a dynamic general-purpose OS with a boot image that will include files from multiple separately-installed packages and will possibly be customized to the system it is installed on. Requiring any image filesystem to be linked into the root server makes updating boot images more complex than being able to use a simple filesystem builder to make an image containing the kernel, root server, and everything else that is required (the main special considerations being placing the kernel and root server at fixed physical addresses and padding the image to allow for bss sections, which are easy enough). Also, I want it to be easy to manually boot UX/RT images, so you can just type something like "boot (hd0,0)/uxrt.boot" (much like manually booting NetBSD, OpenBSD, or most older Unices), and the bootloader will automatically load the kernel and all required modules from within the image as opposed to having to type a lot of boilerplate to load the kernel and root server (and anything else that may be required). In addition I don't think that the root server should need to have any support for parsing image filesystems and should be able to obtain all the files required for early boot from the MBI. I am using Multiboot2 with a few custom tags added and a few extra requirements regarding placement of modules. I currently have an in-memory loader that implements my variant of Multiboot2, and eventually want to implement a full disk-based bootloader. I have also implemented a page-oriented in-memory filesystem called XRFS (originally based on Linux romfs) with support for placing files at fixed addresses. The in-memory loader was parsing the filesystem and using a script to locate the modules within the image, although I have decided that it is overkill to do that, and it would allow the loader to be simpler if the filesystem image has its own MBH separate from that of the kernel (the magic number will be different from the kernel MBH as well), with tags for the kernel and each module, so that the loader's existing MBH-parsing code can be used to locate files in the image. As far as my kernel patches go, they extend the existing Multiboot2 code and do not interfere with the existing boot code. Right now they are x86-only, but I am planning to add Multiboot2 support to other architectures eventually as well. They do not introduce any dependency on my filesystem format in the kernel (it does know that there is an FS image and that there are modules contained within it, and assumes that modules are contiguous). Relocation of the root task is disabled when an FS image is present, since it will already be placed in a usable location in the image. Kernel-level ELF loading of modules is also disabled when using my Multiboot2 extensions, since my loader is capable of parsing ELF modules, loading them, and passing information on module sections and addresses to the kernel through tags. The part of the image containing the kernel is inaccessible to the root task for obvious reasons, so an additional requirement is that the kernel is the first file in the image, followed by the root server, and then all other files (XRFS is structured to allow the remainder of the image to be read even though the beginning is inaccessible). There is also support for passing the MBI through to the root task, which requires that the MBI is allocated immediately after the end of the filesystem image (a new structure is added to the bootinfo to provide the root server with the address of the MBI). >From what I've said, would there be any problems with including my patches in the mainline seL4 repository? Only the boot code is modified. Loading the root server works, but I haven't yet tested the MBI passthrough, so I am not quite ready to submit anything (currently I am working on converting my bootloader from parsing the filesystem itself to parsing an MBH in the FS image, like I said before).

2 3

Non CAmkES VM on x86
by Chris Guikema 08 Nov '18

08 Nov '18

DornerWorks is looking at working with the CAmkES-VM. In previous work with ARM, we've only used a non-camkes VMM, since the hypervisor pieces were more important (and 64-bit ARM CAmkES hadn't been developed). Out of curiosity, has Data61 ever worked with a non-CAmkES VM on x86 similar to how the old ARM VMM worked? If so, is that something that could be released? Thanks, Chris Guikema

2 1

seL4 on Heterogeneous Processing Architectures (Zynq UltraScale+ MPSoCs)
by Blam Kiwi 07 Nov '18

07 Nov '18

I am investigating the use of seL4 on heterogeneous architectures such as the Zynq UltraScale+ MPSoCs. I have a non-trivial use-case I'm investigating that involves utilising both the Cortex-R5 cores and Core-A53 cores for different applications. I'm rather new to seL4 development so I'm a bit stuck and need some advice. It's easiest if I just list my requirements and assumptions for my architecture design: a) I am targeting the Zynq US+ platform and wish to use seL4 as the OS Kernel to manage system resources and run virtual machines. b) I require the use of the Cortex R5 cores in DCLS mode for trusted code with high fault tolerance requirements. c) I require the use of the Cortex A53 cores for running unsafe Linux VMs. d) It's my understanding that seL4 lacks 64-bit multicore support for its own scheduler, but VMs running on seL4 could be provided with access to all the cores? (Eg: Linux) e) It's my understanding that seL4 lacks heterogeneous task scheduling, and cannot manage both the Cortex R5 and Cortex A53 cores. This leads me to make the following architectural conclusions: [1] It's not possible to boot an seL4 kernel on one processor and have it manage the other. [2] Use TrustZone to create vCPUs for the Cortex R5 and A53 modules and boot an seL4 kernel on each. [3] Some domain specific protocol is required for the CPU modules to communicate and share resources. Any help or advice would be appreciated. Regards, Robbie

4 4

Passing Network Resource to Linux VM in TK1-SOM
by Daniel Wang 07 Nov '18

07 Nov '18

Hi all, I got a question, how can I pass the network communication to Linux virtual machine? Following the work of seL4-ARM-VMM with TK1-SOM board, i run seL4 as the microvisor that hosts the buildroot Linux as a user-land process, I was able to mount the MMC storage in the virtual machine, but I cannot get the NIC works. I’m wondering has anyone tried it that can give me some hint? Best Regards -Daniel Wang

2 2

run docker on sel4
by Jia He 06 Nov '18

06 Nov '18

Hi all I am new comer to sel4 community. I knew a little bit virtualisation infrastructe(kvm/qemu), but I know little about sel4/docker. I am investigating the proper implemenatation for running docker on sel4 on arm64. There might several ways I can figure out.Any suggestions are welcome :-) 1. run linux on sel4 vmm (camkes_vm) and run docker on linux. This might be the easiest way. It might have worked well on X86 2. porting l4linux to sel4. Don't know whether it is feasible? 3. run docker as sel4 service without linux. On this way, golang and its library should be ported to sel4. Some missed syscalls which are needed by docker should be implemenated. Is there any other ways or anything else to make the implatation more feasible? --- Cheers, Justin

3 2

seL4 IPC and SMP question.
by 송대영 06 Nov '18

06 Nov '18

HI, I have a question about IPC and SMP. I ran sel4bench on sabre lite(i.mx6, arm v7). 1. I want to confirm performance difference between Lazy Scheduling and Beno Scheduling. Can I configure scheduler? 2. Can you explain the difference when thread state is "ThreadState_Running" and "ThreadState_Restart"? 3. I tried "SMP Benchmark" but I can't understand what this benchmark exactly means. What "Cycles" means in this benchmark? smp : This is an intra-core ipc round-trip benchmark to check overhead of the kernel synchronization on ipc throughput. 4. I try to measure IPC performance with SMP is on. I used "seL4_TCB_SetAffinity" function so server executed in Core1 and client executed Core2. But performance results are too excessive. seL4_Call(same vspace, ipc length is 0)' result is 129331186 cycles. Are these results are available?

3 2