Devel July 2018

devel@sel4.systems

24 participants
32 discussions

RISC-V - sel4test and sel4bench running on SiFive's Unleashed Platform
by Hesham Almatary 19 Jul '18

19 Jul '18

Hi everyone, I pushed my local seL4/RISC-V work to GitHub which contains the following new features: * A new option to run seL4 in machine mode. * A port of seL4 to QEMU's SiFiveU and virt platforms. * DTB parsing in seL4 to read and use UARTs when available. * Ported seL4 to run on VC707 FPGA Freedom Unleashed platform. * Initial Benchmarking support in seL4. * Initial sel4bench port that can measure IPC and trap timing. Link for more details: http://heshamelmatary.blogspot.com/2018/07/new-sel4test-and-sel4bench-relea… -- Hesham

1 0

Porting sel4 on RISCV architecture
by Sathya Narayanan N 16 Jul '18

16 Jul '18

Hi Experts, This is Sathya from IIT Madras. We are working on porting SEL4 on RISCV architecture running on FPGA. We have ported linux on the FPGA. I have some doubts regarding OS porting. I am stuck at the end. Before my actual query, let me tell my platform. Hardware - 64 bit RISCV design running on FPGA. It doesn't support compressed instn and multiarch. Operating system - SEL4, repo synced from latest official repository. Tools - Latest synched from RISCV official repo. Query - I simulated sel4test on spike and then I am trying to port it on FPGA. We have UART to be mapped to 0x11400 address location. I set scan->reg to this value. I understood, incase of simulation, the DTB argument passed to init_first_hart function comes from spike simulator (file - sim.cc). Now, for FPGA I want to pass the DTB value to the init_first_hart() function. I am planning to write a DTS file and somehow read the data from DTS file here. I am trying to know, what is the right method to do for SEL4 ? Can you please let me understand, how you went ahead for SEL4 ? Is there any changes, I have to do in the repo code ? any readings would you suggest to proceed ahead ? -- regards, Sathya

3 4

Re: [seL4] How to write safe C code for free?
by Wean Irdeh 14 Jul '18

14 Jul '18

Thanks again for the reply. I was looking for the foolproof way to write safe C code, but seems like the best way to go forward is to carefully design and code. Your advice is helpful to me. On Friday, July 13, 2018, Dean Pucsek <dean(a)lightbulbone.com> wrote: > >> Clang does have a static analyzer builtin that can be help in some > cases. That being said, the best way forward is for you as a developer to > understand the types of code that can lead to problems and not rely > entirely on a static analyzer. > > >>> >>> >

1 0

Re: [seL4] How to write safe C code for free?
by Wean Irdeh 14 Jul '18

14 Jul '18

Thanks a lot for the reply. What is your opinion on static checking tool and safe subset of C? Does that help? On Friday, July 13, 2018, Dean Pucsek <dean(a)lightbulbone.com> wrote: > Hello Wean, > > It is certainly possible to learn how to program in C without spending any > money; all it requires is a basic toolchain and a willingness to learn. > don't sell yourself short by hinting that you might be "stupid" (you almost > certainly aren't). > > In order to get started with C I suggest setting up an environment to > experiment in; for that look into installing LLVM/Clang ( > http://releases.llvm.org/) there are pre-built binaries for most major > operating systems. Once that is done all you need is a text editor (Notepad > on Windows or one of the other many free options) and some patience. As for > tutorials and resources, some options are: > > - Searching on Google for "c tutorial"; one result that looks interesting > is http://www.learn-c.org/. > - Finding an open source project that interests you and trying to > understand the code then implement a change. > - While not free, may people swear by the K&R book as a great resource to > start. > > In terms of writing code that is free of undefined behaviour and > vulnerabilities your best bet is to learn what code constructs cause those > to occur and how to avoid them. A great book for this is The Art of > Software Security Assessment by Mark Dowd, there is a PDF of Chapter 6 (C > Language Issues) available at https://trailofbits.github.io/ > ctf/vulnerabilities/references/Dowd_ch06.pdf. > > Learning about C, undefined behaviour, and vulnerabilities doesn't happen > overnight so be patient and enjoy the journey. > > --Dean > > > >

1 0

Help ! Simulating SEL4 with Zero testcases running
by Sathya Narayanan N 13 Jul '18

13 Jul '18

Hi Experts, I am running sel4 simulation on spike. I want to disable test cases from running. I tried setting default value "" from ".*" in Kconfig file. Is this enough ? Or is something else to be done ? -- regards, Sathya

2 2

Re: [seL4] sel4test cross compiling for arm
by Kofidoku.Atuah＠data61.csiro.au 13 Jul '18

13 Jul '18

?Hey Thad, Thanks for catching that: it turns out that we weren't passing -nostdlib to the linker when linking the ELFLoader, so the cross-toolchain's linker was trying to link the ELFLoader against the cross toolchain's libc, but it shouldn't be doing that and it should instead be using our libmuslc. A fix has been pushed out and you should be seeing it shortly. Thanks for your patience, -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO

1 0

seL4 vm examples with Qemu
by Mike Clark 12 Jul '18

12 Jul '18

Is it currently possible to boot the camkes-vm-example applications using qemu? I followed the directions here (https://github.com/seL4/camkes-vm-examples) to get a build of the minimal application. I then tried to follow the directions here ( https://docs.sel4.systems/Hardware/Qemu/#running-qemu) to boot using qemu. Unfortunately I get an error when trying to boot. The error says: *"seL4 caled fail at /host/camkes_vm/kernel/src/arch/x86/kernel/boot_sys.c:785 in function boot_sys, saying "boot_sys failed for some reason :("* *halting...* *Kernel entry via Interrupt, irq 0* I'm running this on a ubuntu 16.04 machine with an Intel i5-4200U ( https://ark.intel.com/products/75459/Intel-Core-i5-4200U-Processor-3M-Cache… ). Thanks!

2 1

Re: [seL4] Memory Region overlap error
by Jeremy Fields 12 Jul '18

12 Jul '18

> > > On 11.07.2018 01:45, Jeremy Fields wrote: > > Here's my results from these permutations, using Genode 18.05 / sel4 > 9.0.1 > > (hopefully the formatting works). I know some permutations probably don't > > make sense, but I did them anyways. Any thoughts? I have the serial > output > > from these tests as well, but didn't want to overload this message with > > that. Additionally, can you folks share specific machine make/models that > > you know work with Genode/seL4? Hopefully some 'consumer off the shelf' > > stuff. > > We have no specific Genode/seL4 x86 hardware list, but there exists an > unofficial list at [0] which may serve your question. > > > PermuationResult > > Legacy / Multiboot 2 + Bender Memory region overlap > > Legacy / Multiboot 1 + Bender failed assertion > > 'acpi_rsdt_mapped->header.length >= sizeof(acpi_header_t) > > Legacy / Multiboot 1 crashes/reboots > > Legacy / Multiboot 2 Memory region overlap > > UEFI / Multiboot 2 + Bender Memory region overlap > > UEFI / Multiboot 1 + Bender failed assertion > > 'acpi_rsdt_mapped->header.length >= sizeof(acpi_header_t) > > UEFI / Multiboot 1 freezes? > > UEFI / Multiboot 2 Memory region overlap > > Thanks for testing. > > May you please apply the seL4 kernel patch and test, whether this solves > your issue ? > > > [0] http://usr.sysret.de/jws/genode/hcl.html > > -- > Alexander Boettcher > Genode Labs > > http://www.genode-labs.com - http://www.genode.org > > Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden > Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth >

2 1

Re: [seL4] Memory Region overlap error
by Jeremy Fields 11 Jul '18

11 Jul '18

> > Hello, > > On 05.07.2018 14:34, Jeremy Fields wrote: > > Sure - I've tried a few different combinations, but the latest Genode 18.5 > > used seL4 9.0.1. I'm attempting to use this on an x86 machine that has a > > Xeon 1607 and a dedicated GPU. The thread I referenced in my initial post > > implied that UEFI might be an issue, but I've tried both UEFI and legacy > > boots without success. I tried using/building Genode 17.5 with whatever > > version of seL4 it acquires, but get the same error. Let me know if there's > > anything else I can provide > > some suggestions from my side. > > Try to remove the chain bootloader "bender", just to exclude it as > potential reason of trouble. In genode/tool/run/boot_dir/sel4 remove the > "multiboot2 /boot/bender ..." line and adjust the line below from > "module2 /boot/sel4 ..." -> "multiboot2 /boot/sel4 ...". Use some simple > scenario for testing, like log.run > > If the issue persists, you may try to boot Genode/seL4 the Multiboot 1 > way instead of Multiboot 2, which however will solely work for BIOS > legacy boots (no UEFI). Replace the "multiboot2" and "module2" in > genode/tool/run/boot_dir/sel4 with "multiboot" and "module". > > > Cheers, > > Alex B. > > -- > Alexander Boettcher > Genode Labs > > http://www.genode-labs.com - http://www.genode.org > > Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden > Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth > Here's my results from these permutations, using Genode 18.05 / sel4 9.0.1 (hopefully the formatting works). I know some permutations probably don't make sense, but I did them anyways. Any thoughts? I have the serial output from these tests as well, but didn't want to overload this message with that. Additionally, can you folks share specific machine make/models that you know work with Genode/seL4? Hopefully some 'consumer off the shelf' stuff. PermuationResult Legacy / Multiboot 2 + Bender Memory region overlap Legacy / Multiboot 1 + Bender failed assertion 'acpi_rsdt_mapped->header.length >= sizeof(acpi_header_t) Legacy / Multiboot 1 crashes/reboots Legacy / Multiboot 2 Memory region overlap UEFI / Multiboot 2 + Bender Memory region overlap UEFI / Multiboot 1 + Bender failed assertion 'acpi_rsdt_mapped->header.length >= sizeof(acpi_header_t) UEFI / Multiboot 1 freezes? UEFI / Multiboot 2 Memory region overlap -- Sincerely, Jeremy ______________________________ Software Engineer Critical Technologies Inc.

2 1

Re: [seL4] sel4test cross compiling for arm
by Kofidoku.Atuah＠data61.csiro.au 11 Jul '18

11 Jul '18

Sorry Thad, I want to correct something I said: I recommended that you try the arm-linux-gnueabihf toolchain, but that should have been the arm-linux-gnueabi toolchain. Aside from that, I went and double checked, and this toolchain works just fine -- one thing to note though, is that you don't have to specify the -DCROSS_COMPILER_PREFIX=foo option, and you should be able to just use -DAARCH32=1 and our build system should automatically select the right toolchain to invoke for you (see: https://github.com/seL4/seL4/blob/master/gcc.cmake#L24?) Feel free to ask more questions about the new build system since we expect adaptation to take some time. -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel July 2018