Re: [seL4] CAmkES Tutorial Generation Issues

Hello, LANG=en_US.UTF-8 ./init --tut hello-camkes-0 or LANGUAGE=en_US.UTF-8 ./init --tut hello-camkes-0 did not work. Seems I was able to resolve this with the following commands: update-locale LANG=en_US.UTF-8 dpkg-reconfigure locales update-locale LANG=en_US.UTF-8 export LANG=en_US.UTF-8 After the project built successfully, I tired executing ./simulate and I got the following assertion: Assertion failed: free_slot_end - free_slot_start >= CONFIG_CAPDL_LOADER_MAX_OBJECTS (../projects/camkes/capdl/capdl-loader-app/src/main.c: parse_bootinfo: 562) I recieved the below output: # ./simulate qemu-system-x86_64 -cpu Nehalem,-vme,+pdpe1gb,-xsave,-xsaveopt,-xsavec,-fsgsbase,-invpcid,enforce -nographic -serial mon:stdio -m size=512M -kernel images/kernel-x86_64-pc99 -initrd images/capdl-loader-image-x86_64-pc99 Boot config: debug_port = 0x3f8 Boot config: disable_iommu = false Detected 1 boot module(s): module #0: start=0xa17000 end=0xaef0e8 size=0xd80e8 name='images/capdl-loader-image-x86_64-pc99' Parsing GRUB physical memory map Physical Memory Region from 0 size 9fc00 type 1 Physical Memory Region from 9fc00 size 400 type 2 Physical Memory Region from f0000 size 10000 type 2 Physical Memory Region from 100000 size 1fee0000 type 1 Adding physical memory region 0x100000-0x1ffe0000 Physical Memory Region from 1ffe0000 size 20000 type 2 Physical Memory Region from fffc0000 size 40000 type 2 Multiboot gave us no video information ACPI: RSDP paddr=0xf68c0 ACPI: RSDP vaddr=0xf68c0 ACPI: RSDT paddr=0x1ffe15fc ACPI: RSDT vaddr=0x1ffe15fc Kernel loaded to: start=0x100000 end=0xa16000 size=0x916000 entry=0x10125e ACPI: RSDT paddr=0x1ffe15fc ACPI: RSDT vaddr=0x1ffe15fc ACPI: FADT paddr=0x1ffe1458 ACPI: FADT vaddr=0x1ffe1458 ACPI: FADT flags=0x80a5 ACPI: MADT paddr=0x1ffe154c ACPI: MADT vaddr=0x1ffe154c ACPI: MADT apic_addr=0xfee00000 ACPI: MADT flags=0x1 ACPI: MADT_APIC apic_id=0x0 ACPI: MADT_IOAPIC ioapic_id=0 ioapic_addr=0xfec00000 gsib=0 ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0 ACPI: MADT_ISO bus=0 source=5 gsi=5 flags=0xd ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xd ACPI: MADT_ISO bus=0 source=10 gsi=10 flags=0xd ACPI: MADT_ISO bus=0 source=11 gsi=11 flags=0xd ACPI: 1 CPU(s) detected ELF-loading userland images from boot modules: size=0x210000 v_entry=0x407fef v_start=0x400000 v_end=0x610000 p_start=0xaf0000 p_end=0xd00000 Moving loaded userland images to final location: from=0xaf0000 to=0xa16000 size=0x210000 Starting node #0 with APIC ID 0 Mapping kernel window is done Booting all finished, dropped to user space Assertion failed: free_slot_end - free_slot_start >= CONFIG_CAPDL_LOADER_MAX_OBJECTS (../projects/camkes/capdl/capdl-loader-app/src/main.c: parse_bootinfo: 562) After commenting out the assertion and rebuilding, things seemed to work properly. I see the comment above the assertion says: /* We need to be able to actual store caps to the maximum number of objects * we may be dealing with. * This check can still pass and initialisation fail as we need extra slots for duplicates * for CNodes and TCBs. */ But I still don't quite understand what this assertion is trying to check and why it doesn't really seem needed since commenting it out made things work properly (stdout showed "Hello CAmkES World"). If I were to guess, I'd assume that the check is performed to just make sure there is a decent amount of space to store capabilities in userspace? While I was messing around in the main.c of capdl-loader-app, I wanted to put print statments to see the values of free_slot_end and free_slot_start to get an idea of what these values were, but I didn't see a way to display them to stdout (printf didn't work and I don't know where ZF_LOGD is logging info to). Regards, Austin ________________________________ From: Austin Owens Sent: Saturday, July 20, 2019 5:27 PM To: devel@sel4.systems Subject: CAmkES Tutorial Generation Issues Hello, I am able to generate, build, and execute the majority of tutorials using init, ninja, qemu, etc. within sel4-tutorials-manifest. However, I am having issues generating the tutorials specifically for the CamkES tutorials. I have installed all of the system requirements and I am running on Ubuntu 18. The output I get is the following: # ./init --tut hello-camkes-0 loading initial cache file ../settings.cmake -- The C compiler identification is GNU 7.4.0 -- Check for working C compiler: /usr/bin/gcc -- Check for working C compiler: /usr/bin/gcc -- works -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Detecting C compile features -- Detecting C compile features - done -- The CXX compiler identification is GNU 7.4.0 -- Check for working CXX compiler: /usr/bin/g++ -- Check for working CXX compiler: /usr/bin/g++ -- works -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Detecting CXX compile features -- Detecting CXX compile features - done -- The ASM compiler identification is GNU -- Found assembler: /usr/bin/gcc -- CPIO test cpio_reproducible_flag FAILED -- Performing Test compiler_arch_test -- Performing Test compiler_arch_test - Success -- /root/sel4-tutorials-manifest/hello-camkes-0_build/hello-camkes-0/ast.pickle is out of date. Regenerating... -- /root/sel4-tutorials-manifest/hello-camkes-0_build/hello-camkes-0/camkes-gen.cmake is out of date. Regenerating... CAmkES uses UTF-8 encoding, but your locale's preferred encoding is ansi_x3.4-1968. You can override your locale with the LANG environment variable. CMake Error at tools/seL4/cmake-tool/helpers/make.cmake:19 (file): file failed to open for reading (No such file or directory): /root/sel4-tutorials-manifest/hello-camkes-0_build/hello-camkes-0/camkes_gen/deps_1 Call Stack (most recent call first): tools/seL4/cmake-tool/helpers/make.cmake:77 (MakefileDepsToList) tools/camkes/camkes.cmake:460 (execute_process_with_stale_check) hello-camkes-0/CMakeLists.txt:13 (GenerateCAmkESRootserver) CMake Error at tools/camkes/camkes.cmake:480 (message): Failed to generate /root/sel4-tutorials-manifest/hello-camkes-0_build/hello-camkes-0/camkes-gen.cmake Call Stack (most recent call first): hello-camkes-0/CMakeLists.txt:13 (GenerateCAmkESRootserver) -- Configuring incomplete, errors occurred! See also "/root/sel4-tutorials-manifest/hello-camkes-0_build/CMakeFiles/CMakeOutput.log". Traceback (most recent call last): File "./init", line 96, in <module> File "./init", line 85, in main File "/root/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 107, in init_directories return _init_build_directory(config, initialised, build_directory, tute_directory, output, config_dict=config_dict) File "/root/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 75, in _init_build_directory return sh.cmake(args + ['..'], _cwd=directory, _out=output, _err=output) File "/usr/local/lib/python3.6/dist-packages/sh.py", line 1427, in __call__ return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/usr/local/lib/python3.6/dist-packages/sh.py", line 774, in __init__ self.wait() File "/usr/local/lib/python3.6/dist-packages/sh.py", line 792, in wait self.handle_command_exit_code(exit_code) File "/usr/local/lib/python3.6/dist-packages/sh.py", line 815, in handle_command_exit_code raise exc sh.ErrorReturnCode_1: RAN: /usr/local/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-0 -C ../settings.cmake .. STDOUT: STDERR: I am not sure if ast.pickle and camkes-gen.cmake being out of date has anything to do with deps_1 file not being present. It's not possible to copy the deps_0 file to deps_1 since calling the './init --tut hello-camkes-0' command again creates a new project directory. Is there something obvious that I am missing? Thanks, Austin