Hello, I hope all is well.
I am interested in running seL4 on the Raspberry Pi, and have been following this guidehttps://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 outputhttps://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.
"Brendan" == Brendan Morgenstern bmorgenstern@i-a-i.com writes:
Brendan> Hello, I hope all is well. I am interested in running seL4 Brendan> on the Raspberry Pi, and have been following this Brendan> guidehttps://research.csiro.au/tsblog/sel4-raspberry-pi-3/. I Brendan> have followed the instructions and am able to generate an Brendan> seL4 image correctly, however the guide is geared towards Brendan> running on hardware and in fact when I run the resulting Brendan> 'simulate' script I get the following. "Unsupported platform Brendan> or architecture for simulation".
Yes, sel4test runs on the Raspberry Pi 3b --- QEMU emulates a raspberry Pi 2. The differences between the SoCs are sufficient that an image built for one will not run correctly on the other.
If you want to run on QEMU, I suggest you pick another platform.
-- Peter Chubb Tel: +61 2 9490 5852 http://ts.data61.csiro.au/ Trustworthy Systems Group CSIRO's Data61
Peter> If you want to run on QEMU, I suggest you pick another platform.
Thank you for your response. I was afraid raspberry pi might not be viable, thank you for confirming that. Can you suggest an alternative platform/board I can build and run sel4 on and emulate?
________________________________ From: Chubb, Peter (Data61, Kensington NSW) Peter.Chubb@data61.csiro.au Sent: Wednesday, August 5, 2020 7:00 PM To: Brendan Morgenstern bmorgenstern@i-a-i.com Cc: devel@sel4.systems devel@sel4.systems Subject: Re: [seL4] SeL4 Raspberry Pi -- QEMU support
"Brendan" == Brendan Morgenstern bmorgenstern@i-a-i.com writes:
Brendan> Hello, I hope all is well. I am interested in running seL4 Brendan> on the Raspberry Pi, and have been following this Brendan> guidehttps://research.csiro.au/tsblog/sel4-raspberry-pi-3/. I Brendan> have followed the instructions and am able to generate an Brendan> seL4 image correctly, however the guide is geared towards Brendan> running on hardware and in fact when I run the resulting Brendan> 'simulate' script I get the following. "Unsupported platform Brendan> or architecture for simulation".
Yes, sel4test runs on the Raspberry Pi 3b --- QEMU emulates a raspberry Pi 2. The differences between the SoCs are sufficient that an image built for one will not run correctly on the other.
If you want to run on QEMU, I suggest you pick another platform.
-- Peter Chubb Tel: +61 2 9490 5852 http://ts.data61.csiro.au/ Trustworthy Systems Group CSIRO's Data61
________________________________ 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.
-
Brendan Morgenstern -
Chubb, Peter (Data61, Kensington NSW)