January 2023 - 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

Re: U-boot for Raspberry PI
by Michal Podhradsky 08 Feb '23

08 Feb '23

Hello, thank you for prompt replies! I used the default U-boot, however now I am stuck in the next phase of booting - specifically loading and booting the sel4 test image. Following the instructions in the docs ( https://docs.sel4.systems/Hardware/Rpi4.html) I do: *U-Boot> fatload mmc 0 0x10000000 sel4test-driver-image-arm-bcm2711** Reading file would overwrite reserved memory **Failed to load 'sel4test-driver-image-arm-bcm2711* Which is odd. Perhaps the memory map on Rpi has changed recently? Picking another memory location gets me further (although it is unclear that it is a correct location): *U-Boot> fatload mmc 0 0x00008000 sel4test-driver-image-arm-bcm27115164988 bytes read in 235 ms (21 MiB/s)U-Boot> bootefi 0x00008000* Now, the image gets loaded but the boot fails with an seL4 assertion fail: *U-Boot> bootefi 0x00008000Card did not respond to voltage select! : -110No EFI system partitionBooting /sel4test-driver-image-arm-bcm2711ELF-loader started on CPU: ARM Ltd. Cortex-A72 r0p3 paddr=[6603000..ffffffffffffffff] dtb=6af2000Looking for DTB in CPIO archive...found at 674d958.Loaded DTB from 674d958. paddr=[123f000..1245fff]ELF-loading image 'kernel' to 1000000 paddr=[1000000..123efff] vaddr=[ffffff8001000000..ffffff800123efff] virt_entry=ffffff8001000000ELF-loading image 'sel4test-driver' to 1246000 paddr=[1246000..164bfff] vaddr=[400000..805fff] virt_entry=40ef20Enabling MMU and pagingJumping to kernel-image entry point...Bootstrapping kernelavailable phys memory regions: 3 [1000000..3b400000] [40000000..fc000000] [100000000..200000000]reserved virt address space regions: 3 [ffffff8001000000..ffffff800123f000] [ffffff800123f000..ffffff800124556b] [ffffff8001246000..ffffff800164c000]Booting all finished, dropped to user spaceseL4 failed assertion 'isSchedulable(candidate)' at /tmp/kernel/src/kernel/thread.c:371 in function schedulehalting...Kernel entry via Interrupt, irq 0* Any suggestions what am I missing? Regards Michal On Thu, Jan 19, 2023 at 5:53 PM Sudvarg, Marion <msudvarg(a)wustl.edu> wrote: > I have a version of U-boot that works. I would have to go back through > piles of notes to see what I did to make it work, but I can share the file > with you if it's helpful. > > I also had to change config.txt to set the GPU and coprocessor frequency > to a fixed value; I had issues with boot (which is handled by the GPU) and > UART without that. > > Happy to help with the process if you like. > > Marion Sudvarg > Washington University in St. Louis > > -----Original Message----- > From: mpodhradsky(a)galois.com <mpodhradsky(a)galois.com> > Sent: Thursday, January 19, 2023 7:02 PM > To: devel(a)sel4.systems > Subject: [seL4] U-boot for Raspberry PI > > Hello! > > The instructions for building seL4 for Raspberry Pi 3 and 4 mention ask > for a custom compiled U-boot. The note mentions that an automatic revert of > the specified commit no longer works. Is this patched U-boot still > necessary, or will a vanilla version work? If the customization is still > needed, do you have a modified version available? It is not clear how to > modify the recent U-boot, since it has changed significantly. > > Regards > Michal > _______________________________________________ > Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email to > devel-leave(a)sel4.systems >

4 5

kernel builds w/ different memory configurations
by Sam Leffler 27 Jan '23

27 Jan '23

I have a target platform w/ 2 pre-defined memory configs. I've created separate .dts files w/ the different memory sizes and then in src/plat/sparrow/config.cmake do: if(KernelDebugBuild) list(APPEND KernelDTSList "tools/dts/sparrow-debug.dts") else() list(APPEND KernelDTSList "tools/dts/sparrow.dts") Overloading KernelDebugBuild is awkward (it seems contrary to it's purpose) and fragile. How is this handled for existing platforms? -Sam

2 2

help with Nvidia Jetson Xavier port
by Axel Heider 27 Jan '23

27 Jan '23

Hi, we are working on porting seL4 to the Nvidia Jetson Xavier. The kernel is booting, but then there are random crashes in user mode where the cores seem to stop completely within a minute, no crash output is visible. Our test applications are just doing some integer number crunching to create load, there are no drivers involved (besides a bit of UART output). It looks like this also happened to others, a similar problem was described in this post: https://forums.developer.nvidia.com/t/illegal-instruction-with-i-cache-disa… Did anybody get seL4 userland running stable there? Axel

1 0

Inquiry to Verified Components
by Seoyeon Hwang 26 Jan '23

26 Jan '23

Hello, From this document https://apps.dtic.mil/sti/pdfs/AD1027690.pdf <https://urldefense.com/v3/__https://apps.dtic.mil/sti/pdfs/AD1027690.pdf__;…>, we figured out that system call APIs are verified (except for their composition with sel4 kernel proofs). However, we are not sure whether other process/thread-spawning APIs are also verified. We use the APIs (listed below) in our project, hoping to develop a formally verified root-of-trust architecture atop seL4. Could you let us know if they are all verified, and if so, could you also point out the resources we can cite in our paper? Thanks, Seoyeon APIs used in our projects are: Initial Process-related APIs platsupport_get_bootinfo simple_default_init_bootinfo bootstrap_use_current_simple allocman_make_vka simple_get_cnode simple_get_pd Thread Spawning APIs vka_alloc_tcb vka_alloc_frame seL4_ARCH_Page_Map vka_alloc_page_table seL4_ARCH_PageTable_Map vka_alloc_endpoint vka_mint_object seL4_TCB_Configure seL4_TCB_SetPriority sel4utils_set_instruction_pointer sel4utils_set_stack_pointer seL4_TCB_WriteRegisters sel4runtime_write_tls_image sel4runtime_set_tls_variable seL4_TCB_SetTLSBase seL4_TCB_Resume Process Spawning APIs sel4utils_bootstrap_vspace_with_bootinfo_leaky vspace_reserve_range bootstrap_configure_virtual_pool process_config_default_simple sel4utils_configure_process_custom vka_cspace_make_path sel4utils_mint_cap_to_process sel4utils_create_word_args sel4utils_spawn_process_v IPC/System call APIs seL4_MessageInfo_new seL4_MessageInfo_get_length seL4_SetMR seL4_GetMR seL4_Call seL4_Recv seL4_Reply seL4_Wait seL4_Yield

7 10

sel4test:nested timeout fault test flaky?
by Sam Leffler 25 Jan '23

25 Jan '23

We run sel4test regularly for a 64-bit raspi target under qemu and occasionally see failures like this: Starting test 129: TIMEOUTFAULT0003 > Running test TIMEOUTFAULT0003 (Nested timeout fault) > Error: Check badge(3) == expected_badge(2) failed. at line 9 This is a stock sel4test <https://github.com/AmbiML/sparrow-sel4test> + dep libs but an older kernel <https://github.com/AmbiML/sparrow-kernel>. Anyone know if this is an old (presumably fixed) bug or known issue? -Sam

3 5

Reminder seL4 developer hangout
by Birgit Brecknell 25 Jan '23

25 Jan '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Tue, Jan 24, 9pm (UTC), Topics: (open) * Sydney: Wed, Jan 25, 8am * Central Europe: Tue, Jan 24, 10pm * US Pacific Time: Tue, Jan 24, 1pm Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

3 2

Sel4 on RISC-V AllwinnerD1 MangoPi MQ1PH boot problem
by alex＠nixd.org 19 Jan '23

19 Jan '23

Hello, I just have a small question because I found the documentation about booting the Sel4 on RISC-V systems a bit confusing and not answering my questions. 1) I have ported all necessary code and I have successful compiled the `sel4test`. 2) I have flashed a SPL and U-Boot to 'mmc' which was built including OpenSBI fw_dynamic.bin but against most recent version (Sel4 was also compiled against most recent version OpenSBI v1.2 U-Boot SPL 2022.10-38338-g528ae9bc6c-dirty (Jan 11 2023 - 01:07:54 +0100)). 3) SPL and U-boot runs perfectly. 4) Sel4 does not want to boot. Why? So, in the DTS which I extracted from SDK it is said: ` /memreserve/ 0x40000000 0x200000; /* opensbi */ /memreserve/ 0x42000000 0x100000; /* dsp used 1MB */ memory@40000000 { device_type = "memory"; reg = <0x0 0x40000000 0x0 0x8000000>; }; ` For the elfloader objdump reports the `_start at 0x40a21000` so I hardcoded it into the following #define CONFIG_BOOTCOMMAND \ "if mmc rescan; then " \ "echo SD/MMC found on device ${mmc_dev};" \ "fatload mmc 0 0x40a21000 elfloader;" \ "fatload mmc 0 0x40a27940 archive.archive.o.cpio;" \ "bootelf 0x40a21000;" \ "fi;" \ And it reported an error: "Unhandled exception: Load access fault EPC: 000000007ffbd308 RA: 000000007ffbd33a TVAL: 00000005c66db5aa EPC: 0000000042e50308 RA: 0000000042e5033a reloc adjusted Code: 69a2 6145 8082 7480 1793 0069 9426 943e (641c) resetting ..." It seems that it relocates itself to 42e5033a (or not?) what actually I was trying to do manually. U-boot reports (for the domain0) the next address which is 0x0000000042e00000. And when I am loading elfloader there, it exists back to uboot shell without any errors and nothing happens. I can not understand what I am doing wrong, because FreeBSD and Linux starts normally. The #define seL4_UserTop is generated from DTS file if I understood correctly. But it seems it is incorrect. I will be happy for any hint. Thank you.

3 2

Can I launch two rumprun instances at the same time?
by mincheol＠vt.edu 06 Jan '23

06 Jan '23

Hi, I am trying to run two rumprun instances on seL4. I called launch_process(bin_name, CONFIG_RUMPRUN_COMMAND_LINE, 1); launch_process(bin_name, CONFIG_RUMPRUN_COMMAND_LINE, 2); in run_rr() of rumprun-sel4-demoapps/roottask/src/main.c. Then I got below: <<seL4(CPU 0) [decodeCNodeInvocation/107 T0xffffff801fe14400 "roottask" @4166c1]: CNode Copy/Mint/Move/Mutate: Source slot invalid o> sel4utils_move_cap_to_process@process.c:157 Failed to move cap <<seL4(CPU 0) [decodeX86PortControlInvocation/147 T0xffffff801fe14400 "roottask" @451efa]: IOPortControl: Some ports in range alread> arch_copy_IOPort_cap@arch.c:25 Failed to get IO port cap for range cf8 to cff I don't understand why I got these errors. launch_process() gets rump_process_t *process from process_from_id(id) so I should get a different slot with the different process id.

1 0