August 2020 - Devel - lists.sel4.systems

QEMU, seL4, CAmkES and Linux VM - Insufficient Memory
by Cedric MAIRE 14 Aug '20

14 Aug '20

Dear seL4 developers, I am trying to setup a stack of QEMU, seL4, CAmkES and a Linux VM. I am following the tutorial on "https://docs.sel4.systems/Tutorials/camkes-vm-linux.html" and also the example on "https://github.com/seL4/camkes-vm-examples". I am running in different errors depending on which path I follow. The machine is an old MacBook Pro (running Linux, exact specs are in the main log file). - Main log file: "intel.log", contains steps and workflows - Tests: All tests seem to pass. - CAmkES VM - Tutorial Version: doesn't start QEMU because of unsupported host flags (warnings) or some failing script - CAmkES VM - Example Version: seems to boot into seL4 or even the Linux VM, but fails because of some memory error Does this look familiar to you? Best regards, Cedric Maire =============================================================================== The ICRC - working to protect and assist people affected by armed conflict and other situations of violence. Find out more: www.icrc.org This e-mail is intended for the named recipient(s) only. Its contents are confidential and may only be retained by the named recipient (s) and may only be copied or disclosed with the consent of the International Committee of the Red Cross (ICRC). If you are not an intended recipient please delete this e-mail and notify the sender. ===============================================================================

2 2

Hins for an seL4 virtio pci driver?
by Radev, Martin 10 Aug '20

10 Aug '20

Hello seL4 community, I am currently examining the possibility of using seL4 in a VM and writing a virtio driver to communicate with a virtio pci device in the HV. I looked around the available seL4 projects, and I noticed that there is the `libvirtqueue` and `libpci` projects which should come handy. However, I haven't been able to to find any other project which uses either of the libraries and I haven't found any tests for the two projects. Can you point me to projects which use these two libraries? Kind regards, Martin

2 1

SeL4 Raspberry Pi -- QEMU support
by Brendan Morgenstern 08 Aug '20

08 Aug '20

Hello, I hope all is well. I am interested in running seL4 on the Raspberry Pi, and have been following this guide<https://research.csiro.au/tsblog/sel4-raspberry-pi-3/>. I have followed the instructions and am able to generate an seL4 image correctly, however the guide is geared towards running on hardware and in fact when I run the resulting 'simulate' script I get the following. "Unsupported platform or architecture for simulation". I can run it manually under qemu to an extent with raspi2 as a machine type (): qemu-system-arm -serial null -serial mon:stdio -nographic -M raspi2 -kernel sel4test-driver-image-arm-bcm2837 And it produces this output<https://pastebin.com/LLuum55T>. It seems the image can be *run*, but it doesn't seem to work; it gets stuck on the TIMER0001 test and the previous tests produce errors. It seems that qemu can't quite emulate the raspberry pi hardware. Is there a way to run the seL4 image on the Raspberry Pi in QEMU, or can you provide an alternative for emulation, or any help whatsoever on this matter? Thank you for your time, Brendan Morgenstern ________________________________ 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.

2 2

Re: [seL4] [seL4 Announce] UNSW seL4 teaching videos available
by Heiser, Gernot (Data61, Kensington NSW) 02 Aug '20

02 Aug '20

I’ve (almost) finished teaching and all seL4-related videos from my Advanced OS course are now up on YouTube, details below. Gernot > On 2 Jun 2020, at 10:50, Announcements about seL4 -- low volume list <announce(a)sel4.systems> wrote: > > Dear seL4 community, > > I’m pleased to announce yet another contribution of UNSW Sydney to the seL4 community: This year I’m making the seL4-related videos from my UNSW Advanced Operating Systems class freely available. You’ll find them at the UNSW CSeLearning COMP9242 YouTube channel: https://www.youtube.com/playlist?list=PLbSaCpDlfd6qLbEsKquVo3--0gwYBmrUV > > At present there are the first two modules, which provide some background on microkernels and seL4, and discuss the seL4 API. More material will show up over the next two months. > > The complete course material, including all lecture slides, the project spec and code, are available, as always, from the COMP9042 web site: https://www.cse.unsw.edu.au/~cs9242/current/ > > Enjoy, > Gernot

1 0