raspberry pi 4

newer
Docker / gnat

older
Re: [seL4] Devel Digest, Vol 77,...

Sachin More

24 Oct 2020 24 Oct '20

7:31 a.m.

Hi: Has anyone tried to use seL4 on a raspberry pi 4? thanks, Sachin

Show replies by thread

Nick Spinale

24 Oct 24 Oct

11:20 a.m.

...

Has anyone tried to use seL4 on a raspberry pi 4?

Yes, I am running seL4 on the Raspberry Pi 4 Model B. The project we are working has a userland that is not based on `seL4_libs` and friends, so I’m afraid we have no userland drivers to contribute upstream. However, we do have patches with the necessary kernel configuration and elfloader SMP initialization logic to get seL4 itself running on the Raspberry Pi 4 Model B. Our project uses a different build system from upstream seL4 development, so our patches will require additional preparation before we can open a PR. For now, I’ll publish the patches in a public fork and then link to them in this thread. - - - - Nick Spinale (nickspinale.com) Arm Research, Cambridge UK - - - - IMPORTANT NOTICE: The contents of this email and any attachments are confidential and may also be privileged. If you are not the intended recipient, please notify the sender immediately and do not disclose the contents to any other person, use it for any purpose, or store or copy the information in any medium. Thank you.

Sachin More

25 Oct 25 Oct

6:22 a.m.

On Fri, Oct 23, 2020 at 8:20 PM Nick Spinale wrote:

...

...
Has anyone tried to use seL4 on a raspberry pi 4?

Yes, I am running seL4 on the Raspberry Pi 4 Model B. The project we are working has a userland that is not based on `seL4_libs` and friends, so I’m afraid we have no userland drivers to contribute upstream. However, we do have patches with the necessary kernel configuration and elfloader SMP initialization logic to get seL4 itself running on the Raspberry Pi 4 Model B.

I want to learn to set up seL4 on ARM and happen to have a RP4 lying around. I would like to start with getting the kernel up and running. So I would be grateful for anything that helps in that regard.

...

Our project uses a different build system from upstream seL4 development, so our patches will require additional preparation before we can open a PR. For now, I’ll publish the patches in a public fork and then link to them in this thread.

I am not sure I understand you. Can I prepare, say seL4 11.0 and then apply your patches and then compile using seL4's build system (or your build system if it is in public domain)? thanks, Sachin

...

- - - - Nick Spinale (nickspinale.com) Arm Research, Cambridge UK - - - -

IMPORTANT NOTICE: The contents of this email and any attachments are confidential and may also be privileged. If you are not the intended recipient, please notify the sender immediately and do not disclose the contents to any other person, use it for any purpose, or store or copy the information in any medium. Thank you.

Nick Spinale

29 Oct 29 Oct

11:27 a.m.

...

Can I prepare, say seL4 11.0 and then apply your patches and then compile using seL4's build system (or your build system if it is in public domain)?

At the moment, I’m unable to share the rest of the code for this particular project. I have, however, published our Raspberry Pi 4-related patches to public branches of 'seL4' [1] and ‘seL4_tools' [2]. These patches, which are the extent of our Raspberry Pi 4-related patches for upstream seL4 repositories, only encompasses the bootloader (“elfloader”) and the seL4 kernel itself. The projects that you might use for getting started, such as ‘sel4test’ [3], depend on platform support for userland libraries such as those found in ’seL4_libs’ [4]. If you decide to add Raspberry Pi 4 support to those userland libraries, I’d be happy to help out with that. [1] https://github.com/nspin/seL4/tree/rpi4 [2] https://github.com/nspin/seL4_tools/tree/rpi4 [3] https://github.com/seL4/sel4test-manifest [4] https://github.com/seL4/seL4_libs - - - - Nick Spinale (nickspinale.com) Arm Research, Cambridge UK - - - - IMPORTANT NOTICE: The contents of this email and any attachments are confidential and may also be privileged. If you are not the intended recipient, please notify the sender immediately and do not disclose the contents to any other person, use it for any purpose, or store or copy the information in any medium. Thank you.

Jose A. Pascual

4:45 p.m.

Hi, We are also running seL4 on the RPI4 and we managed to run "sel4test" passing all the tests. Basically, you can build the sel4test project and execute all the tests without errors as in the Rpi3. We are using it in an OS course to build a very simple OS on top of seL4. I'll try to open a PR in the following days. Nick, if you don't mind, I'll compare our patch with yours to check if we are doing everything the same way. I'll keep you informed. Jose (& Mikel) On Thu, Oct 29, 2020 at 1:29 AM Nick Spinale wrote:

...

...
Can I prepare, say seL4 11.0 and then apply your patches and then compile using seL4's build system (or your build system if it is in public domain)?

At the moment, I’m unable to share the rest of the code for this particular project. I have, however, published our Raspberry Pi 4-related patches to public branches of 'seL4' [1] and ‘seL4_tools' [2]. These patches, which are the extent of our Raspberry Pi 4-related patches for upstream seL4 repositories, only encompasses the bootloader (“elfloader”) and the seL4 kernel itself. The projects that you might use for getting started, such as ‘sel4test’ [3], depend on platform support for userland libraries such as those found in ’seL4_libs’ [4].

If you decide to add Raspberry Pi 4 support to those userland libraries, I’d be happy to help out with that.

[1] https://github.com/nspin/seL4/tree/rpi4 [2] https://github.com/nspin/seL4_tools/tree/rpi4 [3] https://github.com/seL4/sel4test-manifest [4] https://github.com/seL4/seL4_libs

- - - - Nick Spinale (nickspinale.com) Arm Research, Cambridge UK - - - -

IMPORTANT NOTICE: The contents of this email and any attachments are confidential and may also be privileged. If you are not the intended recipient, please notify the sender immediately and do not disclose the contents to any other person, use it for any purpose, or store or copy the information in any medium. Thank you. _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

Sachin More

11:30 p.m.

On Wed, Oct 28, 2020 at 8:27 PM Nick Spinale wrote:

...

...
Can I prepare, say seL4 11.0 and then apply your patches and then compile using seL4's build system (or your build system if it is in public domain)?

At the moment, I’m unable to share the rest of the code for this particular project. I have, however, published our Raspberry Pi 4-related patches to public branches of 'seL4' [1] and ‘seL4_tools' [2]. These patches, which are the extent of our Raspberry Pi 4-related patches for upstream seL4 repositories, only encompasses the bootloader (“elfloader”) and the seL4 kernel itself. The projects that you might use for getting started, such as ‘sel4test’ [3], depend on platform support for userland libraries such as those found in ’seL4_libs’ [4].

Thanks for the detailed explanation.

...

If you decide to add Raspberry Pi 4 support to those userland libraries, I’d be happy to help out with that.

I am not confident if I will be able to add RP4 support for the userland libraries. But I will give it a try and keep everyone posted if I get somewhere. thanks, Sachin

...

[1] https://github.com/nspin/seL4/tree/rpi4 [2] https://github.com/nspin/seL4_tools/tree/rpi4 [3] https://github.com/seL4/sel4test-manifest [4] https://github.com/seL4/seL4_libs

- - - - Nick Spinale (nickspinale.com) Arm Research, Cambridge UK - - - -

IMPORTANT NOTICE: The contents of this email and any attachments are confidential and may also be privileged. If you are not the intended recipient, please notify the sender immediately and do not disclose the contents to any other person, use it for any purpose, or store or copy the information in any medium. Thank you.

Sachin More

31 Oct 31 Oct

9:36 a.m.

Hello: On Thu, Oct 29, 2020 at 8:30 AM Sachin More wrote:

...

On Wed, Oct 28, 2020 at 8:27 PM Nick Spinale wrote:

...
...
Can I prepare, say seL4 11.0 and then apply your patches and then compile using seL4's build system (or your build system if it is in public domain)?

At the moment, I’m unable to share the rest of the code for this particular project. I have, however, published our Raspberry Pi 4-related patches to public branches of 'seL4' [1] and ‘seL4_tools' [2]. These patches, which are the extent of our Raspberry Pi 4-related patches for upstream seL4 repositories, only encompasses the bootloader (“elfloader”) and the seL4 kernel itself. The projects that you might use for getting started, such as ‘sel4test’ [3], depend on platform support for userland libraries such as those found in ’seL4_libs’ [4].

Thanks for the detailed explanation.

I started with the seL4 kernel link that you provided. I am using Ubuntu 20 running on the RP4 to build the kernel: git clone https://github.com/nspin/seL4.git git checkout origin/rpi4 mkdir build ; cd build cmake -C /home/smore/seL4/configs/ARM_verified.cmake -G Ninja -DCMAKE_TOOLCHAIN_FILE=/home/smore/seL4/gcc.cmake /home/smore/seL4 However, when I compile, I get the following errors. ninja kernel.elf [9/30] Building C object CMakeFiles/kernel_bf_..._lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj FAILED: CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj /usr/bin/ccache /usr/bin/gcc --sysroot=/home/smore/seL4/build -I../include/plat/default -I../include -I../include/32 -I../include/arch/arm -I../include/arch/arm/arch/32 -I../include/plat/imx6 -I../include/plat/imx6/plat/32 -I../include/arch/arm/armv/armv7-a -I../include/arch/arm/armv/armv7-a/32 -I../libsel4/include -I../libsel4/arch_include/arm -I../libsel4/sel4_arch_include/aarch32 -I../libsel4/sel4_plat_include/imx6 -I../libsel4/mode_include/32 -Igen_config -Iautoconf -Igen_headers -march=armv7-a -marm -D__KERNEL_32__ -O3 -DNDEBUG -nostdinc -nostdlib -O2 -DHAVE_AUTOCONF -mfloat-abi=soft -fno-pic -fno-pie -fno-stack-protector -fno-asynchronous-unwind-tables -std=c99 -Wall -Werror -Wstrict-prototypes -Wmissing-prototypes -Wnested-externs -Wmissing-declarations -Wundef -Wpointer-arith -Wno-nonnull -ffreestanding -E -P -MD -MT CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj -MF CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj.d -o CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj -c kernel_bf_gen_target_1_pbf_temp.c gcc: error: unrecognized command-line option '-marm' gcc: error: unrecognized command-line option '-mfloat-abi=soft' [10/30] Building C object CMakeFiles/kernel_al...lib.dir/kernel_all_pp_prune_wrapper_temp.c.obj FAILED: CMakeFiles/kernel_all_pp_prune_wrapper_temp_lib.dir/kernel_all_pp_prune_wrapper_temp.c.obj /usr/bin/ccache /usr/bin/gcc --sysroot=/home/smore/seL4/build -I../include/plat/default -I../include -I../include/32 -I../include/arch/arm -I../include/arch/arm/arch/32 -I../include/plat/imx6 -I../include/plat/imx6/plat/32 -I../include/arch/arm/armv/armv7-a -I../include/arch/arm/armv/armv7-a/32 -I../libsel4/include -I../libsel4/arch_include/arm -I../libsel4/sel4_arch_include/aarch32 -I../libsel4/sel4_plat_include/imx6 -I../libsel4/mode_include/32 -Igen_config -Iautoconf -Igen_headers -march=armv7-a -marm -D__KERNEL_32__ -O3 -DNDEBUG -nostdinc -nostdlib -O2 -DHAVE_AUTOCONF -mfloat-abi=soft -fno-pic -fno-pie -fno-stack-protector -fno-asynchronous-unwind-tables -std=c99 -Wall -Werror -Wstrict-prototypes -Wmissing-prototypes -Wnested-externs -Wmissing-declarations -Wundef -Wpointer-arith -Wno-nonnull -ffreestanding -E -CC -I/home/smore/seL4/build/generated_prune -MD -MT CMakeFiles/kernel_all_pp_prune_wrapper_temp_lib.dir/kernel_all_pp_prune_wrapper_temp.c.obj -MF CMakeFiles/kernel_all_pp_prune_wrapper_temp_lib.dir/kernel_all_pp_prune_wrapper_temp.c.obj.d -o CMakeFiles/kernel_all_pp_prune_wrapper_temp_lib.dir/kernel_all_pp_prune_wrapper_temp.c.obj -c kernel_all_pp_prune_wrapper_temp.c gcc: error: unrecognized command-line option '-marm' gcc: error: unrecognized command-line option '-mfloat-abi=soft' ninja: build stopped: subcommand failed. It seems that I am using the wrong toolchain for compilation. Any ideas? thanks, Sachin If you decide to add Raspberry Pi 4 support to those userland libraries,

...

...
I’d be happy to help out with that.

I am not confident if I will be able to add RP4 support for the userland libraries. But I will give it a try and keep everyone posted if I get somewhere.

thanks, Sachin

...
[1] https://github.com/nspin/seL4/tree/rpi4 [2] https://github.com/nspin/seL4_tools/tree/rpi4 [3] https://github.com/seL4/sel4test-manifest [4] https://github.com/seL4/seL4_libs

- - - - Nick Spinale (nickspinale.com) Arm Research, Cambridge UK - - - -

IMPORTANT NOTICE: The contents of this email and any attachments are confidential and may also be privileged. If you are not the intended recipient, please notify the sender immediately and do not disclose the contents to any other person, use it for any purpose, or store or copy the information in any medium. Thank you.

Chubb, Peter (Data61, Kensington NSW)

7:56 p.m.

...

...
...
...
...
"Sachin" == Sachin More writes:

Sachin> It seems that I am using the wrong toolchain for Sachin> compilation. Any ideas? Compiling seL4 on its own results in something fairly useless. I suggest starting out by using repo to get the whole caboodle for seL4test (https://github.com/seL4/sel4test-manifest) then replacing the kernel in there with the one for raspi4. That should select the right toolchain (aarch64-linux-gnu-gcc) when you configure it (although you may need to do a bit of porting work first, see https://docs.sel4.systems/projects/sel4/porting.html ) Alternatively you can use ccmake to get the GUI for configuration and set the correct toolchain, but I've never tried that with just the kernel. -- Dr Peter Chubb Tel: +61 2 9490 5852 http://ts.data61.csiro.au/ Trustworthy Systems Group Data61 (formerly NICTA)

1454

Age (days ago)

1462

Last active (days ago)

List overview

Download

7 comments

4 participants

participants (4)

Chubb, Peter (Data61, Kensington NSW)
Jose A. Pascual
Nick Spinale
Sachin More

raspberry pi 4

Sachin More

Nick Spinale

Sachin More

Nick Spinale

Jose A. Pascual

Sachin More

Sachin More

Chubb, Peter (Data61, Kensington NSW)

tags

participants (4)