December 2019 - Devel - lists.sel4.systems

seL4 test on x86
by Yevgeny Lavrov 30 Jan '25

30 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 16 Oct '24

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

Using seL4_DebugSnapshot()
by rasd＠riseup.net 09 Jan '20

09 Jan '20

Can someone provide more information about using seL4_DebugSnapshot? >From its description in documentation, I would expect it to print out a CapDL struct over a debugging port/console. Instead, it waits for user commands for various data types sends back binary data[0]. Since the commands are all 0xa0-0xff[1], it doesn't seem like DebugSnapshot expects a human and a keyboard to be present on the other end. Is there some internal debugging tool that is supposed to be used with this system call? Is DebugSnapshot still used? Any advice or information is appreciated. ras [0] https://github.com/seL4/seL4/blob/master/src/arch/arm/32/machine/capdl.c [1] https://github.com/seL4/seL4/blob/master/include/machine/capdl.h

2 1

答复: some question about the compile of global-components in camkes_arm_vm project
by yadong.li 09 Jan '20

09 Jan '20

I found some example in odroid_vm, I want to make sure my understanding is correct? In CMakeLists.txt DeclareCAmkESComponent(HelloWorld) is just tell me there is a component called “HelloWorld” If you want this component to be compiled to project You must add call in your assembly in .cmakes file like below: assembly { composition { component HelloWorld hello; } Thank you very much 发件人: yadong.li 发送时间: 2019年12月28日 15:32 收件人: 'devel(a)sel4.systems' 主题: some question about the compile of global-components in camkes_arm_vm project hi， I have some question about the compile of global-components in camkes_arm_vm project. 1、In projects/global-components/components, there are some directory include FileServer, SerialServer, TimeServer and the others. I found FileServer had been compiled to project， but the other directory have not been compiled Is there some on-off switch control the compile ？ But I did not find it. 2、The CAmkES of FileServer component did not have a "int run(void) {}, If I want to add an new component with run entry， but it is not rootserver（I think one project only have one rootserver），it run with vm rootserver parallelly？ what should I do ？ Is there some example. Thank you very much

2 1

Error while building in docker
by Edward Sandberg 09 Jan '20

09 Jan '20

This morning I saw this error when building sel4: /bin/sh: 1: PROTOBUF_PROTOC_EXECUTABLE-NOTFOUND: not found I noticed a warning when starting the docker container about trustworthysystems/camkes:latest being over 30 days old. I thought that using an up to date pull of: https://github.com/SEL4PROJ/seL4-CAmkES-L4v-dockerfiles.git would keep the build env up to date but that apparently is either not the case or there is a problem with the repo. I ran: docker pull trustworthysystems/camkes and the warning was resolved and I could build seL4. Is pulling that docker image supposed to be necessary? Thanks! -- Edward Sandberg Adventium Labs 111 3rd Avenue S. Suite #100 Minneapolis, MN 55401 ed.sandberg(a)adventiumlabs.com

2 1

Understand seL4 x86_64 Kernel ABI calling convention
by Alexandre Mutel 03 Jan '20

03 Jan '20

Hello! While looking at the code base and checking generated code, I'm not sure about the pertinence of having a different ABI from user System V ABI for kernel calls, as it is implying a bit more unnecessary register shuffling, and I was wondering why this choice was made to have r10, r8, r9, r15? instead of keeping System V ABI and just replace rcx by r10 as it is discarded by syscall: SystemVABI_x86_64_user: rdi, rsi, rdx, rcx, r8, r9 SystemVABI_x86_64_Linux_kernel: rdi, rsi, rdx, r10, r8, r9 SystemVABI_x86_64_seL4: rdi, rsi, r10, r8, r9, r15 So on a Linux Kernel, only the register rcx will be transferred to r10 (when transitioning from user to syscall), but in seL4, it has to reshuffle arguments rdx to r9. (Note for context: I'm working on a project where I don't use a standard C compiler to interface with the seL4 Kernel API, and where the register allocator of the compiler might not be as efficient as GCC/CLang after everything is inlined, that's why I'm looking into these details)

1 1

Hardware-aided Trusted Computing devroom at FOSDEM
by Vasily A. Sartakov 01 Jan '20

01 Jan '20

Hello I would like to invite your to participate in a new devroom: Hardware-aided Trusted Computing. The devroom is devoted to open source projects on top of modern TEEs like Intel SGX, AMD SEV/SVE, Arm TrustZone. You can find the schedule here: https://fosdem.org/2020/schedule/track/hardware_aided_trusted_computing/ I hope this will be interesting for the community. See you at FOSDEM. -- Dr.-Eng. V. A. Sartakov

2 1

some question about the compile of global-components in camkes_arm_vm project
by yadong.li 28 Dec '19

28 Dec '19

hi， I have some question about the compile of global-components in camkes_arm_vm project. 1、In projects/global-components/components, there are some directory include FileServer, SerialServer, TimeServer and the others. I found FileServer had been compiled to project， but the other directory have not been compiled Is there some on-off switch control the compile ？ But I did not find it. 2、The CAmkES of FileServer component did not have a "int run(void) {}, If I want to add an new component with run entry， but it is not rootserver（I think one project only have one rootserver），it run with vm rootserver parallelly？ what should I do ？ Is there some example. Thank you very much

1 0

Camkes Project on Sabre Lite i.mx6 board
by Parvaneh Ahgajani 19 Dec '19

19 Dec '19

Hello all, I am trying to have my own seL4 demo on Sabre Lite board. I am using this command to create the image file: ../init-build.sh -DPLATFORM=sabre -DCROSS_COMPILER_PREFIX=arm-linux-gnueabi- -DCAMKES_APP=adder After that I run this commands to boot the image: fatload mmc 1 0x41000000 adder(image file) The bootm command gives this error: Wrong Image Format for bootm command ERROR: can't get kernel image! I tried bootelf but it stuck and does not show the correct answer: bootelf 0x41000000 CACHE: Misaligned operation at range [10598000, 105980a4] CACHE: Misaligned operation at range [10599000, 105a3434] CACHE: Misaligned operation at range [105a3434, 105a3c23] CACHE: Misaligned operation at range [107fc000, 1080a038] ## Starting application at 0x10598000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A9 r2p10 paddr=[10598000..1080a037] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 1069c064. Loaded DTB from 1069c064. paddr=[10038000..10042fff] ELF-loading image 'kernel' paddr=[10000000..10037fff] vaddr=[e0000000..e0037fff] virt_entry=e0000000 ELF-loading image 'capdl-loader' paddr=[10043000..1019bfff] vaddr=[10000..168fff] virt_entry=188dc ELF loader relocated, continuing boot... Enabling MMU and paging It seems It does not go to kernel-image entry point and bootstrap the kernel! Is there any thing that I need to perform on board? Thank you, Parvaneh Aghajani.

2 1