Devel November 2019

devel@sel4.systems

19 participants
21 discussions

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

19 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

Userspace debugging with QEMU/gdb
by Jiusheng Liu 02 Dec '19

02 Dec '19

Hi, >From the page https://docs.sel4.systems/DebuggingGuide.html (section Userspace debugging), I know we can debug userspace process by command below: ---------------------------- cmd example start ---------------------------------------- gdb ./dynamic-2 Reading symbols from ./dynamic-2...done. (gdb) target remote :1234 Remote debugging using :1234 0x000000000000fff0 in ?? () (gdb) break main Breakpoint 1 at 0x402011: file sel4-tutorials-manifest/dynamic-2/main.c, line 161. (gdb) c Continuing. Breakpoint 1, main () at sel4-tutorials-manifest/dynamic-2/main.c:161 161 (gdb) ---------------------------- cmd example end ---------------------------------------- It works for normal userspace process (such as the example code in tutorials: https://docs.sel4.systems/Tutorials/dynamic-2.html ). But when I want to debug the userspace process for the code in the tutorials page https://docs.sel4.systems/Tutorials/camkes-vm-linux.html (one virtual machine in seL4), I cannot catch the breakpoints. So can you help me to explain why I cannot catch the breakpoint? and can we debug the vmm create process with qemu/gdb? Thanks.

2 2

Re: [seL4] Devel Digest, Vol 66, Issue 26
by Millar, Curtis (Data61, Kensington NSW) 26 Nov '19

26 Nov '19

> As I'm playing with a prototype language and OS while building it on > top of seL4, > I'm not using any intermediate C layers to connect to the seL4 API (so > custom build and > integration and no C runtime), while most of the samples out there are > heavily relying on > some foundations, which is completely understandable, considering how > it can be involving > to build anything relevant on top of the seL4 API. > So as I'm just really getting started to integrate with seL4 (and > I love?? it!) I have to go through > all these details, but I hope that I won't be spamming unnecessarily > here! ? If you are looking to avoid any C interop or runtime that should be completely possible. The only requirement the kernel makes is that user- level code needs to keep track of the IPC buffer address on its own (unlike previous versions which ensure that a particular register contains the IPC buffer address). If you want a minimal runtime without TLS you could store the IPC buffer address in a global variable and ensure that your system call wrappers use that global variable to load and store data into the IPC buffer.

1 0

Re: [seL4] Understand how TLS is setup in the root server for x64
by Millar, Curtis (Data61, Kensington NSW) 26 Nov '19

26 Nov '19

Hi Alexandre, > I'm trying to understand how the TLS is setup for the root server on > x64 (to access for example the IPC buffer) > but I'm failing to connect the pieces and how the server is correctly > setting the FS register. There is detailed documentation for the TLS change on the page for RFC- 3. https://sel4.atlassian.net/browse/RFC-3 In essence, the new TLS model stores the address of the IPC buffer in a thread-local variable which must be initialised by your process or threading runtime along with general TLS intialisation. https://github.com/seL4/seL4/blob/master/libsel4/include/sel4/functions.h#L… To assist with this there is a simple sel4runtime library which provides a minimal C-runtime and tools for initialising TLS. https://github.com/SEL4PROJ/sel4runtime On x86_64 the TLS register can be set without calling into the kernel by using the `wrfsbase` instruction or by using the `sel4runtime_set_tls_base` function from the sel4runtime library. > Now, I'm failing to find in the codebase where the ELF loader is > actually detecting the TLS segment and the according setup with the > TLS register. The ELF loader is not responsible for TLS initialisation, the C-runtime is responsible for configuring TLS of the initial thread. https://bitbucket.ts.data61.csiro.au/projects/SEL4PROJ/repos/sel4runtime/br… > Never mind, I discovered that I in order to access a TLS variable you > need to call `seL4_TCB_SetTLSBase` on seL4_CapInitThreadTCB first in > the root server, as I'm trying to work on a bare bone usage of seL4 to > better understand it, this part was not obvious from the existing more > complex samples! In general I would recommend having the initial thread in a process initialise its own TLS via the runtime and any new thread configure its own TLS in the initialisation code before the main function call of that thread with the `sel4runtime_set_tls_base`. Each new thread will also need to use `seL4_SetIPCBuffer` to initialise the IPC buffer address in its TLS before performing any invocations or any other system calls. Cheers, Curtis Millar Systems Engineer, Trustworthy Systems, CSIRO's Data61 curtis.millar(a)data61.csiro.au Data61, CSIRO Level 3, K17 Building UNSW Gate 14, Barker St Kensington NSW 2033 Australia

2 1

Is there a "modern" seL4 manifest/configuration that is known to run on CMA34CR?
by Nogin, Aleksey 24 Nov '19

24 Nov '19

Unless I am looking in the wrong place, all the CMA34CR support was removed in https://github.com/seL4/camkes-vm/commit/aab3478acc4705a3161f5bf59625f7c96a…. Is there something that remains? If not, what would be the best starting point to try to port a demo running on CMA34CR board from an old (early 2017) version of the sel4/camkes/etc to a recent stable release (e.g, 10.1.1)? Thanks. Aleksey CONFIDENTIALITY NOTICE: The information transmitted in this email, including attachments, is intended only for the person(s) or entity to which it is addressed and may contain confidential, proprietary and/or privileged material exempt from disclosure under applicable law. Any review, retransmission, dissemination or other use of, or taking of any action in reliance upon this information by persons or entities other than the intended recipient is prohibited. If you received this message in error, please contact the sender immediately and destroy any copies of this information in their entirety.

2 4

Understand how TLS is setup in the root server for x64
by Alexandre Mutel 24 Nov '19

24 Nov '19

Hello! I'm trying to understand how the TLS is setup for the root server on x64 (to access for example the IPC buffer) but I'm failing to connect the pieces and how the server is correctly setting the FS register. For example the sel4_Send function is codegen like this (using -ftls-model=local-exec) Function: seL4_Send push r15 mov rdx,0FFFFFFFFFFFFFFFDh push rbx mov rax,[fs:0] mov r10,[rax+8] mov r8,[rax+10h] mov r9,[rax+18h] mov r15,[rax+20h] mov rbx,rsp syscall mov rsp,rbx pop rbx pop r15 ret The instruction `mov rax,[fs:0]` is accessing the seL4_IPCBuffer* and the the executable has a TLS segments of 8 bytes for the pointer. all good. Now, I'm failing to find in the codebase where the ELF loader is actually detecting the TLS segment and the according setup with the TLS register. And I'm wondering if the setup for the codegen is not wrong on my side (e.g the local-exec is not working), so that instead of having a FS register it would be a direct memory access. Does anyone have a clue about this? Thank you!

1 2

Fwd: port sel4 to RK3308(quad cortex-a35)
by Yun Zhou 22 Nov '19

22 Nov '19

---------- Forwarded message --------- 发件人： Yun Zhou <shiny725829(a)gmail.com> Date: 2019年10月25日周五下午9:52 Subject: port sel4 to RK3308(quad cortex-a35) To: <devel-owner(a)sel4.systems> Dear sel4 Experts How are you I found some information about sel4, and sel4 is great microkernel OS, i want port sel4 to RK3308(quad cortex-a35, GICv2) for real time audio signal processing. Form the Tutorials I found sel4 just support cortex-a53, I would like to ask does sel4 support cortex-a35 SMP mode. and because our application is real time audio processing so system delay must lower than 3ms and hard real-time determinism. Will sel4 support real-time signal processing? Looking forward to your reply Thanks &Kind regards Yun

2 1

Nasty bug in global-components/templates/rpc-signalling.template.c
by Nogin, Aleksey 22 Nov '19

22 Nov '19

After spending a few hours debugging time server not working for me, I realized that global-components/templates/rpc-signalling.template.c that was added earlier this year contains the following /*- set badge = str(configuration[c.instance.name].get("%s_attributes" % c.interface.name)).strip('"') -*/ [...] /*- do badges.sort() -*/ [...] int /*? me.interface.name ?*/_largest_badge(void) { return /*? badges[len(badges) - 1] ?*/; } Unfortunately for me, my Trusted Build generated camkes had the attributes numbered 1,2,3,10,11,12,13 and therefore the above core was claiming that the time_server_largest_badge is 3 :(. Obviously, the issue is the combination of the str and sort, resulting in the last badge being the one largest lexicographically, not numerically :(. Replacing the str with int (and correspondingly removing the strip) solved the problem for me. P.S. Well, solved that particular problem for me, not the problem of time server not working - looks like now I will have to debug FAULT HANDLER: data fault from time_server.time_server_0_control (ID 0x2) on address 0x84b8ba, pc = 0x42439d, fsr = 0x4 FAULT HANDLER: Register dump: FAULT HANDLER: rip :0x42439d FAULT HANDLER: rsp :0x454cf0 FAULT HANDLER: rflags :0x10202 FAULT HANDLER: rax :0x413a33 FAULT HANDLER: rbx :0x437e88 FAULT HANDLER: rcx :0x0 FAULT HANDLER: rdx :0x437e98 FAULT HANDLER: rsi :0x28 FAULT HANDLER: rdi :0x437e98 FAULT HANDLER: rbp :0x454d70 FAULT HANDLER: r8 :0xffffffff FAULT HANDLER: r9 :0x0 FAULT HANDLER: r10 :0xe8 FAULT HANDLER: r11 :0x293 FAULT HANDLER: r12 :0x413a32 FAULT HANDLER: r13 :0x84b8ba FAULT HANDLER: r14 :0x0 FAULT HANDLER: r15 :0x0 FAULT HANDLER: fs_base :0x44a460 FAULT HANDLER: gs_base :0x0 FAULT HANDLER: memory map: FAULT HANDLER: +-- 0x0000000000458fff -- FAULT HANDLER: | guard page FAULT HANDLER: +-- 0x0000000000458000 -- FAULT HANDLER: | IPC buffer FAULT HANDLER: +-- 0x0000000000457000 -- FAULT HANDLER: | guard page FAULT HANDLER: +-- 0x0000000000456000 -- FAULT HANDLER: | guard page FAULT HANDLER: +-- 0x0000000000455000 -- FAULT HANDLER: | stack FAULT HANDLER: +-- 0x0000000000451000 -- FAULT HANDLER: | guard page FAULT HANDLER: +-- 0x0000000000450000 -- FAULT HANDLER: | code and data FAULT HANDLER: +-- 0x0000000000400000 - :( Aleksey CONFIDENTIALITY NOTICE: The information transmitted in this email, including attachments, is intended only for the person(s) or entity to which it is addressed and may contain confidential, proprietary and/or privileged material exempt from disclosure under applicable law. Any review, retransmission, dissemination or other use of, or taking of any action in reliance upon this information by persons or entities other than the intended recipient is prohibited. If you received this message in error, please contact the sender immediately and destroy any copies of this information in their entirety.

2 1

(no subject)
by abdi mahmud haji 22 Nov '19

22 Nov '19

I was trying to build camkes-vm-crossvm tutorials by using "./init --tut camkes-vm-crossvm" and it initiate some folder with some file and some folder is empty and some are missing.So can someone help me how to fix it,and this the following is it output. ============================================== ./init --tut camkes-vm-crossvm loading initial cache file ../settings.cmake -- The C compiler identification is GNU 5.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 5.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 -- Found musllibc: /home/sel4/sel4-tutorials-manifest/projects/musllibc -- Performing Test compiler_arch_test -- Performing Test compiler_arch_test - Success -- CPIO test cpio_reproducible_flag FAILED -- /home/sel4/sel4-tutorials-manifest/camkes-vm-crossvm_build/camkes-vm-crossvm/ast.pickle is out of date. Regenerating... ERROR:CAmkES:/home/sel4/sel4-tutorials-manifest/camkes-vm-crossvm/crossvm_tutorial.camkes:27:1: } ERROR:CAmkES: ^ ERROR:CAmkES:Syntax error in input at '}' (type _ANON_1) line 34 col 1 CMake Error at tools/camkes/camkes.cmake:494 (message): Failed to generate /home/sel4/sel4-tutorials-manifest/camkes-vm-crossvm_build/camkes-vm-crossvm/ast.pickle Call Stack (most recent call first): camkes-vm-crossvm/CMakeLists.txt:37 (GenerateCAmkESRootserver) -- Configuring incomplete, errors occurred! See also "/home/sel4/sel4-tutorials-manifest/camkes-vm-crossvm_build/CMakeFiles/CMakeOutput.log". Traceback (most recent call last): File "./init", line 96, in <module> File "./init", line 85, in main File "/home/sel4/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 "/home/sel4/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 "/home/sel4/.local/lib/python3.5/site-packages/sh.py", line 1427, in __call__ return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/home/sel4/.local/lib/python3.5/site-packages/sh.py", line 774, in __init__ self.wait() File "/home/sel4/.local/lib/python3.5/site-packages/sh.py", line 792, in wait self.handle_command_exit_code(exit_code) File "/home/sel4/.local/lib/python3.5/site-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 -DFORCE_IOMMU=ON -DTUTORIAL_DIR=camkes-vm-crossvm -C ../settings.cmake .. STDOUT: STDERR: =============================================

2 1

compile camkes_arm_vm project(tx1 vm_minimal), The file format is not correct
by yadong.li 22 Nov '19

22 Nov '19

Hi I compile camkes_arm_vm with tx1 vm_minimal Command: ../init-build.sh -DAARCH64=TRUE -DCAMKES_VM_APP=vm_minimal -DPLATFORM=tx1 Buf output file is not elf # aarch64-linux-gnu-objcopy -O binary images/capdl-loader-image-arm-tx1 sel4-vmm-minimal aarch64-linux-gnu-objcopy:images/capdl-loader-image-arm-tx1: File format not recognized see appendix for the log Thank you very much Log: 1、配置环境 #<mailto:root@HP-Z240:/home/yadong.li/seL4/camkes_arm_vm/build_temp> ../init-build.sh -DAARCH64=TRUE -DCAMKES_VM_APP=vm_minimal -DPLATFORM=tx1 loading initial cache file /home/yadong.li/seL4/camkes_arm_vm/projects/vm/settings.cmake correct_platform_strings: Based on toolchain, setting KernelSel4Arch: aarch64 -- Found seL4: /home/yadong.li/seL4/camkes_arm_vm/kernel …………. -- Found camkes-arm-vm: /home/yadong.li/seL4/camkes_arm_vm/projects/vm -- Found camkes-tool: /home/yadong.li/seL4/camkes_arm_vm/projects/camkes-tool -- Found global-components: /home/yadong.li/seL4/camkes_arm_vm/projects/global-components -- Found camkes-vm: /home/yadong.li/seL4/camkes_arm_vm/projects/camkes-vm -- Found camkes-vm-images: /home/yadong.li/seL4/camkes_arm_vm/projects/camkes-vm-images -- Found sel4_projects_libs: /home/yadong.li/seL4/camkes_arm_vm/projects/seL4_projects_libs -- Found elfloader-tool: /home/yadong.li/seL4/camkes_arm_vm/tools/seL4/elfloader-tool -- Found musllibc: /home/yadong.li/seL4/camkes_arm_vm/projects/musllibc -- Found util_libs: /home/yadong.li/seL4/camkes_arm_vm/projects/util_libs -- Found seL4_libs: /home/yadong.li/seL4/camkes_arm_vm/projects/seL4_libs -- Found projects_libs: /home/yadong.li/seL4/camkes_arm_vm/projects/projects_libs -- Found capdl: /home/yadong.li/seL4/camkes_arm_vm/projects/capdl -- /home/yadong.li/seL4/camkes_arm_vm/build_temp/kernel/gen_headers/plat/machine/devices_gen.h is out of date. Regenerating... -- CPIO test cpio_reproducible_flag PASSED -- Found sel4runtime: /home/yadong.li/seL4/camkes_arm_vm/projects/sel4runtime -- Performing Test compiler_arch_test -- Performing Test compiler_arch_test - Success -- /home/yadong.li/seL4/camkes_arm_vm/build_temp/ast.pickle is out of date. Regenerating... -- /home/yadong.li/seL4/camkes_arm_vm/build_temp/camkes-gen.cmake is out of date. Regenerating... -- Configuring done -- Generating done -- Build files have been written to: /home/yadong.li/seL4/camkes_arm_vm/build_temp 2、编译 #<mailto:root@HP-Z240:/home/yadong.li/seL4/camkes_arm_vm/build_temp> ninja [41/320] Performing CAmkES generation for 15 files [58/320] Generating capDL-tool/parse-capDL stack build --fast Building all executables for `capDL-tool' once. After a successful build of all of them, only specified executables will be rebuilt. capDL-tool-1.0.0.1: configure (exe) Configuring capDL-tool-1.0.0.1... capDL-tool-1.0.0.1: build (exe) Preprocessing executable 'parse-capDL' for capDL-tool-1.0.0.1... [ 1 of 16] Compiling CapDL.Model ( CapDL/Model.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/Model.o ) [ 2 of 16] Compiling CapDL.State ( CapDL/State.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/State.o ) [ 3 of 16] Compiling CapDL.PrintUtils ( CapDL/PrintUtils.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/PrintUtils.o ) [ 4 of 16] Compiling CapDL.PrintC ( CapDL/PrintC.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/PrintC.o ) [ 5 of 16] Compiling CapDL.PrintDot ( CapDL/PrintDot.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/PrintDot.o ) [ 6 of 16] Compiling CapDL.PrintIsabelle ( CapDL/PrintIsabelle.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/PrintIsabelle.o ) [ 7 of 16] Compiling CapDL.PrintModel ( CapDL/PrintModel.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/PrintModel.o ) [ 8 of 16] Compiling CapDL.PrintXml ( CapDL/PrintXml.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/PrintXml.o ) [ 9 of 16] Compiling CapDL.Matrix ( CapDL/Matrix.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/Matrix.o ) [10 of 16] Compiling CapDL.STCC ( CapDL/STCC.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/STCC.o ) [11 of 16] Compiling CapDL.AST ( CapDL/AST.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/AST.o ) [12 of 16] Compiling CapDL.MakeModel ( CapDL/MakeModel.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/MakeModel.o ) [13 of 16] Compiling CapDL.ParserUtils ( CapDL/ParserUtils.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/ParserUtils.o ) [14 of 16] Compiling CapDL.DumpParser ( CapDL/DumpParser.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/DumpParser.o ) [15 of 16] Compiling CapDL.Parser ( CapDL/Parser.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/Parser.o ) [16 of 16] Compiling Main ( Main.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/Main.o ) Linking .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL ... capDL-tool-1.0.0.1: copy/register Installing executable(s) in /home/yadong.li/seL4/camkes_arm_vm/build_temp/capDL-tool/.stack-work/install/x86_64-linux/lts-9.21/8.0.2/bin stack install Copying from /home/yadong.li/seL4/camkes_arm_vm/build_temp/capDL-tool/.stack-work/install/x86_64-linux/lts-9.21/8.0.2/bin/parse-capDL to /home/yadong.li/seL4/camkes_arm_vm/build_temp/capDL-tool/parse-capDL Copied executables to /home/yadong.li/seL4/camkes_arm_vm/build_temp/capDL-tool: - parse-capDL Warning: Installation path /home/yadong.li/seL4/camkes_arm_vm/build_temp/capDL-tool not found on the PATH environment variable. [68/320] Building C object CMakeFiles/vm0.instance.bin.dir/components/VM/src/main.c.obj ………………….. musllibc/build-temp/stage/include/inttypes.h:133:27: note: format string is defined here #define PRIuPTR __PRIPTR "u" [320/320] Generating images/capdl-loader-image-arm-tx1 #file images/capdl-loader-image-arm-tx1 images/capdl-loader-image-arm-tx1: data #arch64-linux-gnu-objcopy -O binary images/capdl-loader-image-arm-tx1 sel4-vmm-minimal aarch64-linux-gnu-objcopy:images/capdl-loader-image-arm-tx1: File format not recognized

2 1

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel November 2019