- Devel - lists.sel4.systems

malloc & errno
by Fabrizio Bertocci 05 Jul '17

05 Jul '17

Hi all, I am facing a puzzling problem related to muslc. While running some tests with the ia32 simulator (qemu), have noticed that whenever I call malloc() and I run out of memory (because my morecore buffer is too small), I am getting some kernel crash. I have traced the issue to the place where errno is set to -ENOMEM. Referencing to errno is platform-dependent and end up calling a function that retrieve the struct pthread associated and access errno as one of the field of the struct pthread. What is the correct process to set up a heap from the root task in such a way that we can call malloc() and correctly handle error conditions through errno? I am pretty sure I am doing something wrong in my initialization code (I have based my main(0 on the code from the tutorials), because I am also having other problems with malloc(). (even after I increase my heap area). For example, in some cases a call to malloc() end up calling a cascade of functions that eventually (from inside muslc) end up calling again malloc(). As consequence it enters in an infinite loop that stop only after it exhaust the initial stack. I could not find any clear example that show how to correctly set up a system to use muslc. Can anyone point me to a good example that shows how to bootstrap a system for the 5.2.0 branch? Regards, Fabrizio Bertocci Real-Time Innovations, Inc. Sunnyvale, CA

2 1

make: stack: Command not found
by tj5527 04 Jul '17

04 Jul '17

A newbie question. I follow the link [1] trying to build sel4 with qemu. But when `make`ing the binary, it throws error message `make: stack: Command not found`. I `apt-get install stacks` but it still fails with the same error. What packages should I install for making sel4 with Ubuntu 16.04 LTS, GNU Make 4.1, and gcc version 5.4.0 20160609? Thanks [Error Message] -- Build files have been written to: /path/to/sel4/stage/x86/pc99/accelerator ninja: no work to do. [apps/vm] building... [HEADERS] [STAGE] autoconf.h [apps/vm] done. [parse-capDL] building... make: Entering directory '/path/to/sel4/projects/capdl/capDL-tool' stack setup make: stack: Command not found Makefile:39: recipe for target 'sandbox' failed make: *** [sandbox] Error 127 make: Leaving directory '/path/to/sel4/projects/capdl/capDL-tool' Makefile:53: recipe for target '/path/to/sel4/stage/x86/pc99/parse-capDL/parse-capDL' failed make: *** [/path/to/sel4/stage/x86/pc99/parse-capDL/parse-capDL] Error 2 [1] https://wiki.sel4.systems/Hardware/Qemu

1 1

elfloader-tool
by Yevgeny Lavrov 30 Jun '17

30 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 24 Jun '17

24 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 24 Jun '17

24 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

Questions about TK1-SOM Memory Management
by Daniel Wang 22 Jun '17

22 Jun '17

Hi Adrian, Thank you very much for your explain. I might have some misunderstanding about the source code. First may I ask what the kernel window means? Does it means the virtual memory space kernel can access (through pptr_t)? I can see the dev_p_regs[] (kernel/src/plat/tk1/machine/hardware.c) has multiple parts: the first is the RAM part, VM_HOST_PA_START - VM_HOST_PA_START + VM_HOST_PA_SIZE (0xb0000000 — 0xf0000000), the rest are real device region from 0x01000000 - 0x7c000000 approximately. I guess my question is why put the second half as a “device” instead of putting it together in avail_p_regs[]? Is it somehow due to the support of virtualization? Here is the booting procedure according to my understanding, could you take a look and see if I got it right? 1. the code start at the ELF-loader main() (tools/elfloader/src/arch-arm/boot.c) which is loaded in physical memory 0x82000000 for TK1 (tools/elfloader/gen_boot_image.sh) 2. the boot code unpack the ELF and find the kernel image and the user-land image, the kernel is loaded at 0x80000000 the user land image is loaded at 0x80037000 approximately 3. MMU is enabled and a “boot" page directory is created that maps physical 0x80000000 to (0xe0000000 - 0xf0000000) 4. enter the kernel code _start, which setup up vector table and kernel stack; then init_kernel(); then try_init_kernel() calls map_kernel_window() I’m not sure why map_kernel_windows() remap the virtual address kernelBase (start from 0xe0000000) to physical address physBase (0x80000000) again or did I miss anything? Also I’m not sure what those armHSGlobalPGD[], armHSGlobalPD[] for, I assume it is for context switch? (deleted diagram due to size limit) Thanks -Dan

2 3

drivers in seL4
by 杰尔米 22 Jun '17

22 Jun '17

Hi all， I want to know more about the mechanism of device driver in seL4. How does seL4 support userspace drivers? if I want to write a driver(e.g. serial port) base on seL4, how to do that? can any one help? Best Regards! Jeremy

3 2