Devel June 2017

devel@sel4.systems

25 participants
31 discussions

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

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

20 Jun '17

Hi all, I’m trying to get a better understand about the implementation details of seL4 for TK1-SOM. Most of the code are very clear, but I’m little confused on the available physical memory in TK1-SOM. I’m wondering why In the hardware.c file (/kernel/src/plat/tk1/machine/hardware.c), the avail_p_regs[] ={.start = 0x80000000, .end = 0xa7f00000 } instead of 0x80000000 - 0xffffffff? Thank you very much! -Dan

2 1

Linux binaries constructed by Buildroot cannot run on tk1 board
by li94575 20 Jun '17

20 Jun '17

Hi， I use Buildroot 2016.08.1 with the config "buildroot_tk1_initrd_defconfig" to compile linux-tegra(https://github.com/SEL4PROJ/linux-tegra/tree/sel4), everything goes well. But the linux binary cannot output any logs, camkes-arm-vm stops at “Starting VM”. Can anyone tells me where might be wrong? I have tried using cross-compiler arm-none-linux-gnueabi-(2014.05) to compile linux-tegra, and that linux binary can work.

2 4

seL4test with 4.0, 5.1 failed on Ubuntu
by Daniel Wang 16 Jun '17

16 Jun '17

Hi all, I’m testing the new versions of seL4 (,4.0, 5.0, 5.1, etc.) using the sel4test-manifest. I tried both Ubuntu 16 and Ubuntu 14. For 3.2 version both I32 and KZM_simulation built just fine. However for the higher version (4.0. 5.1, 5.2) only I32 built properly. KZM_simulation keep failing on both Ubuntu 14 and 16. Anyone has the similar issues? Thanks -Dan FYI: [apps/sel4test-tests] done. [KERNEL] [MKDIR] src/arch/arm/api [PBF_GEN] arch/object/structures.pbf [PBF_GEN] arch/api/shared_types.pbf [PBF_GEN] plat/machine/hardware.pbf [PBF_GEN] api/types.pbf [BF_GEN] arch/object/structures_gen.h [BF_GEN] arch/api/shared_types_gen.h [BF_GEN] plat/machine/hardware_gen.h [BF_GEN] api/types_gen.h [CPP] src/arch/arm/armv/armv6/machine_asm.s_pp [AS] src/arch/arm/armv/armv6/machine_asm.o [CPP] src/arch/arm/32/halt.s_pp [AS] src/arch/arm/32/halt.o [CPP] src/arch/arm/32/head.s_pp [AS] src/arch/arm/32/head.o [CPP] src/arch/arm/32/idle.s_pp [AS] src/arch/arm/32/idle.o [CPP] src/arch/arm/32/traps.s_pp [AS] src/arch/arm/32/traps.o [CPP] src/arch/arm/32/hyp_traps.s_pp [AS] src/arch/arm/32/hyp_traps.o [TOUCH] sources_list_updated [CPP_GEN] kernel_all.c [CPP] kernel_all.c_pp [CP] kernel_final.c [CC] kernel_final.s /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c: In function ‘doFlush’: /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:1929:10: error: ‘ARMPDClean_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:1929:10: note: each undeclared identifier is reported only once for each function it appears in /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:1930:10: error: ‘ARMPageClean_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:1933:10: error: ‘ARMPDInvalidate_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:1934:10: error: ‘ARMPageInvalidate_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:1937:10: error: ‘ARMPDCleanInvalidate_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:1938:10: error: ‘ARMPageCleanInvalidate_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:1941:10: error: ‘ARMPDUnify_Instruction’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:1942:10: error: ‘ARMPageUnify_Instruction’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c: In function ‘decodeARMPageDirectoryInvocation’: /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2217:10: error: ‘ARMPDClean_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2218:10: error: ‘ARMPDInvalidate_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2219:10: error: ‘ARMPDCleanInvalidate_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2220:10: error: ‘ARMPDUnify_Instruction’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c: In function ‘decodeARMPageTableInvocation’: /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2335:21: error: ‘ARMPageTableUnmap’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2344:41: error: ‘ARMPageTableMap’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c: In function ‘decodeARMFrameInvocation’: /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2440:10: error: ‘ARMPageMap’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2562:10: error: ‘ARMPageRemap’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2680:10: error: ‘ARMPageUnmap’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2699:10: error: ‘ARMPageClean_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2700:10: error: ‘ARMPageInvalidate_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2701:10: error: ‘ARMPageCleanInvalidate_Data’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2702:10: error: ‘ARMPageUnify_Instruction’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2772:10: error: ‘ARMPageGetAddress’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c: In function ‘decodeARMMMUInvocation’: /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2818:45: error: ‘ARMASIDControlMakePool’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/src/arch/arm/32/kernel/vspace.c:2887:45: error: ‘ARMASIDPoolAssign’ undeclared (first use in this function) /home/daniel/Desktop/sel4test/kernel/Makefile:566: recipe for target 'kernel_final.s' failed make[1]: *** [kernel_final.s] Error 1 tools/common/project.mk:254: recipe for target 'kernel_elf' failed make: *** [kernel_elf] Error 2

2 2

seL4_Fault_t and friends seems to be missing in user libsel4
by Alexander Boettcher 15 Jun '17

15 Jun '17

Hello, if I compile and link seL4 5.2.0 ARCH=x86 PLAT=pc99 SEL4_ARCH=x86_64 make and I finally try to use the generated syscall/libsel4 headers, the compiler complains about missing seL4_Fault types and functions in libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/faults.h like seL4_Fault_t seL4_Fault_tag seL4_Fault_VMFault_new and a lot more. These structs and functions seems to be generated only for the kernel side, e.g. in kernel_final.c they show up, but there are no traces of them on the user level side. Do I just miss a configuration option ? Thanks, -- Alexander Boettcher Genode Labs http://www.genode-labs.com - http://www.genode.org Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth

2 4

[Camkes] Is there any way to declare hierarchical header files and does CamKES support C++ boost preprocessor?
by Tran Cuong 14 Jun '17

14 Jun '17

Hello everybody, I'm conducting a C-project, in which the code is utilizing boost library to define several macros. This source code is running well in Linux and using only standard C library (I had tested this libraries individually by some mini-programs on CamKES). My project is organized as follows: - Top folder: + "components" folder contains my c code + "include" folder contains 1 .h file boost1.h and 1 folder test ++ sub-folder "test" contains 1 file boost2.h ++ content of boost1.h is just include "test/boost2.h" + "Makefile" is declared as below: TARGETS := $(notdir ${SOURCE_DIR}).cdl ADL := tst-macro.camkes Client_CFILES := \ $(patsubst ${SOURCE_DIR}/%,%,$(wildcard ${SOURCE_DIR}/components/Client/src/*.c)) \ $(patsubst ${SOURCE_DIR}/%,%,$(wildcard ${SOURCE_DIR}/components/Client/src/plat/${PLAT}/*.c)) \ $(patsubst ${SOURCE_DIR}/%,%,$(wildcard ${SOURCE_DIR}/components/Client/src/arch/${ARCH}/*.c)) Client_ASMFILES := \ $(patsubst ${SOURCE_DIR}/%,%,$(wildcard ${SOURCE_DIR}/components/Client/crt/arch-${ARCH}/crt0.S)) \ $(patsubst ${SOURCE_DIR}/%,%,$(wildcard ${SOURCE_DIR}/components/Client/src/*.S)) \ $(patsubst ${SOURCE_DIR}/%,%,$(wildcard ${SOURCE_DIR}/components/Client/src/arch/${ARCH}/*.S)) \ $(patsubst ${SOURCE_DIR}/%,%,$(wildcard ${SOURCE_DIR}/components/Client/src/plat/${PLAT}/*.S)) Client_HFILES := \ $(patsubst ${SOURCE_DIR}/%,%,$(wildcard ${SOURCE_DIR}/components/Client/include/*)) include ${PWD}/tools/camkes/camkes.mk - This above Makefile, I imitated from another application, and when I compiled the project, there are some errors related to directory of "test/boost2.h". I suspect that there is something wrong with Client_HFILES declaration, since maybe it is only valid for a list of .h files, not for hierarchical folders. - I really want to dive into CamKES, but I only have a little knowledge about this. My project is due so I hope to get some positive advice from you for 2 questions: + The right way to declare multi-level libraries as in my example. + Besides, does CamKES support boost preprocessing lib. Currently I'm using the toolchain arm-none-eabi- Thank all of you for the time and attention. Dinh-Cuong -- ------------------- TRAN Dinh Cuong (Mr) Email : cuongtd4(a)gmail.com

2 2

Trustworthy and mixed critical
by Jonathan C Day 14 Jun '17

14 Jun '17

Dear all, The first of these terms has an... interesting history. In a nutshell, it's not always used appropriately. Clearly that's not going to be the case with SEL4, but what exactly is meant? Mixed critical is another term that I'm cautious over. It's not completely clear to me if the mixing refers to relaxed constraints for utilisation reasons or something else. (Correct me if I'm mistaken, but I don't think SEL4 implements FLASK, which would be the obvious way to provide differing constraints, relaxed constraints within the trusted computing model. It's totally the wrong level.) I have absolutely no doubt SEL4 will retain all the provable integrity ever claimed (by anyone involved), but this experimental-proto-main branch confuses me on what fundamentally changes. Jonathan Day

2 1

Compilation of seL4 kernel 5.2.0
by Alexander Boettcher 14 Jun '17

14 Jun '17

Hello, I want to compile just the seL4 kernel (5.2.0) and tried it by invoking: alex@max:~/sel4.git$ ARCH=x86 PLAT=pc99 SEL4_ARCH=ia32 make but the compile fails (attached below). Do I need to setup/configure something beforehand ? It seems some defines are not set. The host is a 64bit Ubuntu 16.04 LTS. Thanks, Alex. alex@max:~/sel4.git$ git log commit 3695232f9603af60d56f97072082d90f30e98b0e Author: Kent McLeod <Kent.Mcleod(a)data61.csiro.au> Date: Wed May 31 17:21:29 2017 +1000 update VERSION file to 5.2.0 alex@max:~/sel4.git$ ARCH=x86 PLAT=pc99 SEL4_ARCH=ia32 make [MKDIR] arch/object [PBF_GEN] arch/object/structures.pbf [PBF_GEN] plat/32/plat_mode/machine/hardware.pbf [PBF_GEN] 32/mode/api/shared_types.pbf [BF_GEN] arch/object/structures_gen.h [BF_GEN] plat/32/plat_mode/machine/hardware_gen.h [BF_GEN] 32/mode/api/shared_types_gen.h [CPP] src/arch/x86/32/machine_asm.s_pp [AS] src/arch/x86/32/machine_asm.o [CPP] src/arch/x86/32/traps.s_pp [AS] src/arch/x86/32/traps.o [CPP] src/arch/x86/32/head.s_pp [AS] src/arch/x86/32/head.o [CPP] src/arch/x86/multiboot.s_pp [AS] src/arch/x86/multiboot.o [TOUCH] sources_list_updated [CPP_GEN] kernel_all.c [CPP] kernel_all.c_pp In file included from ./include/arch/x86/arch/fastpath/fastpath.h:14:0, from src/arch/x86/32/c_traps.c:15: ./include/arch/x86/arch/32/mode/fastpath/fastpath.h:137:2: error: #error "Invalid method to set IPCBUF/TLS" #error "Invalid method to set IPCBUF/TLS" ^ ./include/arch/x86/arch/32/mode/fastpath/fastpath.h:168:2: error: #error "Invalid method to set IPCBUF/TLS" #error "Invalid method to set IPCBUF/TLS" ^ src/arch/x86/32/c_traps.c:198:2: error: #error "Invalid method to set IPCBUF/TLS" #error "Invalid method to set IPCBUF/TLS" ^ src/arch/x86/32/c_traps.c:238:2: error: #error "Invalid method to set IPCBUF/TLS" #error "Invalid method to set IPCBUF/TLS" ^ Makefile:729: recipe for target 'kernel_all.c_pp' failed make: *** [kernel_all.c_pp] Error 1 rm plat/32/plat_mode/machine/hardware_gen.h 32/mode/api/shared_types_gen.h src/arch/x86/32/machine_asm.s_pp src/arch/x86/32/traps.s_pp src/arch/x86/multiboot.s_pp arch/object/structures_gen.h src/arch/x86/32/head.s_pp -- Alexander Boettcher Genode Labs http://www.genode-labs.com - http://www.genode.org Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth

2 2

seL4-test on Beaglebone black
by Fabrizio Bertocci 14 Jun '17

14 Jun '17

Hi, I am posting this email as reference to anyone who want/need to run seL4 on a BeagleBone Black (BBB). The post at https://wiki.sel4.systems/Hardware/Beaglebone is great, unfortunately even if I followed exactly those instructions, I ended up hitting some walls here and there. I eventually managed to solve those issues and run successfully seL4test on my BBB. First of all the build system. I have tried unsuccessfully to find arm-linux-eabi for CentOS 7 (my preferred distribution for building on Linux), but apparently is an easy-to-find only on Ubuntu... so I ended up creating a VM with Ubuntu 16.04. If someone knows how to get arm-linux-eabi on CentOS please let me know... Unfortunately even with Ubuntu not everything went as smooth as I hoped. It appears that Python "past" module is no longer available for 16.04, so build fails on kernel/tools/lex.py. According to the comment right before the failing import statement, it appears this module is just declared but not used, so commenting it out (or removing it entirely) would fix this issue: #from past.builtins import cmp One more issue: when using either one of the following configurations as start point: - bamboo_bbone_black_debug_xml_defconfig - bbone_black_debug_xml_defconfig The build system will end up producing a binary image and not an ELF image. Producing an ELF image can be more useful if you want to use objdump to get a disassembly (for debugging later). So I changed the configuration with: make menuconfig Navigate to: Tools -> Build elfloader -> Boot image type and select "ELF Boot Image" instead of "Binary Boot Image" Save your configuration then build: make Now manually convert the produced ELF image in a binary: arm-linux-gnueabi-objcopy --output-target binary images/sel4test-driver-image-arm-am335x sel4test.bin then copy the file 'sel4test.bin' onto the SD card formatted as FAT32 Now, in my BBB (rev A5A) if I try to follow the instructions from the wiki page previously mentioned, I get a crash right away (illegal instruction). The problem is that in my BBB the uBoot environment variable ${loadaddr} is set to 0x80200000 and not 0x82000000 (the start address of the produced image). BBB have RAM mapped from address 0x80000000 to 0x9FFFFFFF (512Mb), so running from 0x82000000 is ok. So to load and run, use instead: fatload mmc 0 0x82000000 sel4test.bin go 0x82000000 That's it. Test should load and run successfully: Test suite passed. 220 tests passed. 220/220 tests passed. All is well in the universe. Hope this help saving some time... Regards, Fabrizio

1 0

Important note for CAmkES users
by Stephen.Sherratt＠data61.csiro.au 13 Jun '17

13 Jun '17

We've just released CAmkES 3.0.0 (release notes<https://wiki.sel4.systems/CAmkES%203.0.0>), and with it, all changes staged on our development branch, CAmkES Next, have been merged into the "master" branch of the camkes-tool repo (https://github.com/seL4/camkes-tool). We'll be continuing to develop CAmkES on its "master" branch, and cease making new commits to the "next" branch. # What this means for you As CAmkES 3.0.0 is incompatible with older versions of CAmkES, any projects tracking the master branch of camkes-tool will probably not build after this change. Also, as all new development is now being done on the master branch, any projects tracking the next branch of camkes-tool will no longer receive updates. If you're in either category, you'll need to update your project's repo manifest. # Migration Instructions If your project tracks either the "master", or "next" branch of the camkes-tool, you'll need to update your project's manifest. To check if this applies to you, look in your projects repo manifest xml file (typically in .repo/manifest.xml at the top level of your project) for the line: <project name="camkes-tool.git" path="tools/camkes"> (this implicitly tracks "master") OR <project name="camkes-tool.git" path="tools/camkes" revision="master"> OR <project name="camkes-tool.git" path="tools/camkes" revision="next"> If your manifest has either of those lines, take a look at the migration guide in the CAmkES 3.0.0 release notes: https://wiki.sel4.systems/CAmkES%203.0.0#Migrating It covers a range of different scenarios and explains how to change your manifest so your project will continue to work. If the camkes-tool revision in your manifest specifies a particular version of CAmkES (e.g. 'revision="camkes-2.3.1"'), you don't need to migrate.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel June 2017