Devel May 2019

devel@sel4.systems

15 participants
13 discussions

Possible newbie question: What are ".bf"-files belonging to the seL4 code base?
by Mike Epoch 15 May '19

15 May '19

Hi! I am new to this list so please forgive me if this question has been asked before. The seL4 code base contains a slew of files with a file type of "bf". These files seem to define packed structs that are to fit into words or d-words. An example of that would be file kernel/libsel4/mode_include/64/sel4/shared_types.bf which can be obtained (as part of an entire source tree, of course) via repo init -u https://github.com/seL4/sel4test-manifest.git followed by repo sync. What I find curious is that these files do not adhere to (common) C syntax yet they are fed into GCC and GCC swallows them. This file format appears to be an extension to GCC. I could not find any documentation on any such extension. I would be grateful if anyone could point me to some kind of documentation pertaining to it. Regards Mike

3 5

Using ARM GIC Virtualization Extensions with seL4
by dan pittman 10 May '19

10 May '19

Hi all! I'm currently trying to understand something about the use of the virtualization extensions available in the PL-400 interrupt controller in seL4. It all starts with this sentence: > The hypervisor supports virtualization also by using address translation tables to trap accesses that the virtual machines make to the virtual distributor. The hypervisor determines the effect of these accesses and might typically update the virtual interface control registers as a result. Source: http://infocenter.arm.com/help/index.jsp?topic=/com.arm.doc.ddi0471b/CHDIHI… My interpretation of this is that by using the IPA which is available with arm hyp, the hardware can trap accesses to the GIC from the guest and "redirect" those accesses to the physical GIC. From this, I draw the conclusion that the need for a completely virtualized GIC when using these extensions is not necessary. However, in seL4—due to the way in which it manages interrupts by handling the hardware interactions itself and instead invoking an endpoint—the use of these extensions in this way is not possible. I'm curious if this understanding is correct, and if not, I welcome any clarity y'all can provide! cheers, dan

2 1

BeagleBone and CAmkES app picoserver
by KAP Benjamin 06 May '19

06 May '19

Hello I am trying to compile the CAmkES app picoserver for the BeagleBone Black but I do encounter some errors which I cannot manage to solve. Steps: - I repo synced the latest camkes-manifest which was added support for the BeagleBone - added am335x implementations to the Ethdriver global-component - created subfolder and issued ../init-build.sh -DPLATFORM=am335x -DSIMULATION=0 -DAARCH32=1 -DCAMKES_APP=picoserver - ninja Errors: [1/48] Building C object projects/util_libs/libethdrivers/CMakeFiles/ethdrivers.dir/src/plat/am335x/cpsw/cpswif.c.obj FAILED: projects/util_libs/libethdrivers/CMakeFiles/ethdrivers.dir/src/plat/am335x/cpsw/cpswif.c.obj ccache /usr/bin/arm-linux-gnueabi-gcc --sysroot=/host/PICO -DHAVE_AUTOCONF -I../projects/util_libs/libethdrivers/src/plat/am335x/cpsw -I../projects/util_libs/libethdrivers/include -I../projects/util_libs/libethdrivers/plat_include/am335x -I../projects/util_libs/libethdrivers/arch_include/arm -Iautoconf -Ikernel/gen_config -Ielfloader-tool/gen_config -Ilibsel4/gen_config -Iprojects/camkes-tool/libsel4camkes/gen_config -Iprojects/capdl/capdl-loader-app/gen_config -Iprojects/projects_libs/libusbdrivers/gen_config -Iprojects/rumprun/gen_config -Iprojects/seL4_libs/libsel4vka/gen_config -Iprojects/seL4_libs/libsel4utils/gen_config -Iprojects/seL4_libs/libsel4platsupport/gen_config -Iprojects/seL4_libs/libsel4serialserver/gen_config -Iprojects/seL4_libs/libsel4debug/gen_config -Iprojects/seL4_libs/libsel4test/gen_config -Iprojects/seL4_libs/libsel4muslcsys/gen_config -Iprojects/seL4_libs/libsel4vmm/gen_config -Iprojects/seL4_projects_libs/libsel4arm-vmm/gen_config -Iprojects/util_libs/libutils/gen_config -Iprojects/util_libs/libplatsupport/gen_config -Iprojects/util_libs/libethdrivers/gen_config -Iprojects/util_libs/libpicotcp/gen_config -Iprojects/musllibc/build-temp/stage/include -I../projects/util_libs/libplatsupport/include -I../projects/util_libs/libplatsupport/plat_include/am335x -I../projects/util_libs/libplatsupport/arch_include/arm -I../projects/util_libs/libutils/include -I../projects/util_libs/libutils/arch_include/arm -Iprojects/util_libs/libpicotcp/picotcp_external/picotcp/build/include -march=armv7-a -marm -D__KERNEL_32__ -g -nostdinc -fno-pic -fno-pie -fno-stack-protector -fno-asynchronous-unwind-tables -ftls-model=local-exec -mfloat-abi=softfp -std=gnu11 -MD -MT projects/util_libs/libethdrivers/CMakeFiles/ethdrivers.dir/src/plat/am335x/cpsw/cpswif.c.obj -MF projects/util_libs/libethdrivers/CMakeFiles/ethdrivers.dir/src/plat/am335x/cpsw/cpswif.c.obj.d -o projects/util_libs/libethdrivers/CMakeFiles/ethdrivers.dir/src/plat/am335x/cpsw/cpswif.c.obj -c ../projects/util_libs/libethdrivers/src/plat/am335x/cpsw/cpswif.c In file included from ../projects/util_libs/libethdrivers/src/plat/am335x/cpsw/cpswif.c:47:0: ../projects/util_libs/libethdrivers/src/plat/am335x/cpsw/../lwiplib.h:46:22: fatal error: lwip/opt.h: No such file or directory #include <lwip/opt.h> ^ compilation terminated. [2/48] Performing build step for 'parse_capdl_tool' make: Nothing to be done for 'all'. [3/48] Building C object projects/util_libs/libethdrivers/CMakeFiles/ethdrivers.dir/src/plat/am335x/beaglebone.c.obj FAILED: projects/util_libs/libethdrivers/CMakeFiles/ethdrivers.dir/src/plat/am335x/beaglebone.c.obj ccache /usr/bin/arm-linux-gnueabi-gcc --sysroot=/host/PICO -DHAVE_AUTOCONF -I../projects/util_libs/libethdrivers/src/plat/am335x/cpsw -I../projects/util_libs/libethdrivers/include -I../projects/util_libs/libethdrivers/plat_include/am335x -I../projects/util_libs/libethdrivers/arch_include/arm -Iautoconf -Ikernel/gen_config -Ielfloader-tool/gen_config -Ilibsel4/gen_config -Iprojects/camkes-tool/libsel4camkes/gen_config -Iprojects/capdl/capdl-loader-app/gen_config -Iprojects/projects_libs/libusbdrivers/gen_config -Iprojects/rumprun/gen_config -Iprojects/seL4_libs/libsel4vka/gen_config -Iprojects/seL4_libs/libsel4utils/gen_config -Iprojects/seL4_libs/libsel4platsupport/gen_config -Iprojects/seL4_libs/libsel4serialserver/gen_config -Iprojects/seL4_libs/libsel4debug/gen_config -Iprojects/seL4_libs/libsel4test/gen_config -Iprojects/seL4_libs/libsel4muslcsys/gen_config -Iprojects/seL4_libs/libsel4vmm/gen_config -Iprojects/seL4_projects_libs/libsel4arm-vmm/gen_config -Iprojects/util_libs/libutils/gen_config -Iprojects/util_libs/libplatsupport/gen_config -Iprojects/util_libs/libethdrivers/gen_config -Iprojects/util_libs/libpicotcp/gen_config -Iprojects/musllibc/build-temp/stage/include -I../projects/util_libs/libplatsupport/include -I../projects/util_libs/libplatsupport/plat_include/am335x -I../projects/util_libs/libplatsupport/arch_include/arm -I../projects/util_libs/libutils/include -I../projects/util_libs/libutils/arch_include/arm -Iprojects/util_libs/libpicotcp/picotcp_external/picotcp/build/include -march=armv7-a -marm -D__KERNEL_32__ -g -nostdinc -fno-pic -fno-pie -fno-stack-protector -fno-asynchronous-unwind-tables -ftls-model=local-exec -mfloat-abi=softfp -std=gnu11 -MD -MT projects/util_libs/libethdrivers/CMakeFiles/ethdrivers.dir/src/plat/am335x/beaglebone.c.obj -MF projects/util_libs/libethdrivers/CMakeFiles/ethdrivers.dir/src/plat/am335x/beaglebone.c.obj.d -o projects/util_libs/libethdrivers/CMakeFiles/ethdrivers.dir/src/plat/am335x/beaglebone.c.obj -c ../projects/util_libs/libethdrivers/src/plat/am335x/beaglebone.c ../projects/util_libs/libethdrivers/src/plat/am335x/beaglebone.c:17:24: fatal error: lwip/netif.h: No such file or directory #include <lwip/netif.h> ^ compilation terminated. ninja: build stopped: subcommand failed. Any help is very much appreciated. Best regards, Benjamin P.S. The file projects/util_libs/libplatsupport/plat_include/am335x/platsupport/plat/timer.h contains the static UNUSED timer_properties_t dmt_properties which caused errors on compilation too. (I deleted the lines since they arent used anyways)

2 1

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel May 2019