June 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

TLB issue
by Stefan Kalkowski 15 Nov '19

15 Nov '19

Dear sel4 community, yesterday I've started to develop a low-level platform test to stress several multi-processor aspects on top of the Genode API. Thereby, I've recognized that on sel4/x86_64 the TLB is practically not always cleaned properly in SMP systems. The test spawns threads of one protection domain on each available cpu. Each thread accesses one of the first words of a shared dataspace. Afterwards the main thread on CPU 0 detaches and destroys the dataspace. Unfortunately, the threads on other CPUs still successfully access the corresponding memory instead of triggering a fault. To be able to reproduce the problem, you might investigate the simple test case here: https://github.com/skalk/genode/commit/2d2d7f982555f551227ad5dcbf9df46705d7… My colleague Alexander Boettcher already investigated the problem in part, and might share his insights with you. Best regards Stefan -- Stefan Kalkowski Genode labs https://github.com.skalk | https://genode.org

3 3

Sel4 for quadcore riscv64imafd
by Sreenadh S 03 Oct '19

03 Oct '19

I want to build sel4 for quadcore riscv64imafd and run the test programs, how to do that? Regards, Sreenadh S, CDAC, Trivandrum, India

2 1

seL4_FailedLookup in vmware
by KAP Benjamin 03 Oct '19

03 Oct '19

Hello I set up VMware according to this guide https://docs.sel4.systems/Hardware/VMware/ (using serial output to file) and compiled the picoserver CAmkES application (for x86_64) to run inside the VMware machine. However, I do encounter a seL4_FailedLookup error. I understand the error message but cannot figure out why it occurs nor how to fix it (probably my pci configuration is wrong). Attached you find the serial_output file. For the ethernet configuration I used linux in the same VM to figure out the details: 1) ip addr: 2: ens32: <BROADCAST,MULTICAST,UP,LOWER_UP> mtu 1500 qdisc fq_codel state UNKNOWN group default qlen 1000 link/ether 00:0c:29:90:a7:4a brd ff:ff:ff:ff:ff:ff 2) lspci -vvv: 02:00.0 Ethernet controller: Advanced Micro Devices, Inc. [AMD] 79c970 [PCnet32 LANCE] (rev 10) Subsystem: Advanced Micro Devices, Inc. [AMD] PCnet - Fast 79C971 Physical Slot: 32 Control: I/O+ Mem+ BusMaster+ SpecCycle- MemWINV- VGASnoop- ParErr- Stepping- SERR- FastB2B- DisINTx- Status: Cap- 66MHz- UDF- FastB2B+ ParErr- DEVSEL=medium >TAbort- <TAbort- <MAbort- >SERR- <PERR- INTx- Latency: 64 (1500ns min, 63750ns max) Interrupt: pin A routed to IRQ 18 Region 0: I/O ports at 2000 [size=128] [virtual] Expansion ROM at fd500000 [disabled] [size=64K] Kernel driver in use: pcnet32 Kernel modules: pcnet32 3) dmesg | grep "02:00.0": ... [ 0.378516] pci 0000:02:00.0: BAR 6: assigned [mem 0xfd500000-0xfd50ffff pref] ... 4) lspci -nn: 02:00.0 Ethernet controller [0200]: Advanced Micro Devices, Inc. [AMD] 79c970 [PCnet32 LANCE] [1022:2000] (rev 10) And here the configuration part inside picoserver.camkes (anything else NOT pasted here is unmodified): picoserver.ethdriver_mac = [0x00, 0x0c, 0x29, 0x90, 0xa7, 0x4a]; .... hwethdriver.mmio_paddr = 0xfd500000 hwethdriver.mmio_size = 0x10000 hwethdriver.irq_irq_type = "pci"; hwethdriver.irq_irq_ioapic = 0; hwethdriver.irq_irq_ioapic_pin = 18; hwethdriver.irq_irq_vector = 18; ethdriver.iospaces = "0x0:0x02:0x00:0"; ethdriver.iospace_id = 0x0200; ethdriver.pci_bdf = "0x02:0x00.0"; I am sorry to bother you with this; I am fairly new to low level stuff. Any help would be very much appreciated. Best regards, Benjamin

2 1

Understanding Camkes Dataport Interface Access Rights
by Amit Goyal 03 Jul '19

03 Jul '19

Hi All, I was looking at hello-camkes-2 tutorial. I understand the concept of dataports and the access rights given on dataport interfaces. I changed the configuration in hello-camkes-2.camkes.template file by adding echo.d = "R"; client.d = "W";. I did some changes in the client.c.template file to read on the dataport interface d by trying to access its contents through str/n/d pointers. Although, it only has write access on "d" in the new configuration. This leads to the fault handler being called when I simulate the build. I was just curious to find out where are such checks being done at the backend in camkes/seL4. I could find the code of fault handler in component.template.c but I could not find anywhere the code which checks that the client only has write access on dataport d and thus calling the fault handler. Can someone point me towards that piece of code or explain what is exactly happening at the backend in camkes/seL4? -- Thanks and Regards, Amit Goyal

4 4

Beaglebone Black: failed to find device frame
by KAP Benjamin 29 Jun '19

29 Jun '19

Hello I am trying to add am335x support to the pico TCP/IP stack and currently working on the following file: projects/global-components/components/Ethdriver/include/plat/am335x/plat/eth_devices.h. Current contents of this file (I am creating it step by step, thus it might be incomplete): #pragma once #define HARDWARE_ETHERNET_COMPONENT #define HARDWARE_ETHERNET_INTERFACES \ consumes Dummy EthDriver; \ emits Dummy dummy_source; #define HARDWARE_ETHERNET_COMPOSITION \ connection seL4DTBHardware ethernet_conn(from dummy_source, to EthDriver); #define HARDWARE_ETHERNET_CONFIG \ EthDriver.dtb = dtb({ "path" : "/ocp/ethernet@4a100000" }); \ EthDriver.generate_interrupts = 1; I test the implementation by using the picoserver CAmkES application. However, on boot I receive the following error: ELF-loader started on CPU: ARM Ltd. Cortex-A8 r3p2 paddr=[82000000..8262e037] No DTB found! Looking for DTB in CPIO archive... Found dtb at 820c1b84 Loaded dtb from 820c1b84 paddr=[80034000..8003cfff] ELF-loading image 'kernel' paddr=[80000000..80033fff] vaddr=[f0000000..f0033fff] virt_entry=f0000000 ELF-loading image 'capdl-loader' paddr=[8003d000..8059afff] vaddr=[10000..56dfff] virt_entry=1e4dc ELF loader relocated, continuing boot... Enabling MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Booting all finished, dropped to user space create_object@main.c:726 device frame/untyped, paddr = 0x48040000, size = 12 bits create_object@main.c:726 device frame/untyped, paddr = 0x48042000, size = 12 bits create_object@main.c:726 device frame/untyped, paddr = 0x4a100000, size = 12 bits create_object@main.c:726 device frame/untyped, paddr = 0x4a101200, size = 12 bits create_object@main.c:730 [Cond failed: err != seL4_NoError] Failed to find device frame/untyped at paddr = 0x4a101200 seL4 root server abort()ed Debug halt syscall from user thread 0xffefd600 "rootserver" halting... Kernel entry via Unknown syscall, word: 65 The am335x.dtb contains the following line in ethernet@4a100000: reg = <0x4a100000 0x00000800 0x4a101200 0x00000100>; I did find related posts (http://sel4.systems/pipermail/devel/2016-June/000850.html, http://sel4.systems/pipermail/devel/2018-July/002031.html and http://sel4.systems/pipermail/devel/2015-October/000530.html) but didn't help me that much.<http://sel4.systems/pipermail/devel/2018-July/002031.html)> If I am correct the hardware block isn't enabled but I don't know exactly how to do this. Could anyone help me out here or give me some hints? Best Regards, Kap Benjamin

3 7

seL4 devs
by James Rolevink 25 Jun '19

25 Jun '19

Hey, guys. After getting it up and running a while back, just wondering: are there any (good) seL4 app devs for hire? Engineer partner-in-crime is looking to develop apps for a smart device. Physically based in Adelaide. Cheers, James Rolevink –––––––––––––––––––––––––––––––––––––––– M: 04123 62 432 E: cybercitadel(a)icloud.com <mailto:james@cybercitadel.co> W: www.cybercitadel.co <https://www.cybercitadel.co/> L: james-r-53986189 <https://www.linkedin.com/in/james-r-53986189/> Cyber Citadel Pty Ltd ACN: 622 880 657

1 0

CMake Error
by Amit Goyal 25 Jun '19

25 Jun '19

Hi, Camkes had been working fine till now. Suddenly, it stopped working. I am running it on x86 system (i7 processor), ubuntu 16.04 on qemu. I am running the following commands: mkdir build cd build ../init --plat pc99 --tut hello-camkes-2 --solution Following error is generated: --------------------------------------------------------------------------------------------------------------------------------- Traceback (most recent call last): File "../init", line 76, in <module> sys.exit(main()) File "../init", line 62, in main result = common.init_build_directory(args.plat, args.tut, args.solution, os.getcwd()) File "/home/goyal/sel4/camkes-tutorials-manifest/projects/sel4-tutorials/common.py", line 59, in init_build_directory result = sh.cmake(args + ['..'], _cwd = directory, _out=output) File "/usr/local/lib/python2.7/dist-packages/sh.py", line 1427, in __call__ return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/uTraceback (most recent call last): File "../init", line 76, in <module> sys.exit(main()) File "../init", line 62, in main result = common.init_build_directory(args.plat, args.tut, args.solution, os.getcwd()) File "/home/goyal/sel4/camkes-tutorials-manifest/projects/sel4-tutorials/common.py", line 59, in init_build_directory result = sh.cmake(args + ['..'], _cwd = directory, _out=output) File "/usr/local/lib/python2.7/dist-packages/sh.py", line 1427, in __call__ return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/usr/local/lib/python2.7/dist-packages/sh.py", line 774, in __init__ self.wait() File "/usr/local/lib/python2.7/dist-packages/sh.py", line 792, in wait self.handle_command_exit_code(exit_code) File "/usr/local/lib/python2.7/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=hello-camkes-2 -DBUILD_SOLUTIONS=TRUE .. STDOUT: -- Configuring incomplete, errors occurred! STDERR: CMake Error at /opt/cmake-3.11.0-Linux-x86_64/share/cmake-3.11/Modules/CMakeDetermineSystem.cmake:100 (message): Could not find toolchain file: ../kernel/gcc.cmake Call Stack (most recent call first): CMakeLists.txt CMake Error: CMake was unable to find a build program corresponding to "Ninja". CMAKE_MAKE_PROGRAM is not set. You probably need to select a different build tool. CMake Error: CMAKE_C_COMPILER not set, after EnableLanguage CMake Error: CMAKE_CXX_COMPILER not set, after EnableLanguage --------------------------------------------------------------------------------------------------------------------------------- Can you please suggest a possible way out? -- Thanks and Regards, Amit Goyal

5 8

Checking if an endpoint is a badged version of another
by Demi Obenour 15 Jun '19

15 Jun '19

I have a server process SB that issues badged endpoints to users. Clients can invoke the endpoints to access memory and possibly other resources. Essentially, it is a version of Robigalia’s space bank. Other programs pass endpoints issued by SB to provide servers the resources needed to do their tasks, and the servers invoke the endpoints to obtain memory that they know cannot be revoked or modified by other programs. SB is part of the TCB, and is trusted by all of its clients. Clients, however, do not trust each other, and may pass forged endpoints to servers to cause servers to misbehave. Therefore, servers need to be able to ask SB if a given capability was actually issued by SB. SB can make that check by checking that the endpoint is a badged version of its master endpoint, which it never gives anyone else access to. What is the correct API function for doing this? Sincerely, Demi M. Obenour

2 1

Re: [seL4] Checking if an endpoint is a badged version of another
by Millar, Curtis (Data61, Kensington NSW) 15 Jun '19

15 Jun '19

Hi Demi, Any time you perform an seL4_Call operation on an endpoint and block waiting for a reply you are trusting that endpoint in a variety of ways. You trust that the messages will eventually get a reply and allow you to resume. You also trust that the message will eventually be received. If you want to perform an seL4_Call on an untrusted endpoint you will require a monitor thread that can handle a timeout and reset the calling thread if it is still blocked. In general, you want to avoid using endpoints where you can't trust that the message will be received and replied to in a timely manner. Asynchronous notifications do not suffer from this trust requirement so it is recommended that communication between mutually distrusting servers use shared memory and notifications. The client should seL4_Signal the server to notify a message has been sent via the shared memory and the server should signal in response to notify the client the message has been handled and the reply is in the shared memory. The problem of setting up a connection, sending the reply badged notification object to the server, acquiring a send notification object from the server, and mapping the shared memory would require either the connection being statically configured at process creation or dynamically configured by some mutually trusted shared component. Cheers, Curtis

1 0

Re: [seL4] camkes error.h include problem
by yogidk . 14 Jun '19

14 Jun '19

sorry, previous email sent by mistake. #include "sys/socket.h" actually solved the problem instead of only "socket.h" many thanks. Regards yk On Fri, Jun 14, 2019 at 10:30 AM yogidk . <yogidk(a)gmail.com> wrote: > thanks Kent and Peter, > > however if I remove > > > On Fri, Jun 14, 2019 at 2:14 AM Mcleod, Kent (Data61, Kensington NSW) < > Kent.Mcleod(a)data61.csiro.au> wrote: > >> > "../muslibc/include/sys"* // necessary for compilation as >> test_2.c has "socket.h"* >> This line shouldn't be here, and instead socket.h should be included via >> <sys/socket.h>. Otherwise many other include directives are going to match >> on the incorrect files. >> >> Kent. >> ------------------------------ >> *From:* Devel <devel-bounces(a)sel4.systems> on behalf of Chubb, Peter >> (Data61, Kensington NSW) <Peter.Chubb(a)data61.csiro.au> >> *Sent:* Friday, 14 June 2019 8:03 AM >> *To:* yogidk . >> *Cc:* devel(a)sel4.systems >> *Subject:* Re: [seL4] camkes error.h include problem >> >> >>>>> "yogidk" == yogidk <yogidk(a)gmail.com> writes: >> >> yogidk> and another file >> >> yogidk> test_2.c which includes "socket.h" >> >> yogidk> DeclareCAmkESComponent(test >> yogidk> INCLUDES "../muslibc/include/sys"* // necessary for >> yogidk> compilation as test_2.c has "socket.h"* >> >> This line means that "#include <errno.h>" picks up sys/errno.h instead >> of errno.h. >> >> Get rid of it. Instead, do '#include <sys/socket.h> instead of >> '#include <socket.h>' >> >> Peter C >> -- >> Dr Peter Chubb Tel: +61 2 9490 5852 >> http://ts.data61.csiro.au/ >> Trustworthy Systems Group Data61, CSIRO (formerly >> NICTA) >> _______________________________________________ >> Devel mailing list >> Devel(a)sel4.systems >> https://sel4.systems/lists/listinfo/devel >> >

1 0

camkes error.h include problem
by yogidk . 14 Jun '19

14 Jun '19

Hi , I have a test_1.c file which includes <camkes.h> camkes.h which is automatically generated has following includes #include <camkes/dataport.h> #include <camkes/error.h> #include <stdint.h> #include <stdlib.h> #include <utils/util.h> #include <platsupport/io.h> and another file test_2.c which includes "socket.h" In CMakeLists.txt, where I compile my test_1.c and test_2.c looks like this DeclareCAmkESComponent(test INCLUDES "../muslibc/include/sys"* // necessary for compilation as test_2.c has "socket.h"* SOURCES "test_1.c" "test_2.c" C_FLAGS -Wall -Werror LIBS seos_libs ) However when I compile , I start getting these errors: In file included from ../projects/util_libs/libplatsupport/include/platsupport/io.h:20:0, from projects/test/include/camkes.h:20, from ../projects/src/test_1.c:8: ../projects/musllibc/include/sys/errno.h:1:2: error: #warning redirecting incorrect #include <sys/errno.h> to <errno.h> [-Werror=cpp] *#warning redirecting incorrect #include <sys/errno.h> to <errno.h>* ^~~~~~~ In file included from ../projects/musllibc/include/sys/errno.h:2:0, from ../projects/util_libs/libplatsupport/include/platsupport/io.h:20, from projects/test/include/camkes.h:20, from ../projects/src/test_1.c:8: ../projects/musllibc/include/sys/errno.h:1:2: error: #warning redirecting incorrect #include <sys/errno.h> to <errno.h> [-Werror=cpp] #warning redirecting incorrect #include <sys/errno.h> to <errno.h> How could this be solved ? thanks --yk

3 2

Roadmap - Status
by Rutherford, Luke 08 Jun '19

08 Jun '19

I see these on your development road map. Any updates on the status of them? Development Roadmap Microkernel in progress 64-bit ARM virtualisation support branch Low-level Userland Status Date Feature Location planned SMP-capable virtual-machine monitor (VMM) master

3 2

Re: [seL4] xilinx ultrascale+: Spurious interrupt
by Shen, Yanyan (Data61, Kensington NSW) 05 Jun '19

05 Jun '19

Hi Leonid, One possible cause I can think of is the trigger type (level vs edge) of an interrupt is incorrect. The Linux device tree should have interrupt type for each interrupt source, so you can change the GIC init code to configure the interrupt types (GICD_ICFGR, assuming GICv2) accordingly and see if the messages disappear. Regards, Yanyan From: Devel <devel-bounces(a)sel4.systems> on behalf of Leonid Meyerovich <lmeyerovich(a)i-a-i.com> Date: Wednesday, 5 June 2019 at 4:28 am To: "devel(a)sel4.systems" <devel(a)sel4.systems> Subject: [seL4] xilinx ultrascale+: Spurious interrupt Hello Everybody, Petalinux is running on VM on the one of the core of Xilinx Ultrascale+ (A53) From time to time I see Spurious Interrupt message from seL4 kernel (handleInterruptEntry) <<seL4(CPU 1) [handleInterruptEntry/54 T0xff805da00400 "vm core" @ffffff80080fa414]: Spurious interrupt!>> <<seL4(CPU 1) [handleInterruptEntry/54 T0xff805da00400 "vm core" @ffffff80083e64bc]: Spurious interrupt!>> <<seL4(CPU 1) [handleInterruptEntry/54 T0xff805da00400 "vm core" @ffffff800894cc98]: Spurious interrupt!>> Could somebody explain why it may happen? How to debug it? Thank you, Leonid ________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.

1 0

xilinx ultrascale+: Spurious interrupt
by Leonid Meyerovich 05 Jun '19

05 Jun '19

Hello Everybody, Petalinux is running on VM on the one of the core of Xilinx Ultrascale+ (A53) >From time to time I see Spurious Interrupt message from seL4 kernel (handleInterruptEntry) <<seL4(CPU 1) [handleInterruptEntry/54 T0xff805da00400 "vm core" @ffffff80080fa414]: Spurious interrupt!>> <<seL4(CPU 1) [handleInterruptEntry/54 T0xff805da00400 "vm core" @ffffff80083e64bc]: Spurious interrupt!>> <<seL4(CPU 1) [handleInterruptEntry/54 T0xff805da00400 "vm core" @ffffff800894cc98]: Spurious interrupt!>> Could somebody explain why it may happen? How to debug it? Thank you, Leonid ________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.

1 0

回复: Devel Digest, Vol 60, Issue 18
by KIM MK 03 Jun '19

03 Jun '19

Hello Sel4 developer, Thanks for your support. Aditya and me are debugging physical memory sel4. Is there visual tool or analysis module or anything to debugging that physical memory to virtual mapping table. If you have any question, please let me know. BR, MK

2 2