Running Sel4 on Rasberry pi 4 4 gb RAM
Hello, i'm trying to upload seL4 ( seL4test-driver-image-bcm2711 image) on raspberry pi 4 but i'm encountering two different errors: 1. If I follow the website procedure and upload the sel4test image into the address 0x10000000 the error is : “Reading file would overwrite reserved memory” 2. If I try to upload the image into 0x1000000 I read the following error: “sel4 failed assertion ‘isSchedulable(candidate)’ at /kernel/thread.c can someone help me? Thanks Daniele
What model of the Raspberry Pi 4 do you have? Specifically how much RAM does it have? Currently seL4 assumes an 8GB model which means if you have a model with less than 8GB you'll run into problems. You can specify how much RAM your model has when building sel4test: ../init-build.sh -DPLATFORM=rpi4 -DAARCH64=1 -DRPI4_MEMORY=4096 This example is for the 4GB model but if you have another model you should just be able to adjust the command to reflect how many megabytes of memory your RPi4 has. Ivan On 13/10/23 17:57, felicianidaniele@gmail.com wrote:
[Some people who received this message don't often get email from felicianidaniele@gmail.com. Learn why this is important at https://aka.ms/LearnAboutSenderIdentification ]
Hello, i'm trying to upload seL4 ( seL4test-driver-image-bcm2711 image) on raspberry pi 4 but i'm encountering two different errors: 1. If I follow the website procedure and upload the sel4test image into the address 0x10000000 the error is : “Reading file would overwrite reserved memory” 2. If I try to upload the image into 0x1000000 I read the following error: “sel4 failed assertion ‘isSchedulable(candidate)’ at /kernel/thread.c
can someone help me?
Thanks Daniele _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
(re-sending since I forgot to 'reply all') Hi Daniele I've made a PR to the documentation website to fix the instructions so hopefully no one has to run into the same issue in the future :) https://github.com/seL4/docs/pull/203. For the virtual machines, I have not run the CAmkES virtual machines with the Raspberry Pi. I believe those part of TII have done a decent amount of work using CAmkES virtual machines and RPi4 so maybe they can comment. I've been working on a separate VMM (https://github.com/au-ts/libvmm) using the seL4 Microkit but it does not have Raspberry Pi 4 support yet. Although if I get time soon I can try get it working and let you know. Thanks, Ivan On 16/10/23 10:11, Ivan Velickovic wrote:
What model of the Raspberry Pi 4 do you have? Specifically how much RAM does it have?
Currently seL4 assumes an 8GB model which means if you have a model with less than 8GB you'll run into problems.
You can specify how much RAM your model has when building sel4test:
../init-build.sh -DPLATFORM=rpi4 -DAARCH64=1 -DRPI4_MEMORY=4096
This example is for the 4GB model but if you have another model you should just be able to adjust the command to reflect how many megabytes of memory your RPi4 has.
Ivan
On 13/10/23 17:57, felicianidaniele@gmail.com wrote:
[Some people who received this message don't often get email from felicianidaniele@gmail.com. Learn why this is important at https://aka.ms/LearnAboutSenderIdentification ]
Hello, i'm trying to upload seL4 ( seL4test-driver-image-bcm2711 image) on raspberry pi 4 but i'm encountering two different errors: 1. If I follow the website procedure and upload the sel4test image into the address 0x10000000 the error is : “Reading file would overwrite reserved memory” 2. If I try to upload the image into 0x1000000 I read the following error: “sel4 failed assertion ‘isSchedulable(candidate)’ at /kernel/thread.c
can someone help me?
Thanks Daniele _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
participants (2)
-
felicianidaniele＠gmail.com -
Ivan Velickovic