November 2017 - 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

UEFI support for x86
by Edward Sandberg 05 Dec '17

05 Dec '17

Is there a plan to add UEFI support in seL4 for x86 hardware in the near future? Newer x86 boards are frequently UEFI only. It is possible to get around the lack of UEFI support, as I have done with the UP board: https://up-community.org/wiki/Hardware_Specification but I am hitting problems which I will detail below. When I compile using ia32_debug_xml_defconfig and boot using the resulting images the board fails to find the RSDP location. To fix this I had to modify the source code a bit: * seL4test/projects/util_libs/libplatsupport/src/plat/pc99/acpi/acpi.h + #define UPBOARD_RSDP 0x5B161000 * seL4test/projects/util_libs/libplatsupport/src/plat/pc99/acpi/acpi.c - acpi->rsdp = acpi_sig_search(acpi, ACPI_SIG_RSDP, strlen(ACPI_SIG_RSDP), - (void *) BIOS_PADDR_START, (void *) BIOS_PADDR_END); + acpi->rsdp = (void *)UPBOARD_RSDP; * seL4test/kernel/src/plat/pc99/machine/acpi.c - for (addr = (char*)BIOS_PADDR_START; addr < (char*)BIOS_PADDR_END; addr += 16) { + for (addr = (char*)0; addr < (char*)PPTR_BASE; addr += 16) { It would be handy to have this as a kernel parameter to cover cases where it is not successfully discovered automatically. With these changes I can boot the board and several tests pass but then I get stuck on INTERRUPT0001 (Test interrupts with timer). I don't get a test failure or an error the board just sits and makes no more progress. Someone had that test fail in this post: https://sel4.systems/pipermail/devel/2017-February/001328.html and the first recommendation was to check if the irq of the timer was correctly found. I booted the board into linux to find the correct irq which was listed as 0 in /proc/interupts. I added a printf to handleInterrupt in the kernel source, recompiled and when I booted seL4 I found that the irq reported to handleInterrupt is 125 (which sel4 reports as the max interrupt value) every time that function is called. Adding this printf also showed me that when the test hangs the board hasn't crashed or locked up as calls to handleInterrupt are made continuously. At this point I noticed that before any tests started to run several ACPI tables are not recognized: Parsing ACPI tables Skipping table FPDTD, unknown Skipping table FIDT<9c>, unknown Skipping table UEFIB, unknown Skipping table TPM24, unknown Skipping table LPIT^D^A, unknown Skipping table BCFG9^A, unknown Skipping table PRAM0, unknown Skipping table CSRTL^A, unknown Skipping table BCFG9^A, unknown Skipping table OEM0<84>, unknown Skipping table OEM1@, unknown Skipping table PIDVÜ, unknown Skipping table RSCI,, unknown Skipping table WDAT^D^A, unknown Warning: skipping table ACPI XSDT Maybe one or more of those tables needs to be loaded to handle interrupts properly. The LPIT table is conspicuous in the case of the timer test but I think other tests are likely to depend on the other tables. Any suggestions about porting this type of hardware? -- Edward Sandberg Adventium Labs 111 3rd Avenue S. Suite #100 Minneapolis, MN 55401 ed.sandberg(a)adventiumlabs.com

4 10

camkes-gen.mk generated prerequisites
by Gordon Clark 01 Dec '17

01 Dec '17

We have a multi component camkes application with each component using a few common services and then having application interfaces to a small number of other components.All these components are imported into a top level system description camkes file. Examining the generated camkes I see that all the generated header and source files have exactly the same make prerequisites meaning a change to logically unrelated components causes them all to be regenerated and recompiled. Now I have discovered the camkes cache this is less of an issue but is there a better way we can structure our application to reduce the edit-compile-go cycle ? Regards Gordon

2 1

seL4SharedData
by Zippy Maniac 30 Nov '17

30 Nov '17

We have a security requirement on our ARM based product using CAmkES 2.2.x to ensure all sensitive data declared in specific seL4SharedData regions are erased on detection of a power failure. We achieve this by overwriting the data with a known pattern that we read back from a separate component before declaring the device as secured. This is working fine. But we need to guarantee that the overwrite data is actually written to DDR and we aren't just using cached values. This means flushing the L1 and L2 data caches specific regions. We could use seL4HardwareMMIO regions and declare our data in the memory map and use these regions as un-cached. Or use the _hardware_cached attribute and call the provided flush method when necessary. Our main issue with doing this, except the fiddle of mapping multiple different sized regions into the memory map, is we could potentially expose the physical locations of the sensitive data rather than having it wrapped in the virtual address space of a component. Having a flush method on seL4SharedData would be the ideal solution. We are not in a position to upgrade our CAmkES version on this product at the moment. Any thoughts? Zippy

4 3

Tx1 UART and GiC distributor PPTR address
by Muneeswaran Rajendran 27 Nov '17

27 Nov '17

Hi, The PPTR address range between UART and GIC distributor was 12k (kernel/include/plat/tx1/plat/machine/device.h). But when refer in TX1 reference sheet the length was specified as 64byte for UART,4k for GIC distributor and 8k for interrupt controller. can you please point out the reference or reason to choose this address for Tx1 board? /* These devices are used by the seL4 kernel. */ #define UARTA_PPTR 0xffffffffffff0000 #define GIC_DISTRIBUTOR_PPTR 0xffffffffffff3000 #define GIC_CONTROLLER_PPTR 0xffffffffffff4000 These addresses are used during kernel device map to access in the userspace map_kernel_devices : kernel_devices[i].paddr :0x50042000 kernel_devices[i].pptr 0xffffffffffff4000 map_kernel_frame - armKSGlobalKernelPT[GET_PT_INDEX(vaddr)]: 0xffffff800002b000 vaddr :0x1f4 map_kernel_devices : kernel_devices[i].paddr :0x50041000 kernel_devices[i].pptr 0xffffffffffff3000 map_kernel_frame - armKSGlobalKernelPT[GET_PT_INDEX(vaddr)]: 0xffffff800002b000 vaddr :0x1f3 map_kernel_devices : kernel_devices[i].paddr :0x70006000 kernel_devices[i].pptr 0xffffffffffff0000 map_kernel_frame - armKSGlobalKernelPT[GET_PT_INDEX(vaddr)]: 0xffffff800002b000 vaddr :0x1f0 Regards, Munees

1 0

Caught cap fault in send phase at address 0x0 @Tx2
by Muneeswaran Rajendran 23 Nov '17

23 Nov '17

Hi seL4 Dev Team, I am bringing up the sel4 kernel on tx2 board with ref of Tx1. I encountered the TLB invalidation hang issue after kernel map window setup. I do not know the exact reason for hang so just disable that piece of code to look further execution of sel4 kernel. After that it dropped into the usersapce and throwing the cap fault or vm fault issue. Does anyone has come across this type of issue and how it debugged?. Please share your thought or pointers to debug this issue. I shared the full log details here. ## Starting application at 0x82000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A57 r1p3 paddr=[82000000..827abfff] kernel_phys_start: 0xffffffff80000000 kernel_phys_end:0xffffffff8022fcdf load_elf : image_size 0x230000 ELF-loading image 'kernel' paddr=[80000000..8022ffff] vaddr=[ffffff8000000000..ffffff800022ffff] virt_entry=ffffff8000000000 load_elf : image_size 0x5e9000 ELF-loading image 'sel4test-driver' paddr=[80230000..80818fff] vaddr=[400000..9e8fff] virt_entry=41b160 Enabling MMU and paging Jumping to kernel-image entry point... kernel_info.virt_entry : 0x0 user_info.phys_region_start : 0xffffffff80230000 user_info.phys_region_end:0xffffffff80819000 user_info.virt_region_start:0x400000 user_info.virt_region_end:0x9e9000 user_info.phys_virt_offset:0x7fe30000 user_info.virt_entry:0x41b160 Bootstrapping kernel Booting all finished, dropped to user space Caught cap fault in send phase at address 0x0 while trying to handle: vm fault on code at address 0x41b160 with status 0x82000010 in thread 0xffffff8027ef4200 "rootserver" at address 0x41b160 With stack: halting... Kernel entry via VM Fault, fault type: 4305248 Thanks in advance Muneeswaran R

1 0

Tx1 SMP and Hypervisor support
by Muneeswaran Rajendran 17 Nov '17

17 Nov '17

Hi Sel4 Dev Team, Any update of SMP and Hypervisor feature which fully functional on TX2. If its not available when will get this feature supported . Regards, Munees

3 4

1:1 Mapping of Zynqmp devices
by Chris Guikema 16 Nov '17

16 Nov '17

Hello, I am attempting to port the camkes-arm-vm to the zynqmp platform. For the TK1 and Exynos platforms, the physical address of the hardware devices are well below the kernelBase of 0xe0000000. However, for the zynqmp, these hardware devices are greater than the kernel base. This causes the "map_emulated_device" function call to fail for the GIC and any other passthrough devices. sel4utils_reserve_range_at_no_alloc@vspace.c:589 Range not available at 0xff010000, size 0x1000 Assertion failed: res.res (/home/chrisguikema/seL4/NAMC/camkes-arm-vm/libs/libsel4arm-vmm/src/devices.c: map_device: 160) Is there a way to 1:1 map these devices, even if they are above the kernelBase? Thanks, Chris

2 1