July 2020 - Devel - lists.sel4.systems

seL4 test on x86
by Yevgeny Lavrov 29 Jan '25

29 Jan '25

Hello, I'm new to seL4 and I'm just doing it for learning purpose. I'm trying to run seL4 test suite or simple hello world task from seL4 tutorials on the real hardware. So far I had no problems compiling seL4 test suite and running via QEMU for both x32 and x64 platforms. However, when I try to run it on the actual hardware following Running on real hardware tutorial for x86 I end up with no output at all and no error msgs that can give me a clue on where something went wrong. After compiling seL4test for x86, I ended up with two images in sel4_dir/images/ folder. Copied them over to /boot/sel4/ folder and created a new GRUB2 entry that looks like this menuentry “seL4 test suite” --class os { load video insmod gzio insmod part_msdos insmod ext2 set root=’(hd0,msdos5)’ multiboot /boot/sel4/kernel-ia32-pc99 module /boot/sel4/sel4test-driver-image-ia32-pc99 } update grub, restart and select the new entry from GRUB menu. I end up with blinking cursor on the top-left side of the screen. Please advise.

4 3

Stuck during invalidate local TLB in Tx2
by Muneeswaran Rajendran 15 Oct '24

15 Oct '24

Hi seL4 Dev team, Can someone explain the reason (share the reference) to invalidate the local TLB during kernel vspace activation as part CPU initialisation. The Tx2 board stuck while performing this operation. As per my understanding both Tx1 and Tx2 are using same A57 core. so the TLB initialisation and invalidation remain same for Tx2 and should not stuck during invalidation.Please correct me if anything wrong here. I understand from that instruction (tlbi vmalle1) which is invalidating stage 1 entries associated to the current VMID. Also from arm mmu code the seL4 setting up (TCR_EL1) TCR register addressing space as 48bit, ASID as 16bit and page table setup 4k granular size. I am using MRS macro to dump the spsr_el1 and dspsr_el0 register to see the state of processor but its throwing synchronous exception. Do we have any other option to dump all the register content to see the state of processor like we have one in 'sel4debug_dump_registers' which is used in sel4test code. Regards, Muneeswaran R

3 4

Questions about Memory Management in seL4
by Daniel Wang 18 May '23

18 May '23

Hi all, Sorry to bother, I have some basic questions about seL4 memory management. Can someone help me? 1. where is the kernel’s address space? I know there are basically three methods: a) separate virtual address space, e.g. through changing page tables on entry into privileged mode to access b) physical space, e.g. through disable automatic hardware translation of virtual addresses on entry into privilege mode c) privilege region in each process’s virtual address space, e.g. through page table to map kernel address into use-mode process. My question is which of this is being used by seL4 microkernel? 2. Objects like CSpace, VSpace, CNode, TCB, Endpoint, etc. are called kernel objects, but it seems all dynamically allocated in thread running/creating time. Are those objects (e.g. Figure 3.3 in seL4 manual) in kernel space or in user space? 3. I read that after the kernel boot up, it passes all resources, untyped memory to the first thread. Are those untyped memory physical memory or virtual memory in a single page? The reason I ask is I’m learning the code of the UNSW AOS project (two of the assignment projects are implementing frame and papers). I’m confused that before the implementation of frames and pages what kind of memory is passed to the the first thread? I saw int AOS project, it uses ut_table_init(), ut_steal_mem(), I wonder what kind of memory it operates on? Thanks -Dan

5 4

help with tutorial
by Sachin More 02 Jul '20

02 Jul '20

Hi: I am new to L4 and have been working through the tutorials. However, I am having a problem doing the hello-camkes-0 tutorial. When I try to install the tutorial, I get the output below. Looks like a file hello-camkes-0_build/camkes_gen/deps_1 is not there. Any help would be greatly appreciated! thanks, Sachin $ ./init --tut hello-camkes-0 loading initial cache file ../projects/sel4-tutorials/settings.cmake -- Found capdl: /compile/sel4-tutorials-manifest/projects/capdl CMake Warning (dev) at /usr/share/cmake3/Modules/FindPackageHandleStandardArgs.cmake:272 (message): The package name passed to `find_package_handle_standard_args` (camkes-tool) does not match the name of the calling package (sel4-tutorials). This can lead to problems in calling code that expects `find_package` result variables (e.g., `_FOUND`) to follow a certain pattern. Call Stack (most recent call first): /compile/sel4-tutorials-manifest/projects/sel4-tutorials/Findsel4-tutorials.cmake:67 (FIND_PACKAGE_HANDLE_STANDARD_ARGS) /compile/sel4-tutorials-manifest/projects/sel4-tutorials/settings.cmake:96 (find_package) This warning is for project developers. Use -Wno-dev to suppress it. -- Found camkes-tool: /compile/sel4-tutorials-manifest/projects/sel4-tutorials CMake Warning (dev) at /usr/share/cmake3/Modules/FindPackageHandleStandardArgs.cmake:272 (message): The package name passed to `find_package_handle_standard_args` (camkes-tool) does not match the name of the calling package (sel4-tutorials). This can lead to problems in calling code that expects `find_package` result variables (e.g., `_FOUND`) to follow a certain pattern. Call Stack (most recent call first): /compile/sel4-tutorials-manifest/projects/sel4-tutorials/Findsel4-tutorials.cmake:67 (FIND_PACKAGE_HANDLE_STANDARD_ARGS) /compile/sel4-tutorials-manifest/projects/sel4-tutorials/settings.cmake:96 (find_package) CMakeLists.txt:3 (include) This warning is for project developers. Use -Wno-dev to suppress it. -- The C compiler identification is GNU 7.3.1 -- The ASM compiler identification is GNU -- Found assembler: /opt/rh/devtoolset-7/root/usr/bin/gcc -- Check for working C compiler: /opt/rh/devtoolset-7/root/usr/bin/gcc -- Check for working C compiler: /opt/rh/devtoolset-7/root/usr/bin/gcc - works -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Detecting C compile features -- Detecting C compile features - done -- Found camkes-tool: /compile/sel4-tutorials-manifest/projects/camkes-tool -- Found seL4: /compile/sel4-tutorials-manifest/kernel -- Found elfloader-tool: /compile/sel4-tutorials-manifest/tools/seL4/elfloader-tool -- Found musllibc: /compile/sel4-tutorials-manifest/projects/musllibc -- Found util_libs: /compile/sel4-tutorials-manifest/projects/util_libs -- Found seL4_libs: /compile/sel4-tutorials-manifest/projects/seL4_libs -- Found projects_libs: /compile/sel4-tutorials-manifest/projects/projects_libs -- Detecting cached version of: capDL-tool -- No cache path given. Set SEL4_CACHE_DIR to a path to enable caching binary artifacts. -- Found sel4runtime: /compile/sel4-tutorials-manifest/projects/sel4runtime -- Performing Test compiler_arch_test -- Performing Test compiler_arch_test - Success -- Detecting cached version of: musllibc -- No cache path given. Set SEL4_CACHE_DIR to a path to enable caching binary artifacts. -- /compile/sel4-tutorials-manifest/hello-camkes-0_build/ast.pickle is out of date. Regenerating... -- /compile/sel4-tutorials-manifest/hello-camkes-0_build/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 /compile/sel4-tutorials-manifest/tools/seL4/cmake-tool/helpers/make.cmake:13 (file): file failed to open for reading (No such file or directory): /compile/sel4-tutorials-manifest/hello-camkes-0_build/camkes_gen/deps_1 Call Stack (most recent call first): /compile/sel4-tutorials-manifest/tools/seL4/cmake-tool/helpers/make.cmake:71 (MakefileDepsToList) /compile/sel4-tutorials-manifest/projects/camkes-tool/camkes.cmake:503 (execute_process_with_stale_check) CMakeLists.txt:17 (GenerateCAmkESRootserver) /compile/sel4-tutorials-manifest/projects/sel4-tutorials/Findsel4-tutorials.cmake:29 (include) CMakeLists.txt:4 (sel4_tutorials_regenerate_tutorial) CMake Error at /compile/sel4-tutorials-manifest/projects/camkes-tool/camkes.cmake:523 (message): Failed to generate /compile/sel4-tutorials-manifest/hello-camkes-0_build/camkes-gen.cmake Call Stack (most recent call first): CMakeLists.txt:17 (GenerateCAmkESRootserver) /compile/sel4-tutorials-manifest/projects/sel4-tutorials/Findsel4-tutorials.cmake:29 (include) CMakeLists.txt:4 (sel4_tutorials_regenerate_tutorial) -- Configuring incomplete, errors occurred! See also "/compile/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 "/compile/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 106, in init_directories return _init_build_directory(config, initialised, build_directory, tute_directory, output, config_dict=config_dict) File "/compile/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 74, in _init_build_directory return sh.cmake(args + [tute_directory], _cwd=directory, _out=output, _err=output) File "/net/freenas/mnt/freenas-4TB/smore/.local/lib/python3.6/site-packages/sh.py", line 1549, in __call__ return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/net/freenas/mnt/freenas-4TB/smore/.local/lib/python3.6/site-packages/sh.py", line 793, in __init__ self.wait() File "/net/freenas/mnt/freenas-4TB/smore/.local/lib/python3.6/site-packages/sh.py", line 849, in wait self.handle_command_exit_code(exit_code) File "/net/freenas/mnt/freenas-4TB/smore/.local/lib/python3.6/site-packages/sh.py", line 877, in handle_command_exit_code raise exc sh.ErrorReturnCode_1: RAN: /bin/cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-0 -C ../projects/sel4-tutorials/settings.cmake /compile/sel4-tutorials-manifest/hello-camkes-0 STDOUT: STDERR:

2 2

Confirming correct syntax of items in devices.camkes.
by Travis Wheatley 01 Jul '20

01 Jul '20

I have been attempting to add support for both USB and SD persistent memory to my vm (See "Re: ramdisk vs. persistant rfs in VMs.” thread.). I seem to be having a problem with power management. In hopes of correcting this I wish to expose the power management unit to the VM. The related stanza looks like this in my device tree file. cci@fd6e0000 { compatible = "arm,cci-400"; reg = <0x0 0xfd6e0000 0x0 0x9000>; ranges = <0x0 0x0 0xfd6e0000 0x10000>; #address-cells = <0x1>; #size-cells = <0x1>; pmu@9000 { compatible = "arm,cci-400-pmu,r1"; reg = <0x9000 0x5000>; interrupt-parent = <0x4>; interrupts = <0x0 0x7b 0x4 0x0 0x7b 0x4 0x0 0x7b 0x4 0x0 0x7b 0x4 0x0 0x7b 0x4>; }; }; The PMU appears to be a child of cci. I am unsure of the proper syntax to use in my devices.camkes file. Since it is a child does one specify the path as /cci/pmu? Does the parent also have to be exposed to the vm? Here is what the related lines inmy devices.camkes look like. Is this correct? vm0.dtb = dtb([ {"path": "/cci@fd6e0000"}, {"path": "/cci/pmu@9000"},

1 0