Re: [seL4] Demo build

I am using cpio v2.11. Even having just updated to Ubuntu 18.04, 2.12 isn't available through normal apt-get upgrade. On Wed, Aug 22, 2018 at 9:29 PM wrote:

​ 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@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 on behalf of Chris Rothrock < cgrothrock@gmail.com> Sent: Thursday, August 23, 2018 10:22 AM To: Lyons, Anna (Data61, Kensington NSW) Cc: devel@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 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 Sent: Thursday, 23 August 2018 3:56 AM To: Lyons, Anna (Data61, Kensington NSW) Cc: devel@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 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

--

Thank You,

Chris Rothrock Senior System Administrator (315) 308-1637

-- Thank You, Chris Rothrock Senior System Administrator (315) 308-1637