Devel

devel@sel4.systems

8 participants
1389 discussions

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

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

23 Mar '16

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

1 0

[CAmkES] CAmkES 2.1.0 Release Notes
by Stephen Sherratt 22 Mar '16

22 Mar '16

CAmkES 2.1.0 Release Notes ========================== ## New Features - runner takes an `--architecture` command line argument which selects the target architecture. Valid arguments are: aarch32, arm_hyp, ia32 - added the ability to specify a hardware dataport as cached. Previously all hardware dataports were mapped uncached. This feature is intended to be used on dataports backed by DMA-able memory to improve access times. Functions to flush dataports from the cache are also provided. - support for seL4 3.0.0 ## Removed Features - `--hyp` command line argument is replaced with `--architecture arm_hyp` ## API Removals ### Unmarshalling Helpers These were intended for use in templates, but are no longer used in any internal templates: - `camkes_marshal` - `camkes_marshal_string` - `camkes_unmarshal` - `camkes_unmarshal_string` ### DMA Utilities These had been deprecated for a long period and are now being removed: - `camkes_dma_page_alloc` - `camkes_dma_page_free` You can find it at: https://github.com/seL4/camkes-tool/tree/camkes-2.1.0 A manifest for the 2.1.0 compatible versions of test and example apps: https://github.com/seL4/camkes-manifest/blob/master/default-2.1.x.xml Release notes on the wiki: https://wiki.sel4.systems/CAmkES%202.1.0 Enjoy! ________________________________ 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.

1 0

What happens to the IPC buffer when you make another process within the same Vspace?
by Qiwei Wen 20 Mar '16

20 Mar '16

Hi, I'm trying to write a multithreaded seL4 application. It's to be made up of sel4util processes with different cspaces and sharing the same Vspace. I managed to achieve this, but what confuses me is that since the processes share the same Vspace, wouldn't GetIPCBuffer() return the same result for each of them? I looked at libsel4/arch_include/arm/sel4/arch/functions.h, and GetIPCBuffer() is simply: return *(seL4_IPCBuffer**)seL4_GlobalsFrame; Since seL4_GlobalsFrame is just a fixed memory location (0xffffc000) in the shared address space, why does seL4_GetIPCBuffer() return different results for different processes? Below is the output: ========================== PARENT: IPCBUFFER: 00273000 CHILD: GlobalsFrame: ffffc000, *GlobalsFrame 10076000 CHILD: setting shared to 97 PARENT: CHILD DIED, shared char: 97, MR16: 00000000 ============================= Is it that the frame ffffc000 mapping is changed on every context switch perhaps? Can I absolutely trust that IPC is still working correctly with this set up? Thanks, David

5 4

Jump to page:

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel