Devel May 2017

devel@sel4.systems

25 participants
18 discussions

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

Fwd: k_vmm_manager: failed on sel4 hypervisor connection
by Michal Podhradsky 08 Jun '17

08 Jun '17

Hello all, I am running camkes-vm on x86 architecture, following the example on wiki https://wiki.sel4.systems/CAmkESVM#Cross_VM_Connectors with the exception that I want to invoke the stringReverse component <https://github.com/podhrmic/camkes-vm/tree/master/components/StringReverse> . I am running the optiplex9020_defconfig example with only one VM, and when I start booting the guest linux system, I see the following error: *[ 1.282326] dataport: loading out-of-tree module taints kernel.* *[ 1.290615] dataport: module license 'unspecified' taints kernel.* *[ 1.306854] Disabling lock debugging due to kernel taint* *[ 1.319664] dataport initialized with major number 247* *vmm_vmcall_handler:55 | Failed to find handler for token:2* *[ 1.325411] incorrect event context magic number (expected 42, got -677408512)insmod: can't insert '/lib/modules/4.8.16/kernel/drivers/vmm/consumes_event.ko': Operation not ermitted* *[ 1.337441] emits_event initialized with major number 245* *[ 1.356391] k_vmm_manager: failed on sel4 hypervisor connection |-1|* Then when I log into linux and call `string_reverse <https://github.com/podhrmic/camkes-vm/tree/master/linux/pkg/string_reverse>` program, I get the following error: *# string_reverse * *[ 8.360164] BUG: unable to handle kernel paging request at d881f2c0* *[ 8.360164] IP: [<d00a69f0>] chrdev_open+0xab/0x100* *[ 8.360164] *pde = 17867067 *pte = 00000000 * *[ 8.360164] Oops: 0000 [#1]* *[ 8.360164] Modules linked in: emits_event(PO) dataport(PO)* *[ 8.360164] CPU: 0 PID: 691 Comm: string_reverse Tainted: P O 4.8.16 #1* *[ 8.360164] task: d79c9740 task.stack: d6ae0000* *[ 8.360164] EIP: 0060:[<d00a69f0>] EFLAGS: 00010286 CPU: 0* *[ 8.360164] EIP is at chrdev_open+0xab/0x100* *[ 8.360164] EAX: d881f2c0 EBX: 00000000 ECX: d79b0d00 EDX: 00000000* *[ 8.360164] ESI: d79b0d00 EDI: d6add808 EBP: d6ae1e10 ESP: d6ae1df8* *[ 8.360164] DS: 007b ES: 007b FS: 0000 GS: 0033 SS: 0068* *[ 8.360164] CR0: 80050033 CR2: d881f2c0 CR3: 16ad9000 CR4: 00102690* *[ 8.360164] DR0: 00000000 DR1: 00000000 DR2: 00000000 DR3: 00000000* *[ 8.360164] DR6: fffe0ff0 DR7: 00000400* *[ 8.360164] Stack:* *[ 8.360164] d7ac9be0 d7ac9be0 00000001 d7ac9be0 d6add808 00000000 d6ae1e30 d00a2370* *[ 8.360164] d6ae1e28 d7ac9be8 d00a6945 d7ac9be0 d69db010 d7462d80 d6ae1e4c d00a2cf8* *[ 8.360164] d79c2b80 d79c2b80 00000000 d6ae1ebc d7462d80 d6ae1eb0 d00ae159 d6ae1e64* *[ 8.360164] Call Trace:* *[ 8.360164] [<d00a2370>] do_dentry_open+0x197/0x216* *[ 8.360164] [<d00a6945>] ? cdev_put+0x1a/0x1a* *[ 8.360164] [<d00a2cf8>] vfs_open+0x45/0x4e* *[ 8.360164] [<d00ae159>] path_openat+0x822/0x970* *[ 8.360164] [<d007a468>] ? __alloc_pages_nodemask+0x11c/0x770* *[ 8.360164] [<d00ae2d8>] do_filp_open+0x31/0x77* *[ 8.360164] [<d00b6293>] ? __alloc_fd+0xbb/0xfe* *[ 8.360164] [<d00a2e56>] do_sys_open+0x54/0xc7* *[ 8.360164] [<d00a2ee1>] SyS_open+0x18/0x1a* *[ 8.360164] [<d0000ee1>] do_fast_syscall_32+0x7a/0xb8* *[ 8.360164] [<d047831f>] sysenter_past_esp+0x40/0x6a* *[ 8.360164] Code: 11 89 f0 e8 e1 fa ff ff 83 f8 01 19 db 31 d2 83 e3 fa 89 d0 e8 4d ff ff ff 85 db 75 59 8b 46 28 85 c0 75 0c* *[ 8.360164] EIP: [<d00a69f0>] chrdev_open+0xab/0x100 SS:ESP 0068:d6ae1df8* *[ 8.360164] CR2: 00000000d881f2c0* *[ 8.360164] ---[ end trace 46873a57a343e435 ]---* *[ 8.376285] string_reverse (691) used greatest stack depth: 6496 bytes left* *Killed* which seems like the program is trying to access memory that it is not supposed to. If I follow the example from wiki (here https://wiki.sel4. systems/CAmkESVM#Cross_VM_Connectors ) I get the same error, but triggered by `print_client` program. Have you seen a problem like this before? How do I correctly load the kernel module? Regards Michal

2 5

Using linux-tk1-debian on camkes-arm-vm
by Mike Clark 05 Jun '17

05 Jun '17

I have seL4 running on a TK1 using linux-tk1-initrd. I'd like to get the linux-tk1-debian version running to load the userspace off of the emmc drive of the TK1. FWIW, I did flash the TK1 to the latest verison, R21.5. The default DTS has root=/dev/mmcblk0p2 in the bootargs. When booting with this, I get a kernel panic. I also tried changing that to root=/dev/mmcblk0p1 (since that partition was the larger one on the emmc). It also gives a kernel panic, albeit a different message. With mmcblk0p1, the message I get is: [ 10.092841] EXT2-fs (mmcblk0p1): error: couldn't mount because of unsupported optional features (240) [ 10.102749] EXT4-fs (mmcblk0p1): couldn't mount as ext3 due to feature incompatibilities [ 10.137427] EXT4-fs (mmcblk0p1): mounted filesystem with ordered data mode. Opts: (null) [ 10.145696] VFS: Mounted root (ext4 filesystem) on device 179:1. [ 10.162679] devtmpfs: mounted [ 10.165845] Freeing unused kernel memory: 252K (c0aa9000 - c0ae8000) [ 10.224352] Kernel panic - not syncing: Attempted to kill init! exitcode=0x00000004 [ 10.224352] [ 10.233480] CPU: 0 PID: 1 Comm: init Tainted: G W 4.3.0-rc5 #1 [ 10.240429] Hardware name: NVIDIA Tegra SoC (Flattened Device Tree) [ 10.246713] [<c0015d30>] (unwind_backtrace) from [<c0012b74>] (show_stack+0x10/0x14) [ 10.254457] [<c0012b74>] (show_stack) from [<c009247c>] (panic+0xa0/0x214) [ 10.261330] [<c009247c>] (panic) from [<c002566c>] (complete_and_exit+0x0/0x1c) [ 10.268627] [<c002566c>] (complete_and_exit) from [<00000000>] ( (null)) [ 10.275408] ---[ end Kernel panic - not syncing: Attempted to kill init! exitcode=0x00000004 With mmcblk0p2, the message I get is: [ 10.095124] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010) - read(0x1000000) [ 10.102907] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem in 1th superblock [ 10.111127] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010) - read(0xfb000000) [ 10.118994] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem in 2th superblock [ 10.126711] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010) - read(0x1000000) [ 10.134472] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem in 1th superblock [ 10.142167] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010) - read(0xfb000000) [ 10.149983] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem in 2th superblock [ 10.159891] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010) - read(0x1000000) [ 10.167669] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem in 1th superblock [ 10.175842] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010) - read(0xfb000000) [ 10.183743] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem in 2th superblock [ 10.191391] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010) - read(0x1000000) [ 10.199146] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem in 1th superblock [ 10.206813] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010) - read(0xfb000000) [ 10.214653] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem in 2th superblock [ 10.222551] Kernel panic - not syncing: VFS: Unable to mount root fs on unknown-block(179,2) [ 10.230976] CPU: 0 PID: 1 Comm: swapper Tainted: G W 4.3.0-rc5 #1 [ 10.238184] Hardware name: NVIDIA Tegra SoC (Flattened Device Tree) [ 10.244462] [<c0015d30>] (unwind_backtrace) from [<c0012b74>] (show_stack+0x10/0x14) [ 10.252205] [<c0012b74>] (show_stack) from [<c009247c>] (panic+0xa0/0x214) [ 10.259079] [<c009247c>] (panic) from [<c0aaa238>] (mount_block_root+0x21c/0x230) [ 10.266554] [<c0aaa238>] (mount_block_root) from [<c0aaa368>] (mount_root+0x11c/0x124) [ 10.274459] [<c0aaa368>] (mount_root) from [<c0aaa4bc>] (prepare_namespace+0x14c/0x194) [ 10.282451] [<c0aaa4bc>] (prepare_namespace) from [<c0aa9dec>] (kernel_init_freeable+0x1c0/0x1d0) [ 10.291315] [<c0aa9dec>] (kernel_init_freeable) from [<c07c4b20>] (kernel_init+0x8/0xe8) [ 10.299397] [<c07c4b20>] (kernel_init) from [<c000f4d8>] (ret_from_fork+0x14/0x3c) [ 10.306959] ---[ end Kernel panic - not syncing: VFS: Unable to mount root fs on unknown-block(179,2) Is there a guide for how to setup the emmc on the TK1 to boot using linux-tk1-debian? Will an older version of the TK1 image from Nvidia work or do I need to do a custom debian install (like this https://wiki.debian.org/InstallingDebianOn/NVIDIA/Jetson-TK1)?

2 3

Running Linux on top of seL4
by Daniel Wang 05 Jun '17

05 Jun '17

Hi all, Is there any guide about how to run Linux on top of seL4? Or has anyone done that before that can give me some hints? Thanks -Dan

4 6

The path where the kernel jumps to apps
by shijun zhao 31 May '17

31 May '17

Hi, I’m tracing the path where sel4 kernel jumps to an application, such as hello-1. >From the Makefile for apps I know that the entry of the hello-1.bin is *_sel4_start* which is defined in the sel4_crt0.S (the directory is sel4_tutorials/projects/sel4_libs_libsel4platsupport/src/arch/arm). The *_sel4_start* function first calls a C function called *sel4_InitBootInfo*, and finally jumps to the *_start* function which is defined in the crt0.S. However the *_start* in crt0.S calls the sel4_InitBootInfo again. What confuses me is that the sel4_InitBootInfo function requires an input argument passed by R0, however the R0 has been set to zero in the _sel4_start function, so I think the calling of sel4_InitBootInfo in the _start will not run correctly. Or is the path where the kernel jumps to the app (_sel4_start->_start->main) wrong? I paste referred codes below: */******sel4_crt0.S********************/* _sel4_start: /* Setup a stack for ourselves. */ ldr sp, =_stack_top /* Setup bootinfo. The pointer to the bootinfo struct starts in 'r0'. */ bl seL4_InitBootInfo ............ mov r0, #0 // *The R0 is modified, so it doesn't store the bootinfo structure anymore!* ............ /* Now go to actual _start */ ldr pc, =_start */*********crt0.S********************/* _start: /* Setup a stack for ourselves. */ ldr sp, =_stack_top */* Setup bootinfo. The pointer to the bootinfo struct starts in 'r0'. */* * bl seL4_InitBootInfo //Since R0 has been modified by _sel4_start, sel4_InitBootInfo will not run correctly.* /* Call constructors and other initialisation functions. */ bl _init /* Call main. */ bl main b exit Best Regards, Shijun Zhao

2 2

How to prove correctness of my own program?
by Adam Badura 30 May '17

30 May '17

I expect this might be (or even probably is) a bad place to ask this but at the same time I didn't find any better coming from the Contact Information page (http://sel4.systems/contact/). I'm working on a conference paper (not sure if I will make it but still trying to - code::dive <http://codedive.pl/> if anyone would be interested) about proving program correctness. Considering my own knowledge in the field and expected knowledge of the audience there would be nothing new in that paper - more like an update on what is the current state of the field. Yet I wanted to supply also some examples. As main example I would like to show proof (or at least parts of it) of correctness (adherence to specification) of C++ code, possibly reduced to C code if need be. After research in this topic and finding this project some time ago it felt natural to reuse its tools. But I fail to do so. Could you possibly guide me? Using your tools and techniques what should I do to prove correctness of some piece of code. I think source code level would be more than enough - for this task no need to verify binary in any form. As a side example I would like to show how your proves look like. I'm not sure what you are generating / writing as a proof (that gets later verified automatically). I imagine a sequence of something. Some formulas in natural deduction perhaps? Or something else? Whatever that would be I guess it must be pretty long so it is not like I would show and analyze it all but instead would like to somehow let the audience "feel the size". If - as I expect - this is not the right place to ask and you cannot help me with above questions, could you at least point me to where to ask them? Adam Badura

2 1

camkes-arm-vm not registering GPIO?
by Steven Johnston 30 May '17

30 May '17

Hi All, I am playing around with the capabilities of the camkes-arm-vm project pn the Tegra TK1 and and wondering if someone else has come across this issue. It looks like GPIO functionality is not available in the buildroot. I can confirm the GPIO source is present and is being built: camkes-arm-vm/libs/libplatsupport/rc/plat/tk1/gpio.c camkes-arm-vm/libs/libplatsupport/plat_include/tk1/platsupport/plat/gpio.h [CC] src/plat/tk1/gpio.o The expected sysfs support is not present and looking and the relevant dmesg: # dmesg | grep gpio [ 0.057543] gpiochip_add: GPIOs 0..255 (tegra-gpio) failed to register [ 1.485061] input: gpio-keys as /devices/soc0/gpio-keys/input/input0 Any thoughts on what could be causing GPIO to the failing to register? Steven

2 4

About timer tests (CONFIG_HAVE_TIMER) in sel4test testsuites
by Jesse-SC Chou (周書正) 26 May '17

26 May '17

Hi seL4-hackers, I am porting the sel4test project to my custom target board, which contains an ARM Cortex-A7 core. The porting work is based on NVidia TK1 Cortex-A15 platform. In current stage, the seL4 kernel has booted up and the test benches can be tested. I can pass all tests except for the timer tests (turn off CONFIG_HAVE_TIMER). In my target, only ARM generic timer is used. My questions are: 1. Are the timer tests (CONFIG_HAVE_TIMER) designed for other platform timer besides ARM generic timer? If I only use ARM generic timer, should these timer tests be passed? 2. My goal is to running Linux with seL4 VMM on my target. The sel4platsupport_get_default_timer() is platform specific. If I only use ARM generic timer, should sel4platsupport_get_default_timer() be ported to return the ARM generic timer? If yes, is there any example for me to reference? BRs, Jesse

2 2

CapDL Spec Error
by Chris Guikema 22 May '17

22 May '17

Hello All, Has anyone come across this error before? [GEN] imx6_net.cdl While forming CapDL spec: failed to find dataport symbol 'camkes router router_send_buf data' in ELF router_group_bin make[1]: *** [imx6_net.cdl] Error 255 make[1]: *** Deleting file `imx6_net.cdl' make: *** [imx6_net] Error 2 Thanks, Chris Guikema

2 4

Blog post: seL4, CAmkES, and L4v dependencies
by Luke.Mondy＠data61.csiro.au 19 May '17

19 May '17

Hello all, We have published a blog post about how we manage software dependencies within Trustworthy Systems, and how it has been adapted to produce a relatively user-friendly interface. It is relevant for people both new and old to the seL4 ecosystem, as it simplifies and compartmentalises the elaborate software dependencies sometimes required to get things to build. You can read the blog post here: https://research.csiro.au/tsblog/getting-started-sel4-camkes-l4v-dependenci… If you have any feedback or changes you would like made, please let us know on the GitHub repo. Cheers, Luke -- Luke Mondy, Systems Administrator, Trustworthy Systems DATA61 | CSIRO M +61 0415 281 991 | https://ts.data61.csiro.au

1 0

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel May 2017