- Devel - lists.sel4.systems

Network Stack and Driver
by Norrathep Rattanavipanon 31 Mar '16

31 Mar '16

Hello, My name is Oak and I'm working with Prof. Gene Tsudik for remote attestation project using sel4. I know that you guys are not interested in developing network stack and drivers for sel4. But do you happen to know if anyone else has done some work with network stack and Wi-fi, Bluetooth or ethernet driver in sel4? Regards, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 1

答复:答复: 答复:Re: About the execution time of seL4 API
by xurongfeik 30 Mar '16

30 Mar '16

裴老师：您好！谢谢您的资料。现在我们学校有两个团队在做这方面的工作：其中我们实验室主要在模型层对seL4微内核进行建模仿真，主要是把微内核基本功能机制建模成为一个基本模型，对User Mode扩展部分以策略模型的方式与基本模型进行编织，从而建立一套在设计早期通过模型仿真验证策略的方法。目前，我们正着手建立一个能准确反映真实seL4微内核运行的模型，但是由于仿真时钟的不准确，我们希望在某一硬件环境上把seL4微内核模型下层的系统调用时间统计出来，通过时间累加计算seL4微内核模型上的应用执行过程。但是目前不知道该如何获取这些系统调用的执行时间，不知道裴老师您那边是否有相关的数据？另外一个团队主要是基于seL4微内核的操作系统开发，主要考虑分区、并发的不确定性。目前主要用于航天的应用中。如果裴老师有相关的研究，非常愿意共同合作！祝好！许荣飞在 2016-03-29 14:39:35，"XilongPei" <pei.xilong(a)kortide.com> 写道： XuRongfei: 我是同济大学电信学院老师裴喜龙，我们从事你说的这个方向好几年了。附件文件是我把seL4的说明书翻译成了中文，下面这个链接是我们做的高可用操作系统的项目工程页面。 http://elastos.org/redmine/projects/rt-elastos这个工程的源码在： https://github.com/elastos/HD-Elastos 我们基于AOP思想做的操作系统（正在开发中），官网：http://elastos.org/project-guide/ 源码开源在github: https://github.com/elastos/ElastosRDK5_0它基于AOP思想，提出一种构件技术CAR，并基于这个构件技术，实现了一… 希望国内做相关工作的人能合作，共同做一些大的工程。同济大学裴喜龙 2016年3月29日星期二发件人: Devel [mailto:devel-bounces@sel4.systems] 代表 xurongfeik 发送时间: 2016年3月29日 14:11 收件人: Thomas Sewell <thomas.sewell(a)nicta.com.au> 抄送:devel@sel4.systems 主题: [seL4] 答复:Re: About the execution time of seL4 API Thank you for your reply！ My name is XuRongfei, and I am a PHD student from China,Beijing. Now I focus on RTOS Modeling and Simulation. As we know, an important principle of microkernel design is the separation of mechanism and policy, it is what enables the construction of arbitrary systems on top of a minimal kernel. This separation of mechanism and policy is similar to AOM(Aspect-Oriented Modeling) and we can model the mechanism and policy separately. The biggest advantage is that analysis and verification of the policy applied in the implementation phase will be advanced to the design stage. As seL4 Microkernel is "the world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement". So if we want to construct an RTOS on top of seL4 Microkernel, it is necessary to simulate and analyse the policy model on the microkernel model first. To simulate the seL4 Microkernel model accurately and agree with the real situation, the execution time of seL4 typical API (such as send\receive\notify message and Resume\Suspend\Create thread) for certain platform. So how can we get the execution time of this APIs for certain platform? Is it possible? Thank you very much! At 2016-03-29 11:45:42, "Thomas Sewell" <thomas.sewell(a)nicta.com.au> wrote: Hmm, what do you mean by measuring the time? You can measure the typical execution time of various system calls easily enough by checking the CPU cycle counter. There is an internal "sel4bench" project which is similar to "sel4test" but measures timing information of some system calls. My understanding is that this will be released at some point in the near future. It's also possible to calculate the worst-case execution time of the kernel for some platforms. There's been a lot of research work on this http://ssrg.nicta.com.au/projects/TS/realtime.pml by various people at Data61/NICTA. It's probably possible to replicate for some platform of interest, but it might be quite difficult to do. Cheers, Thomas. On 29/03/16 14:06, xurongfeik wrote: Hello，everyone： When given a specific platform， is it possible to measure the execution time of seL4 API？ Anyone who has the relative data please send it to me， many thanks！！ -- 许荣飞 Rongfei Xu 北京航空航天大学 Beihang University _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

2 1

About the execution time of seL4 API
by xurongfeik 30 Mar '16

30 Mar '16

Hello，everyone： When given a specific platform， is it possible to measure the execution time of seL4 API？ Anyone who has the relative data please send it to me， many thanks！！ -- 许荣飞 Rongfei Xu 北京航空航天大学 Beihang University

3 4

Where can I get the information about Linux on seL4
by XilongPei 29 Mar '16

29 Mar '16

Hi Gernot, I found that the footer of http://ssrg.nicta.com.au/ is: Served by Apache on Linux on seL4 Whare can I get more information about Linux on seL4? Xilong Pei Tongji University 2016/3/29

2 1

Status of ARMv8 support for seL4 ?
by karim.allah.ahmed＠gmail.com 29 Mar '16

29 Mar '16

Hello, >From this roadmap [0], I can see that ARMv8 support is underway at the moment. Is this something that's going to be released soon given that the roadmap says Q1-2016 (at least 32-bit) ? [0] https://sel4.systems/Info/Roadmap -- Karim Allah Ahmed.

1 0

Porting Qubes OS to seL4 project
by Paul Vlase 28 Mar '16

28 Mar '16

No answer ... Am I doing something wrong? Beside not have patience. Could anyone tell about the status of the seL4 Qubes port project and who can I get in touch with to talk more about it? On Tue, Mar 22, 2016 at 11:35 PM, Paul Vlase <vlase.paul(a)gmail.com> wrote: > Hello, > > My name is Paul Vlase and I am following a master degree right now. I > am interested in porting the Qubes OS to seL4 project and I saw that > you are working already on it. Is there anything I can help you on > this project? > > Thank you, > Paul Vlase

2 1

sel4 in TrustZone
by Norrathep Rattanavipanon 27 Mar '16

27 Mar '16

Hi again :) Is it possible to run sel4 as a secure world OS in TrustZone? Has anyone successfully done that before? Thank you, -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

6 6

(simple?) build error?
by 谢文龙 27 Mar '16

27 Mar '16

I'm getting an error when building from Ubuntu. I'm building from: repo init -u https://github.com/seL4/sel4test-manifest.git I've configured with: make ia32_simulation_release_xml_defconfig and done "make menuconfig" accepting the defaults. Finally I run make and get errors: [KERNEL] [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/x86/32/machine_asm.s [AS] src/arch/x86/32/machine_asm.o [CPP] src/arch/x86/32/traps.s [AS] src/arch/x86/32/traps.o [CPP] src/arch/x86/32/head.s [AS] src/arch/x86/32/head.o [CPP] src/arch/x86/halt.s [AS] src/arch/x86/halt.o [CPP] src/arch/x86/idle.s [AS] src/arch/x86/idle.o [TOUCH] sources_list_updated [CPP_GEN] kernel_all.c [CPP] kernel_all.c_pp [CP] kernel_final.c [CC] kernel_final.s [AS] kernel.o [LD] kernel.elf /usr/bin/ld:linker.lds_pp:5: syntax error collect2: error: ld returned 1 exit status make[1]: *** [kernel.elf] Error 1 make: *** [kernel_elf] Error 2 make V=3 mkdir -p /home/talos/seL4test/stage/x86/pc99 mkdir -p /home/talos/seL4test/build/x86/pc99 mkdir -p /home/talos/seL4test/images mkdir -p /home/talos/seL4test/stage/x86/pc99/common cp -R /home/talos/seL4test/tools/common/* /home/talos/seL4test/stage/x86/pc99/common [libs/libsel4] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4 CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4 -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4 SOURCE_DIR=/home/talos/seL4test/libs/libsel4 V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4' [GEN] include/sel4/types_gen.h [GEN] arch_include/x86/sel4/arch/invocation.h [GEN] include/sel4/shared_types_gen.h [GEN] sel4_arch_include/ia32/sel4/sel4_arch/invocation.h [HEADERS] [STAGE] api/* [STAGE] interfaces/* [STAGE] sel4/* [STAGE] interfaces/* [STAGE] sel4/* [STAGE] interfaces/* [STAGE] sel4/* [STAGE] sel4/* [STAGE] interfaces/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4' [libs/libsel4] done. [libs/libmuslc] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libmuslc CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libmuslc -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libmuslc/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libmuslc SOURCE_DIR=/home/talos/seL4test/libs/libmuslc V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libmuslc' make[1]: Nothing to be done for `default'. make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libmuslc' [libs/libmuslc] done. [libs/libcpio] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libcpio CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libcpio -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libcpio/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libcpio SOURCE_DIR=/home/talos/seL4test/libs/libcpio V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libcpio' [HEADERS] [STAGE] cpio/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libcpio' [libs/libcpio] done. [libs/libutils] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libutils CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libutils -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libutils/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libutils SOURCE_DIR=/home/talos/seL4test/libs/libutils V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libutils' [HEADERS] [STAGE] utils/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libutils' [libs/libutils] done. [libs/libsel4vka] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4vka CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4vka -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4vka/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4vka SOURCE_DIR=/home/talos/seL4test/libs/libsel4vka V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4vka' [HEADERS] [STAGE] vka/* [STAGE] vka/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4vka' [libs/libsel4vka] done. [libs/libsel4vspace] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4vspace CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4vspace -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4vspace/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4vspace SOURCE_DIR=/home/talos/seL4test/libs/libsel4vspace V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4vspace' [HEADERS] [STAGE] vspace/* [STAGE] vspace/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4vspace' [libs/libsel4vspace] done. [libs/libplatsupport] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libplatsupport CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libplatsupport -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libplatsupport/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libplatsupport SOURCE_DIR=/home/talos/seL4test/libs/libplatsupport V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libplatsupport' [HEADERS] [STAGE] platsupport/* [STAGE] platsupport/* [STAGE] platsupport/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libplatsupport' [libs/libplatsupport] done. [libs/libsel4simple] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4simple CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4simple -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4simple/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4simple SOURCE_DIR=/home/talos/seL4test/libs/libsel4simple V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4simple' [HEADERS] [STAGE] simple/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4simple' [libs/libsel4simple] done. [libs/libsel4simple-default] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4simple-default CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4simple-default -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4simple-default/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4simple-default SOURCE_DIR=/home/talos/seL4test/libs/libsel4simple-default V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4simple-default' [HEADERS] [STAGE] simple-default/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4simple-default' [libs/libsel4simple-default] done. [libs/libsel4platsupport] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4platsupport CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4platsupport -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4platsupport/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4platsupport SOURCE_DIR=/home/talos/seL4test/libs/libsel4platsupport V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4platsupport' [HEADERS] [STAGE] sel4platsupport/* [STAGE] sel4platsupport/* [STAGE] sel4platsupport/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4platsupport' [libs/libsel4platsupport] done. [libs/libelf] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libelf CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libelf -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libelf/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libelf SOURCE_DIR=/home/talos/seL4test/libs/libelf V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libelf' [HEADERS] [STAGE] elf/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libelf' [libs/libelf] done. [libs/libsel4utils] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4utils CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4utils -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4utils/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4utils SOURCE_DIR=/home/talos/seL4test/libs/libsel4utils V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4utils' [HEADERS] [STAGE] sel4utils/* [STAGE] sel4utils/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4utils' [libs/libsel4utils] done. [libs/libsel4muslcsys] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4muslcsys CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4muslcsys -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4muslcsys/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4muslcsys SOURCE_DIR=/home/talos/seL4test/libs/libsel4muslcsys V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4muslcsys' [HEADERS] [STAGE] arch_stdio.h [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4muslcsys' [libs/libsel4muslcsys] done. [libs/libsel4allocman] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4allocman CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4allocman -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4allocman/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4allocman SOURCE_DIR=/home/talos/seL4test/libs/libsel4allocman V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4allocman' [HEADERS] [STAGE] allocman/* [STAGE] allocman/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4allocman' [libs/libsel4allocman] done. [libs/libsel4test] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4test CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4test -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4test/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4test SOURCE_DIR=/home/talos/seL4test/libs/libsel4test V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4test' [HEADERS] [STAGE] sel4test/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4test' [libs/libsel4test] done. [apps/sel4test-tests] building... mkdir -p /home/talos/seL4test/build/x86/pc99/sel4test-tests CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/sel4test-tests -f /home/talos/seL4test/.config -f /home/talos/seL4test/apps/sel4test-tests/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/sel4test-tests SOURCE_DIR=/home/talos/seL4test/apps/sel4test-tests V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/sel4test-tests' [HEADERS] [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/sel4test-tests' [apps/sel4test-tests] done. [KERNEL] mkdir -p /home/talos/seL4test/build/kernel make -C /home/talos/seL4test/build/kernel -f /home/talos/seL4test/kernel/Makefile \ SOURCE_ROOT=/home/talos/seL4test/kernel O=/home/talos/seL4test/build/kernel V=3 \ TOOLPREFIX= \ CONFIG_DOMAIN_SCHEDULE= \ HAVE_AUTOCONF=1 NO_PRESERVE_TIMESTAMP=1 seL4 build options: =================== ARCH = x86 PLAT = pc99 CPU = TOOLPREFIX = PATH = /home/talos/bin:/home/talos/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games DEBUG = ASSERT = CONFIG_DEFS = CYCLE_COUNTER PERF_COUNTER=CYCLE_COUNTER DANGEROUS_CODE_INJECTION = CC = gcc CC_PATH = CPP = cpp CPP_PATH = AS = as AS_PATH = LD = ld LD_PATH = PARSER = c-parser PARSER_PATH = BF_GEN = bitfield_gen.py BF_GEN_PATH = SYSCALL_ID_GEN = syscall_header_gen.py SYSCALL_ID_GEN_PATH = INVOCATION_ID_GEN = invocation_header_gen.py INVOCATION_ID_GEN_PATH = XMLLINT_PATH = XMLLINT = xmllint.sh CFLAGS = -fno-stack-protector -m32 --std=c99 -nostdlib -nostdinc -ffreestanding -Wall -Werror -Wstrict-prototypes -Wmissing-prototypes -Wnested-externs -Wmissing-declarations -Wundef -Wpointer-arith -Wno-nonnull -Wdeclaration-after-statement "-I/home/talos/seL4test/kernel/include/arch/x86/arch/32" "-I/home/talos/seL4test/kernel/include/plat/pc99/plat/32" -O2 -mno-mmx -mno-sse -mno-sse2 -mno-3dnow -DCYCLE_COUNTER -DPERF_COUNTER=CYCLE_COUNTER -DFASTPATH ASFLAGS = -Wa,--32 "-I/home/talos/seL4test/kernel/include/arch/x86/arch/32" "-I/home/talos/seL4test/kernel/include/plat/pc99/plat/32" CPPFLAGS = -DHAVE_AUTOCONF -I/home/talos/seL4test/include/generated -DARCH_X86 -DIA32 -DARCH_IA32 -D__KERNEL_32__ -DX86_32 -DPLAT_PC99 -DFASTPATH -DCYCLE_COUNTER -DPERF_COUNTER=CYCLE_COUNTER -DFASTPATH "-I/home/talos/seL4test/kernel/include/arch/x86/arch/32" "-I/home/talos/seL4test/kernel/include/plat/pc99/plat/32" LDFLAGS = -Wl,--build-id=none -Wl,-m,elf_i386 -nostdlib -nostdinc -Wl,--build-id=none -O2 make[1]: Entering directory `/home/talos/seL4test/build/kernel' [LD] kernel.elf /home/talos/seL4test/kernel/tools/changed.sh kernel.elf gcc -Wl,--build-id=none -Wl,-m,elf_i386 -nostdlib -nostdinc -Wl,--build-id=none -O2 -Wl,-T -Wl,linker.lds_pp \ -o kernel.elf src/arch/x86/32/machine_asm.o src/arch/x86/32/traps.o src/arch/x86/32/head.o src/arch/x86/halt.o src/arch/x86/idle.o kernel.o /usr/bin/ld:linker.lds_pp:5: syntax error collect2: error: ld returned 1 exit status make[1]: *** [kernel.elf] Error 1 make[1]: Leaving directory `/home/talos/seL4test/build/kernel' make: *** [kernel_elf] Error 2

2 1

sel4 benchmark
by Norrathep Rattanavipanon 25 Mar '16

25 Mar '16

Hello, What's the best way to benchmark my program inside sel4? I saw wiki page about running sel4 bench (https://wiki.sel4.systems/Benchmarking%20guide) but it wasnt filled yet. So I wonder if there's any public guide or tutorial on that? I also found this https://github.com/seL4/libplatsupport/blob/master/arch_include/x86/platsup… and tried both rdtsc_pure and rdtsc_cpuid but neither of them seems to produce reliable results. Best, -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 1

sel4 job offer
by Julien Delange 24 Mar '16

24 Mar '16

For information, we are looking for people to work on sel4. See https://www.appone.com/maininforeq.asp?Ad=250944&R_ID=1243309&Refer=http://… If you have any question, do not hesitate to contact me and/or apply! Julien.

1 0