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 <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