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 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 on behalf of Chris Rothrock < cgrothrock@gmail.com> *Sent:* Thursday, 16 August 2018 3:16 AM *To:* devel@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