June 2017 - Devel - lists.sel4.systems

seL4 test on x86
by Yevgeny Lavrov 29 Jan '25

29 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

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

18 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

Can I run Android on camkes-arm-vm with tk1 board?
by li94575 04 Aug '17

04 Aug '17

Hi, Now, Linux4.3 kernel can work well on camkes-arm-vm, does that mean we can run an Android system based on this kernel? I have tried to replace the roofs with an Android ramdisk, but Linux can not excute the Init program. The error is showing below: [ 10.598871] Freeing unused kernel memory: 4168K (c0a74000 - c0e86000) [ 10.761443] Kernel panic - not syncing: Attempted to kill init! exitcode=0x00000004 [ 10.761443] [ 10.770568] CPU: 0 PID: 1 Comm: init Tainted: G W 4.3.0-rc5-00024-gec4c02c-dirty #122 [ 10.779510] Hardware name: NVIDIA Tegra SoC (Flattened Device Tree) [ 10.785795] [<c00167ec>] (unwind_backtrace) from [<c0012958>] (show_stack+0x10/0x14) [ 10.793537] [<c0012958>] (show_stack) from [<c008f054>] (panic+0x94/0x220) [ 10.800407] [<c008f054>] (panic) from [<c0025b9c>] (do_exit+0x7fc/0x8f4) [ 10.807101] [<c0025b9c>] (do_exit) from [<c0025d70>] (do_group_exit+0x3c/0xf0) [ 10.814318] [<c0025d70>] (do_group_exit) from [<c002f3ec>] (get_signal+0x1a4/0x754) [ 10.821971] [<c002f3ec>] (get_signal) from [<c001a748>] (do_signal+0x84/0x61c) [ 10.829188] [<c001a748>] (do_signal) from [<c0012604>] (do_work_pending+0xa4/0xb4) [ 10.836750] [<c0012604>] (do_work_pending) from [<c000f6b4>] (slow_work_pending+0xc/0x20) [ 10.844919] ---[ end Kernel panic - not syncing: Attempted to kill init! exitcode=0x00000004 Is this a problem that current VMM does not support FPU? or other reasons caused the problem？

2 11

network on seL4
by Gábor Székely 03 Aug '17

03 Aug '17

Hi, I would like to use network (TCP) on seL4, I know that I should probably be using lwip, however I have no idea how to properly initialize it (this is the first time I'm working in such a hardware close environment), so I need some help or some kind of example, but I don't know where to look. I'm working on ia32. I also tried to run the rumprun hello world, the compillation finishes, however I get the following output when I try to run it: https://pastebin.com/MiMB0N62 Regards, Gábor Székely

4 4

elfloader-tool
by Yevgeny Lavrov 29 Jun '17

29 Jun '17

Hi Is there any instruction on how to compile and use elfloader-tool? More specifically: I want to link seL4 image with other image to try out on i.MX6 platform. Thanks

2 1

vmm documentation
by Mike Clark 29 Jun '17

29 Jun '17

Is there any documentation on how the VMM works? If I wanted to start hacking on the VMM and extend its capability, where should I start looking to learn how it works, etc? That might be a pretty broad topic, because there are lots of ways the VMM can be extended, I'm sure. Broad is fine, until I get things more figured out.

4 17

Why armel for the seL4 ARM VMM?
by John Backes 27 Jun '17

27 Jun '17

I was curious why the ARM VMM for the TK1 only seems to support the use of armel based distributions? Does special care need to be taken in the VMM to handle guest floating point instructions if the OS is armhf based? - John

2 1

How does the seL4 kernel revoke frame cap?
by Norrathep Rattanavipanon 23 Jun '17

23 Jun '17

Hello, I was wondering when we call seL4_cnode_delete on a (mapped) frame cap, does the kernel also handle unmapping the frame (in addition to withdrawing authority) as well? Or the user-space has to ensure that the frame is unmapped first before calling delete? I tried my code without unmapping that frame when deleting the cap and it seems to work fine. So I guess the kernel handles that? Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

3 5

Tutorial app hello-camkes-mcs not working
by Nicholas VanderStel 23 Jun '17

23 Jun '17

I've been able to build and run the hello-camkes-mcs example app from the camkes-mcs-tutorials.xml manifest both on a SabreLite board and in QEMU. However, when I try to run the app with the budget and period values given in the solution file, the client tasks don't appear to be running as they should. See the output from running on the SabreLite here: https://pastebin.com/RM0aisyF After that point it seems to hang. I tried smaller budget & period values and have been able to get one client task running, but the second task doesn't appear to be running. Has anyone been able to run this example with different results? Thanks, Nick VanderStel

1 0

Help with libethdriver
by Fabrizio Bertocci 22 Jun '17

22 Jun '17

Hi all, I am facing an issue with our existing project (currently based on seL4 1.0). I am in the process of migrating our project to the latest version of seL4. After all the required changes I am facing a problem I need some help. In our code, we use libplatsupport for timer & serial I/O as well as the libethdriver in order to use the network interface of the IMX6 board. The problem appears that the IOMUX device registers are mapped twice. A first time from libplatsupport (and never released): -> sel4platsupport_new_io_ops() -> calls: mux_sys_init() -> calls the macro: MAP_IF_NULL(io_ops, IMX6_IOMUXC, _mux.iomuxc); This end up mapping the device region IMX6_IOMUXC: 0x20e0000 - 0x20e100 (size_bits=12). So far so good... but then they are mapped again from the ethernet driver: ethif_new_lwip_driver_no_malloc() -> call my initialization fn -> call ethif_imx6_init() -> call setup_iomux_enet() that end up mapping again the region @ IOMUXC_PADDR = 0x20e1000 This second time, the mapping function _utspace_split_alloc fails because apparently the region 0x20e000 has been already mapped (and is not in the regions available). If I comment out the call to mux_sys_init() in libsel4platsupport_new_io_ops() my ethernet driver successfully initialize (but clearly that's not the correct workaround). Any suggestions? Regards, Fabrizio Bertocci Real-Time Innovations, Inc. Sunnyvale, CA

2 1