- Devel - lists.sel4.systems

seL4 fails to boot multiple core at CPU 0x1.
by Vishal Gupta 30 Oct '24

30 Oct '24

Dear All, I am a seL4 enthusiast , I am trying to port , build and test seL4 for ARM64 Cortex A53 based hardware. For Single core , I am able to boot via elf-loader then jump to kernel and successfully run Hello World program without any issues. But when I am trying to change it to multiple core SMP enabled on my hardware or even in ARM Qemu setup it is failing to boot. Can anyone please guide me , if seL4 supports multicore than for which version of ARM / board it currently supports , as I could see support for only Sabre-Arm32, which is ARMv7A. Boot log attach for reference. ———————————————————————— ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 paddr=[40a4c000…40f57137] No DTB passed in from boot loader. Looking for DTB in CPIO archive…found at 40bacbe8. Loaded DTB from 40bacbe8. paddr=[4024c000…4024dfff] ELF-loading image ‘kernel’ to 40000000 paddr=[40000000…4024bfff] vaddr=[ffffff8040000000…ffffff804024bfff] virt_entry=ffffff8040000000 ELF-loading image ‘sel4test-driver’ to 4024e000 paddr=[4024e000…40654fff] vaddr=[400000…806fff] virt_entry=40e700 Boot cpu id = 0x0, index=0 HVC is not supported for PSCI! Failed to boot cpu 0x1: 18446744073709551615 abort() called. ——————————————————————————— Looking for any guidance, as it will be helpful for me to move forward . Regards, Vishal

2 1

seL4 developer hangout reminder
by Birgit Brecknell 28 Oct '24

28 Oct '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 29 Oct, 9:00pm UTC. For your local date and time please see https://sel4.systems/contact/. Zoom link: https://unsw.zoom.us/j/82640784431 Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

Device memory access issue on sel4 user driver
by misbah khan 25 Oct '24

25 Oct '24

Hello sel4 developers, I am using seL4 for in our arm64 based hardware platform. I need to write a simple driver where i need to read/write some memory mapped registers The device physical address is "0x40520000" When i print the bootinfo using the below code: /*-- filter TaskContent("untyped-start", TaskContentType.ALL, subtask='init') -*/ printf(" CSlot \tPaddr \tSize\tType\n"); for (seL4_CPtr slot = info->untyped.start; slot != info->untyped.end; slot++) { seL4_UntypedDesc *desc = &info->untypedList[slot - info->untyped.start]; printf("%8p\t%16p\t2^%d\t%s\n", (void *) slot, (void *) desc->paddr, desc->sizeBits, desc->isDevice ? "device untyped" : "untyped"); I get the following output: CSlot Paddr Size Type 0x1ac 0 2^30 device untyped 0x1ad 0x40000000 2^28 device untyped 0x1ae 0x50000000 2^23 device untyped 0x1af 0x50810000 2^16 device untyped 0x1b0 0x50820000 2^17 device untyped I am mappint the physical address to virtual and trying to access it as: va = ps_io_map(&ops.io_mapper, (uintptr_t) 0x40520000,0x3000, PS_MEM_NORMAL); ZF_LOGE("Physical address 0x%x mapped to virtual address %p \n",DEV_REG_PADDR,va); for(int j=0;j<DEV_REG_SIZE;j+=sizeof(unsigned int)) { ZF_LOGE("Loc %d --> 0x%x ",j,*(unsigned int*)(va+j)); } I am able to access some registers, but then it gives a fault (after printing 5-6 register values) Similar is the behaviour with any reg between the range 0x40000000 - 0x50000000 Attaching the sample code and output: I am able to access first two address location, after that it gives halt. Regards, Misbah

2 2

sel4 for Imx8Plus
by janarthanan.b＠teclever.com 22 Oct '24

22 Oct '24

Hi sel4 dev team, I'm working on imx8 Plus board for that Building seL4test is done and generated the binary image file of "sel4test-driver-image-arm-imx8mp-evk" with the size of 5mb as per the procedure on sel4 websites. I moved this into sd card and trying to boot into board.but i cant able to boot it. What is the issue on this and how to solve it? if we need to do uboot what's the procedure for that?

3 4

seL4 hangs during invalidate local TLB
by Vishal Gupta 15 Oct '24

15 Oct '24

Dear seL4 developers, I am a seL4 enthusiast. I am trying to port seL4 on arm64 cortex a53. I am able to port elf-loader successfully and move to the kernel initialisation which reaches till “try_init_kernel->init_cpu->activate_global_pd->invalidateLocalTLB->asm volatile()”. Under InvalidatelocalTLB with asm volatile(“tlbi vmalle1”); in this , the system gets hanged and the asm function does not move forward. Any input or guidance would be really appreciated. Thank you . Regards, Vishal

1 0

Stuck during invalidate local TLB in Tx2
by Muneeswaran Rajendran 15 Oct '24

15 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

seL4 developer hangout reminder
by Birgit Brecknell 29 Sep '24

29 Sep '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 1 Oct, 10:00pm UTC. For your local date and time please see https://sel4.systems/contact/. Zoom link: https://unsw.zoom.us/j/82640784431 Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

General Question On Object Methods
by tunacici7＠gmail.com 25 Sep '24

25 Sep '24

I've recently started to learn seL4 by following the Tutorials, which have been great so far. I've been also reading the Manual & API reference to understand and gain insight into different mechanisms. However, I have one fundamental question: Are the object methods system calls? It is said that seL4 only has 3 logical system calls: Send, Recv and Yield. (In all the slides, videos and other documents I have seen) And the rest is just variations of those ones. But what about object methods? Are they system calls? Are they executed in kernel space? If they are system calls, then wouldn't all the resources out there be misleading? Since there are way more than just Send, Recv and Yield. If they are not, then how are they handled? Does 'libsel4' have anything to do with it? I can't imagine 'seL4_Untype_Retype' executing in user space. Unfortunately, I couldn't find any answers to this question online. So that's why I'm asking it here. Maybe there are others who wonders the same thing. NOTE The API Reference page confuses me even more. It lists Object Methods in its own category (instead of being under System Calls). Does this means Object Methods are NOT system calls? Or the term System Call is just not what I think it is(basically an endpoint to kernel)?. END NOTE Thanks for the answers in advance. -T

8 21

seL4 developer hangout reminder
by Birgit Brecknell 15 Sep '24

15 Sep '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 18 Sep, 8:00am UTC. For your local date and time please see https://sel4.systems/contact/. Zoom link: https://unsw.zoom.us/j/82640784431 Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

Less than 1 week left to get the early-bird registration for the seL4 summit
by Birgit Brecknell 08 Sep '24

08 Sep '24

Less than 1 week left to get the early-bird registration for the seL4 summit The early bird cut-off date for the seL4 summit 2024 [0] is 15 September 2024. The summit will be held in Sydney, Australia, 15-17 October 2024. The seL4 summit will cover the complete seL4 ecosystem, consisting of the verified microkernel, as well as all seL4-related technology, tools, infrastructure, products, projects, and people. Tickets include: - Participation in the 3-day conference, including talks, keynotes, seL4 updates & discussions - Networking with other seL4 experts and enthusiasts - Reception and dinner Register here [1] A number of informal social activities [2] are being organised by local Sydney-siders. Check out the list [2] and contact the organiser to register your interest. [0] https://sel4.systems/Foundation/Summit/2024/ [1] https://events.linuxfoundation.org/sel4-summit/register/ [2] https://sel4.systems/Foundation/Summit/2024/social-activities Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0