October 2017 - Devel - lists.sel4.systems

seL4 test on x86
by Yevgeny Lavrov 29 Jan '25

29 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

Questions about Memory Management in seL4
by Daniel Wang 18 May '23

18 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 04 Dec '17

04 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 mutex Question
by Brandon, Jeffrey - 0553 - MITLL 06 Nov '17

06 Nov '17

Hi, I've been taking a look at mutex implementations in the camkes-app example and I had a question. In the mutex example here https://github.com/seL4/camkes/tree/master/apps/mutex suppose I wanted to extend to add a third component C I need to add the corresponding camkes, source, Kbuild, and Kconfig files and then I need to add connections to the master mutex.camkes file correct? My first intuition was to add a connector: Assembly { Composition{ . Connection seL4MyConnector connection(from c.lock, to b.lock); . } } But this yields and error saying something to the effect "seL4MyConnector expects one from endpoint and two are specified" To remedy this I added another lock component to B, and made a connection between C and this new lock B provides. The new lock being implemented by the same template. My Questions: In this scenario do A B and C still have access to the same mutex? If A has a lock on the mutex, then C requests a lock, will this cause A to be unable to release the lock? In my mental model I have three threads of control, one each for A B and C, if A has a lock and then C requests a lock, does this block B (when it receives a message from C and is now blocked on requesting the mutex)? Then when A tries to release, B is blocked and cannot release the mutex on A's behalf. To put it another way, does this mutex example rely on B having direct access to the templated code and there only being two components? Secondarily, in the lockserver example https://github.com/seL4/camkes/tree/master/apps/lockserver a situation is presented where three clients access a single mutex through a single server. Would there be an issue if one of the clients also acted as the server? So for instance if A implemented the three pairs of lock unlock functions instead of the server and then B and C used seL4RPCCall connections to A in order to access them, would there be any synchronization issues? I'm relatively new to this and am trying to build a system with the help of camkes and I want to make sure I understand this before I get too far. I don't want to be working under incorrect assumptions. Thanks for taking the time to read this. Sincerely, Jeff Brandon Associate Staff MIT Lincoln Laboratory Secure Resilient Systems and Technology Ph: +1 781.981.9233

3 2

UART initialisation on seL4 @TX1
by Muneeswaran Rajendran 02 Nov '17

02 Nov '17

Hi sel4 development team, I understand from the seL4 kernel the initial printf message are not routed through sel4 platform uart driver. Because the sel4 UART driver initialisation happened later when seL4 Main kernel initialization is finished. till then sel4 kernel uses u-boot UART driver to route the message. This interpretation is correct as per my understanding. Also mentioned in code as well debug output available via serial interface after kernel init thread started. /* debug output via serial port is only available from here */ printf("Bootstrapping kernel\n"); It means that when sel4 kernel comes up with u-boot uart driver and then later using sel4 uart driver. Please correct me if any thing wrong here and throw some input. Regards, Munees

2 2

Re: [seL4] Devel Digest, Vol 41, Issue 33
by ashokk＠spanidea.com 31 Oct '17

31 Oct '17

Hi Kofi, I tried with go command, but it is not working, board is getting hang... U-boot> go 0x10000000## Starting application at 0x10000000 ... after these i am not able to access the board, i need to reset again... Thanks & RegardsAshok From: "devel-request(a)sel4.systems" <devel-request(a)sel4.systems> To: devel(a)sel4.systems Sent: Monday, 30 October 2017 11:54 PM Subject: Devel Digest, Vol 41, Issue 33 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via the World Wide Web, visit https://sel4.systems/lists/listinfo/devel or, via email, send a message with subject or body 'help' to devel-request(a)sel4.systems You can reach the person managing the list at devel-owner(a)sel4.systems When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..." Today's Topics: 1. Re: Devel Digest, Vol 41, Issue 31 (Kofidoku.Atuah(a)data61.csiro.au) ---------------------------------------------------------------------- Message: 1 Date: Sun, 29 Oct 2017 23:56:03 +0000 From: <Kofidoku.Atuah(a)data61.csiro.au> To: <devel(a)sel4.systems> Subject: Re: [seL4] Devel Digest, Vol 41, Issue 31 Message-ID: <1509321363766.62194(a)data61.csiro.au> Content-Type: text/plain; charset="iso-8859-1" Hi Ashokk, I believe if you replace the command, "bootelf 0x10000000" with "go 0x10000000", That should be all that's needed to boot a raw binary image -- lemme know how things go though~ -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO

1 0

Re: [seL4] Devel Digest, Vol 41, Issue 31
by ashokk＠spanidea.com 29 Oct '17

29 Oct '17

Hi Kofi, Thanks for the steps, i am able to load sel4test-driver-image-arm-bcm2837 on RPI3. but my question is i generated a sel4test-driver-image-arm-bcm2837.bin(binary image) for RPI3 i want to load these image on RPI3, can you help me out to load these image on RPI3... Hardware/Rpi3 - seL4Wiki these steps are used to load elf image on RPI3.... but i want to load binary image on RPI3... | | | Hardware/Rpi3 - seL4Wiki | | | Thanks and Regards Ashokkumar From: "devel-request(a)sel4.systems" <devel-request(a)sel4.systems> To: devel(a)sel4.systems Sent: Thursday, 26 October 2017 8:48 PM Subject: Devel Digest, Vol 41, Issue 31 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via the World Wide Web, visit https://sel4.systems/lists/listinfo/devel or, via email, send a message with subject or body 'help' to devel-request(a)sel4.systems You can reach the person managing the list at devel-owner(a)sel4.systems When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..." Today's Topics: 1. Re: Loading bin image on RPI3(Remainder) (Kofidoku.Atuah(a)data61.csiro.au) ---------------------------------------------------------------------- Message: 1 Date: Thu, 26 Oct 2017 03:23:06 +0000 From: <Kofidoku.Atuah(a)data61.csiro.au> To: <devel(a)sel4.systems> Subject: Re: [seL4] Loading bin image on RPI3(Remainder) Message-ID: <1508988186794.61071(a)data61.csiro.au> Content-Type: text/plain; charset="iso-8859-1" Hi Ashokk, Thanks for pointing this issue out, and sorry I took so long to get back to you -- I've investigated and come up with a workaround until we can fix the underlying caching problem here: could you try following the instructions on this page? https://wiki.sel4.systems/Hardware/Rpi3#preview There should be a pre-built U-Boot binary image there which should successfully load your seL4 kernel image. Please let me know how things go~ -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO

2 1

Re: [seL4] Loading bin image on RPI3(Remainder)
by Kofidoku.Atuah＠data61.csiro.au 26 Oct '17

26 Oct '17

Hi Ashokk, Thanks for pointing this issue out, and sorry I took so long to get back to you -- I've investigated and come up with a workaround until we can fix the underlying caching problem here: could you try following the instructions on this page? https://wiki.sel4.systems/Hardware/Rpi3#preview There should be a pre-built U-Boot binary image there which should successfully load your seL4 kernel image. Please let me know how things go~ -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO

1 0

Some guidance when using AutoCorres.
by Dan DaCosta 25 Oct '17

25 Oct '17

seL4 Developers: Consider the following c structure declarations: struct foo_struct{ uint16_t subfield; }; struct bar_struct{ struct foo foo; }; I am wondering if anyone has any suggestions on how I might go about proving something like this: s[Ptr &(bar→[''foo_C'']) := subfield_C_update (λ_. b) (heap_MissionCommand_struct_C s (Ptr &(bar→[''foo_C''])))] = s[Ptr &(bar→[''missioncommand_C''])→subfield := b] where s of type lifted_globals, bar is of type foo_struct_C, and b is of type word16. I *think* it should be provable, i.e., "updating all of the foo field with a copy of what was there originally modulo some change to subfield is equivalent to making that change directly to the subfield." I apologize in for taking this "into the weeds" but some of the definitions being used are buried in the AutoCorres translation and I am unsure how to make my question more abstract. Thanks in Advance! Dan DaCosta

3 2

Booting seL4 in bbb (beaglebone black)
by Sathish Kumar Balasubramaniam -ERS, HCL Tech 24 Oct '17

24 Oct '17

I tried booting sel4test in bbb. but i got the following after u-boot. Any idea for this crash ? U-Boot# echo $loadaddr 0x82000000 U-Boot# fatload mmc 0 ${loadaddr} sel4test.bin reading sel4test.bin 4108544 bytes read in 245 ms (16 MiB/s) U-Boot# go ${loadaddr} ## Starting application at 0x82000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A8 r3p2 paddr=[82000000..823fc81f] ELF-loading image 'kernel' paddr=[80000000..80036fff] vaddr=[f0000000..f0036fff] virt_entry=f0000000 ELF-loading image 'sel4test-driver' paddr=[80037000..80514fff] vaddr=[8000..4e5fff] virt_entry=21c9c Enabling MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Booting all finished, dropped to user space Caught cap fault in send phase at address 0x0 while trying to handle: unknown syscall 0xf0005 in thread 0xf7fec500 "rootserver" at address 0x18b60 With stack: 0x3d88a0: 0x84ac 0x3d88a4: 0x1711c 0x3d88a8: 0x46c0f 0x3d88ac: 0x0 0x3d88b0: 0x84ac 0x3d88b4: 0x172cc 0x3d88b8: 0x3e5224 0x3d88bc: 0x46c0f 0x3d88c0: 0x84ac 0x3d88c4: 0xecfc 0x3d88c8: 0x31 0x3d88cc: 0x0 0x3d88d0: 0x0 0x3d88d4: 0x0 0x3d88d8: 0x0 0x3d88dc: 0x0 ::DISCLAIMER:: ---------------------------------------------------------------------------------------------------------------------------------------------------- The contents of this e-mail and any attachment(s) are confidential and intended for the named recipient(s) only. E-mail transmission is not guaranteed to be secure or error-free as information could be intercepted, corrupted, lost, destroyed, arrive late or incomplete, or may contain viruses in transmission. The e mail and its contents (with or without referred errors) shall therefore not attach any liability on the originator or HCL or its affiliates. Views or opinions, if any, presented in this email are solely those of the author and may not necessarily reflect the views or opinions of HCL or its affiliates. Any form of reproduction, dissemination, copying, disclosure, modification, distribution and / or publication of this message without the prior written consent of authorized representative of HCL is strictly prohibited. If you have received this email in error please delete it and notify the sender immediately. Before opening any email and/or attachments, please check them for viruses and other defects. ----------------------------------------------------------------------------------------------------------------------------------------------------

2 2