September 2019 - Devel - lists.sel4.systems

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

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

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

Re: [seL4] CapDL output to isabelle file
by Lim, Japheth (Data61, Kensington NSW) 04 Oct '19

04 Oct '19

Hi Norrathep, Norrathep Rattanavipanon wrote: > I have been trying to generate Isabelle file from CapDL specification. But > I run into an error when I'm running the command: > > ./parse-capDL --isabelle=out.thy --object-sizes=object_sizes.yaml > example-arm.cdl > We recently put in a major change to the Isabelle translator. The input capDL file is now required to be pre-allocated, i.e. every object must be placed in an untyped with a known physical address. The existing example files date from before this change, and so they don't meet the requirements to be translated into Isabelle. Sorry that you got confusing error messages as a result. We plan to make this more consistent in the near future. > Is there any step I'm missing? Or does the tool not support the conversion > to Isabelle? The standard way is to build a CAmkES application with the option `CAmkESCapDLStaticAlloc` enabled. This will generate a suitable capDL file for proofs. Based on your other question thread, you may be interested in our README for CAmkES proofs: https://github.com/seL4/camkes-tool/tree/master/cdl-refine-tests This generates proofs between the CAmkES high-level model and the capDL system representation. However, we are not working on C glue code proofs at the moment. This is all work in progress, and quite rough around the edges. Nevertheless, we're happy to try to answer any questions you might have. It would help if we knew more about your work, so that we can give more specific replies. Cheers, Japheth Lim Proof Engineer, Trustworthy Systems

3 5

Initialising Camkes App before another dependent Camkes app
by yogidk . 03 Oct '19

03 Oct '19

Hi, I have a Camkes app (app1) which depends on another Camkes app (app2), which means my app1 must start only after app2 is completely initialized. For this currently I use a signal RPC wait in app1 and the corresponding RPC emit from app2 after app2 is completely initialized. Is there any other way in CamkES which will ensure that app1 starts only after app2 is completely initialized without using RPC signalling (emit and wait) ? How can this dependency be built ? Regards yk

3 2

Run VM guest on seL4 using CAmkEs
by Khalid Amen 03 Oct '19

03 Oct '19

Hello, I am trying to run VM guest on seL4 using CAmkEs. I have setup my linux machine and installed dependencies. I have run seL4 hello world example. What do I need to do run VM guest in seL4? I have serached online to see. The documentation says that to create VM guests and applications on seL4, I need to use CAmkES. I followed this link: https://docs.sel4.systems/Tutorials/camkes-vm-linux.html. What do I need to create VM on top of seL4 using CAmkES? Also, I want seL4 to run as hypervisor. I have found a tutorial on how to run it from these links. https://github.com/seL4/camkes-vm-examples/blob/master/README.md https://docs.sel4.systems/Tutorials/camkes-vm-linux But, I did not understand the following: You can boot the tutorial on an x86 hardware platform with a multiboot boot loader, or use the QEMU <https://www.qemu.org/> simulator. *Note if you are using QEMU it is important to ensure that your host machine has VT-x support and KVM <https://www.linux-kvm.org/page/Main_Page> installed. You also need to ensure you have enabled nested virtulisation with KVM guests as described here <https://www.linux-kvm.org/page/Nested_Guests>.* After building is completed with ninja, how do I excute the following: Then boot images/kernel-x86_64-pc99 and images/capdl-loader-experimental-image-x86_64-pc99 (or *.ia32-pc99 if built for 32-bit) with the multiboot boot loader of your choice. -- Regards, Khalid Ameen

2 1

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

Adding an Extra Component in Camkes
by Amit Goyal 03 Oct '19

03 Oct '19

Hi, I was trying to add an extra component in hello-camkes-1 example. Here are the small tweaks that I did. a) hello-camkes-1-camkes.template import <std_connector.camkes>; import "components/Client1/Client1.camkes"; import "components/Client2/Client2.camkes"; import "components/Echo/Echo.camkes"; assembly { composition { component Client1 client1; component Client2 client2; component Echo echo; connection seL4RPC hello_con(from client1.hello1, to echo.hello2); } } -------------------------------------------------------------------------------------------------------------------------- b) CMakeLists.text cmake_minimum_required(VERSION 3.7.2) project(hello-camkes-1 C) DeclareTutorialsCAmkESComponent(Client TEMPLATE_SOURCES components/Client1/src/client1.c) DeclareTutorialsCAmkESComponent(Client TEMPLATE_SOURCES components/Client2/src/client2.c) DeclareTutorialsCAmkESComponent(Echo TEMPLATE_SOURCES components/Echo/src/echo.c) DeclareCAmkESComponent(EmptyComponent) DeclareTutorialsCAmkESRootserver(hello-camkes-1.camkes ADL_IS_TEMPLATE TEMPLATE_SOURCES interfaces/HelloSimple.camkes TUTORIAL_SOURCES components/Client1/Client1.camkes components/Client2/Client2.camkes components/Echo/Echo.camkes ) ------------------------------------------------------------------------------------------------------------------------ I am getting the following error: STDERR: CMake Warning at tools/seL4/cmake-tool/flags.cmake:123 (message): Kernel supports hardware floating point but toolchain does not Call Stack (most recent call first): tools/seL4/cmake-tool/base.cmake:58 (include) tools/seL4/cmake-tool/all.cmake:16 (include) CMakeLists.txt:21 (include) CMake Error at build/projects/sel4-tutorials/camkes-gen.cmake:192 (target_link_libraries): Error evaluating generator expression: $<TARGET_PROPERTY:CAmkESComponent_Client1,COMPONENT_LIBS> Target "CAmkESComponent_Client1" not found. Call Stack (most recent call first): tools/camkes/camkes.cmake:591 (include) projects/sel4-tutorials/CMakeLists.txt:257 (GenerateCAmkESRootserver) CMake Error at build/projects/sel4-tutorials/cam... (2531 more, please see e.stderr) ----------------------------------------------------------------------------------------------------------------- Can you please suggest a possible solution. -- Thanks and Regards, Amit Goyal

2 1