August 2018 - Devel - lists.sel4.systems

building sel4test for zynqmp platform
by Leonid Meyerovich 27 Aug '18

27 Aug '18

Hello, I have tried to build sel4test following 'running SEL4' instruction. It was successful for x86 platform, but when I try to build it for 'zyncmp' I've got an error: gcc: error: unrecognized command line option '-marm'; did you mean '-mabm'? gcc: error: unrecognized command line option '-mfloat-abi=soft' Thank you, Leonid -- Build files have been written to: /home/lm/sel4test/build-zynqmp lm@u-18:~/sel4test/build-zynqmp$ ninja [2/235] Generating linker.lds_pp FAILED: elfloader-tool/linker.lds_pp cd /home/lm/sel4test/build-zynqmp/elfloader-tool && /usr/bin/gcc -march=armv8-a -marm -D__KERNEL_32__ -I/home/lm/sel4test/build-zynqmp/autoconf -I/home/lm/sel4test/build-zynqmp/kernel/gen_config -I/home/lm/sel4test/build-zynqmp/elfloader-tool/gen_config -I/home/lm/sel4test/build-zynqmp/libsel4/gen_config -I/home/lm/sel4test/build-zynqmp/projects/seL4_libs/libsel4vka/gen_config -I/home/lm/sel4test/build-zynqmp/projects/seL4_libs/libsel4utils/gen_config -I/home/lm/sel4test/build-zynqmp/projects/seL4_libs/libsel4platsupport/gen_config -I/home/lm/sel4test/build-zynqmp/projects/seL4_libs/libsel4serialserver/gen_config -I/home/lm/sel4test/build-zynqmp/projects/seL4_libs/libsel4debug/gen_config -I/home/lm/sel4test/build-zynqmp/projects/seL4_libs/libsel4test/gen_config -I/home/lm/sel4test/build-zynqmp/projects/seL4_libs/libsel4muslcsys/gen_config -I/home/lm/sel4test/build-zynqmp/projects/seL4_libs/libsel4vmm/gen_config -I/home/lm/sel4test/build-zynqmp/projects/sel4test/apps/sel4test-driver/gen_config -I/home/lm/sel4test/build-zynqmp/projects/util_libs/libutils/gen_config -I/home/lm/sel4test/build-zynqmp/projects/util_libs/libplatsupport/gen_config -I/home/lm/sel4test/build-zynqmp/projects/util_libs/libethdrivers/gen_config -P -E -o linker.lds_pp -x c /home/lm/sel4test/tools/seL4/elfloader-tool/src/arch-arm/linker.lds gcc: error: unrecognized command line option '-marm'; did you mean '-mabm'? [3/235] Building C object kernel/CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj FAILED: kernel/CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj ccache /usr/bin/gcc --sysroot=/home/lm/sel4test/build-zynqmp -I../kernel/include -I../kernel/include/32 -I../kernel/include/arch/arm -I../kernel/include/arch/arm/arch/32 -I../kernel/include/plat/zynqmp -I../kernel/include/plat/zynqmp/plat/32 -I../kernel/include/arch/arm/armv/armv8-a -I../kernel/include/arch/arm/armv/armv8-a/32 -Ikernel/gen_config -Ikernel/autoconf -Ikernel/gen_headers -march=armv8-a -marm -D__KERNEL_32__ -O2 -g -DNDEBUG -nostdinc -nostdlib -O2 -DHAVE_AUTOCONF -DDEBUG -g -ggdb -mfloat-abi=soft -fno-pic -fno-pie -fno-stack-protector -fno-asynchronous-unwind-tables -std=c99 -Wall -Werror -Wstrict-prototypes -Wmissing-prototypes -Wnested-externs -Wmissing-declarations -Wundef -Wpointer-arith -Wno-nonnull -ffreestanding -E -P -MD -MT kernel/CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj -MF kernel/CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj.d -o kernel/CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj -c kernel/kernel_bf_gen_target_1_pbf_temp.c gcc: error: unrecognized command line option '-marm'; did you mean '-mabm'? gcc: error: unrecognized command line option '-mfloat-abi=soft' [4/235] Creating C input file for preprocessor ninja: build stopped: subcommand failed. ________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.

2 1

interesting i.MX8 hardware
by Corey Richardson 24 Aug '18

24 Aug '18

https://puri.sm/shop/librem-5/ A seL4 port for that platform might be nice... -- cmr http://octayn.net/ +16038524272

2 2

Re: [seL4] Demo build
by Kent.Mcleod＠data61.csiro.au 23 Aug '18

23 Aug '18

Hi Chris, For your ia32 issue, it appears that you are missing the package libx32gcc-5-dev which provides 32-bit versions of libgcc and libgcc_eh. It is normally installed automatically by gcc-5-multilib. With regards to cpio --reproducible, what version of cpio are you using? The release notes indicate that it was added in version 2.12 (https://www.gnu.org/software/cpio/) but I had it in my Debian package from version 2.11 so I assumed that it was more universally available now. Kent From: Mcleod, Kent (Data61, Kensington NSW) Sent: Thursday, August 23, 2018 11:28 AM To: Chris Rothrock; Lyons, Anna (Data61, Kensington NSW) Cc: devel(a)sel4.systems Subject: Re: [seL4] Demo build Hi Chris, For your ia32 issue, it appears that you are missing the package libx32gcc-5-dev which provides 32-bit versions of libgcc and libgcc_eh. It is normally installed automatically by gcc-5-multilib. With regards to cpio --reproducible, what version of cpio are you using? The release notes indicate that it was added in version 2.12 (https://www.gnu.org/software/cpio/) but I had it in my Debian package from version 2.11 so I assumed that it was more universally available now. Kent From: Devel <devel-bounces(a)sel4.systems> on behalf of Chris Rothrock <cgrothrock(a)gmail.com> Sent: Thursday, August 23, 2018 10:22 AM To: Lyons, Anna (Data61, Kensington NSW) Cc: devel(a)sel4.systems Subject: Re: [seL4] Demo build I am using a newly initialized build directory for ia32. I can get a good, successful build for v 9.0.0 but not 10.0.0. As for x86_64, I was able to get a good build of x86_64 on 10.0.0 before but now I can't. It seems that there is a switch for cpio that is being set in the build that is invalid for that command. Possibly the latest version of cpio no longer support --reproducable switch since this is where it errors. On Wed, Aug 22, 2018 at 7:33 PM <Anna.Lyons(a)data61.csiro.au> wrote: Hi Chris, For the first issue - just making sure you initialised a new build directory for building ia32? The second issue - our HPET driver is very bare and doesn't support the full gamut of features. If you want to continue with this platform you'll need to improve the driver. Thanks, Anna. From: Chris Rothrock <cgrothrock(a)gmail.com> Sent: Thursday, 23 August 2018 3:56 AM To: Lyons, Anna (Data61, Kensington NSW) Cc: devel(a)sel4.systems Subject: Re: [seL4] Demo build So my initial problem is actually resolved - it turns out I had the package 'ninja' installed, not 'ninja-build' which threw everything into a fit when I tried to actually use ninja. That being resolved, I was able to get a clean build of the 64 bit kernel (for x86) and made a simulated run. All looked well during the simulation. I do have 2 problems following up from this, however. When trying to use this build for a hardware boot (not simulated boot) I get an error (listed below). Also, for lengthy reasons, I also need to build a 32 bit version but when I do, this build fails. This is the build output from the ia32 build: Desktop:~/sel4test/build-ia32$ ninja [5/32] Linking CXX executable projects/sel4test/apps/sel4test-tests/sel4test-tests FAILED: : && ccache /usr/bin/g++ --sysroot=/home/jennifer/sel4test/build-ia32 -m32 -march=nehalem -D__KERNEL_32__ -nostdinc++ -g -march=nehalem -D__KERNEL_32__ -Wl,-m -Wl,elf_i386 -static -nostdlib -z max-page-size=0x1000 -u __vsyscall_ptr /home/jennifer/sel4test/build-ia32/lib/crt1.o /home/jennifer/sel4test/build-ia32/lib/crti.o /usr/lib/gcc/x86_64-linux-gnu/5/crtbegin.o projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/arch/x86/arch.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/arch/x86/tests/alignment.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/arch/x86/tests/alignment_asm.S.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/arch/x86/tests/breakpoints.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/helpers.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/main.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/benchmark_api.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/binding.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/breakpoints.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/cache.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/cnodeops.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/cspace.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/domains.cxx.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/endpoints.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/ept.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/faults.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/fpu.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/frames.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/inc_untyped.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/interrupt.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/ioports.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/iopt.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/ipc.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/multicore.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/nbwait.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/pagetables.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/preempt.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/regressions.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/schedcontext.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/scheduler.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/serial_server.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/sync.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/threads.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/trivial.c.obj projects/sel4test/apps/sel4test-tests/CMakeFiles/sel4test-tests.dir/src/tests/vspace.c.obj -lgcc -lgcc_eh libsel4/libsel4.a projects/seL4_libs/libsel4allocman/libsel4allocman.a projects/seL4_libs/libsel4vka/libsel4vka.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/seL4_libs/libsel4test/libsel4test.a projects/seL4_libs/libsel4sync/libsel4sync.a projects/seL4_libs/libsel4muslcsys/libsel4muslcsys.a projects/sel4test/libsel4testsupport/libsel4testsupport.a projects/seL4_libs/libsel4serialserver/libsel4serialserver.a projects/seL4_libs/libsel4test/libsel4test.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/util_libs/libelf/libelf.a projects/util_libs/libcpio/libcpio.a projects/seL4_libs/libsel4sync/libsel4sync.a projects/seL4_libs/libsel4platsupport/libsel4platsupport.a projects/util_libs/libplatsupport/libplatsupport.a projects/seL4_libs/libsel4simple-default/libsel4simple-default.a projects/seL4_libs/libsel4vspace/libsel4vspace.a projects/seL4_libs/libsel4simple/libsel4simple.a projects/seL4_libs/libsel4vka/libsel4vka.a projects/seL4_libs/libsel4debug/libsel4debug.a libsel4/libsel4.a projects/util_libs/libutils/libutils.a projects/musllibc/build-temp/lib/libc.a -lgcc -lgcc_eh libsel4/libsel4.a projects/seL4_libs/libsel4allocman/libsel4allocman.a projects/seL4_libs/libsel4vka/libsel4vka.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/seL4_libs/libsel4test/libsel4test.a projects/seL4_libs/libsel4sync/libsel4sync.a projects/seL4_libs/libsel4muslcsys/libsel4muslcsys.a projects/sel4test/libsel4testsupport/libsel4testsupport.a projects/seL4_libs/libsel4serialserver/libsel4serialserver.a projects/seL4_libs/libsel4test/libsel4test.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/util_libs/libelf/libelf.a projects/util_libs/libcpio/libcpio.a projects/seL4_libs/libsel4sync/libsel4sync.a projects/seL4_libs/libsel4platsupport/libsel4platsupport.a projects/util_libs/libplatsupport/libplatsupport.a projects/seL4_libs/libsel4simple-default/libsel4simple-default.a projects/seL4_libs/libsel4vspace/libsel4vspace.a projects/seL4_libs/libsel4simple/libsel4simple.a projects/seL4_libs/libsel4vka/libsel4vka.a projects/seL4_libs/libsel4debug/libsel4debug.a libsel4/libsel4.a projects/util_libs/libutils/libutils.a projects/musllibc/build-temp/lib/libc.a /usr/lib/gcc/x86_64-linux-gnu/5/crtend.o /home/jennifer/sel4test/build-ia32/lib/crtn.o -o projects/sel4test/apps/sel4test-tests/sel4test-tests && : /usr/bin/ld: skipping incompatible /usr/lib/gcc/x86_64-linux-gnu/5/libgcc.a when searching for -lgcc /usr/bin/ld: cannot find -lgcc /usr/bin/ld: skipping incompatible /usr/lib/gcc/x86_64-linux-gnu/5/libgcc_eh.a when searching for -lgcc_eh /usr/bin/ld: cannot find -lgcc_eh /usr/bin/ld: skipping incompatible /usr/lib/gcc/x86_64-linux-gnu/5/libgcc.a when searching for -lgcc /usr/bin/ld: cannot find -lgcc /usr/bin/ld: skipping incompatible /usr/lib/gcc/x86_64-linux-gnu/5/libgcc_eh.a when searching for -lgcc_eh /usr/bin/ld: cannot find -lgcc_eh collect2: error: ld returned 1 exit status [5/32] Generating from generated/plat_mode/machine/hardware.bf.pbf ninja: build stopped: subcommand failed. Here is the serial output of the x86_64 build boot: Boot config: parsing cmdline '' Boot config: console_port = 0x3f8 Boot config: debug_port = 0x3f8 Boot config: disable_iommu = false Detected 1 boot module(s): module #0: start=0xa11000 end=0xd054f0 size=0x2f44f0 name='' Parsing GRUB physical memory map Physical Memory Region from 0 size 9e800 type 1 Physical Memory Region from 9e800 size 1800 type 2 Physical Memory Region from e0000 size 20000 type 2 Physical Memory Region from 100000 size ac722000 type 1 Adding physical memory region 0x100000-0xac822000 Physical Memory Region from ac822000 size a23000 type 2 Physical Memory Region from ad245000 size 69000 type 3 Physical Memory Region from ad2ae000 size 4b5000 type 4 Physical Memory Region from ad763000 size 430000 type 2 Physical Memory Region from adb93000 size 1000 type 1 Adding physical memory region 0xadb93000-0xadb94000 Physical Memory Region from adb94000 size 206000 type 4 Physical Memory Region from add9a000 size 156000 type 1 Adding physical memory region 0xadd9a000-0xadef0000 Physical Memory Region from adef0000 size 935000 type 2 Physical Memory Region from ae825000 size 4b000 type 1 Adding physical memory region 0xae825000-0xae870000 Physical Memory Region from ae870000 size 781000 type 2 Physical Memory Region from aeff1000 size f000 type 1 Adding physical memory region 0xaeff1000-0xaf000000 Physical Memory Region from e0000000 size 10000000 type 2 Physical Memory Region from feb80000 size 82000 type 2 Physical Memory Region from fec10000 size 1000 type 2 Physical Memory Region from fed00000 size 1000 type 2 Physical Memory Region from fed40000 size 5000 type 2 Physical Memory Region from fed80000 size 10000 type 2 Physical Memory Region from ff000000 size 1000000 type 2 Physical Memory Region from 100000000 size 40000000 type 1 Adding physical memory region 0x100000000-0x140000000 Got VBE info in multiboot. Current video mode is 3 ACPI: RSDP paddr=0xf0490 ACPI: RSDP vaddr=0xf0490 ACPI: RSDT paddr=0xad269028 ACPI: RSDT vaddr=0xad269028 Warning: Your kernel was not compiled for the current microarchitecture. SKIM window for mitigating Meltdown (https://www.meltdownattack.com) not necessary for AMD and performance is being needlessly affected, consider disabling Kernel loaded to: start=0x100000 end=0xa11000 size=0x911000 entry=0x10123e ACPI: RSDT paddr=0xad269028 ACPI: RSDT vaddr=0xad269028 ACPI: FADT paddr=0xad269148 ACPI: FADT vaddr=0xad269148 ACPI: FADT flags=0x385a5 ACPI: MADT paddr=0xad2764a8 ACPI: MADT vaddr=0xad2764a8 ACPI: MADT apic_addr=0xfee00000 ACPI: MADT flags=0x1 ACPI: MADT_APIC apic_id=0x10 ACPI: MADT_APIC apic_id=0x11 ACPI: Not recording this APIC, only support 1 ACPI: MADT_APIC apic_id=0x12 ACPI: Not recording this APIC, only support 1 ACPI: MADT_APIC apic_id=0x13 ACPI: Not recording this APIC, only support 1 ACPI: MADT_IOAPIC ioapic_id=0 ioapic_addr=0xfec00000 gsib=0 ACPI: MADT_IOAPIC ioapic_id=1 ioapic_addr=0xfec01000 gsib=24 ACPI: Not recording this IOAPIC, only support 1 ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0 ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xf ACPI: 1 CPU(s) detected ELF-loading userland images from boot modules: size=0x35b000 v_entry=0x436000 v_start=0x400000 v_end=0x75b000 p_start=0xd06000 p_end=0x1061000 Moving loaded userland images to final location: from=0xd06000 to=0xa11000 size=0x35b000 Starting node #0 with APIC ID 16 Mapping kernel window is done Booting all finished, dropped to user space Received reserved IRQ: 7Skipping table FPDTD, unknown Skipping table FIDT▒, unknown Skipping table TCPA2, unknown Skipping table MSDMU, unknown Skipping table UEFIB, unknown Skipping table IVRSx, unknown Skipping table BGRT8, unknown Skipping table CRAT(, unknown Skipping table LUFT▒), unknown Warning: skipping table ACPI XSDT hpet_init@hpet.c:223 This driver expects hpet timer0 to be 64bit init_timer@main.c:192 [Cond failed: error] Failed to initialise default timer seL4 root server abort()ed Debug halt syscall from user thread 0xffffff80aeff5400 "sel4test-driver" halting... Kernel entry via Unknown syscall, word: 52 On Wed, Aug 15, 2018 at 8:30 PM <Anna.Lyons(a)data61.csiro.au> wrote: Hi Chris, That's strange, the build system definitely should not hang. However I need more information to help at all. Which OS version are you using (host and seL4)? Which gcc version and cmake version? Is there any output from the init-build script at all? Also, have you used a clean build directory after the initial failure? Cheers, Anna. From: Devel <devel-bounces(a)sel4.systems> on behalf of Chris Rothrock <cgrothrock(a)gmail.com> Sent: Thursday, 16 August 2018 3:16 AM To: devel(a)sel4.systems Subject: [seL4] Demo build Most of my experience with the seL5 microkernel has been through the Genode framework, but now I am attempting to build the demo test of seL4 without Genode using the instructions on the "Getting Started" page of seL4.systems but this seems to not be working for me. I have the latest version of repo, ninja and CMake (originally, I was given an error that I needed 3.9.x so I upgraded CMake manually). When I get to the instruction of "../init-build.sh -DPLATFORM=x86_64 -DSIMULATION=TRUE" demo build, the script only hangs. Nothing gets built and no demo is run. Is there something missing that I should be doing? Thanks, Chris -- Thank You, Chris Rothrock Senior System Administrator (315) 308-1637 -- Thank You, Chris Rothrock Senior System Administrator (315) 308-1637 -- Thank You, Chris Rothrock Senior System Administrator (315) 308-1637

2 2

Demo build
by Chris Rothrock 23 Aug '18

23 Aug '18

Most of my experience with the seL5 microkernel has been through the Genode framework, but now I am attempting to build the demo test of seL4 without Genode using the instructions on the "Getting Started" page of seL4.systems but this seems to not be working for me. I have the latest version of repo, ninja and CMake (originally, I was given an error that I needed 3.9.x so I upgraded CMake manually). When I get to the instruction of "../init-build.sh -DPLATFORM=x86_64 -DSIMULATION=TRUE" demo build, the script only hangs. Nothing gets built and no demo is run. Is there something missing that I should be doing? Thanks, Chris -- Thank You, Chris Rothrock Senior System Administrator (315) 308-1637

2 4

formal guarantee about preserving user behaviour
by Abhishek Anand 18 Aug '18

18 Aug '18

I have been reading the following paper for some time: Klein, Gerwin, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser. “Comprehensive Formal Verification of an OS Microkernel.” *Trustworthy Sytems*, 2014. https://ts.data61.csiro.au/publications/nictaabstracts/Klein_AEMSKH_14.abst… This is fantastic work and provides powerful guarantees about kernel behavior. However, I am confused about the guarantees about the behavior of user programs. The paper seems to suggest that in the abstract model of sel4, the user transitions are nondeterministic. page 21 bottom: "User transitions are specified as nondeterministically changing arbitrary user-accessible parts of the state space" Does this mean that the refinement theorem of sel4 (Theorem 3 in the above paper: the C implementation refines the abstract model) provides no guarantee about what the user program does, except that the user program does not mess up with the kernel state? Is it fair to say that the refinement theorem does not preclude the sel4 implementation from incorrectly changing the behavior of the user programs, e.g. by messing up the user state? I was expecting the abstract model in Isabelle to concretely specify how the user programs behave, perhaps according to x86/arm/riscv semantics extended with syscalls. Sorry if I misunderstood the paper. Thanks in advance for any clarification, Abhishek -- -- Abhishek http://www.cs.cornell.edu/~aa755/

3 5

Cap fault in send phase while spawning processes
by Noah Kennedy 17 Aug '18

17 Aug '18

Hi folks, I'm currently porting over a project from the Kbuild/Kconfig build system to the new CMake based build system and am having some issues. I'm trying trying to spawn additional processes (2+) and I am encountering an error when I attempt to call 'process_config_default_simple'. The message reads: Caught cap fault in send phase at address 0x0 while trying to handle: vm fault on data at address 0x0 with status 0x4 in thread 0xffffff801ffb5400 "PRIMARY" at address 0x4252ba I loaded the executables which I am trying to spawn into the new processes into the cpio using a variation of the call MakeCPIO(archive.o $<TARGET_FILE:SECONDARY>;$<TARGET_FILE:TERTIARY>;...) where SECONDARY and TERTIARY are the executables which I am using later to spawn the new processes. The source code in question worked previously when using Kbuild, so I'm wondering if I'm doing something wrong with the CMake. Does anyone have any ideas? I've gone through the tutorials, but I'm still fairly new to seL4, so any help would be very much appreciated.

2 2

sel4test driver can not load big elf file
by Dd Nirvana 17 Aug '18

17 Aug '18

Hi guys, When I try to run some application tests(written by myself) on sel4test (x86-qemu environment), I found the following errors. *Starting test suite sel4test* *Starting test 0: Test that there are tests* *Starting test 1: APPTEST1* *vka_alloc_object_at_maybe_dev@object.h:59 Failed to allocate object of size 4096, error 1* *new_pages_at_vaddr@vspace.c:330 Failed to allocate page number: 0 out of 1* *load_segment@elf.c:103 ERROR: failed to allocate frame by loadee vka: 10* *sel4utils_elf_load_record_regions@elf.c:519 Failed to load segments* *sel4utils_configure_process_custom@process.c:596 Failed to load elf file* It seems seL4test's driver can not load tests with very large size? I also tried to change the "DRIVER_UNTYPED_MEMORY" size from "(1 << 25)" to "(1 << 27)", but it also failed. Any advices about the issue? Dong

2 1

create process in seL4
by Leonid Meyerovich 16 Aug '18

16 Aug '18

Hello, Is there any way to define untyped size while creating process using library functions? process_config_default_simple(simple_t *simple, const char *image_name, uint8_t prio) sel4utils_configure_process_custom(sel4utils_process_t *process, vka_t *vka, vspace_t *spawner_vspace, sel4utils_process_config_t config) The second question is how to initialize allocator (probably I should use bootstrap_use_current_1level, but how where should I get parameters?) in created process to support memory allocation operations? Thank you, Leonid ________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.

2 2

Interrupts in SEL4
by Sathya Narayanan N 16 Aug '18

16 Aug '18

Hi Experts, We are trying to port sel4 to Shakti FPGA. It is similar to Rocket FPGA. The memory footprint is 256 mb [0x80000000 - 0x8fffffff]. Shakti support -march=imafd. A single core 64 bit design. The run in FPGA stops at *"memcpy((char *)dest_vaddr + phys_virt_offset, (char *)elf + data_offset, data_size);*" called in the function " *unpack_elf_to_paddr()".* Earlier it stopped just at the memset (one line above). I manually commented out memset part and made it to run till memcpy. So I doubt it has something to do with wrong memory access. can someone please explain me the above said function (blue color) ? what could be reasons for memcpy to hung ? Can someone please guide me to the area in code where memory related interrupts are coded ? We have the latest upstream of SEL4 (Aug 10). It has the dornerworks upstream changes. We are trying to load at 0x88000000. The image works well in spike simulation. *Commands to build:* ../init-build.sh -DPLATFORM=spike -DKernelPlatformSpikeRocketChip=ON -DSIMULATION=FALSE -DRISCV64=TRUE ninja *Snapshot of the run in FPGA:* DTB { #address-cells = <0x00000002>; #size-cells = <0x00000002>; compatible = "shakti,spike-bare-dev"; model = "shakti,spike-bare"; cpus { #address-cells = <0x00000001>; #size-cells = <0x00000000>; timebase-frequency = <0x00989680>; cpu@0 { device_type = "cpu"; reg = <0x00000000>; status = "okay"; compatible = "riscv"; riscv,isa = "rv64imafd"; mmu-type = "riscv,sv39"; clock-frequency = <0x3b9aca00>; interrupt-controller { #interrupt-cells = <0x00000001>; interrupt-controller; compatible = "riscv,cpu-intc"; linux,phandle = <0x00000001>; phandle = <0x00000001>; } } } memory@80000000 { device_type = "memory"; reg = <0x00000000 0x80000000 0x00000000 0x10000000>; } soc { #address-cells = <0x00000002>; #size-cells = <0x00000002>; compatible = "shakti,spike-bare-soc", "simple-bus"; ranges; } uart { compatible = "shakti,uart0"; reg = <0x00000000 0x00011200 0x00000000 0x00001000>; } htif { compatible = "ucb,htif0"; } } ELF-loader started on paddr=[80200000..8060e7d7] elf check file returned 1 elf check file returned 1 ELF-loading image 'kernel' paddr=[88000000..8802bfff] vaddr=[ffffffff80000000..ffffffff8002bfff] virt_entry=ffffffff80000000 configured page table levels = 3...... elf check file returned 1 image size 2b350 *(char *)dest_vaddr + phys_virt_offset = ffffffff88000000 * *phys_virt_offset = 8000000 * *(char *)elf + data_offset, = ffffffff8020f854* *started memcpy* ------------------------------------------------------------> *Hangs* -- regards, Sathya

2 2

seL4 benchmark cache unable.
by 송대영 15 Aug '18

15 Aug '18

Hi, I have question about sel4 benchmark cache unable. I want to benchmark sel4 without cache but I don't know where is the location that configures cache. Would you give advice?

2 1