December 2017 - Devel - lists.sel4.systems

seL4 bring up on inmate cell of jailhouse.
by Muneeswaran Rajendran 12 Dec '17

12 Dec '17

Hi, I would like to bring up seL4 on inmate cell of Tx1. The jailhouse is running successfully on Tx1 board. I have created root cell and not root cell configuration on jailhouse. I able to load seL4 image successfully on inmate cell then during execution its stuck in the while extracting the program header. I checked with jailhouse forum they suggested some one might have ported seL4 or L4 kernel on jailhouse.also informed that seL4 kernel need to rebuild with some patches. Somehow I do not find the patches for seL4 or Fiasco.OC kernel to bring up on jailhouse.Please share links if you any. Also experimented by changing the PHY_ADDR higher then 2G (0x80000000) configuration ie(0x90000000 to 0xF0000000) and (0x100000000 to 0x170000000) while booting from the u-boot I observed KERNEL DATA abort after boot strapping the kernel. It means that this address cannot accessible in the seL4 kernel. Case 1: 0x90000000 to 0xF0000000 sample logs: ------------------- Bootstrapping kernel KERNEL DATA ABORT! Faulting instruction: 0x1ca9c FAR: 0x90000000 ESR (DFSR): 0x96000044 halting... Kernel entry via Interrupt, irq 0 case 2: 0x100000000 to 0x170000000 It's throwing synchronous data abort during program header extraction. sample logs: ------------------ binaries/elf64: elf64_getNumProgramHeaders "Synchronous Abort" handler, esr 0x96000044 ELR: 82002c8c LR: 820031f4 x0 : 0000000100000000 x1 : 0000000000000000 x2 : 000000000022fc10 x3 : 00000000827a5d40 x4 : 0000000000000000 x5 : 00000000000db8ab x6 : 0000000082007948 x7 : 0000000082008578 x8 : 0000000082008570 x9 : 0000000000000008 x10: 000000000000000f x11: 00000000fed87118 x12: 0000000000000047 x13: 0000000000000040 x14: 0000000000000001 x15: 00000000fed33114 x16: 0000000000000000 x17: 0000000000000000 x18: 00000000fc82ede0 x19: 00000000827a5ff0 x20: 0000000000000002 x21: 0000000082000000 x22: 00000000fc832800 x23: 0000000000000002 x24: 00000000fedaa7fc x25: 0000000000000000 x26: 0000000000000000 x27: 00000000fc8322f0 x28: 0000000000000000 x29: 00000000827a5e80 someone can give suggestion or pointers how we can bring seL4 on Jailhouse. Regards, Munees

3 2

Dynamic Loading of application
by ALVI Aslam (MORPHO) 12 Dec '17

12 Dec '17

Hi everyone, Greetings, I'm just started with seL4. Current Progress: - I have built an application on top of seL4 as learning from tutorials, so this is my current design [seL4,My main_APP,App2,App1,App3] Here My main_App is my main application build on seL4 and App1, App2 and App3 are sub components link with My main_App.( Just like in Tutorial 4 of seL4). When i build and run , this is working fine, no issue with it. when i run make command first i build kernel then libraries, then App1 , App2, App3, then My main_app and in the end it generate a single image file to execute. My Question :- Can i dynamic load my sub components(App1, App2, App3) which is required by My_main_App in run time ? Can we do that in seL4 is yes then how ? i dont want my App1, App2 and App3 part of final image, I want to load them and run them separately using My_main _App? Thank you in Advance, Please Help. Regards, Aslam ALVI # " This e-mail and any attached documents may contain confidential or proprietary information. If you are not the intended recipient, you are notified that any dissemination, copying of this e-mail and any attachments thereto or use of their contents by any means whatsoever is strictly prohibited. If you have received this e-mail in error, please advise the sender immediately and delete this e-mail and all attached documents from your computer system." #

2 1

AARCH64 with CAMKES (Questions)
by Michael DeFrancis 06 Dec '17

06 Dec '17

Can camkes be used with ARM AARCH64? I am attempting to build a linux virtual machine on top of the zynqmp ultrascape+ / sel4 kernel, and using the tk1 vmm project as my reference point. When the build system attempts to generate camkes-gen.mk, it fails - displaying an error indicating that aarch64 is not a valid architecture specification for camkes. I see that valid arm options are aarch32 or arm_hyp. Is arm_hyp what I am looking for here? What would I need to do in order to strip the camkes dependencies out of the tk1 vmm project? Thanks, Mike D Computer Security Engineer - Intelligent Automation, Inc. (301)294-5263 ________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.

3 3

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

seL4_Send vs. seL4_Call
by Stefan Wallentowitz 05 Dec '17

05 Dec '17

Hi everyone, I have built a very simple application that loads another process, which is very similar to the tutorials. For testing I wanted to send from the second process to the first one using seL4_Send and observe that the second process never continues after the seL4_Send blocked, despite the receiver called seL4_Recv and got the message. If I call seL4_Call and the receiver does seL4_Recv + seL4_ReplyRecv it works without any other changes to the code. I am wondering if I am understanding something fundamentally wrong and/or what the best strategy to debug this behavior is. Thanks for your help! Cheers, Stefan

2 1

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